Symmetric Proof that Product is Well-Founded

Question

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?

Answer 1

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.