On Wednesday 20 January 2010 16:02:10 Roger Bishop Jones wrote: > 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. ... > My guess is that the axiom of choice in D2 is weaker than the one in HOL.
Rob tells me that his proof uses choice on sets of non-empty sets. Since D2 is second order you can't do that in D2. 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
