arXiv · 2512.12892
Non-Compact Proofs
Abstract
Non-compact proofs are a class of reasoning that is used in mathematics but overlooked in the analysis of (un)provability of consistency. We focus on proofs of arithmetical statements (*) "for any natural number n, F(n)." A proof of (*) is called 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 given by the standard proof of Mostowski's 1952 reflexivity theorem: PA proves the consistency of its finite fragments. It turns out that G\"odel's second incompleteness theorem prohibits compact proofs and does not rule out non-compact proofs of PA-consistency formalizable in PA. This explains how the recent proof of PA-consistency in PA works. It essentially formalizes in PA the explicit version of Mostowski's proof, which is not in the scope of G\"odel's theorem.
Explore related subjects
Keep this discovery
Sergei Artemov. 2025-12-15. Non-Compact Proofs. https://arxiv.org/abs/2512.12892
Cite the original work for its findings. Save a collection to share your selection of sources.