On the failure of fixed-point theorems for chain-complete lattices in the effective topos (Q418812)

In this paper it is shown that, in the effective topos, there is a chain-complete distributive lattice with a monotone and progressive endomap with no fixed point. As a consquence, Tarski's theorem for chain-complete posets and the Bourbaki-Witt theorem both fail in the effective topos, so that neither is constructively provable. Another (unmentioned) consequence is that Zorn's lemma (ZL) -- of which the Bourbaki-Witt theorem is an immediate constructive consequence -- also fails in the effective topos. This is to be contrasted with the fact that ZL holds in all cocomplete toposes provided it holds in the category of sets. This yields a new proof of the independence of ZL from intuitionistic set theory: the usual proof using permutation models demonstrates the independence of ZL from classical set theory.