Is TREE provably total in analysis?

Question

Is Friedman's TREE-function provably total in second order arithmetic?

A simple definition of the TREE function can be found in an FOM post by Harvey Friedman.

Answer 1

The statement "for all $n$, TREE($n$) exists" is a direct consequence of Kruskal's theorem along with König's lemma. Both of those theorems are provable in second-order arithmetic, and the quoted statement is as well.

The papers by S. Simpson and by R. Smith in the book "Harvey Friedman's Research on the Foundations of Mathematics" have many proof details and references, although the material is technical.

To give a nontechnical summary: the provability of "for all $n$, TREE($n$) exists" from Kruskal's theorem and König's lemma is not much different from the way that the finite versions of Ramsey's theorem are provable from the infinite version of Ramsey's theorem along with König's lemma. This is by design: the definition of TREE($n$) was intentionally chosen to be a kind of finitistic analogue of Kruskal's theorem.

To say one more thing: The way that this kind of nonprovability result goes is by showing that some statement (like "for all $n$, TREE($n$) exists") implies some consistency or reflection statement for some strong theory. For example, Kruskal's theorem itself implies the well foundedness of $\Gamma_0$ and hence the consistency of $\mathsf{ATR}_0$ over $\mathsf{ACA}_0$.

In the end, however, all of these consistency results and reflection results are provable in full second-order arithmetic, because full second order arithmetic has such a high consistency strength. So results about unprovability in subsystems do not lead in any direct way to unprovability over full second-order arithmetic.

Indeed, the only natural result known to be expressible but not provable in second order arithmetic is Borel determinacy (this is due to Harvey Friedman also). As far as I know, no recognizable combinatorial theorem is expressible in second-order arithmetic but not provable in the full system - I would be very interested in an example of that kind...