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 <m...@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 ------------------------------------------------------------------------------ Check out the vibrant tech community on one of the world's most engaging tech sites, Slashdot.org! http://sdm.link/slashdot _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
