Non-Compact Proofs

TL;DR

This paper explores non-compact proofs in arithmetic, showing they are not ruled out by G"odel's second incompleteness theorem and explaining recent PA-consistency proofs.

Contribution

It clarifies the role of non-compact proofs in arithmetic and demonstrates their compatibility with G"odel's theorem, providing insight into recent PA-consistency proofs.

Findings

Non-compact proofs are not excluded by G"odel's second incompleteness theorem.

Recent PA-consistency proofs are formalizable within PA using non-compact reasoning.

Standard proofs like Mostowski's are examples of non-compact reasoning in arithmetic.

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.