Let me summarize what I think I understand about constructivism:

"Constructive mathematics" is generally understood to mean a variety of theories formulated in intuitionist logic (i.e., not assuming the law of excluded middle, $\neg\neg A\Rightarrow A$ (LEM)) so that, broadly speaking, in order to prove $A \lor B$ one must prove either $A$ or $B$ ("disjunction property") and, in order to prove $\exists x.A(x)$ one must "construct" some $x$ and prove $A(x)$ for it ("existential property"). There are a number of systems of constructive mathematics, and variations on the requirements (I don't claim to know the details), but, as far as I understand it, all of them operate in the absence of the LEM which is considered one of, if not "the", root cause of non-constructivism. So constructive mathematics in this sense represents a fairly radical departure from classical mathematics, as the abandonment of the LEM represents a considerable break from accustomed practice; the upside, of course, is that a constructive proof will provide some benefits that a classical proof will not (e.g., extracting algorithms from proofs or something of the sort).

(I hope I didn't write too much nonsense here. Onward to $\mathsf{ZF}$.)

On the other hand, consider $\mathsf{ZF}$, i.e. Zermelo-Fraenkel set theory without the axiom of choice, formulated in classical logic. This also represents a departure from the more habitual $\mathsf{ZFC}$, although not as radical as the abandonment of the LEM. Some of the differences (with classical $\mathsf{ZFC}$), however, are vaguely of the same flavour: e.g., in (some varieties of) constructive mathematics one cannot prove the existence of discontinuous real functions, while in $\mathsf{ZF}$ one cannot prove the existence of non-measurable real functions; in constructive mathematics, the powerset of a finite set might fail to be finite, while in $\mathsf{ZF}$ the powerset of a well-orderable set might fail to be well-orderable; in both cases, one need be careful about what "finite" means (although the subtleties are considerable greater in constructive mathematics as in $\mathsf{ZF}$). This leads me to wonder whether there is a pattern of similarity.

Very often, we ("we" being classical mathematicians) say that we cannot exhibit some object because its construction requires the axiom of choice: e.g., I cannot exhibit a basis of $\mathbb{R}$ as a $\mathbb{Q}$-vector space or a non-principal ultrafilter on $\mathbb{N}$ or this kind of things.

But conversely, we will say that we can exhibit a bijection between $X$ and $Y$ given injections $X\to Y$ and $Y\to X$, because the proof of the Schröder-Bernstein theorem does not use the axiom of choice (even though it is probably not constructive); and, while hardline constructive mathematicians will disagree, I think most classical mathematicians will agree that it does, indeed, "construct" a bijection. Similarly, this paper, which shows in $\mathsf{ZF}$ that if there is a bijection between $n\times X$ and $n\times Y$ (where $n$ is a natural number) then there is one between $X$ and $Y$ does it by "exhibiting" a kind of algorithm which it claims is somehow canonical ("pan galactic division"). This is all reminiscent of the ideas of constructivism, even though it is not fully constructive.

(This is far too long, but I feel it is necessary to illustrate where I'm getting at.)

All of the above leads me to ask whether the similarity/analogy between $\mathsf{ZF}$ and constructive mathematics can be made precise. Or, a little less vaguely:

Question(s): Is there some well-defined sense in which $\mathsf{ZF}$ (in classical logic, but as opposed to $\mathsf{ZFC}$) can be said to be "somewhat constructive"? E.g., does it satisfy some very weak version of the existential property? Can we formalize the intuitive idea that proving the existence of an object in the absence of Choice "exhibits" the object in a stronger sense than proving its existence in $\mathsf{ZFC}$ (as the case of Schröder-Bernstein illustrates)?

A followup or related question might be whether there exist theories defined in classical logic that have an even stronger "constructive flavour" than $\mathsf{ZF}$, i.e., if the above question makes sense, that are "fairly constructive" without going all the way to abandoning the LEM.

Additional comments: One (to me) confusing fact is that constructive theories often incorporate some variant of the axiom of choice (see, e.g., here); the relation between these constructive axioms of choice and the axiom of choice from $\mathsf{ZFC}$ (which, as I explain above, seems to be anti-constructive) is unclear to me: so maybe I'm missing a big part of the picture. And at the other extreme, $V=L$, which seems to be a kind of super axiom of choice, makes it possible to "exhibit" some things which could not be exhibited without it, e.g., a well-ordering of $\mathbb{R}$ (or just about anything: take the $<_L$-least element such that <blah blah blah>).

  • $\begingroup$ In the finite power set, you can talk about Dedekind-finite, and then the power set of a Dedekind-finite set might not be Dedekind-finite if you're only assuming ZF. $\endgroup$
    – Asaf Karagila
    Apr 13, 2018 at 10:44
  • 3
    $\begingroup$ Levy has proved a weak form of the existential property for $ZF$ and $\Pi_2$ sentences in this paper sciencedirect.com/science/article/pii/0020025569900115 $\endgroup$ Apr 13, 2018 at 11:53
  • 1
    $\begingroup$ Very interesting question! I believe that Rodrigo's answer settles the main question. Let me just turn to two the asides. A further advantage of constructive proofs is their wider applicability. For instance, any intuitionistic theorem entails a "parameter-dependent version". For instance, the intermediate value theorem in its usual formulation can't be proven intuitionistically, which seems weird on first sight. But if it could, then it would entail that zeros of continuous families of continuous functions can be picked continuously, which is patently false. $\endgroup$ Apr 14, 2018 at 10:48
  • $\begingroup$ Secondly, it's true that some flavors of constructive mathematics accept some forms choice. The full axiom of choice is never adopted in set-theoretic constructive schools, since it entails the law of excluded middle by Diaconescu's theorem. But there are interesting models of intuitionistic logic where countable choice and even dependent choice hold, for instance the effective topos. The situation is different with type-theory based schools of constructivity, where a naive rendition of full choice is trivially provable. There you need "truncation" to formulate nontrivial versions. $\endgroup$ Apr 14, 2018 at 11:05
  • 2
    $\begingroup$ In addition to @RodrigoFreire's nice answer, there is a double negation translation from ZF to IZF, but not from ZFC to IZF. (IZF is basically ZF without LEM. Considering IZF+Choice isn't very useful, as IZF+Choice proves LEM and hence ZFC.) That is, usage of the law of excluded middle can always be mechanically eliminated from any ZF-proof (at the expense of introducing lots of double negations in the formulation of the statement proven). For ZFC this is not the case. In this sense ZF is much closer to being constructive than ZFC. $\endgroup$ Jan 22, 2021 at 3:39

1 Answer 1


As I have said in a comment, Levy proves a weak form of the existential property for $ZF$ and $\Pi_2$ sentences. He also proves that his results are best possible. Let me state a simple fact that is how I like to think about this existential property. If $ZF$ proves a $\Pi_2$ sentence $\forall x\exists y A$ then $ZF$ proves that $\forall x\exists y\in L(x); A$. That is, for every $\Pi_2$ existential $ZF$-theorem there is a relatively constructible witness. This is easy to prove.

  • 5
    $\begingroup$ Having had the pleasure of knowing Azriel in person, I can testify that his results are indeed the best. $\endgroup$
    – Asaf Karagila
    Apr 13, 2018 at 14:36

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.