A simple proof that super-consistency implies cut elimination

DOI10.1215/00294527-1722692zbMATH Open1270.03120OpenAlexW2081303576MaRDI QIDQ691121FDOQ691121

Authors: Gilles Dowek, Olivier Hermant 

Publication date: 29 November 2012

Published in: Notre Dame Journal of Formal Logic (Search for Journal in Brave)

Full work available at URL: https://projecteuclid.org/euclid.ndjfl/1352383225

Recommendations

• A Simple Proof That Super-Consistency Implies Cut Elimination
• Semantic A-translations and super-consistency entail classical cut elimination
• On the convergence of reduction-based and model-based methods in proof theory
• Axiom Directed Focusing
• Proof normalization modulo

zbMATH Keywords

cut eliminationhigher-order logicsimple type theorysuper-consistencydeduction modulo

Mathematics Subject Classification ID

Cut-elimination and normal-form theorems (03F05) Nonclassical models (Boolean-valued, sheaf, etc.) (03C90)

Cites Work

• Constructivism in mathematics. An introduction. Volume I
• A formulation of the simple theory of types
• Completeness and Cut-elimination in the Intuitionistic Theory of Types
• Theorem proving modulo
• Resolution in type theory
• A uniform semantic proof for cut-elimination and completeness of various first and higher order logics.
• Hauptsatz for higher order logic
• Syntactical and semantical properties of simple type theory
• A proof of cut-elimination theorem in simple type-theory
• HOL-\(\lambda\sigma\): An intentional first-order expression of higher-order logic
• A Constructive Semantic Approach to Cut Elimination in Type Theories with Axioms
• Completeness and cut-elimination in the intuitionistic theory of types. II.
• Truth Values Algebras and Proof Normalization
• Proof normalization modulo
• A Simple Proof That Super-Consistency Implies Cut Elimination
• A nonconstructive proof of Gentzen’s Hauptsatz for second order predicate logic

Cited In (5)

• Axiom Directed Focusing
• Gentzen's second consistency proof and strong cut-elimination
• Superdeduction in \(\bar{\lambda}\mu\tilde{\mu}\)
• Semantic A-translations and super-consistency entail classical cut elimination
• A Simple Proof That Super-Consistency Implies Cut Elimination

This page was built for publication: A simple proof that super-consistency implies cut elimination

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q691121)