*To*: "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>*Subject*: [isabelle] Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic*From*: Ken Kubota <mail at kenkubota.de>*Date*: Mon, 12 Mar 2018 20:12:26 +0100*Cc*: "Prof. Peter B. Andrews" <andrews at cmu.edu>, HOL-info list <hol-info at lists.sourceforge.net>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <B603330D-8B7B-4E2C-83AD-4952419953CE@cam.ac.uk>*References*: <03F02375-13E2-4E53-83E3-435F94EE5A5A@kenkubota.de> <B603330D-8B7B-4E2C-83AD-4952419953CE@cam.ac.uk>

Thanks, this is what I expected. Concerning the Axiom of Choice (answering Mario's email, too), its use should be expressed as a conditional of the form AC => THM (or as a hypothesis) and not as an axiom in order to make the appeal to it explicit. An example is the theorem in exercise X5308 in [Andrews, 2002, p. 237]: "X5308. Prove AC => [...]" (AC is defined in [Andrews, 2002, p. 236], formal verification of X5308 available at http://www.owlofminerva.net/files/formulae.pdf, pp. 151 ff.) For the same reason, language elements embodying the Axiom of Choice (such as the epsilon operator) should be avoided. For good reason Q0 uses the description operator instead [cf. Andrews, 2002, p. 211]. Andrews sees, concerning the "Axiom Schema of Choice, an Axiom of Infinity, and perhaps even the Continuum Hypothesis [...] room for argument whether these are axioms of pure logic or of mathematics" [Andrews, 2002, p. 204], and I also clearly regard all of them as non-logical axioms. Note that they are not Axioms for Q0 [cf. Andrews, 2002, p. 213]. For the references, please see: http://doi.org/10.4444/100.111 Ken Kubota ____________________ Ken Kubota http://doi.org/10.4444/100 > Am 12.03.2018 um 11:19 schrieb Lawrence Paulson <lp15 at cam.ac.uk>: > > The paper in question is Church (1940), which is available online (possibly paywalled): > > DOI: 10.2307/2266170 > http://www.jstor.org/stable/2266170 > > On page 61 we see axiom 9 (description) and axiom 11 (choice). > > Mike Gordon was clearly mistaken when he overlooked that Church's 1940 system already included the axiom of choice. He credits Keith Hanna with introducing him to higher-order logic and it's possible that he wasn't working with the original source, and overlooked the description operator altogether. > > Choice is not necessary to define the conditional operator. But as Church notes, choice is necessary "in order to obtain classical real number theory (analysis)”. > > Larry Paulson > > > >> On 10 Mar 2018, at 19:57, Ken Kubota <mail at kenkubota.de> wrote: >> >> With regard to your statement: >> "Church's formulation of higher-order logic includes the Hilbert >> [epsilon]-operator" (p. 25) >> in your main paper on Isabelle (as a logical framework) at >> http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf >> I would like to ask which particular formulation you had in mind, as no >> explicit reference to any of Church's works is given. >> >> >> As of my knowledge, in the standard reference [Church, 1940] use is made only >> of the description operator instead (cf. pp. 57-59), called "selection >> operator" (p. 59) there, with the "axioms of descriptions" (p. 61). >> Furthermore, in his article "Church's Type Theory" in the Stanford Encyclopedia >> of Philosophy at >> https://plato.stanford.edu/archives/spr2014/entries/type-theory-church/ >> Peter Andrews doesn't mention an epsilon operator. >> >> My understanding is that in higher-order logic the epsilon operator was >> introduced by Mike Gordon in order to obtain definability of expressions like >> the conditional term, although he was well aware of the problems associated >> with the epsilon operator, calling it "suspicious" and mentioning the implicit >> Axiom of Choice: >> "Many things that are normally primitive can be defined using the >> [epsilon]-operator. For example, the conditional term Cond t t1 t2 (meaning 'if >> t then t1 else t2') can be defined" (p. 24). >> "It must be admitted that the [epsilon]-operator looks rather suspicious." (p. >> 24) >> "The inclusion of [epsilon]-terms into HOL 'builds in' the Axiom of Choice >> [...]." (p. 24) >> http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.27.6103&rep=rep1&type=pdf > >

**Follow-Ups**:

**References**:

- Previous by Date: [isabelle] Applying n-ary monotonicity of "eventually" in ML
- Next by Date: [isabelle] Mathematical Logics and Logical Frameworks
- Previous by Thread: Re: [isabelle] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic
- Next by Thread: Re: [isabelle] Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic
- Cl-isabelle-users March 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list