Cut-Elimination: Syntax and Semantics

Studia Logica 102 (6):1217-1244 (2014)

In this paper we first give a survey of reductive cut-elimination methods in classical logic. In particular we describe the methods of Gentzen and Schütte-Tait from the abstract point of view of proof reduction. We also present the method CERES which we classify as a semi-semantic method. In a further section we describe the so-called semantic methods. In the second part of the paper we carry the proof analysis further by generalizing the CERES method to CERESD . In the generalized version CERESD we admit general elimination rules which are based on the mere semantical truth of sentences. We construct complete cut-free LK-derivations originating from derivations potentially containing unproven lemmas. Finally we give a comparison of reductive methods and CERESD by presenting a general simulation result.
Keywords Cut-Elimination  Reductive methods   CERES
Categories (categorize this paper)
DOI 10.1007/s11225-014-9563-2
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: 46,461
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

On the Complexity of Proof Deskolemization.Matthias Baaz, Stefan Hetzl & Daniel Weller - 2012 - Journal of Symbolic Logic 77 (2):669-686.

Add more references

Citations of this work BETA

Ceres in Intuitionistic Logic.David Cerna, Alexander Leitsch, Giselle Reis & Simon Wolfsteiner - 2017 - Annals of Pure and Applied Logic 168 (10):1783-1836.

Add more citations

Similar books and articles

Admissibility of Cut in Congruent Modal Logics.Andrzej Indrzejczak - 2011 - Logic and Logical Philosophy 20 (3):189-203.
A Simple Proof That Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.
The Role of Quantifier Alternations in Cut Elimination.Philipp Gerhardy - 2005 - Notre Dame Journal of Formal Logic 46 (2):165-171.
Quantifier Elimination for Neocompact Sets.H. Jerome Keisler - 1998 - Journal of Symbolic Logic 63 (4):1442-1472.
Natural Deduction with General Elimination Rules.Jan von Plato - 2001 - Archive for Mathematical Logic 40 (7):541-567.


Added to PP index

Total views
10 ( #776,626 of 2,286,454 )

Recent downloads (6 months)
2 ( #588,942 of 2,286,454 )

How can I increase my downloads?


My notes

Sign in to use this feature