[FOM] On the arithmetical conservativity of ZFC + GCH over ZF
dmytro at mit.edu
Sun May 24 22:28:25 EDT 2015
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.
More information about the FOM