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: 74,310

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.
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
38 (#304,377)

6 months
1 (#415,900)

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