[FOM] What ZFC knows about analysis but ZF does not

[Ali Enayat]

This is a reply to a query of Joe Shipman (May 24, 2015), who has asked:

>>What is the lowest possible quantifier-complexity for a sentence of analysis which is a theorem of ZF + DC but not of ZF?

The answer is: Pi^1_5. Here is a brief explanation:

Using (a) Shoenfield absoluteness theorem, and (b) the fact that L(X)
is a model of ZFC when X is a real (both provably in ZF), and (c) the
completeness theorem for first order logic, one can show that ZFC is
conservative over ZF for Pi^1_4 sentences of analysis. This must be
known to the cognoscenti but I have not seen it recorded anywhere.

(2)  On the other hand, based on a classical theorem of Feferman and
Levy (see Remark VII.6.3 of Simpson's Subsystems of Second Order
Arithmetic) there is an instance S of Sigma^1_3-Axiom of Choice that
is unprovable in ZF (and yet S is provable in ZF + DC).  Note that
each such instance S can be written as a Pi^1_5 statement.


Best regards,

Ali Enayat