PreprintCC BY-SA 4.0arXiv
Mechanizing Gödel's Incompleteness Theorems and Provability Logic
Abstract
We mechanized proof of Gödel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \mathbf{GL}, and related results in the Lean 4 theorem prover.
Related
- Completeness of the Gödel--Löb Provability Logic for Finite Derived Ordinal Topologies
- Self-Referential K-SAT and the Finite Analogue of Gödel's Incompleteness Theorem
- Infinitary provability logic
- Optimizing Proof-Search via Linearization for Gödel-Löb Logic with Tree-Hypersequents
- Fixed points in abstract provability structures
BibTeX
@misc{saitou2026mechanizing,
title = {{Mechanizing Gödel's Incompleteness Theorems and Provability Logic}},
author = {Shogo Saitou and Mashu Noguchi},
howpublished = {arXiv},
year = {2026},
month = sep,
doi = {10.48550/arxiv.2609.13780},
eprint = {2609.13780},
archivePrefix = {arXiv},
url = {https://arxiv.org/abs/2609.13780},
note = {CC BY-SA 4.0},
}
RIS
TY - UNPB
TI - Mechanizing Gödel's Incompleteness Theorems and Provability Logic
AU - Shogo Saitou
AU - Mashu Noguchi
PY - 2026
DA - 2026/09/15
PB - arXiv
DO - 10.48550/arxiv.2609.13780
UR - https://arxiv.org/abs/2609.13780
AB - We mechanized proof of Gödel's first and second incompleteness theorems, Solovay's arithmetical completeness theorem of \mathbf{GL}, and related results in the Lean 4 theorem prover.
ER -