[FOM] 271:Clarification of Smith Article

[Andreas Weiermann]

It might be of some general interest to see whether the lower bound in
H. Friedman's Theorem 2 (cited below) is larger 
than the Graham number holding the world record for
a natural number appearing in a mathematical proof.
Presumably such a lower bound can easily be shown 
(following Harvey's outline) when the number 6 is replaced by 
let's say 10.


Best,

Andreas Weiermann
> 
> In http://www.cs.nyu.edu/pipermail/fom/2006-March/010233.html I cited the
> following result (Theroem 2) from
> 
> R.L. Smith, The Consistency Strengths of Some Finite Forms of the Higman and
> Kruskal Theorems, in: Harvey Friedman's Research on the Foundations of
> Mathematics, Studies in Logic and the Foundations of Mathematics, volume
> 117, ed. Harrington, Morley, Scedrov, Simpson, pp. 119-136, 1985.
> 
> THEOREM 1. There exists n >= 1 such that the following holds. Let
> T_1,...,T_n be finite trees with vertices labeled from {1,...,6}, where each
> T_i has at most i vertices. There exists 1 <= i < j <= n such that T_i is
> inf preserving and label preserving embeddable into T_j.
> 
> THEOREM 2. Theorem 1 can be proved in strictly finite mathematics. However,
> any such proof in ACA_0 + Pi12-BI must use at least 2^[1000] symbols.
> 
> Here 2^[1000] is an exponential stack of 2's of height 1000.
>