*To*: "Prof. Lawrence C. Paulson" <lp15 at cam.ac.uk>*Subject*: [isabelle] Skolemization in first-order logic without the Axiom of Choice, Literature on Isabelle*From*: Ken Kubota <mail at kenkubota.de>*Date*: Sat, 3 Mar 2018 17:37:09 +0100*Cc*: "Prof. Peter B. Andrews" <andrews at cmu.edu>, "PD Dr.-Ing. Christoph Benzmüller" <c.benzmueller at gmail.com>, cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <B0A0C47E-5DC3-4D66-BC5A-E155668CE274@cam.ac.uk>*References*: <8379B195-0465-46C6-84A9-50841CCE5209@kenkubota.de> <B0A0C47E-5DC3-4D66-BC5A-E155668CE274@cam.ac.uk>

Dear Larry Paulson, Thank you very much for your kind answer. Please allow me to add a note and rephrase the second question, and add a minor amendment to Christoph Benzmüller's paper you referred to. 1. I apologize for having overlooked that indeed there is a possibility for the model-theoretic justification of Skolemization in first-order logic without the Axiom of Choice, as pointed out by Peter B. Andrews: "If G has a model, it has a denumerable model by the Löwenheim-Skolem Theorem [...] Since the domain of individuals of M is in one-one correspondence with the natural numbers, we may assume it is well-ordered. (This will enable us to avoid any appeal to the Axiom of Choice in the argument below.)" [Andrews, 2002, p. 168] 2. If one publication (or maybe two) should be taken as main reference for Isabelle (the logical framework, not an object logic like Isabelle/HOL) - preferably a printed publication instead of just an online file - which one would you choose? The literature on Isabelle is so vast that it becomes difficult to single out a specific publication. My first guess would be [29] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. LNCS 828. which is newer than your 1989 article available online at https://arxiv.org/pdf/cs/9301105.pdf Concerning Christoph Benzmüller's paper "Automation of Higher-Order Logic" at http://page.mi.fu-berlin.de/cbenzmueller/papers/B5.pdf it should be noted that the first formulation of Peter's logic Q0 can be found in [Andrews, 1963], not only in the much later (Andrews, 1972a), as suggested by the paper: "While Church axiomatized the logical connectives of STT in a rather conventional fashion [...], Henkin (1963) and Andrews (1972a, 2002) provided a formulation of STT in which the sole logical connective was equality (at all types)." (p. 14) [Andrews, 1963] directly follows [Henkin, 1963] in Fundamenta Mathematicae 52: http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52123.pdf http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52124.pdf Their collaboration is described in [Andrews, 2014b], see the quote from there on p. 11 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 > Am 03.03.2018 um 11:14 schrieb Lawrence Paulson <lp15 at cam.ac.uk>: > > Thanks for your message. First, as a general remark, decades-old papers are mainly of motivational and historical interest, connecting Isabelle with earlier systems such as Edinburgh LCF. Isabelle has not used Skolemization since 1989. "The foundation of a generic theorem prover" still contains a useful development of the theoretical ideas behind Isabelle. > > Skolemization in first-order logic does not imply the axiom of choice. In higher-order logic, precautions must be taken (in the calculus) to prevent abstraction over Skolem terms; Skolem functions must always be applied to arguments. See http://page.mi.fu-berlin.de/cbenzmueller/papers/B5.pdf (section 5.1) and the references cited there. > > Larry Paulson > > > >> On 2 Mar 2018, at 20:09, Ken Kubota <mail at kenkubota.de> wrote: >> >> Dear Isabelle Users and Developers, >> >> Concerning the generic theorem prover Isabelle (not the object logic HOL), I >> have two questions. >> >> >> 1. Skolemization does not only rest on model theory, but also requires the >> Axiom of Choice in order to guarantee the existence of the Skolem function >> substituted for the variable bound by the existential quantifier. (Cf. Uwe >> Schöning, Logik für Informatiker, 4th ed., Heidelberg, Berlin, Oxford 1995, >> ISBN 3-86025-684-X, http://d-nb.info/942357612, p. 68: "An dieser Stelle des >> Beweises wird das _Auswahlaxiom_ benötigt, welches gerade die Existenz einer >> derartigen Funktion garantiert.") >> >> Is this discussed anywhere or is the Axiom of Choice implicitly assumed in >> Isabelle? >> Some consider the Axiom of Choice a non-logical axiom. >> Larry Paulson writes: "Many people object to Skolemization." (Natural deduction >> as higher-order resolution, 1986, https://doi.org/10.1016/0743-1066(86)90015-4, >> p. 247.) But in the following only practical reasons are given. >> >> >> 2. According to >> http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2017/doc/tutorial.pdf (p. 3) >> http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle2017/doc/intro.pdf (p. i), >> the following four publications seem to be the main resources on the generic >> theorem prover: >> [29] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994. >> LNCS 828. >> [12] Lawrence C. Paulson. Natural deduction as higher-order resolution. Journal >> of Logic Programming, 3:237-258, 1986. >> [14] Lawrence C. Paulson. The foundation of a generic theorem prover. Journal >> of Automated Reasoning, 5(3):363-397, 1989. >> [15] Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P. >> Odifreddi, editor, Logic and Computer Science, pages 361-386. Academic Press, >> 1990. >> >> Is this correct or are there further papers that are important for the >> foundation of the generic theorem prover Isabelle? >

**Follow-Ups**:

**References**:**[isabelle] Axiom of Choice in Isabelle, Literature on Foundation***From:*Ken Kubota

**Re: [isabelle] Axiom of Choice in Isabelle, Literature on Foundation***From:*Lawrence Paulson

- Previous by Date: Re: [isabelle] 1/0 = 0?
- Next by Date: Re: [isabelle] Skolemization in first-order logic without the Axiom of Choice, Literature on Isabelle
- Previous by Thread: Re: [isabelle] Axiom of Choice in Isabelle, Literature on Foundation
- Next by Thread: Re: [isabelle] Skolemization in first-order logic without the Axiom of Choice, Literature on Isabelle
- Cl-isabelle-users March 2018 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list