[FOM] Re: 177:Strict Reverse Mathematics 1

[Harvey Friedman]

Reply to Newberry 6:37PM 6/11/03.

>Harvey,
>
>
>"However, the problem is: how do we prove that this finitely 
>branching tree exists?"
>
>The recursion formula for finite *binary* trees is the same as for Boolean
>lattices, but interpreted differently as to the meaning of '+'.
>
>                  T/n+1  =df=  T/n + T/n
>
>where, in this case, '+' means "hang a copy of the R.H. T/n  on 
>every branch-tip of
>the  L.H. T/n.
>
>The perfect infinite binary tree is the union over the countable 
>sequence generated by
>the recursiom.
>
>For NON-binary trees I have no suggestions.
>
>"how to introduce infinite objects."
>
>Recursively define a (countably) infinite sequence and then take the 
>union.  It worked for
>Cantor!
>

One has to get the particular finitely branching tree I need. 
Arbitrary recursive definitions - even if they have an elementary 
form such as quantifier free in some appropriate sense - go against 
the whole point of Strict Reverse Mathematics. Things like an 
arbitrary integer, or an arbitrary finite sequence of integers, are 
fine.