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