RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PERSONAL OFFICE
 General information Latest issue Forthcoming papers Archive Impact factor Guidelines for authors Author agreement Search papers Search references RSS Latest issue Current issues Archive issues What is RSS

 Tr. MIAN: Year: Volume: Issue: Page: Find

 Tr. Mat. Inst. Steklova, 2003, Volume 242, Pages 44–58 (Mi tm404)

Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs

S. N. Artemovab

a M. V. Lomonosov Moscow State University, Faculty of Mechanics and Mathematics
b City University of New York, Graduate Center

Abstract: 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 Gö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 Gö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.

Full text: PDF file (231 kB)
References: PDF file   HTML file

English version:
Proceedings of the Steklov Institute of Mathematics, 2003, 242, 36–49

Bibliographic databases:

UDC: 510.6

Citation: S. N. Artemov, “Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs”, Mathematical logic and algebra, Collected papers. Dedicated to the 100th birthday of academician Petr Sergeevich Novikov, Tr. Mat. Inst. Steklova, 242, Nauka, Moscow, 2003, 44–58; Proc. Steklov Inst. Math., 242 (2003), 36–49

Citation in format AMSBIB
\Bibitem{Art03} \by S.~N.~Artemov \paper Embedding of the Modal $\lambda$-Calculus into the Logic of Proofs \inbook Mathematical logic and algebra \bookinfo Collected papers. Dedicated to the 100th birthday of academician Petr Sergeevich Novikov \serial Tr. Mat. Inst. Steklova \yr 2003 \vol 242 \pages 44--58 \publ Nauka \publaddr Moscow \mathnet{http://mi.mathnet.ru/tm404} \mathscinet{http://www.ams.org/mathscinet-getitem?mr=2054484} \zmath{https://zbmath.org/?q=an:1079.03053} \transl \jour Proc. Steklov Inst. Math. \yr 2003 \vol 242 \pages 36--49 

• http://mi.mathnet.ru/eng/tm404
• http://mi.mathnet.ru/eng/tm/v242/p44

 SHARE:

Citing articles on Google Scholar: Russian citations, English citations
Related articles on Google Scholar: Russian articles, English articles

This publication is cited in the following articles:
1. S. N. Artemov, “Kolmogorov and Gödel's approach to intuitionistic logic: current developments”, Russian Math. Surveys, 59:2 (2004), 203–229
•  Number of views: This page: 386 Full text: 93 References: 48