Normalization of intuitionistic set theories.
by Wojciech Moczydlowski
- unofficial PDF
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.
bibTex ref: Moc06b