Dear Larry Paulson, 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 You also mention that it "embodies a strong Axiom of Choice." (p. 25) http://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-130.pdf Andrews has shown that the conditional term can be defined in terms of the description operator (definition of 'C' and Theorem 5313 in [Andrews, 2002, p. 235]). The theorem is available online (p. 6) at http://www.owlofminerva.net/files/fom.pdf and formally verified (pp. 142, 151) at http://www.owlofminerva.net/files/formulae.pdf The use of the description operator is the much more elegant solution, as it doesn't imply the Axiom of Choice, and the description operator is the natural counterpart to equality, which is the basic primitive of Andrews' logic Q0 having "only two basic constants (identity/equality and its counterpart, description)". https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2015-July/msg00147.html So in my opinion Gordon could have circumvented the problems of the epsilon operator for HOL by implementing a natural deduction variant of Q0, as did Cris Perdue at http://prooftoys.org (and http://mathtoys.org). Andrews implemented the description operator following Henkin when stating Axiom 5 for Q0: "Henkin remarks at the end of [Henkin, 1963] that when one passes from the theory of propositional types to the full theory of finite types, it becomes necessary to add a constant [...] to denote a descriptor function, and an appropriate axiom involving this constant. We note that for this axiom it suffices to take the simple formula [...]." [Andrews, 1963, p. 350] http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52123.pdf http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52124.pdf The quote with the formulas is also available (p. 4) at http://www.owlofminerva.net/files/fom.pdf For the references, please see: http://doi.org/10.4444/100.111 Kind regards, Ken Kubota ____________________ Ken Kubota http://doi.org/10.4444/100 ------------------------------------------------------------------------------ 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