As far as I know, the TREE function has no particular relationship to the busy beaver functions. The TREE function is computable, whereas the busy beaver functions are not.
I wonder how TREE(3) compares to Loader’s number. If I understand correctly, if Kruskal’s tree theorem can be proved in the calculus of constructions using a reasonable number of symbols (where 3^^^3 counts as a reasonable number, but TREE(3) does not), then Loader’s number is much larger.
Edit: Wikipedia states that Friedman’s special cases of Kruskal’s tree theorem can “easily” be proved in second-order arithmetic, which can be expressed in the calculus of constructions. I’m pretty sure this means that the TREE function can be written in the calculus of constructions using a reasonable number of symbols, meaning that Loader’s number is much larger than TREE(n) for any reasonable value of n.
As far as I know, the TREE function has no particular relationship to the busy beaver functions. The TREE function is computable, whereas the busy beaver functions are not.
I wonder how TREE(3) compares to Loader’s number. If I understand correctly, if Kruskal’s tree theorem can be proved in the calculus of constructions using a reasonable number of symbols (where 3^^^3 counts as a reasonable number, but TREE(3) does not), then Loader’s number is much larger.
Edit: Wikipedia states that Friedman’s special cases of Kruskal’s tree theorem can “easily” be proved in second-order arithmetic, which can be expressed in the calculus of constructions. I’m pretty sure this means that the TREE function can be written in the calculus of constructions using a reasonable number of symbols, meaning that Loader’s number is much larger than TREE(n) for any reasonable value of n.