Background:


Given a well partial order $X$ (more commonly studied with antisymmetry dropped as well-quasi-orders, but I'm going to say well partial order to make this definition simpler, obviously the two theories are essentially the same), De Jongh and Parikh showed there's always a largest ordinal that can be realized as the order type of a linearization of $X$. There are also several other equivalent characterizations of this quantity. Following De Jongh and Parikh I'll denote this $o(X)$, and following Kriz and Thomas I'll call it the *type* of $X$.


Consider the WPO of finite plane trees (ordered trees) ordered under topological, order-preserving embedding; the statement that this is a WPO is Kruskal's tree theorem. Let's call this $T$.


Fact 1: The type of $T$ is the small Veblen ordinal. Upper bound due to Schmidt, lower bound due (as far as I'm aware) to [Jervell](https://www.researchgate.net/publication/221652708_Finite_Trees_as_Ordinals) (though he didn't state it in that form).


Fact 2: Rathjen and Weiermann -- using Schmidt's techniques -- [showed](https://www.sciencedirect.com/science/article/pii/016800729390192G) that, in a certain sense, the proof-theoretic ordinal of Kruskal's tree theorem is the small Veblen ordinal.


Note that this seems to be a somewhat unusual sense... the sense seems to be something like, for a theory to prove Kruskal's tree theorem, it has to have proof-theoretic ordinal (in the usual sense) of at least the small Veblen ordinal? Apologies, I'm not much of a logician, I'm having some trouble reading the paper... (maybe this is actually a common thing in logic, I wouldn't be familiar).


Question: In general, given a Turing machine $M$ computing a countable WPO $X$ -- probably satisfying additional nice conditions but I'll get to that -- is there a relation between $o(X)$, and the proof-theoretic ordinal in the above sense -- to the extent that this is a well-defined thing, which I'm not clear on -- of the statement "$M$ computes a WPO"? (It may be worth noting here that [Montalbán](https://link.springer.com/article/10.1007%2Fs11083-007-9058-0) showed that the type of a computable WPO is always a computable ordinal.) As in, are they equal? Or at least, is there an inequality in one direction?


I've wondered about this some time but am bringing it up now but am not really qualified to answer it; I bring it up now in particular because discussion on [this answer](https://mathoverflow.net/a/349169/5583) made me realize other people may be wondering about it too and I thought it would be good to have one place where the question is properly stated.


(Although that one talks about $\Gamma\_0$, rather than the small Veblen ordinal, as being an ordinal related to Kruskal's tree theorem? I'm not sure what's going on here; it's not out of nowhere, they reference a paper explaining this, but I'm still not clear what's going on there. Nevermind, see Sylvain's comment about this.)


Two additional notes:


1. Like I said above, we presumably need additional conditions for this to work. These would likely be expressible as conditions on $o(X)$. Like, obviously $o(X)$ should be a power of $\omega$; or really I'd expect it would need to be of the form $\omega^{\omega^\alpha}$. Possibly it'd need to be an epsilon number, or something further along those lines. Possibly the whole question is dependent on some sort of implicit base theory, and how strong this sort of condition needs to be would depend on that.
2. One direction of this maybe seems like it should be easy, but I don't think it actually is. Specifically, it seems like the type $\le$ proof-theory direction ought to be easy, because if a theory can prove that $X$ is a WPO, it ought to be able to prove that $o(X)$ is a well order, right? Since any linearization of a WPO is a well-order. Except, I think this doesn't actually work, because while computable WPOs have computable types, there isn't (according to the paper on this linked above) any computable way to realize this mapping of computable WPOs to their types? (Do I have that right?) Too bad -- if even just that direction were true, that alone would be quite significant...


Anyway this may be an unreasonably difficult question but like I said, thought it would be good to have one place on the internet where this question is explicitly being asked, since I'm not aware of it appearing in the literature already! But, if these were indeed the same thing, or if there were even an inequality, it would be quite something, because it would mean that all the work on computing one could be ported over to the other. (I'd like to be able to port over proof-theoretic computations to computations of types, but I imagine many other people would like the reverse.) Thanks all!



Is there a relation between type (maximum linearization) of a computable WQO and the ordinal strength of a theory needed to prove it?
Let me show that for extensions $T\supseteq\mathsf{ACA}\_0$ the usual proof-theoretic ordinal $|T|\_{WO}$ coincide with $|T|\_{WPO}$ that is the suprema of $\mathsf{o}(X)$, for recursive wpo $X$, for which $T$ proves that $X$ is a wpo. Here $|T|\_{WO}$ is the suprema of order types $\mathsf{ot}(X)$ of recursive well-orderings $X$ for which $T$ proves that they are well-orderings.


Since any well-ordering $X$ is a wpo and $\mathsf{o}(X)=\mathsf{ot}(X)$ (and this is provable in $\mathsf{ACA}\_0$), we have $|T|\_{WO}\le |T|\_{WPO}$.


To establish that $|T|\_{WO}\ge |T|\_{WPO}$ we consider the rank $|T|\_{WF}$ that is the suprema of ranks $\mathsf{rk}(X)$ of well-founded recursive binary relations for which $T$ proves well-foundedness. Since in $\mathsf{ACA}\_0$ it is possible to prove that any well-founded relation is embeddable into a well-ordering (and for recursive well-founded relation the corresponding well-ordering is recursive as well), we have $|T|\_{WF}=|T|\_{WO}$. Thus we


Any anti-chain $Q$ in a partial order $X$ determines a downward-closed set $E(Q)=\{x\in X\mid \forall q\in Q(q\not<\_X x)\}$. This gives us the partial order $A^{\mathsf{fin}}(X)$ on all finite anti-chains in $X$:
$$Q\le\_{A^{\mathsf{fin}}(X)} P \iff E(Q)\subseteq E(P).$$
The function $E$ is an embedding of $A^{\mathsf{fin}}(X)$ into the inclusion order $C(X)$ on all downward-closed subsets of $X$. It is straightforward to prove that the following are equivalent:


1. $X$ is a wpo
2. $C(X)$ is well-founded
3. $A^{\mathsf{fin}}(X)$ is well-founded.


And it is easy to see if $X$ is a wpo, then $E$ is an isomorphism of $A^{\mathsf{fin}}(X)$ and $C(X)$. The proofs of both the facts here require only Ramsey theorem for pairs and could be proved in $\mathsf{ACA}\_0$. Fairly obviously, any linearization $L$ of $X$ is embeddable into $C(X)$ by the map $x\longmapsto \{y\in X\mid y<\_L x\}$. Thus for wpo's $X$ we have $\mathsf{o}(X)\le \mathsf{rk}(C(X))=\mathsf{rk}(A^{\mathsf{fin}})$. 


Notice that for recursive orders $X$ the order $A^{\mathsf{fin}}(X)$ is recursive as well. Thus, $|T|\_{WPO}\le |T|\_{WF}$.


