Truth values algebras and proof normalization
Gilles Dowek (<Gilles DOT Dowek AT polytechnique DOT edu>)
- École polytechnique and INRIA
- Sala 5?? (RDC)
- Horário: 9 horas
- Dia: 06/09/2007
We extend the notion of Heyting algebra to a notion of truth values algebra and prove that a theory is consistent if and only if it has a B-valued model for some non trivial truth values algebra B. A theory that has a B-valued model for all truth values algebras B is said to be super-consistent. We prove that super-consistency is a model-theoretic sufficient condition for strong normalization.