Hostname: page-component-cd9895bd7-mkpzs Total loading time: 0 Render date: 2024-12-24T14:14:08.510Z Has data issue: false hasContentIssue false
  • English
  • Français

Explicit Provability and Constructive Semantics

Published online by Cambridge University Press:  15 January 2014

Sergei N. Artemov
Sergei N. Artemov*
Affiliation:
Department of Computer Science, Cornell University, Ithaca, New york 14853, USAE-mail: [email protected] Department of Mathematics, Moscow State University, Moscow 119899, Russia
Get access Rights & Permissions [Opens in a new window]

Abstract

In 1933 Gödel introduced a calculus of provability (also known as modal logic S4) and left open the question of its exact intended semantics. In this paper we give a solution to this problem. We find the logic LP of propositions and proofs and show that Gödel's provability calculus is nothing but the forgetful projection of LP. This also achieves Gödel's objective of defining intuitionistic propositional logic Int via classical proofs and provides a Brouwer-Heyting-Kolmogorov style provability semantics for Int which resisted formalization since the early 1930s. LP may be regarded as a unified underlying structure for intuitionistic, modal logics, typed combinatory logic and λ-calculus.

Type
Research Article
Information
Bulletin of Symbolic Logic , Volume 7 , Issue 1 , March 2001 , pp. 1 - 36
Copyright
Copyright © Association for Symbolic Logic 2001

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

REFERENCES

[1] Allen, S., Constable, R., Howe, D., and Aitken, W., The semantics of reflected proofs, Proceedings of the fifth annual IEEE Symposium on Logic in Computer Science (Los Alamitos, California, USA), IEEE Computer Society Press, 1990, pp. 95–107.Google Scholar
[2] Alt, J. and Artemov, S., Reflective λ-calculus, Technical Report CFIS 2000-06, Cornell University, 2000.Google Scholar
[3] Artemov, S., Applications of modal logic in proof theory, Voprosy Kibernetiki: Nonclassical logics and application, Nauka, Moscow, 1982, (in Russian), pp. 3–20.Google Scholar
[4] Artemov, S., Non-arithmeticity of truth predicate logics of provability, Soviet Mathematics Doklady, vol. 32 (1985), no. 2, pp. 403–405.Google Scholar
[5] Artemov, S., Kolmogorov logic of problems and a provability interpretation of intuitionistic logic, Theoretical aspects of reasoning about knowledge—III Proceedings, Morgan Kaufman Pbl., 1990, pp. 257–272.Google Scholar
[6] Artemov, S., Logic of proofs, Annals of Pure and Applied Logic, vol. 67 (1994), no. 1, pp. 29–59.CrossRefGoogle Scholar
[7] Artemov, S., Operational modal logic, Technical Report MSI 95-29, Cornell University, 1995.Google Scholar
[8] Artemov, S., Proof realizations of typed λ-calculi, Technical Report MSI 95-02, Cornell University, 1997.Google Scholar
[9] Artemov, S., Logic of proofs: a unified semantics for modality and λ-terms, Technical Report CFIS 98-06, Cornell University, 1998.Google Scholar
[10] Artemov, S., On explicit reflection in theorem proving and formal verification, Automated deduction—CADE-16. Proceedings of the 16th International Conference on Automated Deduction, Trento, Italy, July 1999, Lecture Notes in Artificial Intelligence, vol. 1632, Springer-Verlag, 1999, pp. 267–281.Google Scholar
[11] Artemov, S., Operations on proofs that can be specified by means of modal logic, Advances in modal logic, vol. 2, CSLI Publications, Stanford University, 2001.Google Scholar
[12] Artemov, S., Unified semantics for modality and λ-terms via proof polynomials, Logic, Language and Computation. Volume 3, CSLI Publications, Stanford University, (to appear).Google Scholar
[13] Artemov, S., Kazakov, E., and Shapiro, D., Epistemic logic with justifications, Technical Report CFIS 99-12, Cornell University, 1999.Google Scholar
[14] Artemov, S. and Montagna, F., On first order theories with provability operator, The Journal of Symbolic Logic, vol. 59 (1994), no. 4, pp. 1139–1153.Google Scholar
[15] Artemov, S. and Sidon-Yavorskaya, T., On the first order logic of proofs, Technical Report CFIS99-11, Cornell University, 1999.Google Scholar
[16] Artemov, S. and Strassen, T., Functionality in the basic logic of proofs, Technical Report IAM 92-004, Department of Computer Science, University of Bern, Switzerland, 1992.Google Scholar
[17] Artemov, S. and Strassen, T., The logic of the Gödel proof predicate, Computational logic and proof theory. Proceedings of the Third Kurt Gödel Colloquium, Brno, August 1993 (Gottlob, G., Leitsch, A., and Mundici, D., editors), Lecture Notes in Computer Science, vol. 713, Springer-Verlag, 1993, pp. 71–82.Google Scholar
[18] Avigad, J. and Feferman, S., Gödel's functional (“Dialectica”) interpretation, Handbook of proof theory (Buss, S., editor), Elsevier, 1998, pp. 337–406.Google Scholar
[19] Avron, A., On modal systems having arithmetical interpretation, The Journal of Symbolic Logic, vol. 49 (1984), pp. 935–942.CrossRefGoogle Scholar
[20] Barendregt, H., Lambda calculi with types, Handbook of logic in computer science (Abramsky, S., Gabbay, D.M., and Maibaum, T.S.E., editors), vol. 2, Oxford University Press, 1992, pp. 118–309.CrossRefGoogle Scholar
[21] Barthe, G., Hatcliff, J., and Sørensen, M., A notion of a classical pure type system, Electronic Notes in Theoretical Computer Science, vol. 6 (1997), Proceedings of MFPS'97. (Brookes, S. and Mislove, M., editors).Google Scholar
[22] Beeson, M., Foundations of constructive mathematics, Springer-Verlag, 1980.Google Scholar
[23] Beklemishev, L., Parameter-free induction and provably total computable functions, Theoretical Computer Science, vol. 224 (1999), no. 1–2, pp. 13–33.CrossRefGoogle Scholar
[24] Beth, E.W., Semantic construction of intuitionistic logic, Kon. Nederl. Akad. Wetensch. Afd. Let. Med., Nieuwe Serie, vol. 19/11 (1956), pp. 357–388.Google Scholar
[25] Bierman, G. and de Paiva, V., Intuitionistic necessity revisited, Proceedings of the Logic at Work conference, Amsterdam, 1992, 1996, Second revision, http://theory.doc.ic.ac.uk/tfm/papers.html.Google Scholar
[26] Birkhoff, G., On the structure of abstract algebras, Proceedings of the Cambridge Philosophical Society, vol. 31 (1935), pp. 433–454.CrossRefGoogle Scholar
[27] Boolos, G., The unprovability of consistency: An essay in modal logic, Cambridge University Press, 1979.Google Scholar
[28] Boolos, G., The logic of provability, American Mathematical Monthly, vol. 91 (1984), pp. 470–480.Google Scholar
[29] Boolos, G., The logic of provability, Cambridge University Press, 1993.Google Scholar
[30] Borghuis, V. A. J., Coming to terms with modal logic: On the interpretation of modalities in typed λ-calculus, Ph.D. thesis , Technische Universiteit Eindhoven, 1994.Google Scholar
[31] Brezhnev, V., On explicit counterparts of modal logics, Technical Report CFIS2000-05, Cornell University, 2000.Google Scholar
[32] Buss, S., The modal logic of pure provability, Notre Dame Journal of Formal Logic, vol. 31 (1990), no. 2, pp. 225–231.CrossRefGoogle Scholar
[33] Chagrov, A. and Zakharyaschev, M., Modal logic, Oxford Science Publications, 1997.Google Scholar
[34] Constable, R., Types in logic, mathematics and programming, Handbook of proof theory (Buss, S., editor), Elsevier, 1998, pp. 683–786.Google Scholar
[35] Curry, H. B. and Feys, R., Combinatory logic, North-Holland, Amsterdam, 1958.Google Scholar
[36] Davis, M. and Schwartz, J., Metamathematical extensibility for theorem verifiers and proof checkers, Computers and Mathematics with Applications, vol. 5 (1979), pp. 217–230.Google Scholar
[37] de Jongh, D. and Japaridze, G., Logic of provability, Handbook of proof theory (Buss, S., editor), Elsevier, 1998, pp. 475–546.Google Scholar
[38] Feferman, S., A language and axioms for explicit mathematics, Algebra and logic (Crossley, J. N., editor), Springer-Verlag, 1975, pp. 87–139.Google Scholar
[39] Feferman, S., Constructive theories of functions and classes, Logic colloquium '78 (Boffa, M., van Dalen, D., and McAloon, K., editors), North-Holland, 1979, pp. 159–224.Google Scholar
[40] Flagg, R., Church's Thesis is consistent with epistemic arithmetic, Intensional mathematics (Shapiro, S., editor), North-Holland, 1985, pp. 121–172.CrossRefGoogle Scholar
[41] Flagg, R. and Friedman, H., Epistemic and intuitionistic formal systems, Annals of Pure and Applied Logic, vol. 32 (1986), no. 1, pp. 53–60.CrossRefGoogle Scholar
[42] Gabbay, D. M., Labelled deductive systems, Oxford University Press, 1994.Google Scholar
[43] Girard, J.-Y., Lafont, Y., and Taylor, P., Proofs and types, Cambridge University Press, 1989.Google Scholar
[44] Gödel, K., Eine Interpretation des intuitionistischen Aussagenkalküls, Ergebnisse Math. Colloq., vol. 4 (1933), pp. 39–40.Google Scholar
[45] Gödel, K., Über eine bisher noch nicht benütztwe Erweiterung des finiten Standpunktes, Dialectica, vol. 12 (1958), pp. 280–287.Google Scholar
[46] Gödel, K., Vortrag bei Zilsel, 1938, Kurt Gödel Collected Works (Feferman, S., editor), vol. III, Oxford University Press, 1995, pp. 86–113.Google Scholar
[47] Goldblatt, R., Arithmetical necessity, provability and intuitionistic logic, Theoria, vol. 44 (1978), pp. 38–46.Google Scholar
[48] Goldblatt, R., Topoi, North-Holland, 1979.Google Scholar
[49] Goodman, N. D., Epistemic arithmetic is a conservative extension of intuitionistic arithmetic, The Journal of Symbolic Logic, vol. 49 (1984), pp. 192–203.Google Scholar
[50] Goodman, N. D., A genuinely intensional set theory, Intensional mathematics (Shapiro, S., editor), North-Holland, 1985, pp. 63–79.Google Scholar
[51] Goodman, N.D., A theory of constructions is equivalent to arithmetic, Intuitionism and proof theory (Myhill, J., Kino, A., and Vesley, R. E., editors), North-Holland, 1970, pp. 101–120.Google Scholar
[52] Heyting, A., Die formalen Regeln der intuitionistischen Logik, Sitzungsberichte der Preussischen Akademie von Wissenschaften. Physikalisch-mathematische Klasse, (1930), pp. 42–56.Google Scholar
[53] Heyting, A., Die intuitionistische Grundlegung der Mathematik, Erkenntnis, vol. 2 (1931), pp. 106–115.Google Scholar
[54] Heyting, A., Mathematische Grundlagenforschung. Intuitionismus. Beweistheorie, Springer-Verlag, Berlin, 1934.Google Scholar
[55] Hintikka, J., Knowledge and Belief, Cornell University Press, Ithaca, 1962.Google Scholar
[56] Kleene, S., On the interpretation of intuitionistic number theory, The Journal of Symbolic Logic, vol. 10 (1945), no. 4, pp. 109–124.Google Scholar
[57] Kleene, S., Classical extensions of intuitionistic mathematics, Logic, methodology and philosophy of science 2 (Bar-Hillel, Y., editor), North-Holland, 1965, pp. 31–44.Google Scholar
[58] Kolmogoroff, A., Zur Deutung der intuitionistischen Logik, Mathematische Zeitschrift, vol. 35 (1932), pp. 58–65, English translation in Selected works of A.N. Kolmogorov. Volume I: Mathematics and Mechanics , (V.M. Tikhomirov, editor).Google Scholar
[59] Kolmogorov, A., About my papers on intuitionistic logic, Selected works of A. N. Kolmogorov. Volume I: Mathematics and mechanics (Tikhomirov, V. M., editor), Kluwer, 1985, pp. 451–452.Google Scholar
[60] Kozen, D. and Tiuryn, J., Logic of programs, Handbook of theoretical computer science. Volume B, Formal models and semantics (Leeuwen, J. van, editor), Elsevier, 1990, pp. 789–840.Google Scholar
[61] Kracht, M., Tools and techniques in modal logic, Elsevier, 1999.Google Scholar
[62] Kreisel, G., Foundations of intuitionistic logic, Logic, methodology and philosophy of science. Proceedings of the 1960 International Congress (Nagel, E., Suppes, P., and Tarski, A., editors), Stanford University Press, 1962, pp. 198–210.Google Scholar
[63] Kreisel, G., On weak completeness of intuitionistic predicate logic, The Journal of Symbolic Logic, vol. 27 (1962), pp. 139–158.CrossRefGoogle Scholar
[64] Kreisel, G., Mathematical logic, Lectures in Modern Mathematics III (Saaty, T. L., editor), Wiley and Sons, New York, 1965, pp. 95–195.Google Scholar
[65] Kripke, S., Semantical considerations on modal logic, Acta Philosophica Fennica, vol. 16 (1963), pp. 83–94.Google Scholar
[66] Kripke, S., Semantical analysis of intuitionistic logic. I, Formal systems and recursive functions. Proceedings of the 8th Logic Colloquium (Crossley, J. N. and Dummett, M.A.E., editors), North-Holland, 1965, pp. 92–130.CrossRefGoogle Scholar
[67] Krupski, V., Operational logic of proofs with functionality condition on proof predicate, Logical foundations of Computer Science '97, Yaroslavl' (Adian, S. and Nerode, A., editors), Lecture Notes in Computer Science, vol. 1234, Springer-Verlag, 1997, pp. 167–177.Google Scholar
[68] Krupski, V., The single-conclusion proof logic and inference rules specification, Annals of Pure and Applied Logic, (to appear in 2001), in the volume on the conference St. Petersburg Days of Logic and Computability, 1999 , (Yu. Matiyasevich, editor).Google Scholar
[69] Kuznets, A., On the complexity of explicit modal logics, Computer Science Logic 2000, Lecture Notes in Computer Science, vol. 1862, Springer-Verlag, 2000, pp. 371–383.Google Scholar
[70] Kuznetsov, A. and Muravitsky, A., The logic of provability, Abstracts of the 4th All-union conference on mathematical logic, 1976, in Russian, p. 73.Google Scholar
[71] Läuchli, H., An abstract notion of realizability for which intuitionistic predicate logic is complete, Intuitionism and proof theory (Myhill, J., Kino, A., and Vesley, R. E., editors), North-Holland, 1970, pp. 227–234.Google Scholar
[72] Lemmon, E., New foundations for Lewis's modal systems, The Journal of Symbolic Logic, vol. 22 (1957), pp. 176–186.Google Scholar
[73] Martin-Löf, P., Constructive mathematics and computer programming, Logic, methodology and philosophy of science VI (Cohen, L. J., Løs, J., Pffeifer, H., and Podewski, K.-P., editors), North-Holland, 1982, pp. 153–175.Google Scholar
[74] Martin-Löf, P., Intuitionistic type theory, Bibliopolis, Naples, 1984.Google Scholar
[75] Martini, S. and Masini, A., A computational interpretation of modal proofs, Proof theory of modal logics. workshop proceedings (Wansing, H., editor), Kluwer, 1994.Google Scholar
[76] McKinsey, J. C. C. and Tarski, A., On closed elements of closure algebras, Annals of Mathematics, vol. 47 (1946), pp. 122–162.Google Scholar
[77] McKinsey, J. C. C. and Tarski, A., Some theorems about the sentential calculi of Lewis and Heyting, The Journal of Symbolic Logic, vol. 13 (1948), pp. 1–15.Google Scholar
[78] Medvedev, Yu., Finite problems, Soviet Mathematics Doklady, vol. 3 (1962), pp. 227–230.Google Scholar
[79] Mendelson, E., Introduction to mathematical logic, Wadsworth, 1987.Google Scholar
[80] Mints, G., Lewis' systems and system T (a survey 1965–1973)., Feys. Modal logic (Russian translation), Nauka, Moscow, 1974, (in Russian). English translation in G. Mints, Selected papers in proof theory , Bibliopolis, Napoli, 1992, pp. 422–509.Google Scholar
[81] Mints, G., On Novikov's hypothesis, Modal and intensional logics, Nauka, Moscow, 1978, (in Russian). English translation in G. Mints, Selected papers in proof theory , Bibliopolis, Napoli, 1992.Google Scholar
[82] Mkrtychev, A., Models for the logic of proofs, Logical foundations of Computer Science '97, Yaroslavl' (Adian, S. and Nerode, A., editors), Lecture Notes in Computer Science, vol. 1234, Springer-Verlag, 1997, pp. 266–275.Google Scholar
[83] Montague, R., Syntactical treatments of modality with corollaries on reflection principles and finite axiomatizability, Acta Philosophica Fennica, vol. 16 (1963), pp. 153–168.Google Scholar
[84] Myhill, J., Some remarks on the notion of proof, Journal of Philosophy, vol. 57 (1960), pp. 461–471.Google Scholar
[85] Myhill, J., Intensional set theory, Intensional mathematics (Shapiro, S., editor), North-Holland, 1985, pp. 47–61.Google Scholar
[86] Novikov, P. S., Constructive mathematical logic from the viewpoint of the classical one, Nauka, Moscow, 1977, (in Russian).Google Scholar
[87] Orlov, I. E., The calculus of compatibility of propositions, Matematicheskii Sbornik, vol. 35 (1928), pp. 263–286, (in Russian).Google Scholar
[88] Parigot, M., λü-calculus: an algorithmic interpretation of classical natural deduction, Proceedings of the international conference on logic programming and automated reasoning, Lecture Notes in Computer Science, vol. 624, Springer-Verlag, 1992, pp. 190–201.Google Scholar
[89] Parigot, M., Strong normalization for second order classical natural deduction, Proceedings of the 8th annual IEEE Symposium on Logic in Computer Science, IEEE Computer Society Press, 1993, pp. 39–46.Google Scholar
[90] Parsons, C. and Sieg, W., Introductory note to [44], Kurt Gödel Collected Works. Volume III (Feferman, S., editor), Oxford University Press, 1995, pp. 62–85.Google Scholar
[91] Pfenning, F. and Wong, H. C., On a modal lambda-calculus for S4 , Electronic Notes in Computer Science, vol. 1 (1995).Google Scholar
[92] Rasiowa, H. and Sikorski, R., The mathematics of metamathematics, Polish Scientific Publishers, 1963.Google Scholar
[93] Scedrov, A., Extending Gödel's modal interpretation to type theory and set theory, Intensional mathematics (Shapiro, S., editor), North-Holland, 1985, pp. 81–119.Google Scholar
[94] Scott, D., Constructive validity, Symposium on automatic demonstration (Laudet, M., Lacombe, D., Nolin, L., and Schützenberger, M., editors), Lecture Notes in Mathematics, vol. 125, Springer-Verlag, Berlin, 1970, pp. 237–275.Google Scholar
[95] Shapiro, S., Epistemic and intuitionistic arithmetic, Intensional mathematics (Shapiro, S., editor), North-Holland, 1985, pp. 11–46.Google Scholar
[96] Shapiro, S., Intensional mathematics and constructive mathematics, Intensional mathematics (Shapiro, S., editor), North-Holland, 1985, pp. 1–10.Google Scholar
[97] Sidon, T., Provability logic with operations on proofs, Logical foundations of Computer Science '97, Yaroslavl' (Adian, S. and Nerode, A., editors), Lecture Notes in Computer Science, vol. 1234, Springer-Verlag, 1997, pp. 342–353.Google Scholar
[98] Smoryński, C., Self-reference and modal logic, Springer-Verlag, Berlin, 1985.Google Scholar
[99] Smullyan, R., Diagonalization and self-reference, Oxford University Press, 1994.Google Scholar
[100] Solovay, R., Provability interpretations of modallogic, Israel Journal of Mathematics, vol. 25 (1976), pp. 287–304.Google Scholar
[101] Takeuti, G., Proof theory, North-Holland, 1975.Google Scholar
[102] Troelstra, A., The scientific work of A. Heyting, Logic and foundations of mathematics (Dalen, D. van et al., editors), Wolters-Noordhoff Publishing, 1968, pp. 11–46.Google Scholar
[103] Troelstra, A., Introductory note to [44], Kurt Gödel Collected Works. Volume I (Feferman, S., editor), Oxford University Press, 1986, pp. 296–299.Google Scholar
[104] Troelstra, A. and Schwichtenberg, H., Basic proof theory, Cambridge University Press, Amsterdam, 1996.Google Scholar
[105] Troelstra, A. and van Dalen, D., Constructivism in mathematics. An introduction, vol. 1, North-Holland, Amsterdam, 1988.Google Scholar
[106] Troelstra, A.S., Realizability, Handbook of proof theory (Buss, S., editor), Elsevier, 1998, pp. 407–474.Google Scholar
[107] Uspensky, V. and Plisko, V., Intuitionistic logic. commentary on [58] and [59], Selected works of A. N. Kolmogorov. Volume I: Mathematics and Mechanics (Tikhomirov, V. M., editor), Kluwer, 1985, pp. 452–466.Google Scholar
[108] Uspensky, V.A., Kolmogorov and mathematical logic, The Journal of Symbolic Logic, vol. 57 (1992), no. 2, pp. 385–412.Google Scholar
[109] van Benthem, J., Reflections on epistemic logic, Logique & Analyse, vol. 133-134 (1991), pp. 5–14.Google Scholar
[110] van Dalen, D., Intuitionistic logic, Handbook of philosophical logic (Gabbay, D. and Guenther, F., editors), vol. 3, Reidel, 1986, pp. 225–340.Google Scholar
[111] van Dalen, D., Logic and structure, Springer-Verlag, 1994.Google Scholar
[112] Vardanyan, V., Arithmetic complexity of predicate logics of provability and their fragments, Soviet Mathematics Doklady, vol. 33 (1986), pp. 569–572.Google Scholar
[113] Visser, A., An overview of interpretability logic, Advances in modal logic (Kracht, M., de Rijke, M., and Wansing, H., editors), vol. 1, CSLI Publications, Stanford University, 1996, pp. 307–360.Google Scholar
[114] Weinstein, S., The intended interpretation of intuitionistic logic, Journal of Philosophical Logic, vol. 12 (1983), pp. 261–270.Google Scholar
[115] Sidon, T. Yavorskaya, Logics of proofs and provability, Annals of pure and applied logic, (to appear in 2001), in the volume on the conference St. Petersburg Days of Logic and Computability, 1999 , (Yu. Matiyasevich, editor).Google Scholar
[116] Yavorsky, R., On the logic of the standard proof predicate, Computer Science Logic 2000, Lecture Notes in Computer Science, vol. 1862, Springer-Verlag, 2000, pp. 527–541.Google Scholar