Serial properties, selector proofs and the provability of consistency

The consistency of a theory means that each of its formal derivations D₀, D₁, D₂, … is free of contradictions. For Peano Arithmetic PA, after the standard coding of derivations by numerals, PA-consistency is directly represented by the consistency scheme ConSPA, which is a series of arithmetical statements ‘n is not a code of a derivation of $\ (0=1)$’ for numerals n=0,1,2,…. We note that the consistency formula ConPA, ∀ x ‘x is not a code of a derivation of $(0=1)$,’ is strictly stronger in PA than PA-consistency and corresponds to some other property, which we call uniform consistency. When studying the provability of consistency in PA we ought to work not with the consistency formula ConPA but rather with the consistency scheme ConSPA, which adequately represents PA-consistency. This paper introduces the Hilbert-inspired notion of proof of an infinite series of formulas in a theory and proves PA-consistency in the form ConSPA in PA. These findings show that PA proves its consistency whereas, by Gödel’s second incompleteness theorem, PA cannot prove its uniform consistency.