<p>Every simplification order is indeed a well-partial order because of this simple statement:</p>

<blockquote>
  <p>If $R$ is a <em>well-quasi order</em>, and $S$ is a partial order, and $R\subseteq S$, then $S$ is a well-partial order.</p>
</blockquote>

<p>Proof: Exercise. Note that this nice property is <strong>not</strong> true for well-founded orders in general! In this sense, well-quasi orders are much more "stable". It's often the case that a stronger property is better behaved, even if the weaker property is what we want to prove at the end (well-quasi orderdness vs well-foundedness in this case).</p>

<p>Since every simplification order contains the homeomorphic embedding, it is indeed a WPO.</p>

<p>Your more precise statement is correct: we could directly prove that a simplification ordering is a WPO by re-producing the proof for the homeomorphic embedding, but this is not necessary because of the above statement, which shows that it suffices to prove the statement for the "minimal" such ordering.</p>

CC BY-SA 3.0
2016-08-24T22:37:53.730Z
2016-08-25T14:58:31.637Z
2016-08-25T14:58:31.637Z
cody
<p>I'm contemplating the proof of Kruskal's Tree Theorem, as presented in the book "Term Rewriting and All That." They use it to prove that every simplification order is well-founded: first by showing that the homeomorphic embedding is a wpo, and then by showing that every simplification order contains the homeomorphic embedding.</p>

<p>It seems to me that the only properties they use of the homeomorphic embedding in the proof are that it's well-founded, and that each term is > its subterms -- exactly the property that defines a simplification order. Does the same proof work if I instead use an arbitrary simplification order*? Does this mean every simplification order is a well-partial order*?</p>

<p>*One caveat: restricting terms to a finite set of variables, because it's trivial to construct a counterexample with an infinite set of variables.</p>

CC BY-SA 3.0
2016-08-24T22:29:17.033Z
In your second paragraph, you refer to "the proof" and "the same proof". Are you referring to the proof of Kruskal's theorem?
cody
CC BY-SA 3.0
2016-08-28T05:18:05.243Z
Yes, I am referring to the proof of Kruskal's Theorem
James Koppel
<graph-theory><order-theory><term-rewriting-systems>
Is every well-founded simplification order a well-partial order?
James Koppel
# Is every well-founded simplification order a well-partial order?

(Asked by: username_0 on 2016-08-24)

I'm contemplating the proof of Kruskal's Tree Theorem, as presented in the book "Term Rewriting and All That." They use it to prove that every simplification order is well-founded: first by showing that the homeomorphic embedding is a wpo, and then by showing that every simplification order contains the homeomorphic embedding.

It seems to me that the only properties they use of the homeomorphic embedding in the proof are that it's well-founded, and that each term is > its subterms -- exactly the property that defines a simplification order. Does the same proof work if I instead use an arbitrary simplification order\*? Does this mean every simplification order is a well-partial order\*?

\*One caveat: restricting terms to a finite set of variables, because it's trivial to construct a counterexample with an infinite set of variables.

**Tags:** graph-theory, order-theory, term-rewriting-systems
> **Comments:**
> **username_1**: In your second paragraph, you refer to "the proof" and "the same proof". Are you referring to the proof of Kruskal's theorem?  
> **username_0**: Yes, I am referring to the proof of Kruskal's Theorem  

---

## 1 answers

### Answer by username_1 on 2016-08-24. Score: 5 | Accepted answer

Every simplification order is indeed a well-partial order because of this simple statement:

> If $R$ is a *well-quasi order*, and $S$ is a partial order, and $R\subseteq S$, then $S$ is a well-partial order.

Proof: Exercise. Note that this nice property is **not** true for well-founded orders in general! In this sense, well-quasi orders are much more "stable". It's often the case that a stronger property is better behaved, even if the weaker property is what we want to prove at the end (well-quasi orderdness vs well-foundedness in this case).

Since every simplification order contains the homeomorphic embedding, it is indeed a WPO.

Your more precise statement is correct: we could directly prove that a simplification ordering is a WPO by re-producing the proof for the homeomorphic embedding, but this is not necessary because of the above statement, which shows that it suffices to prove the statement for the "minimal" such ordering.


---

