Simplified Proof of Kruskal’s Tree Theorem

Abstract

There are different versions of proof of Kruskal’s tree theorem. In this paper, we provide a simplified version of proof of Kruskal’s tree theorem. The proof is essentially due to Nash-williams. Though, our proof is similar to the Kruskal’s original proof formulated in terms of well-quasi-orders by Gallier.  In our case, we use well-partial-orders and follow the simplified proof of Kruskal’s theorem of Gallier. Kruskal’s tree theorem is the main ingredient to prove well-foundedness of simplification orders for first-order rewriting. It implies that if an order satisfies some simplification property, well-foundedness is obtained for free. This theorem plays a crucial role in computer science, specially, termination of term rewriting systems.

Keywords: Kruskal’s Theorem, Simplification order, Term rewriting, well-foundedness