A simple proof that super-consistency implies cut elimination

DOI10.1215/00294527-1722692zbMath1270.03120MaRDI QIDQ691121

Olivier Hermant, Gilles Dowek

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 elimination; higher-order logic; simple type theory; super-consistency; deduction modulo

Mathematics Subject Classification ID

03F05: Cut-elimination and normal-form theorems

03C90: Nonclassical models (Boolean-valued, sheaf, etc.)

Cites Work

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