Tukukkk

I'm hoping the answer to this is well-known.

Let $X$ be an ordered set (i.e. poset). An inflationary operator $f$ on $X$ is a function $f: X to X$, not necessarily order-preserving, such that $f(x) geq x$ for all $x in X$. I'm interested in the following result:

Theorem Let $X$ be an ordered set in which every chain has an upper bound. Then every inflationary operator on $X$ has a fixed point.

My questions:

Can this theorem be proved without the axiom of choice? Does it imply the axiom of choice? Or is it equivalent to some weak form of choice?

Here I use the words "without", "imply" and "equivalent" in the usual way, i.e. I'm taking as given that we're allowed to use other standard set-theoretic axioms, such as ETCS without choice or ZF.

Background

This fixed point theorem is "equivalent" to Zorn's lemma in the standard informal sense that either one can be easily deduced from the other. Indeed, the theorem follows from Zorn because a maximal element is a fixed point for any inflationary operator. Conversely, the theorem implies Zorn: define an inflationary operator $f$ by taking $f(x) = x$ whenever $x$ is maximal and choosing some $f(x) > x$ otherwise.

That's fine — but since both my proof of the theorem and my proof of Zorn from the theorem involve the axiom of choice, it doesn't help to answer my questions above.

The fixed point theorem is very close to some results that don't require choice. For instance, the Bourbaki-Witt fixed point theorem states that on an ordered set where every chain has a least upper bound, every inflationary operator has a fixed point. That can be proved without choice. You can even weaken the hypothesis to state that every chain has a specified upper bound (i.e. there exists a function assigning an upper bound to each chain), and you still don't need choice. But neither of these results is as strong as the theorem above, at least superficially.

I'll deduce Zorn's Lemma from your fixed-point theorem. Suppose $P$ is a poset violating Zorn's Lemma; so all chains in $P$ have upper bounds, but there's no maximal element. Consider the poset $Q=Ptimesomega$ with the lexicographic ordering; that is, in $P$ replace every element by a chain ordered like the set $omega$ of natural numbers. I claim this $Q$ serves as a counterexample to your fixed-point theorem. The map $(p,n)mapsto(p,n+1)$ is inflationary and has no fixed point in $Q$. So it remains only to prove that, in $Q$, every chain has an upper bound.

Consider any chain $C$ in $Q$. The first components $p$ of the elements $(p,n)in C$ constitute a chain $C'$ in $P$, and by assumption $C'$ has an upper bound $b$ in $P$. If $bnotin C'$, then $(b,0)$ serves as an upper bound for $C$ in $Q$. If, on the other hand, $bin C'$, then use the assumption that $P$ has no maximal element to get some $b'$ strictly above $b$ in $P$; then $(b',0)$ is an upper bound for $C$ in $Q$.