[FOM] definition of N without quantifying over infinite sets

[friedman@math.ohio-state.edu]

Forster wrote:

> The significance of FFF - Friedman's Finite
> Form of Kruskl's theorem is of course that it is a fct about N probable
> only by reasoning about infinite sets.
>
> When explaining this to my students I of course have to anticipate that
> the inductive definition of N involves quantifying over ininite sets -
>...

FFF has much stronger properties than indicated.

FFF is provable only by reasoning about uncountably many infinite sets -
specifically what is normally called impredicativity.

In particular, the use of infinite sets for FFF is not removable in the
same way that simply regarding N as a predicate removes use of infinite
sets. In fact, the use of infinite sets for FFF is not even removeable
using predicates defined by natural number recursion (along with
quantification over natural numbers). The use of predicates defined by
natural number recursion (along with quantification over natural numbers)
is enough to prove, e.g., the Paris/Harrington Ramsey theorem.

For state of the art FFFs see my paper in the Feferfest volume dedicated
to Solomon Feferman.

Harvey Friedman