Delivery-Date: 
Sender: info-hol-request@lal.cs.byu.edu
Errors-To: info-hol-request@lal.cs.byu.edu
Precedence: list
To: chou@cs.ucla.edu
Cc: info-hol@leopard.cs.byu.edu
Subject: Re: Ordinals in HOL?
In-Reply-To: Your message of "Sun, 19 Mar 1995 04:03:15 PST." <9503191203.AA18595@maui.cs.ucla.edu>
Date: Sun, 19 Mar 1995 14:22:26 +0000
From: John Harrison <John.Harrison@cl.cam.ac.uk>
Message-Id: <"gannet.cl.ca:011410:950319142246"@cl.cam.ac.uk>


Ching Tsun writes:

| Can one have ordinals in HOL (in particular, the ability to do
| transfinite recursive definitions and transfinite inductive proofs)?
| If so, has anyone done it?

The "wellorder" library contains a proof that every set can be wellordered
and theorems to support induction and recursion on a woset. However you
need to instantiate the theorem by hand, which is a bit fiddly. I also have
a more general theorem for recursion on an arbitrary wellfounded relation
(which need not be connected or transitive). The proof (using an inductive
definition) is rather short, and I can send it if anyone is interested.

You cannot really have a class of ordinals in HOL's type theory in the way
you can in ZF set theory. (Though if you look at the proof of the
wellordering theorem in the "wellorder" library, which is more or less
Zermelo's, you have what are essentially local ordinals on a particular
type, in that you impose canonicality on wosets.)

However, even if the Axiom of Choice weren't plumbed into HOL, you could
prove Hartogs's theorem quite easily (for any set A there's a woset (X,<=)
with no injection X -> A), which is enough to support most definitions by
wellfounded recursion.

| Another question: Which recursive type package allows one to
| define the following type?
|
|   ('a,'b)ttt ::= A('a) | B('b -> ttt)

I think Elsa Gunter has a hol90 package to do this, though I'm not sure if
it's finished. You might also glance at my own info-hol posting of 1st Feb
94, which defines a type almost identical to the one you cite.

Cheers,

John.