Serial properties, selector proofs and the provability of consistency

Abstract 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 Con^S₏₀, 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 Con₏₀, 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 Con₏₀ but rather with the consistency scheme Con^S₏₀, 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 Con^S₏₀ in PA. These findings show that PA proves its consistency whereas, by Gödel’s second incompleteness theorem, PA cannot prove its uniform consistency.