[FOM] On the arithmetical conservativity of ZFC + GCH over ZF

[Dmytro Taranovsky]

On 05/24/2015 01:00 AM, Joe Shipman wrote:
> This almost completely answers my earlier question. What remains of it is the following:
>
> What is the lowest possible quantifier-complexity for a sentence of analysis which is a theorem of ZF+DC but not of ZF?

The lowest complexity level is Sigma^1_4.  Here is an example of a 
Sigma^1_4 statement provable in ZF+DC but not ZF:
omega_1 != omega_omega^L.

This is expressible as a Sigma^1_4 statement:
thereis real number X (X codes omega_omega^L  or  X is a positive 
integer and no real number codes omega_X^L).

Note that without countable choice one cannot always absorb quantifiers 
over integers into quantifiers over real numbers, so the above statement 
is not Sigma^1_3 in ZF.

By contrast, ZF+DC is Pi^1_4 conservative over ZF (see Simpson's 
"Subsystems of Second Order Arithmetic" for related conservation 
results).  Also, even  ZFC + thereis X in R V=L[X]  is Pi^1_4 
conservative over ZF.

Sincerely,
Dmytro Taranovsky