On Tuesday 19 January 2010 18:7:32 Lockwood Morris wrote: > Does anyone know if it is possible to prove the well-ordering theorem in > HOL for an arbitrary type? That is, using the terminology of > relationTheory, > > ?R:'a->'a->bool. WF R /\ StrongLinearOrder R .
There is a proof in ProofPower (by Rob Arthan) in the document: http://rbjones.com/rbjpub/pp/doc/t009.pdf (the proof is not actually visible, but the sources can be downloaded). so it will be provable in HOL. > The only relevant information I have come across is Stewart Shapiro's > statement, in Foundations without Foundationalism, that in set theory done > with second-order logic, the well-ordering theorem does not follow from the > axiom of choice, but I don't know what one can conclude for HOL from that. The result in ProofPower does apply of course to a type SET which is the domain of an w-order axiomatisation of set theory (I often work in such a context). So one has to get right exactly what Shapiro is saying, and I haven't succeeded in finding the claim you mention. Can you give me a page number? Roger Jones ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
