On the failure of fixed-point theorems for chain-complete lattices in the effective topos
We show that in the effective topos there is a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. An immediate consequence of this is that both Tarski's theorem for chain-complete posers and the Bourbaki-Witt theorem have no constructive (topos-valid) proofs. (c) 2012 Elsevier B.V. All rights reserved.
effective topos fixed points tarski's theorem bourbaki-witt theorem chain-complete posets constructive logic