Friedman's finite trees

Friedman's finite trees result in an extremely fast-growing function, devised by Harvey Friedman .
== Description ==
Define \([S]^k\) as all the \(k\)-element subsets of the set \(S\). For positive integers \(n\), we will also use the abbreviation \([n]^k\) for \([\{0, 1, 2, \ldots, n - 1\}]^k\). For \(x,y \in [\mathbb{N}]^k\), we say that \(x\) is entirely lower than \(y\) iff all members of \(x\) are less than all members in \(y\). We use "\(\leq^*\)" denote an ordering on \([\mathbb{N}]^k \cup \{\infty\}\) where the members of the sets are listed in strictly descending order and the sets are then ordered lexicographically, and \(\infty\) is the maximum element. 
A partial ordering is a pair \((X,\leq)\) for a nonempty set \(X\) and a reflexive, transitive, and antisymmetric relation \(\leq\). Inside this partial ordering, we say that \(y\) is an ancestor of \(x\) iff \(x < y\). A tree is a partial ordering \(T = (V,\leq)\) with a minimum element and finite \(V\) such that the ancestors of any given element of \(V\) are linearly ordered under \(\leq\). \(V(T) = V\) is the set of vertices in the tree. The root \(r(T)\) of a tree \(T\) is its minimal vertex under \(\leq\), and its children \(\text{Ch}(T) = V(T)\backslash\{r(T)\}\) consist of all the tree's vertices save for the root. A tree \(T\) is trivial iff \(|V(T)| = 1\). The parent of \(x\) in \(T\), denoted \(p(x,T)\), is the vertex \(y\) such that \(x < y\) and there is no \(z\) such that \(x < z < y\).
A \(k\)-tree is defined a tree \(T = (V,\leq)\) such that \(r(T) = \infty\) and \(\text{Ch}(T) \subseteq [\mathbb{N}]^k\). For \(k,n \geq 1\), a \(k,n\)-tree is defined as a \(k\)-tree with \(\text{Ch}(T) \subseteq [n]^k\). We let \(\text{TR}(k,n)\) denote the set of all \(k,n\)-trees.
Next we define some relations on trees and types of trees. Define \(T_1 \subseteq T_2\) for trees \(T_1,T_2\) as the expression \(r(T_1) = r(T_2) \wedge \forall x \in \text{Ch}(T_1): p(x, T_1) = p(x, T_2)\). We say that \(x \in [\mathbb{N}]^k\) dominates a \(k\)-tree \(T\) iff \(x\) is \(>^*\) all the children of \(T\). Finally, for \(k,n\)-trees \(T_1\) and \(T_2\), we say that \(T_1 \leq^* T_2\) iff \(\forall x \in \text{Ch}(T_1): p(x,T_1) \leq^* p(x,T_2)\).
An insertion domain in \(\text{TR}(k,n)\) is a nonempty set \(S \subseteq \text{TR}(k,n)\) such that for all \(T \in S\), \(x \in [n]^k\), \(x\) dominating \(T\), there exists \(T' \in S\) such that \(T \subseteq T'\) and \(\text{Ch}(T') = \text{Ch}(T) \cup \{x\}\). An insertion domain in \(\text{TR}(k,n)\) is initial iff it includes the trivial \(k\)-tree. A subset of \(\text{TR}(k,n)\) is said to be nonincreasing iff \(\forall T_1, T_2 \in S: T_1 \leq^* T_2 \Rightarrow T_1 \subseteq T_2\).
Let \(F(k, p)\) be the least \(n\) such that every nonincreasing initial insertion domain in \(\text{TR}(k, n)\) contains a \(k,n\)-tree in which all \(k\)-element subsets of some \(p\)-element set are vertices with the same entirely lower ancestors. The well-definedness of \(F(k, p)\) is provable under \(\textrm{ZFC}\) set theory augumented by the existence of the axiom "for any \(k \in \mathbb{N}\), there exists a \(k\)-subtle cardinal".
== Explanation ==
Here we provide a more intuitive summary of the very technical description above. 
First, we must define a \(k,n\)-string. These are special strings consisting of \(k\) integers in the range \([0,n)\), in strictly decreasing order. For example, an example of a 7,10-string is [9,7,6,5,3,2,0]. The members must be in strictly decreasing order, so no repetitions are allowed — [9,9,6,5,3,2,0] is not a valid string. (For those comparing this section to the above, \(k,n\)-strings are precisely the members of the set \([n]^k\).) Strings are subject to a lexicographical ordering. If we consider the integers \([0,n)\) to be our "alphabet" and strings to be "words," then this is exactly a dictionary order.
On to trees. Friedman's usage of the term "tree" is identical to a rooted tree in graph theory, or a tree data structure in computer science with no order between siblings. (From here we will be using standard terminology for these trees such as "leaf nodes," "parents," etc., so go ahead and brush up if you're not familiar with those.) \(k,n\)-trees are trees with the following labeling scheme: the root node is given the special label "\(\infty\)," all other nodes are labeled with \(k,n\)-strings, and all labels are distinct. Below is a valid 3,6-tree (which also happens to be a 3,7-tree, 3,8-tree, and so forth):
:
Now we will discuss insertion on \(k,n\)-trees. A string \(X\) dominates a tree if it is lexicographically after all the labels in the tree (other than \(\infty\)). Insertion, then, takes a dominating string \(X\) and inserts it as a leaf node anywhere on the tree, producing a new valid \(k,n\)-tree. The image below demonstrates this process on a 3,6-tree:
:
Let's develop a notation for these trees. The first tree above could be written
 (∞(430(542))(321(410)(421(530))))
An insertion domain, then, is a set of \(k,n\)-trees where for each tree, every possible dominating value of \(X\) can be inserted in some way to form a new tree that is already in the insertion domain. An insertion domain containing a "trivial tree" (with just a root node) is an initial insertion domain.
Next we need to define the "subtree" relation. \(T_1\) is a subtree of \(T_2\) if we can produce \(T_2\) by adding leaf nodes to \(T_1\). A slightly different relation is the "less than or equal to" relation, which means that \(T_2\) can be produced from \(T_1\) from the following operations:
* Adding leaf nodes
* Moving a node to a parent that is equal to or lexicographically after is previous parent
A nonincreasing initial insertion domain, then, is an initial insertion domain such that if \(T_1\) is less than or equal to \(T_2\), \(T_1\) is a subtree of \(T_2\). In other words, there are no "enlarging parents" between any pair of trees, hence the term "nonincreasing."
Alright, that's a lot of definition without an example! Let's try building a plain ol' 3,2 initial insertion domain. First we need a trivial tree...
 (∞)
What strings dominate this? All of them! Namely 10, 20, and 21. In each case there's only one way to insert them:
 (∞(10))
 (∞(20))
 (∞(21))
20 and 21 dominate the first three, 21 dominates the second, and there are no strings that dominate the third. We can insert them anywhere in the tree. The below are just arbitrary choices of mine.
 (∞(10(20)))
 (∞(10(21)))
 (∞(20)(21))
And finally we need a tree by inserting the dominating string 21 to the first tree:
 (∞(10(20)(21)))
All together, we have (∞), (∞(10)), (∞(20)), (∞(21)), (∞(10(20))), (∞(10(21))), (∞(20)(21)), and (∞(10(20)(21))). This is a valid 3,2 initial insertion domain, since for each tree all possible dominating strings may be inserted to form another tree in the domain.
== Sources ==
== See also ==
Category:Functions
Category:Theorems
Category:Unnamed numbers