Further to my last message on this topic, I did discover the place in Shapiro where he talks about this (5.1.3 p107).
On Tuesday 19 January 2010 18:07:32 Lockwood Morris wrote: > 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. He says (and offers a proof) that WOP is not provable in D2, which is, in second order logic, not second order set theory. If he were correct then i would not expect it to be provable in HOL either even though HOL is stronger than D2. His proof involves more advanced set theory than I can cope with, and Robert Solovay was evidently consulted in the process so its not likely to be wrong, which leaves a bit of a conundrum. My guess is that the axiom of choice in D2 is weaker than the one in HOL. 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 [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
