A Simple Proof That Super-Consistency Implies Cut Elimination

2023/04/21 by Dowek, Gilles, Hermant, Olivier
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)

paper · doi:10.48550/arxiv.2304.10975

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.

Related

• Cut-restriction: from cuts to analytic cuts
• Consistency Without Cut Elimination
• A theory of cut-restriction: first steps
• Models and termination of proof reduction in the λΠ-calculus modulo theory
• On the convergence of reduction-based and model-based methods in proof theory