This isn't really a research question, but at least it's research-level mathematics. I'm talking with some other people about the first uncountable ordinal, and I want some facts to inform this discussion. Specifically, what useful or interesting foundations of mathematics do or don't allow one to prove the existence of an uncountable ordinal?


If you don't have a better interpretation, then for "useful", you can probably take "capable of encoding most if not all rigorous applied mathematics"; for "interesting", you can probably take "popular for study by researchers in foundations". For "existence of an uncountable ordinal", you could take "existence of a well-ordered uncountable set", "existence of a set whose elements are precisely the countable ordinals", etc.


Hopefully there is a body of known results or obvious corollaries of such, since it could be a matter of some work to apply this question to foundational system X, and I don't expect anybody to do that.



Foundations: Existence of uncountable ordinals.
For the existence of an uncountable set with a definable well-ordering, it suffices to have $\mathcal P(\mathcal P(\mathbb N))$, where $\mathcal P$ means the power set. Any countable order-type is represented by a well-ordering of $\mathbb N$, and can therefore be coded by a subset of $\mathbb N$. Call two such codes equivalent if the well-orderings they code are isomorphic. Then the equivalence classes are elements of $\mathcal P(\mathcal P(\mathbb N))$, they correspond naturally to the countable ordinals, and so they constitute an uncountable well-ordered set. (If you want the well-ordering itself to be a set, rather than given by a definition, and if you want it to be literally a set of ordered pairs, with ordered pairs defined in the usual Kuratowski fashion, then you'll need some more assumptions to ensure the existence of the relevant ordered pairs, etc. But if you're willing to settle for some other coding of ordered pairs, then $\mathcal P(\mathcal P(\mathbb N))$ seems to suffice.)


In particular, the existence of an uncountable well-ordered set is well within the power of Zermelo set theory (like ZF but without the axiom of replacement). If, on the other hand, you want the set of countable ordinals and if you use von Neumann's (nowadays standard) representation of ordinals by sets, then Zermelo set theory is not enough. One natural model of Zermelo set theory is the collection of sets of rank smaller than $\omega+\omega$; this contains plenty of uncountable well-ordered sets, but its ordinals are just those below $\omega+\omega$. (The moral of this story is that, in Zermelo set theory and related systems, ordinals should not be defined using the von Neumann representation but rather as isomorphism classes of well-orderings.)


