[FOM] FFF

[Harvey Friedman]

On 12/30/03 9:41 AM, "Thomas Forster" <T.Forster at dpmms.cam.ac.uk> wrote:

> 
> `FFF' is the TLA for Friedman's Finite Form of Kruskal's
> tree theorem (trees over a WQO)
> 
>  I'm steeling myself to lecture WQO theory next term, and
> i discover in my notes the bold assertion that FFF is the
> earliest example of a simple arithmetical assertion not provable
> in (for example) PA - that is  **mathematically natural**
> 
>  This is true isn't it?  Or have my ageing neurons let another
> piece of history slip through their grasp?
> 
>      Thomas
> 
> 

Some comments.

1. Usually, Paris Harrington Ramsey Theorem is quoted as the earliest
example for PA. 

2. However, for extensions of PA such as formalizations of predicativity
(see Feferman), or the system ATR_0 from reverse mathematics, it is the
earliest example. 

3. In fact, FFF is the earliest example even for ACA (arithmetic
comprehension axiom with full induction). Jazzing up Paris Harrington to
handle ACA does not work too well, and in any case, this jazzing up probably
wasn't done earlier than FFF (and may not be published).

4. Moreover, Kruskal's theorem itself and variants were the earliest
semi-arithmetic examples, too (i.e., of 2,3). By semi-arithmetic, I mean
Pi-1-1, which is arithmetic with a free function (or set) variable.

5. The state of the art concerning FFF and related matters can be found in

H. Friedman, Internal finite tree embeddings, in: Reflections on the
Foundations of Mathematics, Lecture Notes in Logic 15, ASL, 2002, pp. 60-91.

and also by looking at work of Andreas Weiermann.

Harvey Friedman