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



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?


Kind regards,

Ken Kubota

____________________

Ken Kubota
http://doi.org/10.4444/100





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