An Analytic Calculus for the Intuitionistic Logic of Proofs

Notre Dame Journal of Formal Logic 60 (3):353-393 (2019)

The goal of this article is to take a step toward the resolution of the problem of finding an analytic sequent calculus for the logic of proofs. For this, we focus on the system Ilp, the intuitionistic version of the logic of proofs. First we present the sequent calculus Gilp that is sound and complete with respect to the system Ilp; we prove that Gilp is cut-free and contraction-free, but it still does not enjoy the subformula property. Then, we enrich the language of the logic of proofs and we formulate in this language a second Gentzen calculus Gilp∗. We show that Gilp∗ is a conservative extension of Gilp, and that Gilp∗ satisfies the subformula property.
Keywords logic of proofs   normalization   proof sequents  cut-elimination
Categories (categorize this paper)
DOI 10.1215/00294527-2019-0008
Edit this record
Mark as duplicate
Export citation
Find it on Scholar
Request removal from index
Revision history

Download options

Our Archive

Upload a copy of this paper     Check publisher's policy     Papers currently archived: 43,914
External links

Setup an account with your affiliations in order to access resources via your University's proxy server
Configure custom proxy (use this if your affiliation does not provide a proxy)
Through your library

References found in this work BETA

No references found.

Add more references

Citations of this work BETA

No citations found.

Add more citations

Similar books and articles

Imperative Programs as Proofs Via Game Semantics.Martin Churchill, Jim Laird & Guy McCusker - 2013 - Annals of Pure and Applied Logic 164 (11):1038-1078.
Explicit Provability and Constructive Semantics.Sergei N. Artemov - 2001 - Bulletin of Symbolic Logic 7 (1):1-36.
A Mixed Λ-Calculus.Marie-Renée Fleury & Myriam Quatrini - 2007 - Studia Logica 87 (2-3):269-294.
Hypothetical Logic of Proofs.Eduardo Bonelli & Gabriela Steren - 2014 - Logica Universalis 8 (1):103-140.
Analytic Logic of Proofs.Francesca Poggiolesi & Brian Hill - forthcoming - Annals of Pure and Applied Logic.
Bi-Simulating in Bi-Intuitionistic Logic.Guillermo Badia - 2016 - Studia Logica 104 (5):1037-1050.
A Short Introduction to Intuitionistic Logic.G. E. Mint͡s - 2000 - Kluwer Academic / Plenum Publishers.


Added to PP index

Total views
21 ( #411,138 of 2,266,272 )

Recent downloads (6 months)
21 ( #37,785 of 2,266,272 )

How can I increase my downloads?


My notes

Sign in to use this feature