Non-Compact Proofs
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2025
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866915675255078912 |
|---|---|
| author | Artemov, Sergei |
| author_facet | Artemov, Sergei |
| contents | 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ödel'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ödel's theorem. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2512_12892 |
| institution | arXiv |
| publishDate | 2025 |
| record_format | arxiv |
| spellingShingle | Non-Compact Proofs Artemov, Sergei Logic 03A05, 03B30, 03F03, 03F07, 03F30, 03F40 F.3.0; F.4.0; F.4.1; I.2.0; I.2.3 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ödel'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ödel's theorem. |
| title | Non-Compact Proofs |
| topic | Logic 03A05, 03B30, 03F03, 03F07, 03F30, 03F40 F.3.0; F.4.0; F.4.1; I.2.0; I.2.3 |
| url | https://arxiv.org/abs/2512.12892 |