[FOM] Status of AC

[joeshipman@aol.com]

Friedman:

>Every Pi^1_4 sentence provable in ZFC is provable in ZF.

Solovay:

>If a Sigma^1_3 sentence follows from V=L it is a theorem of ZFC. This 
is best possible since "Every real
>is constructible" is Pi^1_3.


How do you show that choice is eliminable from proofs of Pi^1_4 
sentences? And how much of an expansion in proof length is involved in 
the elimination procedure?

It is remarkable how useful Choice is, considering how much of 
mathematics can be coded into sentences of type Pi^1_4 or lower. There 
are plenty of theorems which cannot be coded into second-order 
arithmetic at all; but can anyone identify a well-known theorem or open 
problem which CAN be coded into second-order arithmetic but not into a 
Pi^1_4 sentence?

Harvey's example is VERY far from what I would call a "well-known 
theorem". I would hazard a guess that the Sigma^1_4 sentence he 
describes (which is provable in ZFC but not in ZF) cannot actually be 
formalized in second-order-arithmetic in fewer than 10,000 symbols (I'm 
talking about the length of the sentence, not of its proof!).

-- JS