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*?



Symmetric Proof that Product is Well-Founded
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](http://en.wikipedia.org/wiki/Cantor_normal_form#Natural_operations), 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.


