Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Standard

Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant. / Popescu, Andrei; Traytel, Dmitriy.

I: Journal of Automated Reasoning, Bind 65, 2021, s. 1027–1070.

Publikation: Bidrag til tidsskrift › Tidsskriftartikel › Forskning › fagfællebedømt

Harvard

Popescu, A & Traytel, D 2021, 'Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant', Journal of Automated Reasoning, bind 65, s. 1027–1070. https://doi.org/10.1007/s10817-021-09599-8

APA

Popescu, A., & Traytel, D. (2021). Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant. Journal of Automated Reasoning, 65, 1027–1070. https://doi.org/10.1007/s10817-021-09599-8

Vancouver

Popescu A, Traytel D. Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant. Journal of Automated Reasoning. 2021;65:1027–1070. https://doi.org/10.1007/s10817-021-09599-8

Author

Popescu, Andrei ; Traytel, Dmitriy. / Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant. I: Journal of Automated Reasoning. 2021 ; Bind 65. s. 1027–1070.

Bibtex

@article{5ff9e45ba74f4ae4a8904ae97b39958d,
title = "Distilling the Requirements of G{\"o}del{\textquoteright}s Incompleteness Theorems with a Proof Assistant",
abstract = "We present an abstract development of G{\"o}del{\textquoteright}s incompleteness theorems, performed with the help of the Isabelle/HOL proof assistant. We analyze sufficient conditions for the applicability of our theorems to a partially specified logic. In addition to the usual benefits of generality, our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser{\textquoteright}s variation of the first theorem, Jeroslow{\textquoteright}s variation of the second theorem, and the {\'S}wierczkowski–Paulson semantics-based approach. As part of the validation of our framework, we upgrade Paulson{\textquoteright}s Isabelle proof to produce a mechanization of the second theorem that does not assume soundness in the standard model, and in fact does not rely on any notion of model or semantic interpretation.",
author = "Andrei Popescu and Dmitriy Traytel",
year = "2021",
doi = "10.1007/s10817-021-09599-8",
language = "English",
volume = "65",
pages = "1027–1070",
journal = "Journal of Automated Reasoning",
issn = "0168-7433",
publisher = "Springer Netherlands",

}

RIS

TY - JOUR

T1 - Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant

AU - Popescu, Andrei

AU - Traytel, Dmitriy

PY - 2021

Y1 - 2021

N2 - We present an abstract development of Gödel’s incompleteness theorems, performed with the help of the Isabelle/HOL proof assistant. We analyze sufficient conditions for the applicability of our theorems to a partially specified logic. In addition to the usual benefits of generality, our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser’s variation of the first theorem, Jeroslow’s variation of the second theorem, and the Świerczkowski–Paulson semantics-based approach. As part of the validation of our framework, we upgrade Paulson’s Isabelle proof to produce a mechanization of the second theorem that does not assume soundness in the standard model, and in fact does not rely on any notion of model or semantic interpretation.

AB - We present an abstract development of Gödel’s incompleteness theorems, performed with the help of the Isabelle/HOL proof assistant. We analyze sufficient conditions for the applicability of our theorems to a partially specified logic. In addition to the usual benefits of generality, our abstract perspective enables a comparison between alternative approaches from the literature. These include Rosser’s variation of the first theorem, Jeroslow’s variation of the second theorem, and the Świerczkowski–Paulson semantics-based approach. As part of the validation of our framework, we upgrade Paulson’s Isabelle proof to produce a mechanization of the second theorem that does not assume soundness in the standard model, and in fact does not rely on any notion of model or semantic interpretation.

U2 - 10.1007/s10817-021-09599-8

DO - 10.1007/s10817-021-09599-8

M3 - Journal article

VL - 65

SP - 1027

EP - 1070

JO - Journal of Automated Reasoning

JF - Journal of Automated Reasoning

SN - 0168-7433

ER -

ID: 278041128