Re: [isabelle] Axiom of Choice in Isabelle, Literature on Foundation



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 <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 <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 <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 <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.