A cut-elimination proof in intuitionistic predicate logic

Annals of Pure and Applied Logic 99 (1-3):105-136 (1999)
  Copy   BIBTEX

Abstract

In this paper we give a new proof of cut elimination in Gentzen's sequent system for intuitionistic first-order predicate logic. The point of this proof is that the elimination procedure eliminates the cut rule itself, rather than the mix rule.

Categories

Keywords

Reprint years

DOI

10.1016/s0168-0072(98)00062-1

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 91,349

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

A proof-theoretical investigation of global intuitionistic (fuzzy) logic.Agata Ciabattoni - 2005 - Archive for Mathematical Logic 44 (4):435-457.
Cut-elimination and proof-search for bi-intuitionistic logic using nested sequents.Rajeev Goré, Linda Postniece & Alwen Tiu - 1998 - In Marcus Kracht, Maarten de Rijke, Heinrich Wansing & Michael Zakharyaschev (eds.), Advances in Modal Logic. CSLI Publications. pp. 43-66.
On Gabbay's Proof of the Craig Interpolation Theorem for Intuitionistic Predicate Logic.Michael Makkai - 1995 - Notre Dame Journal of Formal Logic 36 (3):364-381.
Quantifier Elimination for a Class of Intuitionistic Theories.Ben Ellison, Jonathan Fleischmann, Dan McGinn & Wim Ruitenburg - 2008 - Notre Dame Journal of Formal Logic 49 (3):281-293.
Algebraic proofs of cut elimination.Jeremy Avigad - manuscript
A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
Intuitionistic Logic according to Dijkstra's Calculus of Equational Deduction.Jaime Bohórquez V. - 2008 - Notre Dame Journal of Formal Logic 49 (4):361-384.
An approach to infinitary temporal proof theory.Stefano Baratella & Andrea Masini - 2004 - Archive for Mathematical Logic 43 (8):965-990.
Undecidability and intuitionistic incompleteness.D. C. McCarty - 1996 - Journal of Philosophical Logic 25 (5):559 - 565.
Cut-elimination and a permutation-free sequent calculus for intuitionistic logic.Roy Dyckhoff & Luis Pinto - 1998 - Studia Logica 60 (1):107-118.
Completeness and incompleteness for intuitionistic logic.Charles Mccarty - 2008 - Journal of Symbolic Logic 73 (4):1315-1327.
A translation of intuitionistic predicate logic into basic predicate logic.Mohammad Ardeshir - 1999 - Studia Logica 62 (3):341-352.
Constructing a continuum of predicate extensions of each intermediate propositional logic.Nobu-Yuki Suzuki - 1995 - Studia Logica 54 (2):173 - 198.

Analytics

Added to PP
2014-01-16

Downloads
36 (#432,773)

6 months
10 (#251,846)

Historical graph of downloads
How can I increase my downloads?

Author's Profile

Mirjana Borisavljević
University of Belgrade

Citations of this work

A Connection Between Cut Elimination and Normalization.Mirjana Borisavljević - 2006 - Archive for Mathematical Logic 45 (2):113-148.
Computing interpolants in implicational logics.Makoto Kanazawa - 2006 - Annals of Pure and Applied Logic 142 (1):125-201.

Add more citations

References found in this work

Untersuchungen über das logische Schließen. I.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 35:176–210.
Untersuchungen über das logische Schließen. II.Gerhard Gentzen - 1935 - Mathematische Zeitschrift 39:405–431.
The correspondence between cut-elimination and normalization.J. Zucker - 1974 - Annals of Mathematical Logic 7 (1):1-112.
The correspondence between cut-elimination and normalization II.J. Zucker - 1974 - Annals of Mathematical Logic 7 (2):113.

Add more references