[isabelle] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic



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





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.