On the Failure of Fixed-Point Theorems for Chain-complete Lattices in the Effective Topos

TL;DR

This paper demonstrates that certain fixed-point theorems do not hold constructively within the effective topos, revealing limitations of classical fixed-point results in a constructive setting.

Contribution

It provides a counterexample of a chain-complete lattice with a fixed-point-free monotone endomap in the effective topos, challenging the universality of classical fixed-point theorems.

Findings

Existence of a chain-complete lattice without fixed points in the effective topos

Classical fixed-point theorems like Bourbaki-Witt do not have constructive proofs in this setting

Counterexample impacts constructive mathematics and theoretical computer science

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.