FOM: Why Friedman's result is a big improvement

[JOE SHIPMAN, BLOOMBERG/ SKILLMAN]

Franzen has argued that the Diophantine equations representing ZFC-provability
are already independent combinatorial statements of a simple type and questions
how much of an improvement Harvey's independent statements about finite trees
and insertion rules can be.  The obvious retort is that the tree theorems are
statements of independent mathematical interest.  But even if we ignore
"independent interest" and try to measure the complexity of the statements in
question, the finite tree results win by most measures.  They can be stated in
informal mathematics much more simply.  They can be stated in finite set theory
in much less space.  They can be stated in the language of arithmetic (0,1,+,*)
in much less space even if you allow constants for all natural numbers
(contrary to my earlier remarks) because the Godel coding of exponentiation
(which straightforwardly gets you finite set theory) is much simpler than the
sum (MDRP Diophantine coding plus ZFC->Turing machine coding).  The one way
they might be comparable is in L(0,1,2,...,+,*,^) with exponentiation and all
constants, when the extra ZFC-coding buys you a reduction from AE to A. - JS