Hi Cris, I'm not sure about the original motivation for using the axiom of choice in the HOL logic, and would be interested to know. But given that the HOL logic has this, and given that excluded middle is provable from this, we may as well not have excluded middle as an axiom. The philosophy is to make the logical core as minimalist as possible, and not have axioms that can be proved from other axioms and inference rules.
The early HOL systems (HOL88, HOL90 and ProofPower) had 5 axioms, including both SELECT_AX (the axiom of choice) and BOOL_CASES_AX (effectively the law of the excluded middle) as axioms. HOL Light has an alternative formulation of the HOL logic, and proves the law of the excluded middle using the axiom of choice. This was based on a relatively recent result in mathematical logic by Radu Diaconescu. HOL Zero uses another alternative formulation, but excluded middle is derived like it is in HOL Light. HOL4's formulation of the HOL logic is much the same as in the early systems, but does away with a different axiom (IMP_ANTISYM_AX), proving this using excluded middle. I wonder whether HOL Zero's or HOL4's formulations could be further minimalised... Mark. on 5/8/12 10:33 PM, Cris Perdue <c...@perdues.com> wrote: > 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 ------------------------------------------------------------------------------ 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
