FOM: 23-symbol formulas

[Matthew Frank]

Dear Prof. Friedman,

Now that I see better where this particular program is going, I'm not so
convinced that everything will turn out to be independent of the measure
of simplicity.

If we start with EFA or with Robinson's theory Q and add to it the
*shortest* formulas (with schemes) that are independent of it, then the
14-symbol induction scheme (A(0) & (forall x)(A(x) implies A(S(x)))
implies A(x) will come pretty quickly.

If instead we add the formulas *with the fewest occurences of schematic
letters* that are independent of it, then we will add "definable van der
Waerden's theorem" first:

for any definable subset of the integers, either it or its complement
contains arbitrarily long arithemetic sequences, i.e.

[ (forall n)(exists a)(exists b)(forall c)(forall d)
     c + d = n -> A(a + (sb)*c) ] or
[ (forall n)(exists a)(exists b)(forall c)(forall d)
     c + d = n -> not A(a + (sb)*c) ]

I would find it very strange if this turned out to be equivalent to
standard induction, so I suspect that this change of simplicity-measure
would affect the resulting theory.

(There is a hopefully-small problem here:  van der Waerden's theorem is
certainly independent of Q, but I don't know whether it's independent of
EFA.  If it is provable in EFA, you probably know some other examples of
formulas with only two or three occurrences of schematic letters which are
independent.)

Generally I don't have the same gut feeling of the inevitability of Peano
arithmetic that you (and almost everyone else) seem to have.

Sincerely,

Matt Frank

P.S.  I enjoyed your 20-symbol open question a lot.