[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 
available at
	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

Ken Kubota


Ken Kubota

> 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
> 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
>> 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
>> 	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=

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