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

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

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 Gö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} 

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

 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. R. È. Yavorskii, “On Prenex Fragment of Provability Logic with Quantifiers on Proofs”, Proc. Steklov Inst. Math., 242 (2003), 112–124
2. S. N. Artemov, “Kolmogorov and Gödel's approach to intuitionistic logic: current developments”, Russian Math. Surveys, 59:2 (2004), 203–229
3. Yavorskiy R., “On Kripke-style semantics for the provability logic of Gödel's proof predicate with quantifiers on proofs”, Journal of Logic and Computation, 15:4 (2005), 539–549
4. Krupski V.N., “Reference constructions in the single-conclusion proof logic”, Journal of Logic and Computation, 16:5 (2006), 645–661
5. Krupski V.N., “Referential logic of proofs”, Theoretical Computer Science, 357:1–3 (2006), 143–166
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
7. Artemov S.N., Yavorskaya (Sidon) Tatiana, “Binding Modalities”, J. Logic Comput., 26:1, SI (2016), 451–461
8. Steren G., Bonelli E., “The First-Order Hypothetical Logic of Proofs”, J. Logic Comput., 27:4 (2017), 1023–1066