In PA one can define the ordered pair function in term of naturals, i.e. the ordered pair of naturals is a natural itself. let's label these ordered pairs as natural ordered pairs.
Now working in second order arithmetic (formalized in first order logic language) can we speak of existence of a well ordering on $N$ that is defined in terms of being a set of natural ordered pairs, that satisfy the so and so.. well ordering conditions?
What confuses me is that this well ordering itself would be a subset of $N$, so it would well order itself by the way, so it would be a kind of auto-well ordering relation? Is that possible?
My attempts to solve this question to the positive relied on seeing that in the finite world a well ordering of a finite set $X$ must be at least of a size equal to $|X|-1 + |X|-2 + |X|-3 + ..+|X|-|X|$. So if $X$ is of $\aleph_0$ cardinality then the well ordering relation can be of $\aleph_0$ cardinality. I think a mapping showing this possibility for well ordering subset $R$ of $N$, is for the first element $\alpha$ of $R$ to code $\langle 0,1 \rangle$, then we jump by taking $\alpha + 2^n$ to represent the successive elements of the form $\langle 0, n \rangle$, etc.., now to represent pairs of the form $\langle 1,n \rangle$ for $n > 1$, we start with $\alpha+1$ and jump similarly by $+2^n$, this way we can have enough room to well order all $N$ including $R$ itself! But I'm not sure if this solves it?
Best Answer
I'm not quite certain what you're trying to do in your last paragraph, so it may be I've missed some more specific aspect of the question you're trying to answer, but...
Absolutely we can talk about well-orders defined in such a way, and it can be very interesting to do so. To see that it's possible is trivial: if we use the coding $\langle m,n\rangle:=(m+n)^2+m$, it's easy enough in anything at least as strong as $\mathsf{ACA}_0$ (really this is more than we need) to describe the lexicographic ordering on $N\times N$ with natural ordered pairs. It's even possible to prove that it's well-ordered, in the form of proving that every strictly decreasing sequence is finite. Such well-orders are, as you say, always countable, but the way pairs are coded usually means it isn't a well-ordering of all of $N$.
But note that this is an important point: we may be able to describe what is a well-ordering in the "real world", but be unable to prove that it is well-ordered. With some ingenuity one can code a well-ordering of length $\Gamma_0$ in $\mathsf{ACA}_0$ (using a Gödel numbering of ordinals in the Veblen hierarchy) but only initial segments of length less than $\varepsilon_0$ are provably well-ordered.