Normalization of intuitionistic set theories.

unofficial copies [PDF],

by Wojciech Moczydlowski

Proceedings of Eighth International Workshop on Termination (WST 2006), 27-31.


Abstract. IZF is a well-investigated impredicative constructive counterpart of Zermelo-Fraenkel set theory. We de ne a weakly-normalizing lambda calculus λZ corresponding to proofs in an intensional version of IZF with Replacement according to the Curry-Howard isomorphism principle. By adapting a counterexample invented by M. Crabb, we show that λZ does not strongly normalize. Moreover, we prove that the calculus corresponding to a non-well-founded IZF does not even weakly normalize. Thus λZ and IZF are positioned on the fine line between weak, strong and lack of normalization.