On the Failure of Fixed-point Theorems for Chain-complete Lattices in the Effective Topos
Abstract: In the effective topos there exists a chain-complete distributive lattice with a monotone and progressive endomap which does not have a fixed point. Consequently, the Bourbaki-Witt theorem and Tarskiâ€™s fixed-point theorem for chain-complete lattices do not have constructive (topos-valid) proofs.
Published in: Theoretical Computer Science Volume 430, 27 April 2012, Pages 43–50. Mathematical Foundations of Programming Semantics (MFPS XXV)