[FOM] Status of AC
joeshipman at aol.com
Thu Mar 2 14:15:57 EST 2006
>Every Pi^1_4 sentence provable in ZFC is provable in ZF.
>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
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!).
More information about the FOM