Kruskal's tree theorem states that finite trees are well-quasi-ordered under homeomorphic embedding (i.e. inf-preserving injections). In order to prove the Robertson-Seymour theorem, the "Extended Kruskal's Theorem" was formulated by allowing the vertices $a$ of the trees to be labeled by natural numbers $\ell a$, and strengthening homeomorphic embedding to the notion of gap-embedding. A homeomorphic embedding $f:(B_1,\leq_1,\ell_1)\to(B_2,\leq_2,\ell_2)$ is a gap-embedding if:
- It preserves labels, i.e. for all $b\in B_1$ we have $\ell_1b=\ell_2f(b)$.
- Gap-condition: if $a,b\in B_1$ are such that $b$ is a child vertex of $a$, then for any $c\in B_2$ in the interval $f(a)<_2 c<_2 f(b)$, we have $\ell_2c\geq_2\ell_2f(b)$. This causes a "gap" between $a$'s image and $b$'s image in which only vertices with higher label than $b$'s are permitted.
In "The Realm of Ordinal Analysis", when explaining the high reverse-mathematical strength of Robertson-Seymour, Rathjen says "the gap condition imposed on the embeddings between trees is actually gleaned from the ordering of the terms in $\mathcal T(\psi_0(\Omega_\omega))$ [ordinal notation system used in analyzing $\Pi_1^1-CA_0$]". If we were to change the gap-condition to match some stronger ordinal notation, the analogue of Kruskal's theorem using those embeddings would be independent of stronger theories.
My question is, if we modify the gap-condition in this way, can there be such a condition which still well-quasi-orders the finite trees, but now with order type greater than $\psi_0(\Omega_\omega)$? To keep gap-conditions "nice", I require "modified gap-condition" here to have the label-preserving property and satisfy a weaker property of the original gap-condition:
- If $a,b\in B_1$ are such that $b$ is a child vertex of $a$, then there exists $c\in B_2$ in the interval $f(a)<_2 c<_2 f(b)$ such that $\ell_2c\geq_2\ell_2f(b)$. Now the gap may contain lesser labels, but must contain at least one point where they witness the size of the inital $\ell b$.
Edits: One slight modification previously published is to label the nodes from a set of ordinals instead of from naturals. (Tzameret 2002, shown unprovable in Gordeev 1990) A change of label set may be too close to the original definition to qualify as a brand new modification. There is also a condition known as the symmetric gap condition in Gordeev and Weiermann's "Phase transitions in Proof Theory" (proceedings of DMTCS, 2010) that gives independence from $\Pi_1^1\textrm{-TR}_0$ (which has proof-theoretic ordinal larger than $\psi_0(\Omega_\omega)$, although I do not see the order type explicitly stated. However it does not have the "nice" gap-condition property.
Some thoughts:
- The most straightforward such condition is to only require the weakened gap-condition, but it shouldn't be hard to show the trees are not wqo under it.
- The next most straightforward is "the interval $f(a)<_2 c <_2 f(b)$ may contain at most one $c$ with $\ell_2c<_2\ell_2f(b)$". My first guess is the resulting ordering on trees would superficially resemble Taranovsky's $n=2$ ordinal notation due to its "shifted" nature: For shorthand write $d_ka$ for $C(\Omega_2k+a,0)$, then if we look at the parse tree of a 2-built-from-below term, some parts of it look like the witness inside the gap that happens in this altered gap-embeddability. (For example, the bold part of $d_1d_0\boldsymbol{d_2}d_20$ stands for the relevant node in the parse tree of $d_1d_0d_2d_20$, and $d_1d_20$ modified-gap-embeds into $d_1d_0d_2d_20$.)