@Secret Not quite correct. It is countable only from the meta-system perspective if we only consider definable objects to exist. Which is fine, really, just like Z has a 'simple' model if consistent, since you can add a constant for N and add set-builder notation, and then all the terms will actually refer to some definable object, so modulo provable equality will give a model of Z. Internally, it does (predicatively) know that there is no list of all ordinals.

Wait I must be more precise. We can (predicatively) determine that there is no (countable) list of all well-orderings. After all, we know that func(N,bool) is uncountable, and if you split N into pairs (0,1),(2,3),(4,5),... then you can construct one well-ordering for each choice of pairs to be swapped. So there are uncountably many well-orderings.

However, if you mean the equivalence classes of well-orderings under isomorphism, then you have a problem even constructing that because you can't assume (without LEM) that any two well-orderings are either isomorphic or not. However, isomorphism is still a pseudo equivalence relation on well-orderings in the sense that you only lack total ordering. So you still can go ahead and construct the type WO = { { (T,◁) : (S,<) is isomorphic to (T,◁) } : (S,<) is a well-order }.

I'd have to think about whether one can prove that WO is uncountable or not. We certainly can't (predicatively) prove that WO is countable.

A third alternative you may have been referring to is the set ORD of von Neumann ordinals. If you construct ORD as the type { S : S is well-ordered under ∈ }, if I'm not wrong you will be unable to prove that ORD is totally ordered by ∈.

But I suspect we can't (predicatively) prove that ORD is uncountable.

Because as discussed before we can't construct the canonical ordinal for an arbitrary well-ordering. Even the canonical ω seems unconstructible.

Notice that the ability to define partial functions and the last step are a bit like having replacement on N, which can be sort of justified by noting that we don't assume f is a total function at the start, but can prove by induction that it is, and hence the range of f makes sense.