Consistency formula is strictly stronger in PA than PA-consistency
Sergei Nikolaevich Artemov · arXiv (Cornell University) · 2025
In this note, we show that, despite the widespread assumption, the consistency formula for Peano Arithmetic PA, Con(PA), "for all x, x is not a code of a derivation of (0=1)," is not equivalent in PA to the consistency of PA. Specifically, we demonstrate that "PA is consistent" is provably in PA equivalent to the series ConS(PA) of arithmetical sentences "n is not a code of a derivation of (0=1)" for n=0,1,2,.... Since Con(PA) is strictly stronger in PA than ConS(PA), the unprovability of Con(PA) in PA does not yield the unprovability of PA-consistency.