Re: [Hol-info] HOL and the axiom of choice
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
Re: [Hol-info] HOL and the axiom of choice
Hi Cris, To chime in on this: I don't have any problems with a system that doesn't allow you to disable the axiom of choice. In other words: hardwire choice all you like as far as I'm concerned. Without AC you get weirdnesses as that a union of countably many countable sets doesn't need to be provably countable. Who would like to reason in such a weak system :-) I know, keeping track of where you used AC in a proof is a fun game, and textbooks sometimes do this too. But _mathematically_ it doesn't seem _too_ interesting to me. However, I _do_ have problems with HOL's choice operator! Mainly this is for philosophical -- i.e., for not very good -- reasons. See, I'm a Platonist (that is to say: during the week; in the weekend I'm a formalist :-)) So when I think about mathematics, I imagine a space of ZF sets, where the ZF sets live. And when writing mathematics I would like to consider that as pointing at those sets and talking about them. (Look, that set there, that's the natural numbers!) Now, _without_ Hilbert's choice operator epsilon, every HOL term clearly denotes at a welldetermined set. (That is, if you fix some straight-forward set theoretic encoding of the HOL universe.) However, once you add the epsilon, that's no longer true. It then depends on _what_ choice operator you choose, what the set is that you are talking about. And it's not clear how to (Platonically!) distinguish one choice operator from the other. Therefore once you write HOL terms that contain an epsilon somewhere, _I_ don't know (Platonically!) anymore what they mean. So the choice operator in HOL always makes me a bit uneasy. Not that it really matters of course. And a choice operator _is_ a really useful thing to have :-) Freek -- 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
Re: [Hol-info] rigorous axiomatic geometry proof in HOL Light
On Sun, 5 Aug 2012, Konrad Slind wrote: My opinion is that Peter Homeier's HOL-Omega is the right setting to properly implement something locale-like, since it provides quantification over type variables in the logic. In plain old HOL the implementation of locales as essentially assumptions on goals is too limiting for polymorphism. In the 1.5 decades refining Isabelle locales, we have separated these two concerns: (1) management of local contexts and definitional specifications wrt. local contexts, (2) logical foundations for building actual abstract contexts. (1) is the infrastructure, consisting of quite a bit of abstract non-sense. It is now called local theory in Isabelle. It provides some interfaces for definitions in a local context, where the results are polymorphic in the sense of Hindley-Milner, but some types may remain fixed according to the context. (2) are concrete implementations of locales, type classes, type-class instantiation, unrestricted overloading etc. This could cover other concepts for modular theories using facilities of HOL-Omega, or external theory interpretation as in Isabelle/AWE from Bremen. Both (1) and (2) are difficult to implement. We are still working on various fine points concerning local syntax (via notation or abbreviation) that moves between such local contexts. Another challenge that I have boldly revisited this year is to allow nesting of locale-like contexts. What is also difficult to get right are declarations for proof tools associated with theorems produced in abstract situations, when they start moving around to other contexts. E.g. ways to manage simpset-like containers in conformance to abstract theories and their interpretations by concrete instances. Type classes have turned out an important special case for all that, because the abstraction looks concrete, via polymorphic constants with some specific type constraints. Syntax and tool declarationas are often stable wrt. type-instantiation of class constants, without further ado. Makarius -- 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
Re: [Hol-info] HOL and the axiom of choice
Freek, Mark, Bill, Thanks very much for the stimulating and I think helpful responses, including Mark's historical sketch. I'm glad to learn that inclusion of an axiom of choice is considered unsurprising, perhaps leading to less weird consequences than if it is left out. Freek's example of the union of countably many countable sets is certainly interesting and surprising. At a philosophical level I'm surprised that Freek's intervals of Platonism are during the week, with formalism on weekends. Formalism seems like such a practical attitude for the working week. ;-) On choice operators, as a constructive software engineer / computer scientist I certainly prefer my sets tidy and countable with least elements I can pick out in a clear way. Wandering in the wilds of larger infinities less well-ordered sets can get disorienting. Regards, -Cris On Mon, Aug 6, 2012 at 6:31 AM, Freek Wiedijk fr...@cs.ru.nl wrote: Hi Cris, To chime in on this: I don't have any problems with a system that doesn't allow you to disable the axiom of choice. In other words: hardwire choice all you like as far as I'm concerned. Without AC you get weirdnesses as that a union of countably many countable sets doesn't need to be provably countable. Who would like to reason in such a weak system :-) I know, keeping track of where you used AC in a proof is a fun game, and textbooks sometimes do this too. But _mathematically_ it doesn't seem _too_ interesting to me. However, I _do_ have problems with HOL's choice operator! Mainly this is for philosophical -- i.e., for not very good -- reasons. See, I'm a Platonist (that is to say: during the week; in the weekend I'm a formalist :-)) So when I think about mathematics, I imagine a space of ZF sets, where the ZF sets live. And when writing mathematics I would like to consider that as pointing at those sets and talking about them. (Look, that set there, that's the natural numbers!) Now, _without_ Hilbert's choice operator epsilon, every HOL term clearly denotes at a welldetermined set. (That is, if you fix some straight-forward set theoretic encoding of the HOL universe.) However, once you add the epsilon, that's no longer true. It then depends on _what_ choice operator you choose, what the set is that you are talking about. And it's not clear how to (Platonically!) distinguish one choice operator from the other. Therefore once you write HOL terms that contain an epsilon somewhere, _I_ don't know (Platonically!) anymore what they mean. So the choice operator in HOL always makes me a bit uneasy. Not that it really matters of course. And a choice operator _is_ a really useful thing to have :-) Freek -- 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
