Does negative trichotomy hold for constructive ordinals?

Question

I don't know if there is a standard term for this, but by "negative trichotomy" I mean ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴). This holds for constructive real numbers as an easy consequence of 𝐴 ≤ 𝐵 ↔ ¬ 𝐵 < 𝐴 and 𝐴 = 𝐵 ↔ (𝐴 ≤ 𝐵 ∧ 𝐵 ≤ 𝐴) but the ordinal analogue to the former is 𝐴 ⊆ 𝐵 ↔ ¬ 𝐵 ∈ 𝐴 and I only am aware of a proof of that for the special case of the natural numbers.

One possible literature reference is https://www.cs.bham.ac.uk/~mhe/TypeTopology/Ordinals.Notions.html#is-decidable-order but I don't read agda in general, or TypeTopology in particular, well enough to know whether that is relevant or not.

At the risk of stating the obvious, ¬ (¬ 𝐴 < 𝐵 ∧ ¬ 𝐴 = 𝐵 ∧ ¬ 𝐵 < 𝐴) is equivalent to ¬ ¬ ( 𝐴 < 𝐵 ∨ 𝐴 = 𝐵 ∨ 𝐵 < 𝐴) in intuitionistic logic, so the problem can be stated either way.

Answer 1

I'll assume by ordinal you mean a set with a transitive, well-founded, and extensional relation. Then it's not constructively valid that $\neg \neg (A < B \vee A = B \vee A > B)$ for ordinals $A$, $B$. In fact we don't even have $\neg \neg (A \le B \vee A \ge B)$ for all $A$, $B$. To see this, we construct a presheaf topos with two ordinals $A$, $B$ such that $\neg (A \le B)$ and $\neg (A \ge B)$ both hold. Specifically, we look at presheaves on $\omega^{\mathrm{op}}$, i.e. sequences $X_0 \to X_1 \to \cdots$. From the internal perspective, $A$ and $B$ will be downward closed subsets of $\omega$. Indeed any downward closed subset of an ordinal is again an ordinal. Now take $f, g : \omega \to \omega$ to be two increasing functions such that $f(x) < g(x)$ and $f(x) > g(x)$ each happen for infinitely many $x$. We take $A_n$ to be the set $\{ x \in \omega \mid x < f(n)\}$, and $B_n$ to be the set $\{ x \in \omega \mid x < g(n)\}$. We claim that $\neg(A \le B)$ in the internal language of our topos (the other claim is proved the same way). To this end, we have to show that there is no $n \in \omega$ such that $A \le B$ holds at stage $n$. Indeed, if $A \le B$ held at stage $n$, then we would have $\{x \in \omega \mid x < f(m)\} \subseteq \{x \in \omega \mid x < g(m)\}$ for all $m \ge n$. This contradicts the assumption that $f(x) > g(x)$ for infinitely many $x$.

Answer 2

David already gave a nice example showing that you do not get negative trichotomy constructively but it turns out that the situation is more drastic than was obvious to me when I originally encountered this question, so I thought I should write another answer. I'm curious about the status of this question relative to more restrictive notions of constructive ordinal, such as Paul's plump ordinals, but I wasn't able to really make any progress on that question.

---

I'm going to phrase this in terms of constructive set theory (with power sets and full separation), but something analogous holds in any topos or any type theory with an impredicative $\mathtt{Prop}$. I did not come up with this argument, but I also don't remember where I saw it. Hopefully someone will point out a reference.

As you specified in the comments, an ordinal is a transitive set of transitive sets (and, recall, a binary relation $(R,<)$ is isomorphic to an ordinal $(\alpha,\in)$ iff it is transitive, extensional, and well-founded). Let $0 = \varnothing$, $\Omega = \mathcal{P}(\{0\})$, and $x + 1 = x\cup \{x\}$. Let $1 = 0 + 1 = \{0\}$, $2 = 1 + 1 = \{0,1\}$, etc.

Note that $\mathsf{LEM}$ is equivalent to the statement $\Omega = 2$. Also note that $\Omega$ and $\Omega + 1$ are ordinals.

Proposition. If $\neg \mathsf{LEM}$ holds, then $\Omega +1 \neq 3$ and $\Omega+1$ and $3$ are both $\in$-incomparable and $\subseteq$-incomparable.

Proof. Since $\neg \mathsf{LEM}$, we have that $\Omega \neq 2$. We also clearly have that $\Omega \neq 0$ and $\Omega \neq 1$, so $\Omega \notin 3$. Since $\Omega \in \Omega + 1$, we have that $\Omega + 1 \neq 3$. Since $\Omega \notin 0$, $\Omega \notin 1$, and $\Omega \notin 2$, we have that $\Omega+1$ is not equal to $0$, $1$, or $2$, whereby $\Omega + 1 \notin 3$.

Assume for the sake of contradiction that $3 \in \Omega + 1$. By definition, this means that $3 \in \Omega$ or $3 = \Omega$. $\Omega$ is not $3$ (because $2$ is not a subset of $1 =\{0\}$), but $3$ is also not an element of $\Omega$ (because $3$ is also not a subset of $1$). Therefore $3 \notin \Omega +1$.

Assume for the sake of contradiction that $3 \subseteq \Omega + 1$. This implies that $2 \in \Omega +1$, so either $2 \in \Omega$ or $2 = \Omega$. The second fails because $\neg \mathsf{LEM}$, and the first fails because $2$ is not a subset of $1$. Therefore $3 \not \subseteq \Omega +1$.

Finally, we already know that $\Omega \notin 3$, so is must be that $\Omega + 1 \not \subseteq 3$. $\square$

This implies that in a lot of sheaf toposes (and in the corresponding models of $\mathsf{IZF}$), you don't get negative trichotomy for this definition of ordinal. For instance, $\neg \mathsf{LEM}$ holds in sheaves over Cantor space and the reals. $\neg \mathsf{LEM}$ also holds in the effective topos/realizability model of $\mathsf{IZF}$. Moreover the proposition implies the following:

Corollary. The following are equivalent (where all quantifiers range over ordinals).

1. $\neg \neg \forall \alpha \beta (\alpha \in \beta \vee \alpha = \beta \vee \beta \in \alpha)$
2. $\neg \neg \forall \alpha \beta (\alpha \subseteq \beta \vee \beta \subseteq \alpha)$
3. $\forall \alpha \beta \neg \neg (\alpha \in \beta \vee \alpha = \beta \vee \beta \in \alpha)$
4. $\forall \alpha \beta \neg \neg (\alpha \subseteq \beta \vee \beta \subseteq \alpha)$
5. $\neg\neg \mathsf{LEM}$

Proof. 5 clearly implies 1 and 2. 1 implies 3 and likewise 2 implies 4 by basic intuitionistic logic. 3 and 4 both imply 1 by instantiating $\alpha = \Omega +1$ and $\beta = 3$. $\square$

That said there are also a decent number of toposes in which $\neg\neg\mathsf{LEM}$ (and therefore negative trichotomy) does hold (assuming a classical world of sets). It holds in finite Kripke frames and therefore (equivalently) in presheaf toposes over finite posetal categories. In particular this means that negative trichotomy does in fact hold in the 'simplest non-classical topos' (i.e., presheaves over $\bullet \to \bullet$).

Answer 3

It's three decades since I wrote Intuitionistic Sets and Ordinals, at which time I knew how to express well founded relations as coalgebras, but I had very little understanding of the subject.

In recent years I have come back to this topic and written two substantial draft papers, the second being Ordinals as Coalgebras. So I would encourage people who are interested in constructive or categorical ordinals to look at those works.

Since it's more than three decades since I believed Excluded Middle, I have long since got out of the habit of looking for ways in which the classical ideas might almost hold. Really, constructive mathematics is much more interesting when you let it lead you where it wants to go, instead of tracking its heresies against classical logic.

However, I would point out that almost all of the (counter)examples in Ordinals as Coalgebras appear in the simplest non-classical topos, ie presheaves on a single arrow. The classical ideas about ordinals really are very fragile.

I do have a constructive result there (Lemma 9.13) that looks a bit like trichotomy: if the join $x\curlyvee y$ exists with respect to the reflexive(-transitive) closure of the well founded relation then $x$ and $y$ are comparable ($x\prec y$ or $x=y$ or $y\prec x$).

However, the purpose of writing that paper was not to give a new "official" account of ordinals using category theory, but to destroy the single notion.

The point is that set theory provides partial models for the (non-existent) free algebra for the covariant powerset functor. So there should be other, different kinds of ordinals that do the same for other functors and constructions.

See (http://www.paultaylor.eu/ordinals) for all the papers (including the old ones).