# Is the axiom of dependent choice constructive?

Page xvii of Schechter's Handbook of Analysis and its Foundation says that the Principle of Dependent Choice(DC) is constructive.

Is DC considered constructive? Different debaters may have different positions, but what are the reasons for those who argue that DC is constructive?

• This question and the answer by Bauer mathoverflow.net/questions/25664/… suggest that Dependent Choice can be considered constructive, but in practice the issue is complex because there are different ways of understanding exactly what constructive means. Jan 23, 2023 at 3:25
• @Frank It’s typo. I edited. Jan 23, 2023 at 3:28
• I don't know if "constructive" can be said of axioms. I thought it was said of existence proofs, where the existence of the object is proved by showing a construction for the object, as opposed to inferring the existence of the object via reductio ad absurdum. I thought "constructivists" required their mathematics to only contain objects that can actually be constructed. Jan 23, 2023 at 3:34
• @Frank It can be. For constructivists, constructions precede axioms, so an axiom is acceptable when there is an "intuitive" construction for what it asserts. There is some wiggle room in it, because justification of axioms is informal and intuitions vary, but the law of excluded middle and the axiom of choice for continuum are universally rejected by them, for example. On the other hand, according to nLab, "for a number of schools of constructive mathematics, dependent choice is considered an acceptable alternative to full AC". Jan 23, 2023 at 11:15
• What does "constructive" mean in this context? Jan 24, 2023 at 13:26

The Axiom of Dependent Choice (ADC) can be considered constructive (or perhaps more correctly, effective) as Schechter wrote, for the reason that it does not have any of the paradoxical consequences of the full Axiom of Choice, such as the Banach-Tarski paradox, or the existence of nonmeasurable sets. In a classical paper, Solovay constructed a model of ZF+ADC where all sets of real numbers are Lebesgue-measurable. Why then isn't all of mathematics done in the ZF+ADC framework? The answer is simply that too many useful mathematical tools depend on stronger forms of Choice. For example, the Hahn-Banach theorem is considered by many to be a tool of fundamental importance, and is used in applications such as mathematical physics. But the full Hahn-Banach theorem cannot be proved from ZF+ADC. The stronger foundational system ZFC can perhaps be viewed as epistemologically more risky than ZF+ADC, but has advantages that ZF+ADC doesn't possess. Mathematicians are beginning to get used to the idea that perhaps there isn't a single all-purpose foundation of mathematics.

Whether AC has counterintuitive/nonconstructive ramifications is a finely parsed question. In "Types, Sets, and Categories", John L. Bell says (pg. 43):

... to assert AC under the “formulas-as-monotypes” interpretation, is tantamount to asserting AC in [a specific form, there called "**"], so leading in turn to classical logic. This is in sharp contrast with AC under the “propositions-as-types” interpretation, where, as we have seen, its assertion is automatically correct and so has no nonconstructive consequences.

So, for example, there can be an initially constructivism-flavored set theory such that, if it has AC in it, this leads to the law of the excluded middle. Validating the LEM for infinite sets is the point of contention, here: all standard finite sets, including those accepted by intuitionistic/constructivist mathematics broadly, are well-orderable without any axiom floating overhead.

Before getting into that squarely, though, then, some comments about what "intuitive" is supposed to mean, here. An infamous quip goes, "The axiom of choice is obviously true, the well-ordering principle is obviously false, and who can say about Zorn's lemma?" (Zorn's lemma was not a lemma on Zorn's own conception of the principle, but a "law of thought" such as Cantor thought the well-ordering principle to be. At any rate, Zorn's lemma implies AC and/or the well-ordering principle.) Indeed, not only might one think that intuition supports AC, but that intuitions about the meaning of negation and disjunction operators in logic itself support the LEM. So what are intuitionists getting at, here?

I don't know the details for sure, but I do know that Brouwer styled himself as an inheritor of Immanuel Kant, with space-and-time lapsed to just-time as the intuitive basis for mathematics. So here, "intuition" has a fairly sharp meaning (Kant uses the word "Anschauung" for a sufficiently particular representation, whereas concepts are, on his account, sufficiently general). This plays into the issue of existence proofs like so: Kant also says that all existence propositions are synthetic, meaning grounded (if grounded) in intuition, or particular representation; to hold otherwise leads to the perfect islands of Anselm's paradise (whereby general/conceptual existence, or what Anselm called "existence in the understanding," is conflated with empirical reality, despite that empirical reality by the concept of the thing requires that its content be delivered empirically; one cannot define oneself as seeing something that one is not actually seeing).

So did Brouwer get his rejection of the LEM from Kant? I'm not sure, but it seems possible for Brouwer to have taken Kant's claim that the continuous physical world is "neither finite nor infinite" as such a rejection. And on the surface, finite and infinite are A and ~A; however, if this is where Brouwer got his denial of infinitary intuition from, I think he was misreading Kant. Kant doesn't reject the LEM for infinity; he is parsing "infinite" as a substantive opposite of finite, as the antifinite. This turns on his twofold definition of infinity:

The thesis might also have been unfairly demonstrated, by the introduction of an erroneous conception of the infinity of a given quantity. A quantity is infinite, if a greater than itself cannot possibly exist. The quantity is measured by the number of given units—which are taken as a standard—contained in it. Now no number can be the greatest, because one or more units can always be added. It follows that an infinite given quantity, consequently an infinite world (both as regards time and extension) is impossible. It is, therefore, limited in both respects. In this manner I might have conducted my proof; but the conception given in it does not agree with the true conception of an infinite whole. In this there is no representation of its quantity, it is not said how large it is; consequently its conception is not the conception of a maximum. We cogitate in it merely its relation to an arbitrarily assumed unit, in relation to which it is greater than any number. Now, just as the unit which is taken is greater or smaller, the infinite will be greater or smaller; but the infinity, which consists merely in the relation to this given unit, must remain always the same, although the absolute quantity of the whole is not thereby cognized.

The true (transcendental) conception of infinity is: that the successive synthesis of unity in the measurement of a given quantum can never be completed.

Now Kant either means to say that there are true and untrue concepts of infinity simpliciter, and the transcendental concept is the true one; or he means to say that there are true and untrue transcendental concepts of infinity, and he has taken himself to give the true one (but then there are also true non-transcendental definitions, perchance). His earlier assertion about infinity not being a number suggests the latter meaning; and so we can say that Kant differentiated the notion of a closed infinity (cannot be increased) from that of an open one (can always be increased).

At any rate, if Brouwer thought that Kant denied the LEM for statements about infinity, perhaps this is where he got his sense that intuitionism is in tension/conflict with the LEM. But I think there's more to it, and here is where we come to the issue of whether Dependent Choice is consonant with intuitionism/constructivism (or not!).

For another aspect of intuitionistic mathematics for infinite sets is a denial of the powerset axiom and an intuitive rejection of the well-ordering lemma. If I understand DC correctly, it says "merely" that countable subsequences of (possibly) uncountable sequences are well-orderable, but so not that the whole of an uncountable sequence is. (I might be misunderstanding the idea, though; it is said that DC implies the axiom of countable choice, which I would have to say was the same as DC except that we don't have subsequences in play, but it is only self-contained countable sequences that are well-orderable; I don't know if that's the exact distinction.) This jives with the quip from earlier, which says that the well-ordering principle is "obviously false," the "obvious" case being the uncountable enormity of the Continuum.

Note that this relativizes Brouwer's implied rejection of the LEM for statements about infinity; the neo-intuitionist, here, is able to allow that countable infinity is well-orderable, but not necessarily so for uncountable infinity. The alephs, for example, might be well-orderable, but then the intuitionist will be moved to say that the cardinality of the Continuum is not an aleph. (Indeed, there is the relatively undesirable possibility in play, here, that intuitionism generates a Continuum that is the size of a proper class.)

So, if DC doesn't imply that the Continuum is well-orderable, that's another way in which a version of a choice axiom can be more consonant with the sensibilities of intuitionists. If DC doesn't imply the LEM, or implies it only modulo extra assumptions that intuitionists do not make (or are not inclined to make), that would be the deeper reason for this consonance, then.

ADDENDUM: Miquey[19] offers a constructive proof of dependent choice in a given context. Herbelin[??] provides a way "to constructively prove the axiom of countable choice, the axiom of dependent choice, and a form of bar induction in ways that make each of them computationally compatible with classical logic." Rathjen[??] concerns "several forms of the axiom of choice that have been deemed constructive."