On 16/11/12 12:28 PM, John Harrison wrote: > Michael wrote: > | As Ramana said, I recently proved this (every set can be well-ordered) as > | part of my development of the ordinal numbers. I needed Scott Owens' > | earlier proof of Zorn's Lemma. My proof is in > | examples/set-theory/hol_sets, in Kananaskis-8 onwards.
> There has been a proof of these results and a couple of other AC > equivalents (as well as a nonce notion of ordinal) available in the > HOL88 "wellorder" library since about 1992. As far as I can see this > got lost somewhere in the evolution from HOL88 to HOL4, though it > does live on in HOL Light: > http://code.google.com/p/hol-light/source/browse/trunk/Library/wo.ml Yes, I made a HOL4 version of your development a number of years ago. I would have used it and committed it to our repository, but I didn’t want to have two incompatible notions of ordinal hanging around, and (with Scott’s more recent work) I got Zorn’s Lemma without it. I don’t think I could have used your “nonce” ordinals to get the results (ordinal arithmetic, Cantor Normal Form, epsilon-0) I wanted, though it’s been a little while since I thought about this, so I’m now not sure exactly why I came to that conclusion. Best, Michael
signature.asc
Description: OpenPGP digital signature
------------------------------------------------------------------------------ Monitor your physical, virtual and cloud infrastructure from a single web console. Get in-depth insight into apps, servers, databases, vmware, SAP, cloud infrastructure, etc. Download 30-day Free Trial. Pricing starts from $795 for 25 servers or applications! http://p.sf.net/sfu/zoho_dev2dev_nov
_______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
