Sergei Artemov's talk "The consistency of Peano Arithmetic PA is provable in PA, after all"

Sergei Artemov, Distinguished Professor at the City University of New York, gave a talk at the seminar "Mathematical Logic and Category Theory," which took place on September 13.

Abstract 

We show that the famous consistency formula Con(PA) for Peano Arithmetic PA,  "no x is a code of a derivation of (0=1)," is strictly stronger in PA than the statement "PA is consistent." Hence, despite the widespread belief, the unprovability of Con(PA) in PA does not yield the unprovability of consistency. Furthermore, we demonstrate that "PA is consistent" is provable in PA. These findings apply to a broad class of formal theories, including ZF set theory.

We also discuss the potential impact of these findings on the foundations of mathematics and the theory of cognition.

References:

Sergei Artemov, Consistency formula is strictly stronger in PA than PA-consistency. https://doi.org/10.48550/arXiv.2508.20346

Sergei Artemov, Serial properties, selector proofs and the provability of consistency, Journal of Logic and Computation, Volume 35, Issue 3, April 2025, exae034, https://doi.org/10.1093/logcom/exae034

Видео доклада Сергея Артёмова «The consistency of Peano Arithmetic PA is provable in PA, after all»

Video: МЛ ЛогЛинФФ