Return to Question

3 Corrected well-ordered to well-founded

Symmetric Proof that Product is Well-OrderedWell-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-orderings 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-orderedwell-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?

2 fixed latex

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-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-ordered. 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?

1

Symmetric Proof that Product is Well-Ordered

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-orderings (not necessarily linearly ordered, though I don't think it matters). Consider the ordering \$

Obviously $X\times Y$ is well-ordered. 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 \$

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 \$

Which brings me to my question: is there a proof that $Acc(X\times Y)=X\times Y$ which is symmetric?
{"extraction_info": {"found_math": true, "script_math_tex": 0, "script_math_asciimath": 0, "math_annotations": 0, "math_alttext": 0, "mathml": 0, "mathjax_tag": 0, "mathjax_inline_tex": 91, "mathjax_display_tex": 6, "mathjax_asciimath": 0, "img_math": 0, "codecogs_latex": 0, "wp_latex": 0, "mimetex.cgi": 0, "/images/math/codecogs": 0, "mathtex.cgi": 0}, "config": {"markdown_headings": false, "markdown_code": true, "boilerplate_config": {"ratio_threshold": 0.18, "absolute_threshold": 10, "end_threshold": 15, "enable": true}, "remove_buttons": true, "remove_image_figures": true, "remove_link_clusters": true, "table_config": {"min_rows": 2, "min_cols": 3, "format": "github"}, "remove_chinese": true, "remove_edit_buttons": true, "extract_latex": true}, "english_confidence": 0.9645456671714783, "perplexity_flag": "head"}