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

Research output: Contribution to journal › Journal article › Research › peer-review

Standard

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

In: Journal of Automated Reasoning, Vol. 65, 2021, p. 1027–1070.

Research output: Contribution to journal › Journal article › Research › peer-review

Harvard

Popescu, A & Traytel, D 2021, 'Distilling the Requirements of Gödel’s Incompleteness Theorems with a Proof Assistant', Journal of Automated Reasoning, vol. 65, pp. 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. In: Journal of Automated Reasoning. 2021 ; Vol. 65. pp. 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