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 There is an interesting intermediate property between TO, the fact that every set can be totally ordered (which is what Lockwood wanted) and WO, the fact that every set can be wellordered, namely PE, the fact that every partial order can be extended to a total order. This is a bit like the possibility of topological sorting. If I recall correctly, the implications WO ==> PE ==> TO in ZF are all proper, i.e. there is a model of ZF where TO /\ ~PE and one where PE /\ ~WO. But I might be misremembering. I was shown a very nice, almost "1-line", proof of WO ==> PE by the late internet legend Alexander Abian. Suppose <= is a partial order on a set S. Set up an SxS matrix ordering the rows and columns using a wellordering (which exists by WO) and putting a 1 in position (x,y) if x <= y and 0 otherwise. Now define a total order by lexicographic order on the rows of the matrix. John. ------------------------------------------------------------------------------ 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
