Every non-increasing sequence of polynomial towers stabilizes -- Finitary proof

In this question we are concerned only with positive integers $\mathbb N$ and other finitary objects that can be encoded using integers. A term function means a total computable function $\mathbb N^n\to\mathbb N$ with one or multiple arguments. Letters $m,n,k$ range over $\mathbb N$. Letters $f,g$ range over functions.

A term sequence of functions $f_m(n)$ is just a different name for two-argument total computable function $f(m,n)$. An element of a sequence is a one-argument function obtained by fixing the first argument, e.g. $f_2(n)=f(2,n)$.

We say that a one-argument function is a polynomial tower iff it can be constructed in a finite number of steps using the following 3 rules:

• The constant function $f(n)=1$ is a polynomial tower.
• If $f(n)$ is a polynomial tower, then $n^{f(n)}$ is a polynomial tower.
• If $f(n)$ and $g(n)$ are polynomial towers, then $f(n)+g(n)$ is a polynomial tower.

Obviously, all polynomial towers are total computable functions. Some examples are $5,n^3+7n+2, n^{n^{n^5+10n}+n^3+1}+2n^{n^2+5}+5n^7+2n+3$.

A function $f(n)$ is dominated by a function $g(n)$ iff $f(n)<g(n)$ for all sufficiently large $n$; formally $\exists k\,\forall n\ge k,f(n)<g(n)$.

A sequence of functions $f_m(n)$ is non-increasing iff none of its elements is dominated by the next element.

A sequence of functions $f_m(n)$ stabilizes iff all its elements are the same for all sufficiently large $m$; formally $\exists k\,\forall m\ge k\,\forall n,f_m(n)=f_k(n)$.

Proposition. Every non-increasing sequence of polynomial towers stabilizes.

Apparently, the proposition can be formalized as a purely arithmetical statement. I'm interested in a proof of this proposition that would not appeal to infinite sets in any way. For example, it should not use arbitrary infinite sequences or real numbers, except computable ones that can be represented by a corresponding algorithm, and it should not borrow any results from analysis, except those that can be proved in constructive analysis. We could use a theory of hereditary finite sets with natural numbers, computable functions, or any other finitary objects as urelements (they can be encoded as hereditary finite sets anyways).

A relatively easy infinitary proof can be outlined as follows. Observe, that a shape of a polynomial tower written as an expression resembles the Cantor normal form of some ordinal below $\varepsilon_0$. Indeed, there a bijection between them (obtained by replacing $n$ with $\omega$ or vice versa), and it's not difficult to see that this bijection preserves order (where polynomial towers are ordered by domination, and ordinals ordered, as usual, by $\in$). So, the set of polynomial towers is order isomorphic to $\varepsilon_0$. Now, because every ordinal is well-ordered, we see that the set of polynomial towers is also well-ordered -- in other words, there is no infinite decreasing sequence of them. So, every infinite non-increasing sequence must stabilize.

Of course, this proof uses many terms and lemmas that usually introduced and proved in terms of infinite sets. E.g. we need to define $\omega$ and $\varepsilon_0$, define well-order, bijection and isomorphism, prove that every ordinal below $\varepsilon_0$ has a unique non-recursive Cantor normal form -- all that is usually done using infinite sets. I'm not a finitist in any way, but it feels that all that could be avoided for purposes of proving this relatively simple arithmetic statement (of course, not as simple if you want to write in completely formalized form -- but we do not want that). It sometimes even looks obvious, if I think of it long enough :)

Every step either decreases a number of steps remaining (if you already below $n$), or requires you to make a decison about how many steps remaining (when you go from $n$ to some constant below), or requires you to make a decision about how many times more you can make a decision that you will be able to review later (when you go from $n^2$ below), or about number of decisions about number of decisions about number of decisions ..., or about number of clauses in the previous ellipsis, and so on towards an inevitable end.

But I hope to find a finitary proof can rigorously capture the idea from the previous paragraph, perhaps by constructing a chain of applications of the induction principle, and then using some meta-reasoning by induction that this chain can be made arbitrarily long. I heard (but never seen a proof of it) that the proposition from my question cannot be proved from axioms of Peano arithmetic alone, so we are free to invoke new meta-axioms like "everything provable from Peano axioms is true", or "everything provable from Peano axioms plus the previous axiom is true", and so on. I consider this as a valid finitary reasoning.

Solution 1:

It is not possible to give a finitary proof of this fact.

Consider, for instance, the statement that all Goodstein sequences terminate. This is an arithmetic claim, it is independent of $\mathsf{PA}$, and it is equivalent to the claim that some (very specific) computable non-increasing sequences of polynomial towers stabilize. Instead of Goodstein sequences, you could use just as well Hercules-Hydra games, or a variety of other combinatorial statements independent of $\mathsf{PA}$ whose proof essentially goes by invoking the well-foundedness of $\epsilon_0$.

(Typical combinatorial statements independent of $\mathsf{PA}$ are $\Pi^0_2$ in complexity, that is, they are equivalent to the claim that some partial computable function is actually total. Quite a few of them only require transfinite induction up to $\epsilon_0$ to check this claim, and usually this ends up being equivalent to checking that a computable non-increasing sequences of polynomial towers stabilize, though I do not recall seeing this explicitly pointed out in the literature.)