A simple proof that super-consistency implies cut elimination
From MaRDI portal
Publication:691121
DOI10.1215/00294527-1722692zbMath1270.03120OpenAlexW2081303576MaRDI QIDQ691121
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
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
This page was built for publication: A simple proof that super-consistency implies cut elimination
