In a post earlier today Rob Arthan commented that "in HOL you are working
in a model of Zermelo set theory with choice", which certainly seems to be
true of HOL Light. I'm a bit surprised that HOL Light (and HOL Zero, and
Proof Power, etc.) has this as a rather fundamental part.
John Harrison goes on to say that HOL Light's choice axiom makes the law of
excluded middle provable in HOL Light, so maybe that was the motivation.
In the end I'm quite curious to know: is there some philosophical or
engineering reason not to introduce the law of the excluded middle
separately from an axiom of choice in HOL logics? Or is it mostly an
accident of history that the axiom of choice is treated as being rather
fundamental?
Also -- for comparison, in Peter Andrews' quite similar Q0 there is a
weaker description operator that basically only promises to give the back
the single element of a singleton. Is there some notable concern or
disadvantage seen in this description operator compared with a choice
operator?
Q0 has been my introduction to these logics, so I'm very interested in
points of comparison.
thanks much,
Cris
------------------------------------------------------------------------------
Live Security Virtual Conference
Exclusive live event will cover all the ways today's security and
threat landscape has changed and how IT managers can respond. Discussions
will include endpoint security, mobile security and the latest in malware
threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
