[FOM] Status of AC

[Harvey Friedman]

On 3/1/06 9:39 PM, "joeshipman at aol.com" <joeshipman at aol.com> wrote:

> Nguyen:
> 
>> I have a question: what is the current status of AC among
> mathematicians and
>> philosophers of mathematics?
> 
> For practically all the most important mathematical questions, the use
> of AC is eliminable, because of metatheorems like Shoenfield's
> Absoluteness Theorem, which ensures that AC can be eliminated from the
> proof of any statement of logical type no higher than Sigma^1_2 or
> Pi^1_2. 

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

If my memory is correct, many years ago an example of a Sigma^1_4 sentence
provable in ZFC but not in ZF was given.

I think it goes something like this.

1. There is a model of ZF with infinitely many c-degrees, but no infinite
sequence of c-degress. c-degrees are the degrees of constructibility of
sugbsets of omega.

2. ZFC refutes this.

3. In particular, ZFC proves the negation of the following:

i. For all n there exists n distinct c-degrees; and
ii. There is no infinite sequence of distinct c-degrees.

Note that i is of the form

(forall n)(therexists x)(forall y)(therexists z).

Note that ii is Pi^1_3.

3. So the statement that ZFC proves the negation of is (somewhat better
than) Pi^1_4. Hence ZFC proves a Sigma^1_4 sentence that ZF doesn't.

Again if my memory is correct, in the old days people had given an example
of a 

(therexists n)(forall x)(therexists y)(forall z)

statement provable in ZFC but not in ZF.

Harvey Friedman