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 .
Or just the StrongLinearOrder part would suit me too. My motivation is
somewhat practical: I would like to define a type constructor, say
'a TotOrd, for the linear orders in some form or other (strong, weak,
or maybe 3-way comparison) on type 'a, and am of course required to have
it yield non-empty types.
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.
Thanks to anyone who can help,
Lockwood
|- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |- |-
Lockwood Morris lockw...@ecs.syr.edu (315)443-3046 Rm. 4-125 CST
EECS Syracuse University 111 College Place Syracuse NY 13244-4100
------------------------------------------------------------------------------
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
