Serial Properties, Selector Proofs, and the Provability of Consistency
Fuente:
arXiv
Saved in:
| Main Author: | |
|---|---|
| Format: | Preprint |
| Published: |
2024
|
| Subjects: | |
| Online Access: | |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1866911802807287808 |
|---|---|
| author | Artemov, Sergei |
| author_facet | Artemov, Sergei |
| contents | For Hilbert, the consistency of a formal theory T is an infinite series of statements "D is free of contradictions" for each derivation D and a consistency proof is i) an operation that, given D, yields a proof that D is free of contradictions, and ii) a proof that (i) works for all inputs D. Hilbert's two-stage approach to proving consistency naturally generalizes to the notion of a finite proof of a series of sentences in a given theory. Such proofs, which we call selector proofs, have already been tacitly employed in mathematics. Selector proofs of consistency, including Hilbert's epsilon substitution method, do not aim at deriving the Gödelian consistency formula Con(T) and are thus not precluded by Gödel's second incompleteness theorem. We give a selector proof of consistency of Peano Arithmetic PA and formalize this proof in PA. |
| format | Preprint |
| id |
arxiv_https___arxiv_org_abs_2403_12272 |
| institution | arXiv |
| publishDate | 2024 |
| record_format | arxiv |
| spellingShingle | Serial Properties, Selector Proofs, and the Provability of Consistency Artemov, Sergei Logic 03A05, 03B30, 03F03, 03F07, 03F30, 03F40 F.3.0; F.4.0; F.4.1; I.2.0; I.2.3 For Hilbert, the consistency of a formal theory T is an infinite series of statements "D is free of contradictions" for each derivation D and a consistency proof is i) an operation that, given D, yields a proof that D is free of contradictions, and ii) a proof that (i) works for all inputs D. Hilbert's two-stage approach to proving consistency naturally generalizes to the notion of a finite proof of a series of sentences in a given theory. Such proofs, which we call selector proofs, have already been tacitly employed in mathematics. Selector proofs of consistency, including Hilbert's epsilon substitution method, do not aim at deriving the Gödelian consistency formula Con(T) and are thus not precluded by Gödel's second incompleteness theorem. We give a selector proof of consistency of Peano Arithmetic PA and formalize this proof in PA. |
| title | Serial Properties, Selector Proofs, and the Provability of Consistency |
| 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/2403.12272 |