*To*: Ken Kubota <mail at kenkubota.de>*Subject*: Re: [isabelle] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Mon, 12 Mar 2018 10:19:58 +0000*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*: <03F02375-13E2-4E53-83E3-435F94EE5A5A@kenkubota.de>*References*: <03F02375-13E2-4E53-83E3-435F94EE5A5A@kenkubota.de>

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] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic
- Next by Date: [isabelle] F-IDE-18 / call for papers
- Previous by Thread: [isabelle] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic
- Next by Thread: [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