Must non-constructive existential proofs use axioms of foundation or choice?

Question

I have been getting confused thinking about non-constructive proofs.

Several axioms of ZFC imply existence of a set with certain properties, and for each axiom except foundation, infinity, and choice, the set is uniquely characterized by the properties. If I'm not mistaken, the axiom of infinity is equivalent to the existence of $\omega$, which is unique. So it seems to me that a non-constructive proof that a set exists must use choice or foundation.

If there is a proof in (ZF - foundation) that a set with a certain properties exists, is the proof necessarily constructive?

If the answer if 'yes', I am curious about something else. In many branches of math there are non-constructive existential theorems requiring choice. But I can't think of similar examples requiring foundation.

Are there examples of existential theorems of ZF (let's say in branches of math other than set theory) that are non-constructive because the proof requires foundation?

Answer 1

If there is a proof in (ZF - foundation) that a set with a certain properties exists, is the proof necessarily constructive?

No, not at all. The nonconstructivity in ZFC doesn't come from the axiom of choice or the axiom of foundation. It comes from the underlying logic that is used. Even ZF without foundation is able to prove many theorems that are not constructively valid.

One specific example is the intermediate value theorem from calculus: if $f\colon [0,1] \to \mathbb{R}$ is continuous and $f(0)\cdot f(1) < 0$ then there is an $x \in [0,1]$ such that $f(x) = 0$. This theorem is well known to not be constructively valid: it can be shown that there is no way, given a procedure to compute $f$, to compute a root of $f$. However, the theorem can be proved in ZF with no reference to the axiom of choice or the axiom of foundation.

One actual source of nonconstructivity is the law of the excluded middle, which allows us to divide proofs into cases even when we cannot determine which of the cases holds. In constructive mathematics, the underlying logic is different, and does not allow that kind of nonconstructive reasoning (or other kinds of nonconstructive reasoning).

Answer 2

One specific example of a nonconstructive existence proof, where the nonconstructivity is due to a use of excluded middle, rather than using the axiom of choice or axiom of foundation:

We prove there exist irrational numbers $\alpha, \beta$ such that $\alpha^\beta$ is rational. Now, if $\sqrt{2}^{\sqrt{2}}$ is rational, then we use $\alpha := \sqrt{2}$, $\beta := \sqrt{2}$. Otherwise, $\sqrt{2}^{\sqrt{2}}$ is irrational, while $(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = (\sqrt{2})^2 = 2$ is rational; so $\alpha := \sqrt{2}^{\sqrt{2}}$, $\beta := \sqrt{2}$ will work.

Here we use the excluded middle in arguing that $\sqrt{2}^{\sqrt{2}}$ is either rational or irrational; therefore, this argument would be considered nonconstructive. (On the other hand, for example if we had an explicit constructive proof that $\sqrt{2}^{\sqrt{2}}$ is irrational, and used that, then the resulting argument would be considered constructive.)

(Credit goes to the Wikipedia page where I first saw this example - can't remember exactly where it was, but it was probably on one of the main pages related to constructive or intuitionistic logic.)

Answer 3

Although the other answers by Carl and Daniel are correct that LEM in the FOL underlying Z set theory is not constructive, that is actually nowhere near the biggest issue with Z. The reason is that from a predicative but not finitist point of view, LEM is acceptable and one might even accept $ℕ$ as a 'completed infinity', but $\def\pow{\mathcal{P}}$$\pow(ℕ)$ (i.e. the powerset of $ℕ$) is generally not accepted to be a sufficiently well-defined notion for quantification over $\pow(ℕ)$ to be well-defined.

In more detail, suppose you can justify that $Q(k)$ has a well-defined truth-value for every $k∈ℕ$. Then it is generally predicatively acceptable that $∀k{∈}ℕ\ ( \ Q(k) \ )$ has a well-defined truth-value too, because $ℕ$ is fixed. But $\pow(ℕ)$ may not be fixed (completed) from a predicative perspective. Thus quantification over $\pow(ℕ)$ does not enjoy the same privilege.

This is why ACA (see here and here) is considered predicative but the comprehension schema in full second-order arithmetic Z$_2$ is considered impredicative, since for a general property $R$ we may not be able to justify that $Q(k) ≡ ∀S{⊆}ℕ\ ( \ R(k,S) \ )$ has a well-defined truth-value for every $k∈ℕ$, which we need in order to justify that $\{ \ k : k∈ℕ ∧ Q(k) \ \}$ is a well-defined subset of $ℕ$ (i.e. has well-defined membership).

In-between ACA and Z$_2$ are ATR$_0$ and Π$^1_1$-CA$_0$. Most logicians consider ATR$_0$ still predicative. It is not so clear whether Π$^1_1$-CA$_0$ can be considered predicative, because it is roughly speaking equivalent to the extension of ATR$_0$ by a closure principle for justifiable monotonic operators on subsets of $ℕ$.

But see, Z set theory can trivially construct every subset of $ℕ$ that Z$_2$ can, and way more than that. Even if you change its underlying logic to intuitionistic logic, it does not reduce its impredicativity via its comprehension schema at all. So, no, even intuitionistic Z set theory cannot be considered 'constructive' in any truly meaningful sense, since it proves the existence of sets that can by no means be ever 'constructed'.

After all, the comprehension schema of Z set theory already yields 1-line existential proofs of a whole host of 'sets'. No need for any other axioms, not to say AC or Regularity!