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

Sergei Artemov
Distinguished Professor of the Graduate Center of the City University of New York

«The consistency of Peano Arithmetic PA is provable in PA, after all»

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