A simple proof that super-consistency implies cut elimination

DOI10.1215/00294527-1722692MaRDI QIDQ691121zbMATH OpenOpenAlexFDO

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

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)

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

Cites work

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

Cited in

(5)

• A Simple Proof That Super-Consistency Implies Cut Elimination
• 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

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)