PAPER / ARXIV:2609.13780

Mechanizing Gödel's Incompleteness Theorems and Provability Logic

Shogo Saitou , Mashu Noguchi

Lógica · cruzada Lógica em ciência da computação

RESUMO

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.

NO MESMO MAPA

Papers relacionados

math.LO15 de set. de 2026

Medvedev logic is undecidable

Rodrigo Nicolau Almeida , Søren Brinck Knudstorp

Mechanizing Gödel's Incompleteness Theorems and Provability Logic

Papers relacionados

Medvedev logic is undecidable

Finite Dependence and Invariance Hierarchies for Finitely Supported Structures

A Catalogue of Properties of Binary Relations: Entailments, Incompatibilities, and Independence Results

Inequalities and equalities of means in Constructive Mathematics

Rice's Theorem under Self-Modification: Elevation Operators and a Normal Form

Medvedev Logic is Not Decidable. It is π01 -complete. Who Would Have Guessed?