[FOM] eliminating AC for statements of analysis

[Ali Enayat]

This is a response to following two questions posed by Paul Levy in
his recent posting (March 31):

Question 1. Do ZFC and ZF + dependent choice have the same
second-order consequences?

Answer: I will take DC (dependent choice) here to mean "dependent
choice of countable length" (since the more general formulation which
allows arbitrary ordinal lengths is equivalent to AC within ZF).

The answer to Question (1) is positive; the two ideas at work are:
(a) the use of a forcing argument to add a well-ordering of the reals
without adding any new reals (to a countable model of ZF + DC), and
(b) the use of the model HOD(W), where W is a well-ordering of the
reals within the generic extension in (a).

This above does not seem to have been previously explicitly noted, but
something close to it was credited to Kripke and Silver in the
1969-paper of Platek (Eliminating the Continuum Hypothesis; Journal of
Symbolic Logic,  34, pp. 219-225).

Question 2. Do ZFC + Martin's axiom at aleph_1 and ZFC have the same
second-order consequences?

Here I take Martin's axiom at aleph_1 to mean "if P is a ccc notion of
forcing, and D is a collection of cardinality at most aleph_1 of dense
subsets of P, then there is a filter G that meets each element of D".

The answer to Question 2 is in the negative. Martin's axiom at aleph_1
implies that there is a nonconstructible real, essentially because ZFC
can prove that there are at most aleph_1 constructible reals, and
therefore MA at aleph_1 implies that there is a non-constructible real
number.

It is well-known that the existence of a non-constructible real can be
expressed as a sentence of second order arithmetic.

Best regards,

Ali Enayat