Kruskal's tree theorem

<h2 id="history">History</h2>
The <a href="/facts/Theorem/f2Pe1FMD">theorem</a> was <a href="/facts/Conjecture/oPWUb7SF">conjectured</a> by <a href="/facts/Andrew_V%25C3%25A1zsonyi/x5IXPdVU">Andrew Vázsonyi</a> and <a href="/facts/Mathematical_proof/7ECDrU80">proved</a> by <a href="/facts/Joseph_Kruskal/KzpLEAyF">Joseph Kruskal</a> (1960); a short proof was given by <a href="/facts/Crispin_St._J._A._Nash-Williams/YY5uresp">Crispin Nash-Williams</a> (1963). It has since become a prominent example in <a href="/facts/Reverse_mathematics/nHLm6JUQ">reverse mathematics</a> as a statement that cannot be proved in ATR0 (a <a href="/facts/Second-order_arithmetic/abBxQsaH">second-order arithmetic</a> theory with a form of <a href="/facts/Arithmetical_transfinite_recursion/nHLm6JUQ">arithmetical transfinite recursion</a>).
In 2004, the result was generalized from trees to <a href="/facts/Graph_(discrete_mathematics)/kw3eIBUe">graphs</a> as the <a href="/facts/Robertson%25E2%2580%2593Seymour_theorem/J7g4CJ74">Robertson–Seymour theorem</a>, a result that has also proved important in reverse mathematics and leads to the even-faster-growing <a href="/facts/Friedman%2527s_SSCG_function/sCPQslJQ">SSCG function</a>, which dwarfs 
 
 
 
 
 TREE
 
 (
 3
 )
 
 
 {\displaystyle {\text{TREE}}(3)}
 
.

<h2 id="statement">Statement</h2>
The version given here is that proven by Nash-Williams; Kruskal's formulation is somewhat stronger. All trees we consider are finite.
Given a tree T with a <a href="/facts/Rooted_tree/TCWk4Joy">root</a>, and given vertices v, w, call w a successor of v if the unique path from the root to w contains v, and call w an immediate successor of v if additionally the path from v to w contains no other vertex.
Take X to be a <a href="/facts/Partially_ordered_set/qb4a3FAX">partially ordered set</a>. If T1, T2 are rooted trees with vertices labeled in X, we say that T1 is inf-embeddable in T2 and write 
 
 
 
 
 T
 
 1
 
 
 ≤
 
 T
 
 2
 
 
 
 
 {\displaystyle T_{1}\leq T_{2}}
 
 if there is an <a href="/facts/Injective_map/5ES6tqf5">injective map</a> F from the vertices of T1 to the vertices of T2 such that:

<ul><li>For all vertices v of T1, the label of v precedes the label of 
 
 
 
 F
 (
 v
 )
 
 
 {\displaystyle F(v)}
 
;</li>
<li>If w is any successor of v in T1, then 
 
 
 
 F
 (
 w
 )
 
 
 {\displaystyle F(w)}
 
 is a successor of 
 
 
 
 F
 (
 v
 )
 
 
 {\displaystyle F(v)}
 
; and</li>
<li>If w1, w2 are any two distinct immediate successors of v, then the path from 
 
 
 
 F
 (
 
 w
 
 1
 
 
 )
 
 
 {\displaystyle F(w_{1})}
 
 to 
 
 
 
 F
 (
 
 w
 
 2
 
 
 )
 
 
 {\displaystyle F(w_{2})}
 
 in T2 contains 
 
 
 
 F
 (
 v
 )
 
 
 {\displaystyle F(v)}
 
.</li></ul>
Kruskal's tree theorem then states:

<blockquote>If X is <a href="/facts/Well-quasi-ordering/suQavGN9">well-quasi-ordered</a>, then the set of rooted trees with labels in X is well-quasi-ordered under the inf-embeddable order defined above. (That is to say, given any infinite sequence T1, T2, … of rooted trees labeled in X, there is some 
 
 
 
 i
 <
 j
 
 
 {\displaystyle i<j}
 
 so that 
 
 
 
 
 T
 
 i
 
 
 ≤
 
 T
 
 j
 
 
 
 
 {\displaystyle T_{i}\leq T_{j}}
 
.)</blockquote>
<h2 id="friedmans-work">Friedman's work</h2>
For a <a href="/facts/Countable_set/Wj4DmWPv">countable</a> label set X, Kruskal's tree theorem can be expressed and proven using <a href="/facts/Second-order_arithmetic/abBxQsaH">second-order arithmetic</a>. However, like <a href="/facts/Goodstein%2527s_theorem/W2SvUUpk">Goodstein's theorem</a> or the <a href="/facts/Paris%25E2%2580%2593Harrington_theorem/YcvXywQb">Paris–Harrington theorem</a>, some special cases and variants of the theorem can be expressed in subsystems of second-order arithmetic much weaker than the subsystems where they can be proved. This was first observed by <a href="/facts/Harvey_Friedman_(mathematician)/Yq10dMrt">Harvey Friedman</a> in the early 1980s, an early success of the then-nascent field of reverse mathematics. In the case where the trees above are taken to be unlabeled (that is, in the case where X has size one), Friedman found that the result was unprovable in <a href="/facts/Arithmetical_transfinite_recursion/nHLm6JUQ">ATR0</a>,<a class="footnote-ref" id="fnref:2" href="#fn:2">2</a> thus giving the first example of a <a href="/facts/Impredicativity/gDuxRrb5">predicative</a> result with a provably impredicative proof.<a class="footnote-ref" id="fnref:3" href="#fn:3">3</a> This case of the theorem is still provable by Π11-CA0, but by adding a "gap condition"<a class="footnote-ref" id="fnref:4" href="#fn:4">4</a> to the definition of the order on trees above, he found a natural variation of the theorem unprovable in this system.<a class="footnote-ref" id="fnref:5" href="#fn:5">5</a><a class="footnote-ref" id="fnref:6" href="#fn:6">6</a> Much later, the Robertson–Seymour theorem would give another theorem unprovable by Π11-CA0.
<a href="/facts/Ordinal_analysis/bx5joaVU">Ordinal analysis</a> confirms the strength of Kruskal's theorem, with the <a href="/facts/Proof-theoretic_ordinal/bx5joaVU">proof-theoretic ordinal</a> of the theorem equaling the <a href="/facts/Small_Veblen_ordinal/gEPQRRH4">small Veblen ordinal</a> (sometimes confused with the smaller <a href="/facts/Ackermann_ordinal/QSxRdozk">Ackermann ordinal</a>).<a class="footnote-ref" id="fnref:7" href="#fn:7">7</a>

<h2 id="weak-tree-function">Weak tree function</h2>
Suppose that 
 
 
 
 P
 (
 n
 )
 
 
 {\displaystyle P(n)}
 
 is the statement:

There is some m such that if T1, ..., Tm is a finite sequence of unlabeled rooted trees where Ti has 
 
 
 
 i
 +
 n
 
 
 {\displaystyle i+n}
 
 vertices, then 
 
 
 
 
 T
 
 i
 
 
 ≤
 
 T
 
 j
 
 
 
 
 {\displaystyle T_{i}\leq T_{j}}
 
 for some 
 
 
 
 i
 <
 j
 
 
 {\displaystyle i<j}
 
.
All the statements 
 
 
 
 P
 (
 n
 )
 
 
 {\displaystyle P(n)}
 
 are true as a consequence of Kruskal's theorem and <a href="/facts/K%25C5%2591nig%2527s_lemma/eCU93PN9">Kőnig's lemma</a>. For each n, <a href="/facts/Peano_axioms/DhhDnNug">Peano arithmetic</a> can prove that 
 
 
 
 P
 (
 n
 )
 
 
 {\displaystyle P(n)}
 
 is true, but Peano arithmetic cannot prove the statement "
 
 
 
 P
 (
 n
 )
 
 
 {\displaystyle P(n)}
 
 is true for all n".<a class="footnote-ref" id="fnref:8" href="#fn:8">8</a> Moreover, the length of the shortest <a href="/facts/Formal_proof/6nEhV4cw">proof</a> of 
 
 
 
 P
 (
 n
 )
 
 
 {\displaystyle P(n)}
 
 in Peano arithmetic grows phenomenally fast as a function of n, far faster than any <a href="/facts/Primitive_recursive_function/4z97gRnl">primitive recursive function</a> or the <a href="/facts/Ackermann_function/WQNpCWHn">Ackermann function</a>, for example. The least m for which 
 
 
 
 P
 (
 n
 )
 
 
 {\displaystyle P(n)}
 
 holds similarly grows extremely quickly with n.
Define 
 
 
 
 
 tree
 
 (
 n
 )
 
 
 {\displaystyle {\text{tree}}(n)}
 
, the weak tree function, as the largest m so that we have the following:

There is a sequence T1, ..., Tm of unlabeled rooted trees, where each Ti has at most 
 
 
 
 i
 +
 n
 
 
 {\displaystyle i+n}
 
 vertices, such that 
 
 
 
 
 T
 
 i
 
 
 ≤
 
 T
 
 j
 
 
 
 
 {\displaystyle T_{i}\leq T_{j}}
 
 does not hold for any 
 
 
 
 i
 <
 j
 ≤
 m
 
 
 {\displaystyle i<j\leq m}
 
.
It is known that 
 
 
 
 
 tree
 
 (
 1
 )
 =
 2
 
 
 {\displaystyle {\text{tree}}(1)=2}
 
, 
 
 
 
 
 tree
 
 (
 2
 )
 =
 5
 
 
 {\displaystyle {\text{tree}}(2)=5}
 
, 
 
 
 
 
 tree
 
 (
 3
 )
 ≥
 844
 ,
 424
 ,
 930
 ,
 131
 ,
 960
 
 
 {\displaystyle {\text{tree}}(3)\geq 844,424,930,131,960}
 
 (about 844 trillion), 
 
 
 
 
 tree
 
 (
 4
 )
 ≫
 
 g
 
 64
 
 
 
 
 {\displaystyle {\text{tree}}(4)\gg g_{64}}
 
 (where 
 
 
 
 
 g
 
 64
 
 
 
 
 {\displaystyle g_{64}}
 
 is <a href="/facts/Graham%2527s_number/7IJYxN2x">Graham's number</a>), and 
 
 
 
 
 TREE
 
 (
 3
 )
 
 
 {\displaystyle {\text{TREE}}(3)}
 
 (where the argument specifies the number of labels; see below) is larger than 
 
 
 
 
 
 t
 r
 e
 e
 
 
 
 
 t
 r
 e
 e
 
 
 
 
 t
 r
 e
 e
 
 
 
 
 t
 r
 e
 e
 
 
 
 
 t
 r
 e
 e
 
 
 8
 
 
 (
 7
 )
 
 
 (
 7
 )
 
 
 (
 7
 )
 
 
 (
 7
 )
 
 
 (
 7
 )
 .
 
 
 {\displaystyle \mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{8}(7)}(7)}(7)}(7)}(7).}

To differentiate the two functions, "TREE" (with all caps) is the big TREE function, and "tree" (with all letters in lowercase) is the weak tree function.

<h2 id="tree-function">TREE function</h2>

By incorporating labels, Friedman defined a far faster-growing function.<a class="footnote-ref" id="fnref:9" href="#fn:9">9</a> For a positive <a href="/facts/Integer/PUwwrawx">integer</a> n, take 
 
 
 
 
 TREE
 
 (
 n
 )
 
 
 {\displaystyle {\text{TREE}}(n)}
 
[a] to be the largest m so that we have the following:

There is a sequence T1, ..., Tm of rooted trees labelled from a set of n labels, where each Ti has at most i vertices, such that 
 
 
 
 
 T
 
 i
 
 
 ≤
 
 T
 
 j
 
 
 
 
 {\displaystyle T_{i}\leq T_{j}}
 
 does not hold for any 
 
 
 
 i
 <
 j
 ≤
 m
 
 
 {\displaystyle i<j\leq m}
 
.
The TREE sequence begins 
 
 
 
 
 TREE
 
 (
 1
 )
 =
 1
 
 
 {\displaystyle {\text{TREE}}(1)=1}
 
, 
 
 
 
 
 TREE
 
 (
 2
 )
 =
 3
 
 
 {\displaystyle {\text{TREE}}(2)=3}
 
, before 
 
 
 
 
 TREE
 
 (
 3
 )
 
 
 {\displaystyle {\text{TREE}}(3)}
 
 suddenly explodes to a value so large that many other "large" combinatorial constants, such as Friedman's 
 
 
 
 n
 (
 4
 )
 
 
 {\displaystyle n(4)}
 
, 
 
 
 
 
 n
 
 n
 (
 5
 )
 
 
 (
 5
 )
 
 
 {\displaystyle n^{n(5)}(5)}
 
, and <a href="/facts/Graham%2527s_number/7IJYxN2x">Graham's number</a>,[b] are extremely small by comparison. A <a href="/facts/Lower_bound/YJje9oC2">lower bound</a> for 
 
 
 
 n
 (
 4
 )
 
 
 {\displaystyle n(4)}
 
, and, hence, an extremely weak lower bound for 
 
 
 
 
 TREE
 
 (
 3
 )
 
 
 {\displaystyle {\text{TREE}}(3)}
 
, is 
 
 
 
 
 A
 
 A
 (
 187196
 )
 
 
 (
 1
 )
 
 
 {\displaystyle A^{A(187196)}(1)}
 
.[c]<a class="footnote-ref" id="fnref:10" href="#fn:10">10</a> Graham's number, for example, is much smaller than the lower bound 
 
 
 
 
 A
 
 A
 (
 187196
 )
 
 
 (
 1
 )
 
 
 {\displaystyle A^{A(187196)}(1)}
 
, which is approximately 
 
 
 
 
 g
 
 3
 
 ↑
 
 187196
 
 
 3
 
 
 
 
 {\displaystyle g_{3\uparrow ^{187196}3}}
 
, where 
 
 
 
 
 g
 
 x
 
 
 
 
 {\displaystyle g_{x}}
 
 is <a href="/facts/Graham%2527s_number/7IJYxN2x">Graham's function</a>.

<h2 id="see-also">See also</h2>
<ul><li><a href="/facts/Paris%25E2%2580%2593Harrington_theorem/YcvXywQb">Paris–Harrington theorem</a></li>
<li><a href="/facts/Kanamori%25E2%2580%2593McAloon_theorem/jw5DDRAR">Kanamori–McAloon theorem</a></li>
<li><a href="/facts/Robertson%25E2%2580%2593Seymour_theorem/J7g4CJ74">Robertson–Seymour theorem</a></li></ul>
<h2 id="notes">Notes</h2>
^ a Friedman originally denoted this function by TR[n].
^ b n(k) is defined as the length of the longest possible sequence that can be constructed with a k-letter alphabet such that no block of letters xi,...,x2i is a subsequence of any later block xj,...,x2j.<a class="footnote-ref" id="fnref:11" href="#fn:11">11</a> 
 
 
 
 n
 (
 1
 )
 =
 3
 ,
 n
 (
 2
 )
 =
 11
 ,
 
 
 
 and
 
 
 
 n
 (
 3
 )
 >
 2
 
 ↑
 
 7197
 
 
 158386
 
 
 {\displaystyle n(1)=3,n(2)=11,\,{\textrm {and}}\,n(3)>2\uparrow ^{7197}158386}
 
.
^ c A(x) taking one argument, is defined as A(x, x), where A(k, n), taking two arguments, is a particular version of <a href="/facts/Ackermann%2527s_function/WQNpCWHn">Ackermann's function</a> defined as: A(1, n) = 2n, A(k+1, 1) = A(k, 1), A(k+1, n+1) = A(k, A(k+1, n)).

Citations

Bibliography

<ul><li><a href="/facts/Harvey_Friedman_(mathematician)/Yq10dMrt">Friedman, Harvey M.</a> (2002). <a href="https://books.google.com/books?id=o-dhDwAAQBAJ&pg=PA60">"Internal finite tree embeddings"</a>. In Sieg, Wilfried; <a href="/facts/Solomon_Feferman/Bt6DRjuk">Feferman, Solomon</a> (eds.). Reflections on the foundations of mathematics: essays in honor of Solomon Feferman. Lecture notes in logic. Vol. 15. Natick, Mass: <a href="/facts/AK_Peters/kIyEuk1n">AK Peters</a>. pp. 60–91. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-56881-170-3. <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1943303">1943303</a>.</li>
<li><a href="/facts/Jean_Gallier/gRCtnPsS">H. Gallier, Jean</a> (September 1991). <a href="http://www.cis.upenn.edu/~jean/kruskal.pdf">"What's so special about Kruskal's theorem and the ordinal Γ0? A survey of some results in proof theory"</a> (PDF). <a href="/facts/Annals_of_Pure_and_Applied_Logic/tR1Pk1tr">Annals of Pure and Applied Logic</a>. 53 (3): 199–260. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2F0168-0072%2891%2990022-E">10.1016/0168-0072(91)90022-E</a>. <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1129778">1129778</a>.</li>
<li><a href="/facts/Joseph_Kruskal/KzpLEAyF">Kruskal, J. B.</a> (May 1960). <a href="https://www.ams.org/journals/tran/1960-095-02/S0002-9947-1960-0111704-1/S0002-9947-1960-0111704-1.pdf">"Well-Quasi-Ordering, The Tree Theorem, and Vazsonyi's Conjecture"</a> (PDF). <a href="/facts/Transactions_of_the_American_Mathematical_Society/JmKtyCwK">Transactions of the American Mathematical Society</a>. 95 (2). <a href="/facts/American_Mathematical_Society/fr5gotCt">American Mathematical Society</a>: 210–225. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.2307%2F1993287">10.2307/1993287</a>. <a href="/facts/JSTOR_(identifier)/YTeVmaJ7">JSTOR</a> <a href="https://www.jstor.org/stable/1993287">1993287</a>. <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0111704">0111704</a>.</li>
<li>Marcone, Alberto (2005). Simpson, Stephen G. (ed.). <a href="https://users.dimi.uniud.it/~alberto.marcone/wqobqo.pdf">"WQO and BQO theory in subsystems of second order arithmetic"</a> (PDF). Reverse Mathematics. Lecture Notes in Logic. 21. Cambridge: <a href="/facts/Cambridge_University_Press/fgEBSSRq">Cambridge University Press</a>: 303–330. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1017%2F9781316755846.020">10.1017/9781316755846.020</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-1-316-75584-6.</li>
<li><a href="/facts/Crispin_St._J._A._Nash-Williams/YY5uresp">Nash-Williams, C. St. J. A.</a> (October 1963). <a href="https://www.cs.umd.edu/~gasarch/COURSES/752/S22/slides/nashwilliams.pdf">"On well-quasi-ordering finite trees"</a> (PDF). <a href="/facts/Mathematical_Proceedings_of_the_Cambridge_Philosophical_Society/KUUzcS7S">Mathematical Proceedings of the Cambridge Philosophical Society</a>. 59 (4): 833–835. <a href="/facts/Bibcode_(identifier)/9HtdQSGB">Bibcode</a>:<a href="https://ui.adsabs.harvard.edu/abs/1963PCPS...59..833N">1963PCPS...59..833N</a>. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1017%2FS0305004100003844">10.1017/S0305004100003844</a>. <a href="/facts/ISSN_(identifier)/DPAflDvU">ISSN</a> <a href="https://search.worldcat.org/issn/0305-0041">0305-0041</a>. <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=0153601">0153601</a>. <a href="/facts/S2CID_(identifier)/ldJsHa2Y">S2CID</a> <a href="https://api.semanticscholar.org/CorpusID:251095188">251095188</a>.</li>
<li>Rathjen, Michael; Weiermann, Andreas (February 1993). <a href="https://core.ac.uk/download/pdf/82187099.pdf">"Proof-theoretic investigations on Kruskal's theorem"</a> (PDF). <a href="/facts/Annals_of_Pure_and_Applied_Logic/tR1Pk1tr">Annals of Pure and Applied Logic</a>. 60 (1): 49–88. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2F0168-0072%2893%2990192-G">10.1016/0168-0072(93)90192-G</a>. <a href="/facts/MR_(identifier)/uP137L11">MR</a> <a href="https://mathscinet.ams.org/mathscinet-getitem?mr=1212407">1212407</a>.</li>
<li><a href="/facts/Steve_Simpson_(mathematician)/33WuyqGs">Simpson, Stephen G.</a> (1985). "Nonprovability of certain combinatorial properties of finite trees". In Friedman, Harvey; Harrington, L. A.; Scedrov, A.; et al. (eds.). Harvey Friedman's research on the foundations of mathematics. Studies in logic and the foundations of mathematics. Amsterdam ; New York: <a href="/facts/North-Holland_(imprint)/jkPSAEmR">North-Holland</a>. pp. 87–117. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-0-444-87834-2.</li>
<li>Smith, Rick L. (1985). "The Consistency Strengths of Some Finite Forms of the Higman and Kruskal Theorems". In <a href="/facts/Harvey_Friedman_(mathematician)/Yq10dMrt">Friedman, Harvey</a>; Harrington, L. A. (eds.). Harvey Friedman's research on the foundations of mathematics. Studies in logic and the foundations of mathematics. Vol. 117. Amsterdam ; New York: <a href="/facts/North-Holland_(imprint)/jkPSAEmR">North-Holland</a>. pp. 119–136. <a href="/facts/Doi_(identifier)/muM9Etpq">doi</a>:<a href="https://doi.org/10.1016%2Fs0049-237x%2809%2970157-0">10.1016/s0049-237x(09)70157-0</a>. <a href="/facts/ISBN_(identifier)/15AdSPa9">ISBN</a> 978-0-444-87834-2.</li></ul>

<h2 id="references">References</h2>

<ol>
<li id="fn:1">"The Enormity of the Number TREE(3) Is Beyond Comprehension". Popular Mechanics. 20 October 2017. Retrieved 4 February 2025. <a href="https://www.popularmechanics.com/science/math/a28725/number-tree3/" target="_blank">https://www.popularmechanics.com/science/math/a28725/number-tree3/</a> <a href="#fnref:1" class="footnote-back-ref">↩</a></li>
<li id="fn:2">Simpson 1985, Theorem 1.8 - Simpson, Stephen G. (1985). "Nonprovability of certain combinatorial properties of finite trees". In Friedman, Harvey; Harrington, L. A.; Scedrov, A.; et al. (eds.). Harvey Friedman's research on the foundations of mathematics. Studies in logic and the foundations of mathematics. Amsterdam ; New York: North-Holland. pp. 87–117. ISBN 978-0-444-87834-2. <a href="#fnref:2" class="footnote-back-ref">↩</a></li>
<li id="fn:3">Friedman 2002, p. 60 - Friedman, Harvey M. (2002). "Internal finite tree embeddings". In Sieg, Wilfried; Feferman, Solomon (eds.). Reflections on the foundations of mathematics: essays in honor of Solomon Feferman. Lecture notes in logic. Vol. 15. Natick, Mass: AK Peters. pp. 60–91. ISBN 978-1-56881-170-3. MR 1943303. <a href="https://books.google.com/books?id=o-dhDwAAQBAJ&pg=PA60" target="_blank">https://books.google.com/books?id=o-dhDwAAQBAJ&pg=PA60</a> <a href="#fnref:3" class="footnote-back-ref">↩</a></li>
<li id="fn:4">Simpson 1985, Definition 4.1 - Simpson, Stephen G. (1985). "Nonprovability of certain combinatorial properties of finite trees". In Friedman, Harvey; Harrington, L. A.; Scedrov, A.; et al. (eds.). Harvey Friedman's research on the foundations of mathematics. Studies in logic and the foundations of mathematics. Amsterdam ; New York: North-Holland. pp. 87–117. ISBN 978-0-444-87834-2. <a href="#fnref:4" class="footnote-back-ref">↩</a></li>
<li id="fn:5">Simpson 1985, Theorem 5.14 - Simpson, Stephen G. (1985). "Nonprovability of certain combinatorial properties of finite trees". In Friedman, Harvey; Harrington, L. A.; Scedrov, A.; et al. (eds.). Harvey Friedman's research on the foundations of mathematics. Studies in logic and the foundations of mathematics. Amsterdam ; New York: North-Holland. pp. 87–117. ISBN 978-0-444-87834-2. <a href="#fnref:5" class="footnote-back-ref">↩</a></li>
<li id="fn:6">Marcone 2005, pp. 8–9 - Marcone, Alberto (2005). Simpson, Stephen G. (ed.). "WQO and BQO theory in subsystems of second order arithmetic" (PDF). Reverse Mathematics. Lecture Notes in Logic. 21. Cambridge: Cambridge University Press: 303–330. doi:10.1017/9781316755846.020. ISBN 978-1-316-75584-6. <a href="https://users.dimi.uniud.it/~alberto.marcone/wqobqo.pdf" target="_blank">https://users.dimi.uniud.it/~alberto.marcone/wqobqo.pdf</a> <a href="#fnref:6" class="footnote-back-ref">↩</a></li>
<li id="fn:7">Rathjen & Weiermann 1993. - Rathjen, Michael; Weiermann, Andreas (February 1993). "Proof-theoretic investigations on Kruskal's theorem" (PDF). Annals of Pure and Applied Logic. 60 (1): 49–88. doi:10.1016/0168-0072(93)90192-G. MR 1212407. <a href="https://core.ac.uk/download/pdf/82187099.pdf" target="_blank">https://core.ac.uk/download/pdf/82187099.pdf</a> <a href="#fnref:7" class="footnote-back-ref">↩</a></li>
<li id="fn:8">Smith 1985, p. 120 - Smith, Rick L. (1985). "The Consistency Strengths of Some Finite Forms of the Higman and Kruskal Theorems". In Friedman, Harvey; Harrington, L. A. (eds.). Harvey Friedman's research on the foundations of mathematics. Studies in logic and the foundations of mathematics. Vol. 117. Amsterdam ; New York: North-Holland. pp. 119–136. doi:10.1016/s0049-237x(09)70157-0. ISBN 978-0-444-87834-2. <a href="https://doi.org/10.1016%2Fs0049-237x%2809%2970157-0" target="_blank">https://doi.org/10.1016%2Fs0049-237x%2809%2970157-0</a> <a href="#fnref:8" class="footnote-back-ref">↩</a></li>
<li id="fn:9">Friedman, Harvey (28 March 2006). "273:Sigma01/optimal/size". Ohio State University Department of Maths. Retrieved 8 August 2017. <a href="http://www.cs.nyu.edu/pipermail/fom/2006-March/010279.html" target="_blank">http://www.cs.nyu.edu/pipermail/fom/2006-March/010279.html</a> <a href="#fnref:9" class="footnote-back-ref">↩</a></li>
<li id="fn:10">Friedman, Harvey M. (1 June 2000). "Enormous Integers In Real Life" (PDF). Ohio State University. Retrieved 8 August 2017. <a href="https://u.osu.edu/friedman.8/files/2014/01/EnormousInt.12pt.6_1_00-23kmig3.pdf" target="_blank">https://u.osu.edu/friedman.8/files/2014/01/EnormousInt.12pt.6_1_00-23kmig3.pdf</a> <a href="#fnref:10" class="footnote-back-ref">↩</a></li>
<li id="fn:11">Friedman, Harvey M. (8 October 1998). "Long Finite Sequences" (PDF). Ohio State University Department of Mathematics. pp. 5, 48 (Thm.6.8). Retrieved 8 August 2017. <a href="https://u.osu.edu/friedman.8/files/2014/01/LongFinSeq98-2f0wmq3.pdf" target="_blank">https://u.osu.edu/friedman.8/files/2014/01/LongFinSeq98-2f0wmq3.pdf</a> <a href="#fnref:11" class="footnote-back-ref">↩</a></li>
</ol>

Kruskal's tree theorem open-in-new

Kruskal's tree theorem