Self-verifying axiom systems, the incompleteness theorem and related reflection principles. (English) Zbl 0991.03053
In the paper several weak axiom systems that use the subtraction and division primitives (rather than addition and multiplication) to formally encode the theorems of arithmetic are studied. It is shown that under appropriate assumptions it is feasible for such systems to verify their semantic tableaux, Herbrand, and cut-free consistencies and that they are capable of recognizing the consistency of their Hilbert-style deductive proofs as well as some forms of the reflection principle.
Reviewer: Roman Murawski (Poznań)
MSC:
| 03F30 | First-order arithmetic and fragments |
References:
| [1] | Self-reflection principles and NP-hardness 39 (1997) |
| [2] | Collected papers of Gerhard Gentzen (1969) |
| [3] | Technical report (1994) |
| [4] | Proceedings of the third Kurt Gödel symposium 173 pp 325– (1993) |
| [5] | Transfinite recursive progressions of axiomatic theories 27 pp 259– (1962) |
| [6] | Fundamenta Mathematicae 49 pp 35– (1960) |
| [7] | A mathematical introduction to logic (1972) |
| [8] | DOI: 10.1016/0168-0072(87)90066-2 · Zbl 0647.03046 · doi:10.1016/0168-0072(87)90066-2 |
| [9] | Proof theory 81 (1987) |
| [10] | The logic of provability (1993) |
| [11] | Japan Journal on Mathematics 23 pp 39– (1953) |
| [12] | Gödel’s second incompleteness theorem for Q 41 pp 503– (1976) · Zbl 0328.02017 |
| [13] | Handbook on mathematical logic pp 897– (1983) |
| [14] | On tableau consistency in weak theories (1999) |
| [15] | First order logic (1968) · Zbl 0172.28901 |
| [16] | Handbook on mathematical logic pp 821– (1983) |
| [17] | Mathematical logic (1967) · Zbl 0149.24309 |
| [18] | Theory of recursive functions and effective compatibility (1967) |
| [19] | DOI: 10.1007/978-3-7091-9461-4_5 · doi:10.1007/978-3-7091-9461-4_5 |
| [20] | Cuts consistency statements and interpretations 50 pp 423– (1985) · Zbl 0569.03024 |
| [21] | Proceedings of the Jadswin logic conference (Poland) pp 237– (1981) |
| [22] | A note on the undefinability of cuts 48 pp 564– (1983) |
| [23] | Existence and feasibility in arithmetic 36 pp 494– (1971) |
| [24] | Predicative arithmetic (1986) · Zbl 0617.03002 |
| [25] | 17th ACM Symposium on theory of computation pp 285– (1985) |
| [26] | Introduction to mathematical logic (1987) |
| [27] | A solution to a problem by Leon Henkin 20 pp 115– (1955) |
| [28] | Dissertations Mathematica 118 pp 1– (1974) |
| [29] | Journal of Symbolic Logic pp 321– (1968) |
| [30] | Propositional proof systems, the consistency of first-order theories and the complexity of computation 54 pp 1063– (1989) |
| [31] | Bounded propositional logic and complexity theory (1995) · Zbl 0835.03025 |
| [32] | DOI: 10.1007/BF02017501 · Zbl 0633.03056 · doi:10.1007/BF02017501 |
| [33] | On the notation of ordinal numbers 3 pp 150– (1938) |
| [34] | Fundamenta Mathematicae 72 pp 17– (1971) · Zbl 0245.01016 |
| [35] | Grundlagen der Mathematik 2 (1934) · JFM 60.0017.02 |
| [36] | DOI: 10.1137/0207018 · Zbl 0375.68030 · doi:10.1137/0207018 |
| [37] | Metamathematics of first order arithmetic (1991) |
| [38] | Automated reasoning with Semantic Tableaux and related methods pp 415– (2000) |
| [39] | Communications in Mathematics from the University of Carolina 22 pp 595– (1981) |
| [40] | The proceedings of the third Kurt Gödel colloquium 1289 pp 319– (1997) |
| [41] | First order logic and automated theorem proving (1990) · Zbl 0692.68002 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
