Email Gateway (Aug 22 2022 at 16:55): Email Gateway (Aug 22 2022 at 16:55):From: Ken Kubota <mail@kenkubota.de>
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
Email Gateway (Aug 22 2022 at 16:55):From: Lawrence Paulson <lp15@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
Last updated: Apr 19 2024 at 04:17 UTC