The Coq mailing list

[Dan Doel <dan.doel AT gmail.com>]

On Thursday 22 October 2009 9:50:18 am Edsko de Vries wrote:
> Thank you for your extensive answer. Much appreciated. The link to Dan
> Piponi's blog post was also very helpful. I think I have a better
> understanding of ordinals now.

Incidentally, while googling for Brouwer ordinal (which is, apparently, the 
formulation I talked about), I came across this short paper which looks 
pretty 
interesting:

  http://www.cs.nott.ac.uk/~pgh/nc.ps

It centers around the idea that you can keep extending my O:

  O₀ = 1 + O₀ = ℕ
  O₁ = O₀ + (O₀ → O₁)
  O₂ = O₁ + (O₁ → O₂)
  ⋮

where these are all intended to be inductive fixed points. So now we have a ℕ-
indexed series of ordinal encodings. Can we build an O-indexed one? We can:

  O_α = Σ β<α O_β ~ O_(lim f) = Σ n:ℕ O_(f n)

So now we have an O-indexed series of ordinal encodings, and O = O₁. Can we 
have an O₂ indexed series? And so on. It also turns out you can use a 
modified 
(for convenience) W-type constructor to express the above series. If I 
understand correctly, it's:

  W A T = Z | S (W A T) | Sup (x:A) (T x -> W A T)

  O_i = W (Fin i) (n ↦ O_n)

for i : ℕ, at least, where 'Fin i' is the finite set with i elements (in the 
case of i = 0, n ↦ O_n is intended to be the empty function, since Fin 0 is 
empty). The author ties all this together with an inductive-recursive 
definition of a type On, which in some sense represents the union of an On-
indexed series of ordinal representations. Ordinal arithmetic can be defined 
almost identically to arithmetic on O in my previous message.

I'm not really sure how much further this goes in modeling the behavior of 
the 
ordinals. However, it still doesn't get you coinduction-like behavior (I'm 
pretty sure). The inductive case for a limit ordinal still represents a 
choice 
to progress to some unbounded but well-founded and lesser value(s). So even 
though we have ordinals that live unions of ordinal-indexed families, each 
particular ordinal can be seen as corresponding to some ultimately 
terminating 
procedure.

Cheers,

-- Dan