克魯斯卡爾樹定理

TREE函數、Kruskal樹定理（英語：Kruskal's tree theorem）是逆數學的突出示例。由安德魯·瓦茲尼（英語：Andrew Vázsonyi）推測並由約瑟夫·克魯斯卡爾證明。

已隱藏部分未翻譯內容，歡迎參與翻譯。

In mathematics, Kruskal's tree theorem states that the set of finite trees over a well-quasi-ordered（英語：well-quasi-ordering） set of labels is itself well-quasi-ordered under homeomorphic（英語：homeomorphism (graph theory)） embedding. 在數學中，克魯斯卡樹定理指出，在準有序（英文：well-quasi-ordering）標籤集上的有限樹集合本身在同胚下也是良準有序的（英文：同胚（圖論））嵌入。

歷史該定理由安德魯·瓦茲索尼（Andrew Vázsonyi）猜想並由約瑟夫·克魯斯卡爾（Joseph Kruskal，1960）證明； Crispin Nash-Williams（1963）給了一個簡短的證明。它從此成為逆向數學（英語：reverse math）中的一個突出例子，作為在 ATR0 內無法證明的陳述（算術超限遞歸（英語：arithmetic transfinite recursion）的一種形式）和有限（英語：finitary）應用該定理給出了快速增長的TREE 函數的存在性。

2004年，這個結果被從樹推廣到圖，成為羅伯遜-西摩定理（英語：Robertson-Seymour theorem），這一結果在逆向數學中也被證明很重要，並導致了增長更快的SSCG 函數（英語： Friedman 的 SSCG 函數）。

陳述這裏給出的版本是由 Nash-Williams 證明的；克魯斯卡爾的表述要強一些。我們認為的所有樹木都是有限的。

給定一棵有根的樹T，並給定頂點v、w，如果從根到w 的唯一路徑包含v，則稱w 為v 的後繼；如果從v 到w 的路徑另外不包含v，則稱w 為v 的直接後繼其他頂點。

取X為偏序集（中文：partiallyorderedset）。如果 T1、T2 是頂點標記為 X 的有根樹，我們說 T1 可 inf-embeddable 在 T2 中，並且如果存在從 T1 的頂點到 T2 的頂點的單射映射 F，則寫 T1 ≤ T2，使得

弗里德曼的工作對於可數標籤集 X X.克魯斯卡樹定理可以用二階算術來表達和證明（中文：二階算術）。然而，就像古德斯坦定理或巴黎-哈靈頓定理（英語：Paris-Harrington theorem）一樣，該定理的一些特殊情況和變體可以用比可以證明它們的子系統弱得多的二階算術子系統來表達。這是哈維·弗里德曼（Harvey Friedman）在 20 世紀 80 年代初首次觀察到的，這是當時新興的逆向數學領域的早期成功。在上面的樹被認為是未標記的情況下（即，在 X X 有順序一），Friedman 發現結果在 ATR0（英語：算術超限遞歸）,[2] 從而給出了第一個謂詞（英語：impredicativity）結果的例子，並帶有可證明的謂詞證明.[3]此定理的這種情況仍可由 Π1 證明 1-CA0，但透過在上述樹的順序定義中添加「間隙條件」[4]，他發現該定理的自然變體在該系統中無法證明。[5][6]很久以後，羅伯森-西摩定理給了另一個無法由 Π1 證明的定理 1-CA0。

序數分析（中文：序數分析）證實了克魯斯卡爾定理的強度，該定理的證明論序數等於小維勃倫序數（英文：小維勃倫序數）（有時與較小的阿克曼序數（英文：阿克曼序數）相混淆） ).[來源請求]

樹(3) 假設 P(n) 是這樣的語句：

存在一些 m，如果 T1,...,Tm 是未標記有根樹的有限序列，其中 Tk 有 n+k 個頂點，則對於某些 i < j，Ti ≤ Tj。根據克魯斯卡定理和柯尼格引理，所有陳述 P(n) 都是正確的。對於每個n，皮亞諾算術（英語：Peano axioms）可以證明P(n)為真，但皮亞諾算術不能證明「P(n)對於所有n都為真」這一命題。[7]此外，皮亞諾算術中 P(n) 的最短證明的長度作為 n 的函數增長得非常快，遠遠快於任何原始遞歸函數（英語：primitive recursive function）或阿克曼函數。 P(n) 所適用的最小 m 同樣隨 n 增長得非常快。

透過合併標籤，弗里德曼定義了一個成長速度更快的函數。[8]對於正整數 n，取 TREE(n)[*] 為最大的 m，這樣我們有：

有一個由 n 個標籤集標記的有根樹序列 T1,...,Tm，其中每個 Ti 最多有 i 個頂點，使得 Ti ≤ Tj 對於任何 i < j ≤ m 不成立。 TREE 序列開始為TREE(1) = 1, TREE(2) = 3，然後突然TREE(3) 爆炸到非常大的值，以至於許多其他「大」組合常數，例如Friedman 的n(4), [*相較之下，*] 非常小。事實上，它比 nn(5)(5) 大得多。 n(4) 的下界（因此 TREE(3) 的下界極弱）為 AA(187196)(1),[9]，其中 A(x) 採用一個參數，定義為 A(x, x)，其中A (k, n) 有兩個參數，是阿克曼函數（英語：Ackermann's function）的一個特定版本，定義為： A(1, n) = 2n, A(k+1, 1) = A (k , 1), A(k+1, n+1) = A(k, A(k+1, n))。例如，葛立恆數遠小於下限 AA(187196)(1)。可以證明函數TREE的成長率至少為 F θ （ Ω ω ω ） {\displaystyle f_{\theta (\Omega ^{\omega }\omega )}} 中的快速成長層次結構（中文：快速成長層次結構）。 AA(187196)(1) 大約為 G 3 ↑ 187196 3 {\displaystyle g_{3\uparrow ^{187196}3}}，其中 gx 是格雷厄姆函數（中文：格雷厄姆數）。

History

The theorem was conjectured by Andrew Vázsonyi（英語：Andrew Vázsonyi） and proved by Joseph Kruskal （1960）; a short proof was given by Crispin Nash-Williams （1963）. It has since become a prominent example in reverse mathematics（英語：reverse mathematics） as a statement that cannot be proved within ATR₀ (a form of arithmetical transfinite recursion（英語：arithmetical transfinite recursion）), and a finitary（英語：finitary） application of the theorem gives the existence of the fast-growing TREE function.

In 2004, the result was generalized from trees to graphs as the Robertson–Seymour theorem（英語：Robertson–Seymour theorem）, a result that has also proved important in reverse mathematics and leads to the even-faster-growing SSCG function（英語：Friedman's SSCG function）.

Statement

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 root, 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 partially ordered set（英語：partially ordered set）. If $T 1$ , $T 2$ are rooted trees with vertices labeled in $X$ , we say that $T 1$ is inf-embeddable in $T 2$ and write $T 1 \leq T 2$ if there is an injective map $F$ from the vertices of $T 1$ to the vertices of $T 2$ such that

For all vertices $v$ of $T 1$ , the label of $v$ precedes the label of $F (v)$ ,
If $w$ is any successor of $v$ in $T 1$ , then $F (w)$ is a successor of $F (v)$ , and
If $w 1$ , $w 2$ are any two distinct immediate successors of $v$ , then the path from $F (w 1)$ to $F (w 2)$ in $T 2$ contains $F (v)$ .

Kruskal's tree theorem then states:

If $X$ is well-quasi-ordered（英語：well-quasi-ordering）, 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 $T 1, T 2, \dots$ of rooted trees labeled in $X$ , there is some $i < j$ so that $T i \leq T j$ .)

Weak tree function

Define $tree(n)$ , the weak tree function, as the length of the longest sequence of 1-labelled trees (i.e. $X = {1}$ ) such that:

The tree at position $k$ in the sequence has no more than $k + n$ vertices, for all $k$ .
No tree is homeomorphically embeddable into any tree following it in the sequence.

It is known that tree(1) = 2, tree(2) = 5, and tree(3) ≥ 844424930131960,^[1]^{[需要較佳來源]} but $TREE(3)$ (where the argument specifies the number of labels; see below（英語：Kruskal's tree theorem#TREE(3)）) is larger than $\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{\mathrm {tree} ^{8}(7)}(7)}(7)}(7)}(7)$

Friedman's work

For a countable label set $X$ , Kruskal's tree theorem can be expressed and proven using second-order arithmetic（英語：second-order arithmetic）. However, like 古德斯坦定理 or the Paris–Harrington theorem（英語：Paris–Harrington theorem）, 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 Harvey Friedman（英語：Harvey Friedman） 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 order one), Friedman found that the result was unprovable in <span class="ilh-all " data-orig-title="ATR₀" data-lang-code="en" data-lang-name="英語" data-foreign-title="arithmetical transfinite recursion">[[:ATR₀|ATR₀]]（英語：arithmetical transfinite recursion）,^[2] thus giving the first example of a predicative（英語：impredicativity） result with a provably impredicative proof.^[3] This case of the theorem is still provable by Π1
1-CA₀, but by adding a "gap condition"^[4] to the definition of the order on trees above, he found a natural variation of the theorem unprovable in this system.^[5]^[6] Much later, the Robertson–Seymour theorem would give another theorem unprovable by Π1
1-CA₀.

Ordinal analysis（英語：Ordinal analysis） confirms the strength of Kruskal's theorem, with the proof-theoretic ordinal of the theorem equaling the small Veblen ordinal（英語：small Veblen ordinal） (sometimes confused with the smaller Ackermann ordinal（英語：Ackermann ordinal）).^{[來源請求]}

TREE(3)

Suppose that P(n) is the statement:

There is some m such that if T₁,...,T_m is a finite sequence of unlabeled rooted trees where T_k has n+k vertices, then T_i ≤ T_j for some i < j.

All the statements P(n) are true as a consequence of Kruskal's theorem and 柯尼格引理. For each n, Peano arithmetic（英語：Peano axioms） can prove that P(n) is true, but Peano arithmetic cannot prove the statement "P(n) is true for all n".^[7] Moreover the length of the shortest proof of P(n) in Peano arithmetic grows phenomenally fast as a function of n, far faster than any primitive recursive function（英語：primitive recursive function） or the 阿克曼函數 for example. The least m for which P(n) holds similarly grows extremely quickly with n.

By incorporating labels, Friedman defined a far faster-growing function.^[8] For a positive integer n, take TREE(n)^[*] to be the largest m so that we have the following:

There is a sequence T₁,...,T_m of rooted trees labelled from a set of n labels, where each T_i has at most i vertices, such that T_i ≤ T_j does not hold for any i < j ≤ m.

The TREE sequence begins TREE(1) = 1, TREE(2) = 3, then suddenly TREE(3) explodes to a value so immensely large that many other "large" combinatorial constants, such as Friedman's n(4),^[**] are extremely small by comparison. In fact, it is much larger than nⁿ⁽⁵⁾(5). A lower bound for n(4), and hence an extremely weak lower bound for TREE(3), is A^A(187196)(1),^[9] where A(x) taking one argument, is defined as A(x, x), where A(k, n), taking two arguments, is a particular version of Ackermann's function（英語：Ackermann's function） defined as: A(1, n) = 2n, A(k+1, 1) = A(k, 1), A(k+1, n+1) = A(k, A(k+1, n)). 葛立恆數, for example, is much smaller than the lower bound A^A(187196)(1). It can be shown that the growth-rate of the function TREE is at least $f_{\theta (\Omega ^{\omega }\omega )}$ in the fast-growing hierarchy（英語：fast-growing hierarchy）. A^A(187196)(1) is approximately $g_{3\uparrow ^{187196}3}$ , where g_x is Graham's function（英語：Graham's number）.

參見

Paris–Harrington theorem（英語：Paris–Harrington theorem）
Kanamori–McAloon theorem（英語：Kanamori–McAloon theorem）
Robertson–Seymour theorem（英語：Robertson–Seymour theorem）

註釋

^{^ *} Friedman originally denoted this function by TR[n].

^{^ **} 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 x_i,...,x_2i is a subsequence of any later block x_j,...,x_2j.^[10]

n(1)=3,n(2)=11,\,{\textrm {and}}\,n(3)>2\uparrow ^{7197}158386

.

Category:Trees (graph theory)（英語：Category:Trees (graph theory)）

參考

Citations

^ TREE sequence. Googology Wiki | Fandom. [9 July 2020]. （原始內容存檔於2020-01-09）.
^ Simpson 1985, Theorem 1.8
^ Friedman 2002, p. 60
^ Simpson 1985, Definition 4.1
^ Simpson 1985, Theorem 5.14
^ Marcone 2001, p. 8–9
^ Smith 1985, p. 120
^ Friedman, Harvey. 273:Sigma01/optimal/size. Ohio State University Department of Maths. 28 March 2006 [8 August 2017]. （原始內容存檔於2022-12-07）.
^ Friedman, Harvey M. Enormous Integers In Real Life (PDF). Ohio State University. 1 June 2000 [8 August 2017]. （原始內容存檔 (PDF)於2016-10-18）.
^ Friedman, Harvey M. Long Finite Sequences (PDF). Ohio State University Department of Mathematics: 5, 48 (Thm.6.8). 8 October 1998 [8 August 2017]. （原始內容存檔 (PDF)於2017-08-09）.

Bibliography

Friedman, Harvey M., Internal finite tree embeddings. Reflections on the foundations of mathematics (Stanford, CA, 1998), Lect. Notes Log. 15, Urbana, IL: Assoc. Symbol. Logic: 60–91, 2002, MR 1943303
Gallier, Jean H., What's so special about Kruskal's theorem and the ordinal Γ₀? A survey of some results in proof theory (PDF), Ann. Pure Appl. Logic, 1991, 53 (3): 199–260 [2022-11-07], MR 1129778, doi:10.1016/0168-0072(91)90022-E  , （原始內容存檔 (PDF)於2023-02-03）
Kruskal, J. B., Well-quasi-ordering, the tree theorem, and Vazsonyi's conjecture (PDF), Transactions of the American Mathematical Society (American Mathematical Society), May 1960, 95 (2): 210–225 [2022-11-07], JSTOR 1993287, MR 0111704, doi:10.2307/1993287, （原始內容存檔 (PDF)於2021-10-21）
Marcone, Alberto. Wqo and bqo theory in subsystems of second order arithmetic (PDF). Reverse Mathematics. 2001, 21: 303–330 [2022-11-07]. （原始內容存檔 (PDF)於2022-05-08）.
Nash-Williams, C. St.J. A., On well-quasi-ordering finite trees, Proc. Camb. Phil. Soc., 1963, 59 (4): 833–835, Bibcode:1963PCPS...59..833N, MR 0153601, S2CID 251095188, doi:10.1017/S0305004100003844
Rathjen, Michael; Weiermann, Andreas. Proof-theoretic investigations on Kruskal's theorem. Annals of Pure and Applied Logic. 1993, 60 (1): 49–88. doi:10.1016/0168-0072(93)90192-g  .
Simpson, Stephen G., Nonprovability of certain combinatorial properties of finite trees, Harrington, L. A.; Morley, M.; Scedrov, A.; et al (編), Harvey Friedman's Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics, North-Holland: 87–117, 1985
Smith, Rick L., The consistency strengths of some finite forms of the Higman and Kruskal theorems, Harrington, L. A.; Morley, M.; Scedrov, A.; et al (編), Harvey Friedman's Research on the Foundations of Mathematics, Studies in Logic and the Foundations of Mathematics, North-Holland: 119–136, 1985

[1] TREE sequence. Googology Wiki | Fandom. [9 July 2020]. （原始內容存檔於2020-01-09）.

[2] Simpson 1985, Theorem 1.8

[3] Friedman 2002, p. 60

[4] Simpson 1985, Definition 4.1

[5] Simpson 1985, Theorem 5.14

[6] Marcone 2001, p. 8–9

[SmiA-7] Smith 1985, p. 120

[8] Friedman, Harvey. 273:Sigma01/optimal/size. Ohio State University Department of Maths. 28 March 2006 [8 August 2017]. （原始內容存檔於2022-12-07）.

[9] Friedman, Harvey M. Enormous Integers In Real Life (PDF). Ohio State University. 1 June 2000 [8 August 2017]. （原始內容存檔 (PDF)於2016-10-18）.

[10] Friedman, Harvey M. Long Finite Sequences (PDF). Ohio State University Department of Mathematics: 5, 48 (Thm.6.8). 8 October 1998 [8 August 2017]. （原始內容存檔 (PDF)於2017-08-09）.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[*]

[**]

[9]

[10]