Is there a constructive well-ordering on the set of finite rooted trees?

Question

My motivation to this question is to quantify whether or not Gentzen's consistency proof of Peano arithmetic could be considered acceptable under a constructive framework.

I admit that in some sense this is not a well-defined question, as "constructive" can have a variety of meanings, so for the purposes of this question, take "constructive" to mean that we are either working under a common constructive framework (IZF, IZF + CT, MLTT, etc...), or are simply going from possibly informal constructive principles, such as Brouwer's intuitionism that at least some constructivists would find acceptable.

Answer 1

Suppose our underlying logic is such that we do not assume LEM for statements whose truth-value is uncomputable. But suppose that we accept inductive constructions for natural numbers, and we have higher-order types. I shall also write "$x_k$" for "$x(k)$" where $x$ is a sequence and $k$ is a natural number.

Call a type $S$ well-ordered under $<$ iff every sequence from $S$ has a minimum under $<$. $ \def\nn{\mathbb{N}} \def\then{\mathrel{?}} $

We can then construct and prove a well-ordering on finite (rooted) trees (which in ZFC would have order-type $ε_0$) as follows.

First we prove a lemma:

Given any $S$ that is well-ordered under $\le$, the type $T$ of (non-strict) $\le$-decreasing sequences from $S$ is well-ordered under lexicographic order.

Proof:

Take any sequence $f$ from $T$. Namely, $f_0,f_1,f_2,\cdots$ are $\le$-decreasing sequences from $S$.

Let $g = \Big( \nn\ n \mapsto \min\big( \nn\ k \mapsto \forall x\in\nn_{<n}\ ( f_k(x) = g(x) ) \then f_k(n) : g(0) \big) \Big)$.   [C++/Java syntax]

[By induction, given $f$ and $\le$ on $S$ and $\min$ on $(\nn \to S)$ we can compute each item of $g$.]

Then $g$ is a sequence from $S$, and hence let $m = \min(g)$ and $c \in \nn$ such that $g(c) = m$.

Also $g$ is $\le$-decreasing, and hence $g(n) = m$ for every $n \in \nn_{\ge c}$.

Let $d \in \nn$ such that $f_d(x) = g(x)$ for every $x \in \nn_{\le c}$, which exists by induction.

Then by definition of $g$ and induction, $f_d(x) = g(x)$ for every $x \in \nn_{>c}$, and hence $g = f_d \in T$.

Finally by one more induction, $g \le_{lex} f_k$ for every $k \in \nn$.

I will leave you to fill in the details.

Now define the ordering of finite trees inductively. All trees of depth at most $0$ are equal. Compare two trees of depth $k$ by first sorting their sequences of subtrees in decreasing order (which is valid because their subtrees have depth less than $k$) then comparing them lexicographically. By the lemma and induction, the resulting comparison is a well-ordering on the trees of depth $k$. And compare two trees of different depth by their depth.

We can then easily prove that the resulting comparison is a total-ordering on the finite trees. And then we can prove that it is a well-ordering on the finite trees, since for every sequence $f$ of trees we can construct $g = ( \nn\ n \mapsto n=0 \then f(0) : \min(g(n-1),f(n)) )$ inductively, which then is a decreasing sequence of trees, whose depths are eventually constant at some $k \in \nn$, from which point the sequence has a minimum by the above argument.

---

Of course, first-order PA is not strong enough to express the above proof, since it implies Con(PA). However, another way in which the well-ordering of $ε_0$ is constructive is that PA can construct the above-defined ordering and also prove each instance of the usage of the lemma in the above proof, and hence can prove that the ordering is a well-ordering on trees of depth at most $k$, for each fixed meta-natural $k$.