This continues the previous post on A lower bound for .
Only recently I was made aware of a note dated November 22, 2001, posted on Harvey Friedman‘s page, “Lecture notes on enormous integers”. In section 8, Friedman recalls the definition of the function , the length of the longest possible sequence
from
with the property that for no
, the sequence
is a subsequence of
.
Friedman says that “A good upper bound for is work in progress”, and states (without proof):
Theorem.
, where
.
Here, are the functions of the Ackermann hierarchy (as defined in the previous post).
He also indicates a much larger lower bound for . We need some notation first: Let
. Use exponential notation to denote composition, so
.
Theorem. Let
. Then
.
He also states a result relating the rate of growth of the function to what logicians call subsystems of first-order arithmetic. A good reference for this topic is the book Metamathematics of First-order Arithmetic, by Hájek and Pudlák, available through Project Euclid.
There is a recent question on MathOverflow on this general topic.