Skip to main content
PRL Project

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

cite link