1. A Simple Proof that Super-Consistency Implies Cut Elimination
- Author
-
Olivier Hermant, Gilles Dowek, Hermant, Olivier, Laboratoire d'informatique de l'École polytechnique [Palaiseau] (LIX), Centre National de la Recherche Scientifique (CNRS)-École polytechnique (X), Preuves, Programmes et Systèmes (PPS), Centre National de la Recherche Scientifique (CNRS)-Université Paris Diderot - Paris 7 (UPD7), Deduction modulo, interopérabilité et démonstration automatique (DEDUCTEAM), Inria Paris-Rocquencourt, Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria), Centre de Recherche en Informatique (CRI), MINES ParisTech - École nationale supérieure des mines de Paris, Université Paris sciences et lettres (PSL)-Université Paris sciences et lettres (PSL), Inria Saclay - Ile de France, Institut National de Recherche en Informatique et en Automatique (Inria), Institut Supérieur d'Electronique de Paris (ISEP), and Mines Paris - PSL (École nationale supérieure des mines de Paris)
- Subjects
Normalization (statistics) ,deduction modulo ,FOS: Computer and information sciences ,Computer Science - Logic in Computer Science ,[INFO.INFO-LO] Computer Science [cs]/Logic in Computer Science [cs.LO] ,Logic ,Modulo ,0102 computer and information sciences ,Mathematical proof ,super-consistency ,01 natural sciences ,[INFO.INFO-FL]Computer Science [cs]/Formal Languages and Automata Theory [cs.FL] ,Simple type theory ,03F05 ,Direct proof ,Structural proof theory ,0101 mathematics ,Mathematics ,Discrete mathematics ,Geometry of interaction ,simple type theory ,03C90 ,Proof complexity ,Proof by contradiction ,010102 general mathematics ,[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO] ,16. Peace & justice ,cut elimination ,Logic in Computer Science (cs.LO) ,03B15 ,TheoryofComputation_MATHEMATICALLOGICANDFORMALLANGUAGES ,Proof theory ,010201 computation theory & mathematics ,TheoryofComputation_LOGICSANDMEANINGSOFPROGRAMS ,03B99 ,Analytic proof - Abstract
We give a simple and direct proof that super-consistency implies cut elimination 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. In particular, it gives a generalization, to all super-consistent theories, of the notion of V-complex, introduced in the semantic cut elimination proofs for simple type theory.
- Published
- 2012
- Full Text
- View/download PDF