Return to Revisions

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$.