Email Gateway (Aug 22 2022 at 20:30): Email Gateway (Aug 22 2022 at 20:30):From: Ken Kubota <mail@kenkubota.de>
The formalization by Russell O’Connor is also very helpful because of the type safety:
III. The Proofs by Russell O'Connor (in Coq) and Lawrence C. Paulson (in
Isabelle)A particularly elegant formulation of Goedel's First Incompleteness Theorem was
presented by Russell O'Connor using the proof assistant Coq, as he takes
advantage of "type safety by coding using an inductive type" [Russell O'Connor,
e-mail to Ken Kubota, February 13, 2016], such that all three language levels
use a different type. A short description is given in [O'Connor, 2006]
available online athttp://arxiv.org/pdf/cs/0505034v2.pdf
The formal proof is available at
http://www.lix.polytechnique.fr/coq/pylons/contribs/view/Goedel/trunk
O'Connor uses different types for the three different levels of language:
L1: type "prop"
L2: type "Formula" (which may contain expressions of type "Term")
L3: type "nat"
Full text:
https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2016-July/msg00029.html
Ken Kubota
http://doi.org/10.4444/100
Am 06.09.2019 um 13:20 schrieb Lawrence Paulson <lp15@cam.ac.uk>:
I have written two papers about this proof development. One is aimed at logicians, while the other focuses on formalisation issues.
• A Machine-Assisted Proof of Gödel’s Incompleteness Theorems for the Theory of Hereditarily Finite Sets.
Review of Symbolic Logic 7 3 (2014), 484–498.• A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle.
J. Automated Reasoning 55 1 (2015), 1–37.https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic-mine.pdf
https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdfThere are many articles and books written about Gödel’s theorems. The Isabelle Col code itself is not in any way relevant.
Larry Paulson
On 5 Sep 2019, at 14:38, Juho Kupiainen <juho.kupiainen.general.ai.group@gmail.com> wrote:
I want to gain an understanding of Gödel's incompleteness theorems,
https://www.isa-afp.org/entries/Incompleteness.htmlI would like to do this by understanding the above code from Isabelle
kernel code to all the dependencies. I'm completely new to Isabelle. I
think starting with a rough "in English" understanding of all the code
could be beneficial. I can pay for your help.
Email Gateway (Aug 22 2022 at 20:38):From: Juho Kupiainen <juho.kupiainen.general.ai.group@gmail.com>
I want to gain an understanding of Gödel's incompleteness theorems,
https://www.isa-afp.org/entries/Incompleteness.html
I would like to do this by understanding the above code from Isabelle
kernel code to all the dependencies. I'm completely new to Isabelle. I
think starting with a rough "in English" understanding of all the code
could be beneficial. I can pay for your help.
My email: juho.kupiainen.general.ai.group@gmail.com
Email Gateway (Aug 22 2022 at 20:39):From: Lawrence Paulson <lp15@cam.ac.uk>
I have written two papers about this proof development. One is aimed at logicians, while the other focuses on formalisation issues.
• A Machine-Assisted Proof of Gödel’s Incompleteness Theorems for the Theory of Hereditarily Finite Sets.
Review of Symbolic Logic 7 3 (2014), 484–498.
• A Mechanised Proof of Gödel's Incompleteness Theorems using Nominal Isabelle.
J. Automated Reasoning 55 1 (2015), 1–37.
https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-logic-mine.pdf
https://www.cl.cam.ac.uk/~lp15/papers/Formath/Goedel-ar.pdf
There are many articles and books written about Gödel’s theorems. The Isabelle Col code itself is not in any way relevant.
Larry Paulson
Last updated: Apr 18 2024 at 04:17 UTC