Event Detail

Fri Apr 26, 2024
Evans 60
4–6 PM
Logic Colloquium
Sergei Artemov
The Provability of Consistency

Gödel’s second incompleteness theorem does not apply to Hilbert’s approach to proving consistency in the way it was previously thought. This is because Hilbert’s understanding of consistency as a series of claims “D is consistent” for each PA-derivation D is not provably in PA equivalent to the Gödelian consistency formula Con(PA). Kripke showed in 2022 that Hilbert’s epsilon-substitution method for PA, HES, fails for non-Gödelian reasons. We modify HES to prove the Hilbertian consistency of PA within PA. As expected, our proof of consistency does not yield a PA-derivation of Con(PA). This undermines the unprovability of consistency thesis that “there exists no consistency proof of a system that can be formalized in the system itself” (Encyclopedia Britannica).

[text of paper]