Доклад Сергея Артёмова «The consistency of Peano Arithmetic PA is provable in PA, after all»
Сергей Артёмов, заслуженный профессор Городского университета Нью-Йорка, выступил с докладом на заседании семинара «Математическая логика и теория категорий», который состоялся 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
