Geodesic
Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs
Informatics and Automation, Mathematical logic and algebra, Tome 242 (2003), pp. 44-58.

Voir la notice de l'article provenant de la source Math-Net.Ru

The Logic of Proofs LP introduced by the author may be regarded as a basic formal system for reasoning about propositions and proofs. LP comes from Gödel's calculus of provability, also known as modal logic S4 to which P. S. Novikov devoted the well-known monograph Constructive Mathematical Logic from the Point of View of the Classical One. LP gives an exact mathematical answer to the question of the provability semantics of S4 raised by Gödel. This paper gives a comparison of the expressive powers of LP, the typed $\lambda$-calculus, and the modal $\lambda$-calculus. It is shown that a small (namely, Horn) fragment of LP is sufficient for a natural embedding of the typed $\lambda$-calculus. It is also shown that LP models the modal $\lambda$-calculus. 
@article{TRSPY_2003_242_a3,
     author = {S. N. Artemov},
     title = {Embedding of the {Modal} $\lambda${-Calculus} into the {Logic} of {Proofs}},
     journal = {Informatics and Automation},
     pages = {44--58},
     publisher = {mathdoc},
     volume = {242},
     year = {2003},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a3/}
}
TY  - JOUR
AU  - S. N. Artemov
TI  - Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs
JO  - Informatics and Automation
PY  - 2003
SP  - 44
EP  - 58
VL  - 242
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a3/
LA  - ru
ID  - TRSPY_2003_242_a3
ER  - 
%0 Journal Article
%A S. N. Artemov
%T Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs
%J Informatics and Automation
%D 2003
%P 44-58
%V 242
%I mathdoc
%U http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a3/
%G ru
%F TRSPY_2003_242_a3
S. N. Artemov. Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs. Informatics and Automation, Mathematical logic and algebra, Tome 242 (2003), pp. 44-58. http://geodesic.mathdoc.fr/item/TRSPY_2003_242_a3/

[1] Artemov S., Operational modal logic, Tech. Rept. MSI 95-29, Cornell Univ., 1995 ; http://www.cs.gc.cuny.edu/~sartemov | MR

[2] Artemov S., “Explicit provability and constructive semantics”, Bull. Symb. Logic, 7:1 (2001), 1–36 ; http://www.cs.gc.cuny.edu/~sartemov | DOI | MR | Zbl

[3] Artemov S., “Unified semantics for modality and lambda-terms via proof polynomials”, Algebras, diagrams and decisions in language, logic and computation, CSLI Publ., eds. K. Vermeulen, A. Copestake, Stanford Univ., Stanford, 2002 | MR

[4] Bierman G., de Paiva V., “Intuitionistic necessity revisited”, Proc. Logic at Work Conf. (Amsterdam, Dec. 1992); Second revision, June, 1996; http://theory.doc.ic.ac.uk/tfm/papers.html

[5] Boolos G., Logic of provability, Cambridge Univ. Press, Cambridge, 1993 | MR | Zbl

[6] Buss S., “The modal logic of pure provability”, Notre Dame J. Formal Logic, 31:2 (1990), 225–231 | DOI | MR | Zbl

[7] Girard J.-Y., Lafont Y., Taylor P., Proofs and types, Cambridge Univ. Press, Cambridge, 1989 | MR | Zbl

[8] Gödel K., “Eine Interpretation des intuitionistischen Aussagenkalkuls”, Ergeb. Math. Kolloq., 4 (1933), 39–40 | Zbl

[9] Gödel K., “Vortrag bei Zilsel”, 1938, Kurt Gödel collected works, v. 3, eds. S. Feferman, Oxford Univ. Press, New York, 1995, 86–113 | MR

[10] Goldblatt R., “Arithmetical necessity, provability and intuitionistic logic”, Theoria, 44 (1978), 38–46 | MR | Zbl

[11] Heyting A., “Die intuitionistische Grundlegung der Mathematik”, Erkenntnis, 2 (1931), 106–115 | DOI | Zbl

[12] Heyting A., Matematische Grundlagenforschung. Intuitionismus. Beweistheorie, Springer, Berlin, 1934 | MR | Zbl

[13] Kolmogoroff A., “Zur Deutung der intuitionistischen Logik”, Math. Ztschr., 35 (1932), 58–65 | DOI | MR | Zbl

[14] Kolmogorov A. N., “K rabotam po intuitsionistskoi logike”, Izbr. trudy. Matematika i mekhanika, Nauka, M., 1985, 393 | MR

[15] Kozen D., Tiuryn J., “Logic of programs”, Handbook of theoretical computer science. V. B: Formal models and semantics, MIT Press, Elsevier, Boston, Amsterdam, 1990, 789–840. | MR

[16] Kreisel G., “Foundations of intuitionistic logic”, Logic, methodology and philosophy of science, Proc. 1960 Intern. Congr., eds. E. Nagel, P. Suppes, A. Tarski, Stanford Univ. Press, Stanford, 1962, 198–210 | MR

[17] Kreisel G., “On weak completeness of intuitionistic predicate logic”, J. Symb. Logic, 27 (1962), 139–158 | DOI | MR

[18] Kreisel G., “Mathematical logic”, Lectures in modern mathematics, 3, ed. T. L. Saaty, J. Wiley and Sons, New York, 1965, 95–195 | MR | Zbl

[19] Kripke S., “Semantical considerations on modal logic”, Acta Philos. Fenn., 16 (1963), 83–94 | MR | Zbl

[20] Kripke S., “Semantical analysis of intuitionistic logic, I”, Formal systems and recursive functions, Proc. 8th Logic Colloq., eds. J. N. Crossley, M. A. E. Dummett, North-Holland, Amsterdam, 1965, 92–130 | MR

[21] Krupski V. N., “Operational logic of proofs with functionality condition on proof predicate”, Logical Foundations of Computer Science (Yaroslavl, 1997), Lect. Notes Comput. Sci., 1234, 1997, 167–177 | MR | Zbl

[22] Kuznetsov A. V., Muravitskii A. Yu., Logika dokazuemosti, Abstr. 4-i Vsesoyuz. konf. po matematicheskoi logike, Kishinev, 1976, 73

[23] Läuchli H., “An absract notion of realizability for which intuitionistic predicate logic is complete”, Intuitionism and proof theory, eds. J. Myhill, A. Kino, R. E. Vesley, North-Holland, Amsterdam, 1970, 227–234 | MR

[24] Lemmon E., “New foundations for Lewis's modal systems”, J. Symb. Logic, 22 (1957), 176–186 | DOI | MR | Zbl

[25] Lewis C. I., Langford C. H., Symbolic logic, Appleton-Century-Crifts, New York, 1932; Reprinted Dover Publ., New York, 1951, 1959

[26] Martini S., Masini A., “A computational interpretation of modal proofs”, Proof theory of modal logics, Workshop Proc., Kluwer, Dordrecht, 1994 | Zbl

[27] McKinsey J. C. C., Tarski A., “Some theorems about the sentential calculi of Lewis and Heyting”, J. Symb. Logic, 13 (1948), 1–15 | DOI | MR | Zbl

[28] Medvedev Yu. T., “Finitnye zadachi”, DAN SSSR, 142:5 (1962), 1015–1018 | MR | Zbl

[29] Montague R., “Syntactical treatments of modality with corollaries on reflection principles and finite axiomatizability”, Acta Philos. Fenn., 16 (1963), 153–168 | MR

[30] Myhill J., “Some remarks on the notion of proof”, J. Philos., 57 (1960), 461–471 | DOI | MR

[31] Myhill J., “Intensional set theory”, Intensional mathematics, ed. S. Shapiro, North-Holland, Amsterdam, 1985, 47–61 | MR

[32] Novikov P. S., Konstruktivnaya matematicheskaya logika s tochki zreniya klassicheskoi, Nauka, M., 1977 | MR

[33] Orlov I. E., “Ischislenie sovmestimosti vyskazyvanii”, Mat. sb., 35 (1928), 263–286 | Zbl

[34] Pfenning F., Wong H. C., On a modal lambda-calculus for S4, El. Notes Theor. Comput. Sci., 1, Elsevier, Amsterdam, 1995 | MR | Zbl

[35] Shapiro S., “Intensional mathematics and constructive mathematics”, Intensional mathematics, North-Holland, Amsterdam, 1985, 1–10 | MR

[36] Smorynski C., “The incompleteness theorems”, Handbook of mathematical logic, North-Holland, Amsterdam, 1977, 821–865 | MR

[37] Troelstra A. S., van Dalen D., Constructivism in mathematics. An introduction, V. 1, North-Holland, Amsterdam, 1988

[38] Troelstra A. S., Schwichtenberg H., Basic proof theory, Cambridge Univ. Press, Cambridge, 1996 | MR | Zbl

[39] Uspenskii V. A., Plisko V. E., “Intuitsionistskaya logika”, Kolmogorov A. N., Izbr. trudy. Matematika i mekhanika, Nauka, M., 1985, 394–404

[40] Weinstein S., “The intended interpretation of intuitionistic logic”, J. Philos. Logic, 12 (1983), 261–270 | DOI | MR | Zbl