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
