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






Personal entry:
Login:
Password:
Save password
Enter
Forgotten password?
Register


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. 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 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.

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, 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


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

    SHARE: VKontakte.ru FaceBook Twitter Mail.ru Livejournal Memori.ru


    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 Gödel's approach to intuitionistic logic: current developments”, Russian Math. Surveys, 59:2 (2004), 203–229  mathnet  crossref  crossref  mathscinet  zmath  adsnasa  isi  elib
  • Труды Математического института им. В. А. Стеклова Proceedings of the Steklov Institute of Mathematics
    Number of views:
    This page:386
    Full text:93
    References:48

     
    Contact us:
     Terms of Use  Registration  Logotypes © Steklov Mathematical Institute RAS, 2017