Re: [Hol-info] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic

[Lawrence Paulson]

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

Re: [Hol-info] Hilbert's epsilon operator in Church's Type Theory and Gordon's HOL logic

[Mario Xerxes Castelán Castro]

By the way, the _definite_ description operator is also called
“Russell's operator” or “Russell’s iota”
(http://us.metamath.org/mpegif/df-iota.html”.




signature.asc
Description: OpenPGP digital signature
--
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