[isabelle] Axiom of Choice – Re: Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic
Thanks, this is what I expected.
Concerning the Axiom of Choice (answering Mario's email, too), its use should
be expressed as a conditional of the form AC => THM (or as a hypothesis) and
not as an axiom in order to make the appeal to it explicit.
An example is the theorem in exercise X5308 in [Andrews, 2002, p. 237]:
"X5308. Prove AC => [...]"
(AC is defined in [Andrews, 2002, p. 236], formal verification of X5308
http://www.owlofminerva.net/files/formulae.pdf, pp. 151 ff.)
For the same reason, language elements embodying the Axiom of Choice (such as
the epsilon operator) should be avoided. For good reason Q0 uses the
description operator instead [cf. Andrews, 2002, p. 211].
Andrews sees, concerning the "Axiom Schema of Choice, an Axiom of Infinity, and
perhaps even the Continuum Hypothesis [...] room for argument whether these are
axioms of pure logic or of mathematics" [Andrews, 2002, p. 204], and I also
clearly regard all of them as non-logical axioms. Note that they are not Axioms
for Q0 [cf. Andrews, 2002, p. 213].
For the references, please see: http://doi.org/10.4444/100.111
> Am 12.03.2018 um 11:19 schrieb Lawrence Paulson <lp15 at cam.ac.uk>:
> The paper in question is Church (1940), which is available online (possibly paywalled):
> DOI: 10.2307/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 <mail at 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
>> 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
>> 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.
>> "The inclusion of [epsilon]-terms into HOL 'builds in' the Axiom of Choice
>> [...]." (p. 24)
This archive was generated by a fusion of
Pipermail (Mailman edition) and