[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 
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?
> 





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