ZF+DC as the boundary of constructive mathematics

Question

This is mainly a request for references.

I seem to recall hearing somewhere that ZF+DC is "the boundary of constructive mathematics" in the sense that theorems not provable from ZF+DC are nonconstructive.

Can someone point me to a reference for a claim like this? (I may have seen the claim in Schecter's book on the foundations of analysis, but a quick skim didn't turn it up.)

(If my recollection is correct, and you'd like to shed some light on why ZF+DC provides a good theory of constructive mathematics, that would be great too.)

Secondarily, what's the primary reference for the fact that the Hahn-Banach theorem isn't constructive in the above sense, i.e. isn't provable in ZF+DC?

Answer 1

A closer look at Schechter turned up the following quote, which may well be what I had in mind:

"Dependent Choice, introduced in 6.28, is generally considered to be constructive. In fact, it is the strongest form of Choice that is accepted by most schools of constructivism" (14.76, p. 403).

Answer 2

The easy case for proving HB does not follow from DC is to combine:

1. Solovay, R. M., A model of set-theory in which every set of reals is Lebesgue measurable, Ann. Math. (2) 92, 1-56 (1970). ZBL0207.00905.

2. Foreman, Matthew; Wehrung, Friedrich, The Hahn-Banach theorem implies the existence of a non-Lebesgue measurable set, Fundam. Math. 138, No. 1, 13-19 (1991). ZBL0792.28005.

Since it's morning and I don't remember all the subtleties, you might also find an answer in the first theorem of the following paper, perhaps by combining it with further results, though:

3. Pincus, David; Solovay, Robert M., Definability of measures and ultrafilters, J. Symb. Log. 42, 179-190 (1977). ZBL0384.03030.