Sergei Artemov, Dept. of Philosophy, The Graduate Center, CUNY— Non-compact proofs are used in mathematics but overlooked in the analysis of (un)provability of consistency. We focus on arithmetical proofs of universal statements (*) "for any natural number n, F(n)." A proof of (*) is compact if all proofs of F(n)'s for n=0,1,2,... fit into some finitely axiomatized fragment of Peano Arithmetic PA. An example of non-compact reasoning is the standard proof of Mostowski's 1952 reflexivity theorem: PA proves the consistency of its finite fragments.

It turns out that Gödel's Second Incompleteness Theorem, G2, prohibits compact proofs but does not rule out non-compact proofs of PA-consistency formalizable in PA. This explains why and how the recent proofs of PA-consistency in PA work: they essentially formalize in PA the explicit version of Mostowski's non-compact proof and use Gödelian provable explicit reflection to rid redundant provability operators.

These findings yield a new foundational reading of G2: the consistency of PA is not provable within a finite fragment of PA, complemented with the positive message: the consistency of PA is provable within the whole PA. This perspective suggests that Gödel's theorem does not represent a failure of the system to "know" its own consistency, but rather a structural limit on how that knowledge can be packaged into a single finite string.