A Simple Proof that Super-Consistency Implies Cut Elimination

Notre Dame Journal of Formal Logic 53 (4):439-456 (2012)
  Copy   BIBTEX

Abstract

We give a simple and direct proof that super-consistency implies the cut-elimination property in deduction modulo. This proof can be seen as a simplification of the proof that super-consistency implies proof normalization. It also takes ideas from the semantic proofs of cut elimination that proceed by proving the completeness of the cut-free calculus. As an application, we compare our work with the cut-elimination theorems in higher-order logic that involve V-complexes

Links

PhilArchive



    Upload a copy of this work     Papers currently archived: 90,593

External links

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

Through your library

Similar books and articles

Proof normalization modulo.Gilles Dowek & Benjamin Werner - 2003 - Journal of Symbolic Logic 68 (4):1289-1316.
Cut-elimination for simple type theory with an axiom of choice.G. Mints - 1999 - Journal of Symbolic Logic 64 (2):479-485.
A note on the proof theory the λII-calculus.David J. Pym - 1995 - Studia Logica 54 (2):199 - 230.
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.
The Computational Content of Arithmetical Proofs.Stefan Hetzl - 2012 - Notre Dame Journal of Formal Logic 53 (3):289-296.
A proof of the cut-elimination theorem in simple type theory.Satoko Titani - 1973 - Journal of Symbolic Logic 38 (2):215-226.
Indexed systems of sequents and cut-elimination.Grigori Mints - 1997 - Journal of Philosophical Logic 26 (6):671-696.
Complete infinitary type logics.J. W. Degen - 1999 - Studia Logica 63 (1):85-119.
Bunched Logics Displayed.James Brotherston - 2012 - Studia Logica 100 (6):1223-1254.

Analytics

Added to PP
2012-11-09

Downloads
42 (#332,036)

6 months
4 (#319,344)

Historical graph of downloads
How can I increase my downloads?

Citations of this work

A Simple Proof that Super-Consistency Implies Cut Elimination.Gilles Dowek & Olivier Hermant - 2012 - Notre Dame Journal of Formal Logic 53 (4):439-456.

Add more citations

References found in this work

A formulation of the simple theory of types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (2):56-68.
A Formulation of the Simple Theory of Types.Alonzo Church - 1940 - Journal of Symbolic Logic 5 (3):114-115.
Resolution in type theory.Peter B. Andrews - 1971 - Journal of Symbolic Logic 36 (3):414-432.
Hauptsatz for higher order logic.Dag Prawitz - 1968 - Journal of Symbolic Logic 33 (3):452-457.
Syntactical and semantical properties of simple type theory.Kurt Schütte - 1960 - Journal of Symbolic Logic 25 (4):305-326.

View all 8 references / Add more references