I once did a proof of the well-ordering principle and several other Axiom of Choice equivalents (Zorn's Lemma etc.) in HOL88:
http://www.cl.cam.ac.uk/~jrh13/papers/wellorder-library.html This proof certainly survives in HOL Light (Examples/wo.ml), and possibly in other versions of HOL too. For example, the well-ordering principle looks like: WO = |- !P. ?l. woset l /\ fl l = P where "fl" denotes the field of a binary relation: fl = |- !l x. fl l x <=> (?y. l (x,y) \/ l (y,x)) and "woset" is a well-ordered relation: |- !l. woset l <=> (!x. fl l x ==> l (x,x)) /\ (!x y z. l (x,y) /\ l (y,z) ==> l (x,z)) /\ (!x y. l (x,y) /\ l (y,x) ==> x = y) /\ (!x y. fl l x /\ fl l y ==> l (x,y) \/ l (y,x)) /\ (!P. (!x. P x ==> fl l x) /\ (?x. P x) ==> (?y. P y /\ (!z. P z ==> l (y,z)))) The version Lockwood wanted should be the case of WO where P is instantiated to the whole type. John. ------------------------------------------------------------------------------ Throughout its 18-year history, RSA Conference consistently attracts the world's best and brightest in the field, creating opportunities for Conference attendees to learn about information security's most important issues through interactions with peers, luminaries and emerging and established companies. http://p.sf.net/sfu/rsaconf-dev2dev _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
