# * Normalization of intuitionistic set theories. *

## by Wojciech Moczydlowski

2006

- unofficial PDF

**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.

**bibTex ref: Moc06b**

cite link