Olivier Hermant

From normalization to cut elimination

Normalization proof and semantic cut admissibility proofs have a relatively long history but have been developed separatly.

We show how to generically simplify normalization proofs into cut elimination proofs, by collapsing proofs down to their conclusion sequent. The reducibility candidates argument is still applicable to this settings as we can build reducibility candidates made of sequents. More interestingly, we are able to adapt this work to sequent calculus. As well, we generate usual (Boolean / Heyting) models and the obtained cut admissibility proof simplifies old V-complex arguments in the case of higher-order logic.

The framework we work in is Deduction modulo, that combines a first-order deduction system and a congruence on propositions generated by rewrite rules (on terms and on propositions). We also use superconsistency to generate adequate models of the congruence.

Since you ask for a general part, I will start by a presentation of: - deduction modulo - semantic cut-admissibility proofs (Okada-style) - maybe I will cite the other technique (tableaux and Kripke-style as Hugo does - it might be useful at the end of the talk) - syntactic cut-elimination proofs (Reducibility candidates)