# Symmetric Proof that Product is Well-Founded

This is a fairly minor, technical question, but I'll toss it out in case someone has a good idea on it.

Suppose $(X,<_X)$ and $(Y,<_Y)$ are well-founded orderings (not necessarily linearly ordered, though I don't think it matters). Consider the ordering ${<}$ on $X\times Y$ given by $(x',y') < (x,y)$ if $x'\leq x$ and $y'\leq y$, and either $x' < x$ or $y' < y$. Note that this is not the lexicographic ordering; indeed, it's symmetric.

Obviously $X\times Y$ is well-founded. Suppose I want to prove this carefully (by which I really mean "in the formal theory $ID_1$"); more precisely, let's take $X$ to be a set with two properties: $$Cl_X:\forall x(\forall x'<_X x. x'\in X)\rightarrow x\in X$$ and $$Ind_X: \forall Z[\forall x(\forall x'<_X x. x'\in Z)\rightarrow x\in Z)\rightarrow X\subseteq Z]$$ and similarly for $Y$. (These just characterize that $X$ is its own well-founded part.) I want to prove that for all $(x,y)\in X\times Y$, $(x,y)$ are in the well-founded part of $X\times Y$ under ${<}$; call the well-founded part of $X\times Y$ $Acc(X\times Y)$.

I know one way to prove this: for each $x\in X$, define $Y_x=\{y\in Y\mid (x,y)\in Acc(X\times Y)\}$. Let $X'$ be the set of $x\in X$ such that $Y\subseteq Y_x$. Then it would be good enough to show that $X'$ satisfies the closure property, so I can apply $Ind_X$. To do this, in turn, I show that, if $Y\subseteq Y_{x'}$ for all $x'<_X x$ then $Y_x$ satisfies the closure property, so I can apply $Ind_Y$.

Of course, that means I know I second way: I could swap $X$ and $Y$ in the above proof. Moreover, when one works through the details, it's clear that I'm really proving that the lexicographic ordering is well-founded, and using the fact that ${<}$ is a subrelation of the lexicographic ordering.

Which brings me to my question: is there a proof that $Acc(X\times Y)=X\times Y$ which is symmetric?

-
Shouldn't well-ordered' be well-founded' throughout? (In my book `well-ordered' implies linearly ordered because, in particular, every two-element sets has a minimum.) –  KP Hart Oct 7 '10 at 12:41
KP Hart: You're right, it should be. –  Henry Towsner Oct 7 '10 at 19:59

I've found a symmetric proof.

First, every well-founded relation admits an ordinal rank function, an assignment of points to ordinals that respects the relation. For example, in your case $\alpha_x=\sup\{\ \alpha_u+1\mid u\mathrel{\lt_X} x\ \}$ is the canonical rank function for $X$ and $\beta_y=\sup\{\ \beta_w+1\mid w\mathrel{\lt_Y} y\ \}$ is the canonical rank function for $Y$.

Second, the key idea is to use the symmetric version of ordinal addition, called natural sum, an associative and commutative addition operation on ordinals. Specifically, the natural sum $\alpha\mathop{\sharp}\beta$ of two ordinals is the supremum of the order types arising in any linear completion of the disjoint sum partial order $\alpha\sqcup\beta$. Alternatively, if you express $\alpha$ and $\beta$ in Cantor normal form, then $\alpha\mathop{\sharp}\beta$ is the ordinal obtained by mixing the Cantor normal forms together and putting the terms in the correct order. The natural sum is defined in a completely symmetric way, and this is why it is commutative.

In your product order $X\times Y$, let us associate to the point $(x,y)$ the ordinal $\alpha_x\mathop{\sharp}\beta_y$. This ordinal assignment is completely symmetric, since we would assign the same ordinal to $(y,x)$ in $Y\times X$, as the natural sum is commutative. The point now is that this ordinal assignment serves as a rank function in $X\times Y$, since if $(x',y')\lt (x,y)$, then we know that $\alpha_{x'}\leq \alpha_x$ and $\beta_{y'}\leq \beta_y$, and at least one of these is strict. It follows that $\alpha_{x'}\mathop{\sharp}\beta_{y'}\lt \alpha_x\mathop{\sharp}\beta_y$, essentially because $(\alpha+1)\mathop{\sharp}\beta=(\alpha\mathop{\sharp}\beta)+1$, and so this really does rank the product relation, and so it is well-founded.

-
This proof certainly works in a theory that can handle ordinal ranks, but Henry indicated (parenthetically) that he wants a proof formalizable in $ID_1$. In other contexts, I've encountered difficulties formalizing, in theories similar to (but admittedly not identical to) $ID_1$, arguments that were quite easy in terms of ordinals. So I'll be interested to hear from Henry (or other people knowledgeable about $ID_1$) whether this argument does what he wants. –  Andreas Blass Nov 11 '10 at 17:07
I just wanted to congratulate Joel on breaking the 30K barrier with this answer! ;-) –  Suvrit Nov 11 '10 at 17:07
Thanks very much Suvrit; it's been a lot of fun! And Andreas, you are right, I didn't consider $ID_1$, and I will have to leave that to the $ID_1$ experts. –  Joel David Hamkins Nov 11 '10 at 17:36
Regarding $ID_1$, it may help to obserrve that the Cantor normal form version shows that the natural sum of two well-orders is obtained by cutting each of them into finitely many intervals, and then interleaving them so as to attain the largest possible order type. Furthermore, the cutting points in each factor do not depend on the other factor (since they arise from the terms in the Cantor normal form). Thus, we may in effect code the natural sum rank of $(x,y)$ with a finite list of predecessors of $x$ and predecessors of $y$. Perhaps such a plan can be carried out in $ID_1$? –  Joel David Hamkins Nov 12 '10 at 0:01
That's very nice, particularly since it gives what is clearly the correct bound on the size of the ordering (and one much lower than the product bound given by the proof I knew). I expect the proof is formalizable in $ID_1$, though the details might be tricky. ($ID_1$ can code ordinal ranks, albeit with some awkwardness. For the specific use I have in mind, though, it's probably okay to add ordinal ranks if it's absolutely necessary.) –  Henry Towsner Nov 12 '10 at 17:41