Quickest way to understand Kruskal's Tree Theorem

I came across the Kruskal Tree Theorem the other day and thought it looked pretty interesting (especially the stronger finite form due to Friedman). I'm currently a first year mathematics undergraduate, but I've been to third-year first courses in Logic and Set Theory and Graph Theory, which I'm hoping will help me understand the theorem (before you get worried - understanding this theorem was not the reason I went to the courses).

I'm now wondering what sort of undergraduate courses I should be going to which will enable me to understand the theorem and its proof, including Friedman's form. If you know of any good books for exposing the subject (especially ones like R. P. Burn's 'Numbers and Functions', which teach the subject matter through a well chosen set of exercises) then I'd be grateful if you could tell me their names.

Thanks!

A good reference for the theorem is the paper by Jean H. Gallier, "What's so special about Kruskal's theorem and the ordinal $\Gamma_0$? A survey of some results in proof theory." Ann. Pure Appl. Logic 53 (1991), no. 3, 199-260.

(With a short erratum in Ann. Pure Appl. Logic 89 (1997), no. 2-3, 275.)

I do not know of any (undergraduate) books where Friedman's result is discussed in any sort of detail, but this paper is very good.

For some background, you may also want to read the paper by Joseph B. Kruskal, "The theory of well-quasi-ordering: A frequently discovered concept." J. Combinatorial Theory Ser. A 13 (1972), 297–305.

Here is the review from MathScinet:

MR0306057 (46 #5184)

This is a survey paper outlining the history and present state of the theory of well-quasi-ordered sets. A wqo is a qo in which each strictly descending sequence is finite and each set of pairwise incomparable elements is finite or, equivalently, each nonempty subset has one but no more than a finite number of nonequivalent minimal elements. If $s$ and $t$ are sequences from a wqo set then $s\leq t$ means that some subsequence of $t$ majorizes $s$ term by term. A basic question is: when is a set of sequences from a wqo set itself wqo? The author traces the history of this problem and points out that over the years many of the results have been rediscovered and republished. This paper and this section in MR should help eliminate further duplication of these results.

Reviewed by P. F. Conrad

A good book to learn about well-quasi-ordering theory itself, from a logician's perspective, is "Recursive Aspects of Descriptive Set Theory" (Oxford Logic Guides), by Richard Mansfield and Galen Weitkamp. I think the level is fairly accessible. The chapter on wqo theory is by S. Simpson, who is a very good expositor.