Abstract: We show that PA consistency is mathematically equivalent to the serial property, which we call the consistency scheme ConS(PA):
"n is not a proof of 0=1", for n=0,1,2,... .
The proof of this equivalence is formalizable in PA. Since the standard consistency formula Con(PA)
"for all x, x is not a code of a proof of 0=1"
is strictly stronger than the scheme ConS(PA) in PA, Goedel's Second Incompleteness theorem, stating that PA |-\- Con(PA) does not yield the unprovability of PA consistency. Hence, the widespread belief that a consistent theory cannot establish its consistency has never been justified.
Moreover, we show that this belief is false. The question of proving PA consistency in PA reduces to proving the scheme ConS(PA) in PA. We build on Hilbert's ideas and prove ConS(PA) in PA.
This talk is a "dress rehearsal" for the speaker's plenary talk at the ASL meeting on May 13, 2025.
Reference:
S.Artemov "Serial Properties, Selector Proofs, and the Provability of Consistency," Journal of Logic and Computation, Volume 35, Issue 3, April 2025.
https://doi.org/10.1093/logcom/exae034
Published: 26 July 2024.