[isabelle] Skolemization in first-order logic without the Axiom of Choice, Literature on Isabelle
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
My first guess would be
 Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994.
which is newer than your 1989 article available online at
Concerning Christoph Benzmüller's paper "Automation of Higher-Order Logic" at
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:
Their collaboration is described in [Andrews, 2014b], see the quote from there
on p. 11 at
For the references, please see: http://doi.org/10.4444/100.111
> 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
>> 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:
>>  Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994.
>> LNCS 828.
>>  Lawrence C. Paulson. Natural deduction as higher-order resolution. Journal
>> of Logic Programming, 3:237-258, 1986.
>>  Lawrence C. Paulson. The foundation of a generic theorem prover. Journal
>> of Automated Reasoning, 5(3):363-397, 1989.
>>  Lawrence C. Paulson. Isabelle: The next 700 theorem provers. In P.
>> Odifreddi, editor, Logic and Computer Science, pages 361-386. Academic Press,
>> Is this correct or are there further papers that are important for the
>> foundation of the generic theorem prover Isabelle?
This archive was generated by a fusion of
Pipermail (Mailman edition) and