RUS  ENG JOURNALS   PEOPLE   ORGANISATIONS   CONFERENCES   SEMINARS   VIDEO LIBRARY   PACKAGE AMSBIB
General information
Latest issue
Archive
Impact factor

Search papers
Search references

RSS
Latest issue
Current issues
Archive issues
What is RSS



Mosc. Math. J.:
Year:
Volume:
Issue:
Page:
Find






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


Mosc. Math. J., 2001, Volume 1, Number 4, Pages 475–490 (Mi mmj32)  

This article is cited in 8 scientific papers (total in 8 papers)

On first order logic of proofs

S. N. Artemova, T. Yavorskayab

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

Abstract: The Logic of Proofs LP solved long standing Gödel's problem concerning his provability calculus (cf. [1]). It also opened new lines of research in proof theory, modal logic, typed programming languages, knowledge representation, etc. The propositional logic of proofs is decidable and admits a complete axiomatization. In this paper we show that the first order logic of proofs is not recursively axiomatizable.

Key words and phrases: Logic of proofs, provability, recursive axiomatizability.

DOI: https://doi.org/10.17323/1609-4514-2001-1-4-475-490

Full text: http://www.ams.org/.../abst1-4-2001.html
References: PDF file   HTML file

Bibliographic databases:

MSC: Primary 03F45; Secondary 03F30, 03F50
Received: July 7, 2001; in revised form January 9, 2002
Language:

Citation: S. N. Artemov, T. Yavorskaya, “On first order logic of proofs”, Mosc. Math. J., 1:4 (2001), 475–490

Citation in format AMSBIB
\Bibitem{ArtYav01}
\by S.~N.~Artemov, T.~Yavorskaya
\paper On first order logic of proofs
\jour Mosc. Math.~J.
\yr 2001
\vol 1
\issue 4
\pages 475--490
\mathnet{http://mi.mathnet.ru/mmj32}
\crossref{https://doi.org/10.17323/1609-4514-2001-1-4-475-490}
\mathscinet{http://www.ams.org/mathscinet-getitem?mr=1901071}
\zmath{https://zbmath.org/?q=an:1011.03045}
\isi{http://gateway.isiknowledge.com/gateway/Gateway.cgi?GWVersion=2&SrcApp=PARTNER_APP&SrcAuth=LinksAMR&DestLinkType=FullRecord&DestApp=ALL_WOS&KeyUT=000208587600001}


Linking options:
  • http://mi.mathnet.ru/eng/mmj32
  • http://mi.mathnet.ru/eng/mmj/v1/i4/p475

    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. R. È. Yavorskii, “On Prenex Fragment of Provability Logic with Quantifiers on Proofs”, Proc. Steklov Inst. Math., 242 (2003), 112–124  mathnet  mathscinet  zmath
    2. 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
    3. Yavorskiy R., “On Kripke-style semantics for the provability logic of Gödel's proof predicate with quantifiers on proofs”, Journal of Logic and Computation, 15:4 (2005), 539–549  crossref  mathscinet  zmath  isi
    4. Krupski V.N., “Reference constructions in the single-conclusion proof logic”, Journal of Logic and Computation, 16:5 (2006), 645–661  crossref  mathscinet  zmath  isi
    5. Krupski V.N., “Referential logic of proofs”, Theoretical Computer Science, 357:1–3 (2006), 143–166  crossref  mathscinet  zmath  isi  elib
    6. Krupski V.N., “Symbolic Models for Single-Conclusion Proof Logics”, Computer Science - Theory and Applications, Lecture Notes in Computer Science, 6072, 2010, 276–287  crossref  mathscinet  zmath  isi
    7. Artemov S.N., Yavorskaya (Sidon) Tatiana, “Binding Modalities”, J. Logic Comput., 26:1, SI (2016), 451–461  crossref  mathscinet  zmath  isi
    8. Steren G., Bonelli E., “The First-Order Hypothetical Logic of Proofs”, J. Logic Comput., 27:4 (2017), 1023–1066  crossref  zmath  isi  scopus
  • Moscow Mathematical Journal
    Number of views:
    This page:190
    References:36

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