*To*: Ken Kubota <mail at kenkubota.de>*Subject*: Re: [isabelle] Axiom of Choice in Isabelle, Literature on Foundation*From*: Lawrence Paulson <lp15 at cam.ac.uk>*Date*: Sat, 3 Mar 2018 10:14:01 +0000*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <8379B195-0465-46C6-84A9-50841CCE5209@kenkubota.de>*References*: <8379B195-0465-46C6-84A9-50841CCE5209@kenkubota.de>

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?

**Follow-Ups**:

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

- Previous by Date: [isabelle] Parsing abbreviations in a local context
- Next by Date: [isabelle] Approximation tactic for very large numbers
- Previous by Thread: [isabelle] Axiom of Choice in Isabelle, Literature on Foundation
- Next by Thread: [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