FOM: polynomial v. combinatorial independence

[Neil Tennant]

I had mentioned a statement

(B)	Con(ZFC + existence of appropriate large cardinals)

in my discussion of Harvey Friedman's independence result concerning
his combinatorial claim about trees, a claim which I had labelled (A).

Torkel Franzen supposed (Mar 19 08:50 EST 1998) that my distinctions
of "provenance" also explained why I am "not equally impressed by an
equivalent of (B) in the form of a statement of the form 'the
Diophantine equation p(k1,..kn)=0 has no solution'."

All the metamathematical independent statements, like (B), are Pi_0_1
statements. Torkel is adverting to the fact that all Pi_0_1 statements
are known to be equivalent to some statement of the form

(B*)	(x_1)...(x_k)(~p(x_1,...,x_k)=q(x_1,...,x_k))

where p and q are polynomials in the variables x_1,...,x_k and k can
be chosen so as not to exceed 9.

Note that nothing is said about exponents and coefficients in these
polynomials, which could be gargantuan.  (B*) constitutes the merest
tweak of the form of (B) written in primitive notation. I invite
Torkel to give a recipe for writing down (B*) in primitive notation so
that it fills no more than a 100-page A4 exercise book in symbols of
readable size.

Friedman's (A), by contrast, is pretty natural, and is given by a much
more feasible recipe for primitive rendering.  Within the limits
already set by the results of G"odel and Davis-Matiyasevich, it is
difficult to imagine much in the way of further improvements of
independence results. Right now, large cardinal assumptions represent
pretty much the only known way of significantly increasing the
strength of ZFC. To have a method that assigns to any such strenthened
set-theoretic system a feasibly inscribable combinatorial principle
provably independent of that system is just about optimal, is it not?

Or is Torkel unwilling to be impressed by a result that gets from the
likes of gargantuan-polynomial (B*) to manageable (A), and by a method
applicable to further strengthenings of the base set theory from which
independence is established?

Neil Tennant