Logic of proofs and provability

Annals of Pure and Applied Logic 113 (1-3):345-372 (2001)
  Copy   BIBTEX

Abstract

In the paper the joint Logic of Proofs and Provability is presented that incorporates both the modality □ for provability 287–304) and the proof operator tF representing the proof predicate “t is a proof of F” . The obtained system naturally includes both the modal logic of provability GL and Artemov's Logic of Proofs . The presence of the modality □ requires two new operations on proofs that together with operations of allow to realize all the invariant operations on proofs admitting description in the modal propositional language. Logic is proved to be decidable and complete with the intended provability semantics

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(01)00066-5

Other Versions

No versions found

Links

PhilArchive

    This entry is not archived by us. If you are the author and have permission from the publisher, we recommend that you archive it. Many publishers automatically grant permission to authors to archive pre-prints. By uploading a copy of your work, you will enable us to better index it, making it easier to find.

    Upload a copy of this work     Papers currently archived: 106,168

External links

Setup an account with your affiliations in order to access resources via your University's proxy server

Through your library

My notes

Similar books and articles

On logic of proofs and provability.Elena Nogina - 2006 - Bulletin of Symbolic Logic 12 (2):356.
Provability logics with quantifiers on proofs.Rostislav E. Yavorsky - 2001 - Annals of Pure and Applied Logic 113 (1-3):373-387.
A modal provability logic of explicit and implicit proofs.Evan Goris - 2010 - Annals of Pure and Applied Logic 161 (3):388-403.
The single-conclusion proof logic and inference rules specification.Vladimir N. Krupski - 2001 - Annals of Pure and Applied Logic 113 (1-3):181-206.
Realization of Intuitionistic Logic by Proof Polynomials.Sergei N. Artemov - 1999 - Journal of Applied Non-Classical Logics 9 (2-3):285-301.
Logic of proofs.Sergei Artëmov - 1994 - Annals of Pure and Applied Logic 67 (1-3):29-59.
Montague’s Paradox, Informal Provability, and Explicit Modal Logic.Walter Dean - 2014 - Notre Dame Journal of Formal Logic 55 (2):157-196.
An operational logic of proofs with positive and negative information.Duccio Luchi & Franco Montagna - 1999 - Studia Logica 63 (1):7-25.
A formalization of Sambins's normalization for GL.Edward Hermann Haeusler & Luiz Carlos Pereira - 1993 - Mathematical Logic Quarterly 39 (1):133-142.
On modal logic of deductive closure.Pavel Naumov - 2006 - Annals of Pure and Applied Logic 141 (1):218-224.

Analytics

Added to PP
2014-01-16

Downloads
46 (#535,828)

6 months
3 (#1,170,603)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

Justification logic.Sergei Artemov - forthcoming - Stanford Encyclopedia of Philosophy.
Tableaux and hypersequents for justification logics.Hidenori Kurokawa - 2012 - Annals of Pure and Applied Logic 163 (7):831-853.
Provability logic.Rineke Verbrugge - 2008 - Stanford Encyclopedia of Philosophy.

View all 6 citations / Add more citations

References found in this work

Explicit provability and constructive semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
Logic of proofs.Sergei Artëmov - 1994 - Annals of Pure and Applied Logic 67 (1-3):29-59.

Add more references