Start / Iowa Type Theory Commute / Normalization and logical consistency

Normalization and logical consistency

15 min • 9 mars 2020

Discussion of the connection between normalization and logical consistency. One approach is to prove normalization and type preservation, to show (in proof-theoretic terms) that all detours can be eliminated from proofs (this is normalization) and that the resulting proof still proves the same theorem (this is type preservation). I mention an alternative I use for Cedille, which is to use a realizability semantics (often used for normalization proofs) directly to prove consistency.