Constructive Proofs of Kruskal's Theorem

Monika Seisenberger

(University of Munich)

Kruskal's tree theorem is a famous theorem in infinitary combinatorics, saying that for every infinite sequence t_1, t_2,... of trees there exist indices i t' < j such that t_i is embeddable in t_j. Here a tree t is embeddable in t' if there exists a one-to-one map f:t--> t' respecting infima of nodes. The theorem became famous since it is a simple statement neither provable in Peano arithmetic nor in ATR_0, two systems where large parts of mathematics can be developed. The main field of application of Kruskal's theorem is term rewriting theory where it is used prove termination of simplification orderings. Kruskal's theorem has a very elegant proof due to Nash-Williams using the minimal-bad-sequence argument. However, this proof is highly non-constructive and does not lead to an algorithm. We discuss the ideas behind several constructive proofs of Kruskal's theorem, including the question whether the non-constructive Nash-Williams' proof can be constructivized.
Tuesday 10th October 2000, 14:00
Robert Recorde Room
Department of Computer Science