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.

Download: fixed-points.pdf

Published in: Theoretical Computer Science Volume 430, 27 April 2012, Pages 43–50. Mathematical Foundations of Programming Semantics (MFPS XXV)

2 thoughts on “On the Failure of Fixed-point Theorems for Chain-complete Lattices in the Effective Topos

  1. Very nice paper!

    I think there may be a typo in the first paragraph of Sect. 2, by the way: you define that X is discrete if the diagonal map X –> X^{\nabla 2} is _constant_. But if internally this is the condition that every map fron \nabla 2 to X is constant, i.e. in the image of the diagonal map, should the original condition be that the diagonal map is _epimorphic_?

Leave a Reply to Andrej Bauer Cancel reply

Your email address will not be published. Required fields are marked *

*