On the Bourbaki-Witt Principle in Toposes

TL;DR

This paper investigates the validity of the Bourbaki-Witt fixed point principle within various topos-theoretic and intuitionistic frameworks, revealing conditions under which it holds or fails.

Contribution

It characterizes the circumstances in which the Bourbaki-Witt principle fails or holds in toposes and intuitionistic settings, linking it to properties of ordinals and models.

Findings

Fails when trichotomous ordinals form a set

Does not imply fixed points via transfinite iteration

Holds in all cocomplete toposes

Abstract

The Bourbaki-Witt principle states that any progressive map on a chain-complete poset has a fixed point above every point. It is provable classically, but not intuitionistically. We study this and related principles in an intuitionistic setting. Among other things, we show that Bourbaki-Witt fails exactly when the trichotomous ordinals form a set, but does not imply that fixed points can always be found by transfinite iteration. Meanwhile, on the side of models, we see that the principle fails in realisability toposes, and does not hold in the free topos, but does hold in all cocomplete toposes.