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 (section 5.1) and the references cited there.

Larry Paulson

> On 2 Mar 2018, at 20:09, Ken Kubota <mail at> 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, <>, 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, <>, 
> p. 247.) But in the following only practical reasons are given.
> 2. According to
> <> (p. 3)
> <> (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.