Explicit provability and constructive semantics.

*(English)*Zbl 0980.03059Gödel introduced a calculus of provability, which is the modal logic known as S4 now, and left open its exact intended semantics. As is also well known, Solovay established afterwards that arithmetical provability is formalized as a modality by another modal logic which is usually called GL. This gap is filled in this paper by a logic, called LP, of propositions and proofs, in which, by making use of the newly introduced notion of proof constants, explicit provability is formalized as “(a proof constant) \(c\) is a (code of) proof of (a formula)” not as the usual “there exists some (code of) proof of (a formula)”. The author proves not only the completeness of LP with respect to the standard arithmetical provability interpretation but also that LP is considered as a realization of the modal logic S4 in the sense, in short, that the S4 modality formalizes the meta-level existence of some proof constant \(c\) such that “\(c\) is a (code of) proof of (a formula)”. Thus the provability interpretation of S4 modality is established through explicit provability. Moreover, according to the well-known correspondence between the modal logic S4 and intuitionistic logic this provability interpretation of S4 achieves Gödel’s objective of defining intuitionistic propositional logic via classical proofs, and provides a Brouwer-Heyting-Kolmogorov style provability semantics for intuitionistic logic. The author also remarks that the logic LP may be regarded as a unified underlying structure for intuitionistic logic, modal logics, typed combinatory logic, and lambda-calculus.

Reviewer: Osamu Sonobe (Follonica)

##### MSC:

03F45 | Provability logics and related algebras (e.g., diagonalizable algebras) |

03B45 | Modal logic (including the logic of norms) |

03B20 | Subsystems of classical logic (including intuitionistic logic) |

03F50 | Metamathematics of constructive systems |

03B40 | Combinatory logic and lambda calculus |

##### Keywords:

Gödel’s calculus of provability; provability logic; modal logic S4; explicit provability; arithmetical provability interpretation; intuitionistic logic; BHK semantics; lambda-calculus; provability semantics##### References:

[1] | Handbook of logic in computer science 2 pp 118– (1992) |

[2] | DOI: 10.2307/2023664 |

[3] | Acta Philosophica Fennica 16 pp 153– (1963) |

[4] | DOI: 10.1007/3-540-63045-7_27 |

[5] | Modal and intensional logics (1978) |

[6] | Feys. Modal logic (Russian translation) (1974) |

[7] | Computer Science Logic 2000 1862 pp 527– (2000) |

[8] | Annals of pure and applied logic (2001) |

[9] | Journal of Philosophical Logic 12 pp 261– (1983) |

[10] | Advances in modal logic 1 pp 307– (1996) |

[11] | DOI: 10.2307/2274147 · Zbl 0587.03016 |

[12] | Soviet Mathematics Doklady 33 pp 569– (1986) |

[13] | Selected works of A. N. Kolmogorov. Volume I: Mathematics and mechanics pp 451– (1985) |

[14] | DOI: 10.1007/BF01186549 · Zbl 0004.00201 |

[15] | Logic, methodology and philosophy of science 2 pp 31– (1965) |

[16] | DOI: 10.2307/2269016 · Zbl 0063.03260 |

[17] | Knowledge and Belief (1962) |

[18] | Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie (1934) · Zbl 0009.38501 |

[19] | DOI: 10.1007/BF02028143 · JFM 57.0053.01 |

[20] | Sitzungsberichte der Preussischen Akademie von Wissenschaften. Physikalisch-mathematische Klasse pp 42– (1930) |

[21] | Intuitionism and proof theory pp 101– (1970) |

[22] | Intensional mathematics pp 63– (1985) · Zbl 0547.00010 |

[23] | DOI: 10.2307/2274102 · Zbl 0597.03012 |

[24] | Topoi (1979) · Zbl 0429.18005 |

[25] | Theoria 44 pp 38– (1978) |

[26] | Kurt Gödel Collected Works III pp 86– (1995) |

[27] | DOI: 10.1111/j.1746-8361.1958.tb01464.x · Zbl 0090.01003 |

[28] | Ergebnisse Math. Colloq. 4 pp 39– (1933) |

[29] | Proofs and types (1989) · Zbl 0671.68002 |

[30] | Labelled deductive systems (1994) |

[31] | DOI: 10.1016/0168-0072(86)90043-6 · Zbl 0626.03050 |

[32] | Intensional mathematics pp 121– (1985) · Zbl 0547.00010 |

[33] | Logic colloquium ’78 pp 159– (1979) |

[34] | Algebra and logic pp 87– (1975) |

[35] | Handbook of proof theory pp 475– (1998) |

[36] | DOI: 10.1016/0898-1221(79)90044-0 · Zbl 0418.68079 |

[37] | Combinatory logic (1958) |

[38] | Diagonalization and self-reference (1994) · Zbl 0810.03001 |

[39] | Handbook of proof theory pp 683– (1998) |

[40] | Self-reference and modal logic (1985) · Zbl 0596.03001 |

[41] | Modal logic (1997) · Zbl 0871.03007 |

[42] | DOI: 10.1007/3-540-63045-7_35 |

[43] | DOI: 10.1305/ndjfl/1093635417 · Zbl 0713.03009 |

[44] | Intensional mathematics pp 1– (1985) |

[45] | Technical Report CFIS2000-05 (2000) |

[46] | Intensional mathematics pp 11– (1985) |

[47] | DOI: 10.1007/BFb0060636 |

[48] | Intensional mathematics pp 81– (1985) · Zbl 0547.00010 |

[49] | The mathematics of metamathematics (1963) |

[50] | Electronic Notes in Computer Science 1 (1995) |

[51] | Kurt Gödel Collected Works. Volume III pp 62– (1995) |

[52] | The logic of provability (1993) |

[53] | DOI: 10.2307/2322568 · Zbl 0562.03007 |

[54] | The unprovability of consistency: An essay in modal logic (1979) · Zbl 0409.03009 |

[55] | DOI: 10.1017/S0305004100013463 · JFM 61.1026.07 |

[56] | Proceedings of the Logic at Work conference, Amsterdam, 1992 (1996) |

[57] | Kon. Nederl. Akad. Wetensch. Afd. Let. Med., Nieuwe Serie 19 pp 357– (1956) |

[58] | DOI: 10.1007/BFb0013061 |

[59] | DOI: 10.1016/S0304-3975(98)00305-3 · Zbl 0930.03082 |

[60] | Matematicheskii Sbornik 35 pp 263– (1928) |

[61] | Foundations of constructive mathematics (1980) |

[62] | Constructive mathematical logic from the viewpoint of the classical one (1977) |

[63] | Electronic Notes in Theoretical Computer Science 6 (1997) |

[64] | Intensional mathematics pp 47– (1985) · Zbl 0547.00010 |

[65] | Proceedings of the 8th annual IEEE Symposium on Logic in Computer Science pp 39– (1993) |

[66] | Handbook of proof theory pp 337– (1998) |

[67] | Logic and structure (1994) |

[68] | Computational logic and proof theory. Proceedings of the Third Kurt Gödel Colloquium, Brno, August 1993 713 pp 71– (1993) |

[69] | Handbook of philosophical logic 3 pp 225– (1986) |

[70] | Technical Report IAM 92-004 (1992) |

[71] | Technical Report CFIS99-11 (1999) |

[72] | Introduction to mathematical logic (1987) |

[73] | DOI: 10.2307/2275696 · Zbl 0860.03016 |

[74] | Soviet Mathematics Doklady 3 pp 227– (1962) |

[75] | Technical Report CFIS 99-12 (1999) |

[76] | DOI: 10.2307/2268135 · Zbl 0037.29409 |

[77] | Logic, Language and Computation. Volume 3 · Zbl 0885.00030 |

[78] | DOI: 10.2307/1969038 · Zbl 0060.06207 |

[79] | Advances in modal logic 2 (2001) |

[80] | Proof theory of modal logics. workshop proceedings (1994) |

[81] | Automated deduction–CADE-16. Proceedings of the 16th International Conference on Automated Deduction, Trento, Italy, July 1999 1632 pp 267– (1999) |

[82] | Intuitionistic type theory (1984) |

[83] | Logic, methodology and philosophy of science VI pp 153– (1982) |

[84] | DOI: 10.2307/2964179 · Zbl 0080.24203 |

[85] | Intuitionism and proof theory pp 227– (1970) |

[86] | Abstracts of the 4th All-union conference on mathematical logic pp 73– (1976) |

[87] | Logique & Analyse 133 pp 5– (1991) |

[88] | DOI: 10.2307/2275276 · Zbl 0767.03003 |

[89] | Selected works of A. N. Kolmogorov. Volume I: Mathematics and Mechanics pp 452– (1985) |

[90] | Handbook of proof theory pp 407– (1998) |

[91] | Constructivism in mathematics. An introduction 1 (1988) · Zbl 0653.03040 |

[92] | Basic proof theory (1996) |

[93] | Kurt Gödel Collected Works. Volume I pp 296– (1986) |

[94] | Technical Report CFIS 98-06 (1998) |

[95] | Logic and foundations of mathematics pp 11– (1968) |

[96] | Technical Report MSI 95-02 (1997) |

[97] | Proof theory (1975) · Zbl 0354.02027 |

[98] | Technical Report MSI 95-29 (1995) |

[99] | DOI: 10.1007/BF02757006 · Zbl 0352.02019 |

[100] | DOI: 10.1016/0168-0072(94)90007-8 · Zbl 0796.03029 |

[101] | Theoretical aspects of reasoning about knowledge–III Proceedings pp 257– (1990) |

[102] | Soviet Mathematics Doklady 32 pp 403– (1985) |

[103] | Computer Science Logic 2000 1862 pp 371– (2000) |

[104] | Voprosy Kibernetiki: Nonclassical logics and application pp 3– (1982) |

[105] | Annals of Pure and Applied Logic (2001) |

[106] | Technical Report CFIS 2000-06 (2000) |

[107] | DOI: 10.1007/3-540-63045-7_18 |

[108] | Proceedings of the fifth annual IEEE Symposium on Logic in Computer Science pp 95– (1990) |

[109] | Formal systems and recursive functions. Proceedings of the 8th Logic Colloquium pp 92– (1965) |

[110] | Acta Philosophica Fennica 16 pp 83– (1963) |

[111] | Lectures in Modern Mathematics III pp 95– (1965) |

[112] | DOI: 10.2307/2964110 · Zbl 0117.01005 |

[113] | Logic, methodology and philosophy of science. Proceedings of the 1960 International Congress pp 198– (1962) |

[114] | Tools and techniques in modal logic (1999) · Zbl 0927.03002 |

[115] | Handbook of theoretical computer science. Volume B, Formal models and semantics pp 789– (1990) |

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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.