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




This article is cited in 1 scientific paper (total in 1 paper)
Embedding of the Modal $\lambda$Calculus into the Logic of Proofs
S. N. Artemov^{ab} ^{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 Gödel's calculus of provability, also known as modal logic S4 to which P. S. Novikov devoted the wellknown 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.
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 Received in November 2002
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, MAIK «Nauka/Inteperiodika», M., 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 4458
\publ Nauka, MAIK «Nauka/Inteperiodika»
\publaddr M.
\mathnet{http://mi.mathnet.ru/tm404}
\mathscinet{http://www.ams.org/mathscinetgetitem?mr=2054484}
\zmath{https://zbmath.org/?q=an:1079.03053}
\transl
\jour Proc. Steklov Inst. Math.
\yr 2003
\vol 242
\pages 3649
Linking options:
http://mi.mathnet.ru/eng/tm404 http://mi.mathnet.ru/eng/tm/v242/p44
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:

S. N. Artemov, “Kolmogorov and Gödel's approach to intuitionistic logic: current developments”, Russian Math. Surveys, 59:2 (2004), 203–229

Number of views: 
This page:  395  Full text:  97  References:  49 
