Is every well-founded simplification order a well-partial order?

Question

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.

Answer 1

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.