Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Axiom of Choice in Isabelle, Literature on Fou...

view this post on Zulip Email Gateway (Aug 22 2022 at 16:58):

From: Ken Kubota <mail@kenkubota.de>
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.

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

view this post on Zulip Email Gateway (Aug 22 2022 at 17:00):

From: Lawrence Paulson <lp15@cam.ac.uk>
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

Last updated: Apr 16 2024 at 20:15 UTC