Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Skolemization in first-order logic without the...

Email Gateway (Aug 22 2022 at 16:53):

From: Ken Kubota <mail@kenkubota.de>
Dear Larry Paulson,

Thank you very much for your kind answer.
Please allow me to add a note and rephrase the second question, and add a minor
amendment to Christoph Benzmüller's paper you referred to.

1. I apologize for having overlooked that indeed there is a possibility for the
   model-theoretic justification of Skolemization in first-order logic without the
   Axiom of Choice, as pointed out by Peter B. Andrews: "If G has a model, it has
   a denumerable model by the Löwenheim-Skolem Theorem [...] Since the domain of
   individuals of M is in one-one correspondence with the natural numbers, we may
   assume it is well-ordered. (This will enable us to avoid any appeal to the
   Axiom of Choice in the argument below.)" [Andrews, 2002, p. 168]

2. If one publication (or maybe two) should be taken as main reference for
   Isabelle (the logical framework, not an object logic like Isabelle/HOL)

• preferably a printed publication instead of just an online file - which one
  would you choose?
  The literature on Isabelle is so vast that it becomes difficult to single out a
  specific publication.
  My first guess would be
  [29] Lawrence C. Paulson. Isabelle: A Generic Theorem Prover. Springer, 1994.
  LNCS 828.
  which is newer than your 1989 article available online at
  https://arxiv.org/pdf/cs/9301105.pdf

Concerning Christoph Benzmüller's paper "Automation of Higher-Order Logic" at
http://page.mi.fu-berlin.de/cbenzmueller/papers/B5.pdf
it should be noted that the first formulation of Peter's logic Q0 can be found
in [Andrews, 1963], not only in the much later (Andrews, 1972a), as suggested
by the paper: "While Church axiomatized the logical connectives of STT in a
rather conventional fashion [...], Henkin (1963) and Andrews (1972a, 2002)
provided a formulation of STT in which the sole logical connective was equality
(at all types)." (p. 14)

[Andrews, 1963] directly follows [Henkin, 1963] in Fundamenta Mathematicae 52:
http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52123.pdf
http://matwbn.icm.edu.pl/ksiazki/fm/fm52/fm52124.pdf

Their collaboration is described in [Andrews, 2014b], see the quote from there
on p. 11 at
http://www.owlofminerva.net/files/fom.pdf

For the references, please see: http://doi.org/10.4444/100.111

Kind regards,

Ken Kubota

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

Email Gateway (Aug 22 2022 at 16:53):

From: Lawrence Paulson <lp15@cam.ac.uk>
The 1994 book is frequently cited, but it is merely the three manuals of the time joined together. Those manuals continued to be updated for years afterwards, so that book is a snapshot, and it doesn't present any theory. The 1989 paper covers Isabelle as a logical framework. In the past year or two, papers have emerged giving an account of the semantics of Isabelle/HOL, including type classes and other extended definitional mechanisms.

Larry Paulson

Last updated: Apr 24 2024 at 01:07 UTC