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
http://doi.org/10.4444/100
> Am 12.03.2018 um 11:19 schrieb Lawrence Paulson <l...@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 <m...@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=10.1.1.27.6103&rep=rep1&type=pdf
>
>
------------------------------------------------------------------------------
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
