[FOM] Eliminating AC [from statements of analysis]

[Ali Enayat]

This is a reply to Paul Levy's posting (March 27), who asked whether
the conservativity of ZFC over ZF for arithmetical sentences holds
also for sentences of analysis (aka second order number theory).

1. The answer to Levy's question is in the negative; for example, ZFC
can prove that the so-called full "choice scheme" holds in analysis;
but it has been known (since the work of Feferman and (Azriel) Levy in
the 1960's) that there are models of ZF that `believe' that the choice
schema fails in analysis; see Remark VII.6.3 (p.295) of Simpson's text
on Subsystems of Second Order Arithmetic.

2. (Paul) Levy had also asked whether ZF + CH is conservative over ZF
for statements of analysis (of course in the choice-less setting CH
stands for "the reals can be injected into every uncountable subset of
the reals").  I do not know the answer to this question; hopefully
someone reading this note can enlighten us. However:

3. ZFC + CH is conservative over ZFC for statements of analysis. This
follows from coupling the completeness theorem for first order logic
with the well-known fact that every countable model M of ZFC has a
generic extension N such that:

(a) CH holds in N, and

(b) N has the same reals as M (hence the truth-value of statements of
analysis does not change in the passage between M and N).

The notion of forcing at work is the set of countable injective
partial functions from omega_1 into the reals (in the sense of M),
ordered under (reverse) inclusion; see, e.g, Kunen's text on set
theory (Theorem 8.3, p.227) for the forcing argument, however, note
that expositions of forcing--Kunen's included--state their theorems in
terms of countable *transitive* models, but  the assumption of
transitivity can be dropped in such arguments by taking a detour
through  Boolean-valued models.

4. In contrast to (1), by coupling two venerable classical theorems
(Gödel's theorem that GCH and AC both hold in the constructible
universe, with Shoenfield's absoluteness theorem ) one obtains: if a
sentence  S of  analysis is of sufficiently low quantifier complexity,
and ZFC + GCH proves S, then ZF already proves S (when S is written in
normal form, it should be of the form "there exists f such that for
all g ...", where f and g range over reals, and the matrix ...
involves no quantification over reals).

Best regards,

Ali Enayat