A semantic normalization proof for a system with recursors

Lisa Allali (1) , Paul Brauner (2)

1 LIX - Laboratoire d'informatique de l'École polytechnique [Palaiseau]
2 PAREO - Formal islands: foundations and applications

Semantics methods have been used to prove cut elimination theorems for a long time. It is only recently that they have been extend to prove strong normalization results, in particular for theories in deduction modulo. However such semantic methods did not apply for systems with recursors like Godel system T. We show in this paper how super natural deduction provides a bridge between superconsistency of arithmetic and strong normalization of system T. We then generalize this result to a family of inductive types before discussing the dependant case.

Mots clés: deduction modulo; inductive types; super-consistency; superdeduction; system T

Domaines: Logique en informatique [cs.LO]

Lisa Allali, Paul Brauner. A semantic normalization proof for a system with recursors. 2008. ⟨inria-00211877⟩