Sets in constructive mathematics

It is not completely clear how Bridges, Richman and Youchuan treated sets in their paper. Example is in the following lemma (Lemma 7 on p. 7):

Let $$U$$ and $$V$$ be (inhabited to mean $$\exists u \in U, \exists v \in V$$) sets of a Banach space such that $$U \cup V$$ is dense. Then, the following holds:

1. If $$u_0 \in U$$ and $$v_0 \in V$$, then $$\rho([u_0, v_0], \bar U \cap \bar V) = 0$$
2. $$\rho(x, \bar U \cap \bar V) = \rho(x, U) \wedge \rho(x, V)$$

...

To do this, choose $$w$$ in $$U \cup V$$ within ...

If a set $$X$$ is inhabited, then there is (at least) one point that can be constructed. How can other points be constructed?

The lemma has an existence hypothesis; it is this existence hypothesis that allows the proof to “choose” a point when necessary.

$\newcommand{\x}{\vec{x}}$Specifically, the lemma assumes that $U \cup V$ is dense. That says (by definition) that for every suitable $x$ and $\varepsilon$, there exists some point in $U \cup V$ within $\epsilon$ of $x$.

But then the logical rules for the existential quantifier tell us: if we’re trying to prove some goal, and we have established that there exists some object with some property, it suffices to prove the goal assuming that we have some specific object with that property.

Formally, this is the natural deduction rule that says: If $\Gamma,\, \varphi(\x, y) \vdash \psi(\x)$, then $\Gamma,\, \exists y. \varphi(\x, y)\vdash \psi(\x)$ (where $y$ is not free in $\Gamma$ or $\psi(\x)$). (Most other formalisations of constructive logic have some similar rule or axiom.) But in prose, it is often phrased as e.g. “We know there exists some $y$ such that […]. So, choose some such $y$; then …”

So the proof is not “constructing” some new point in the sense which — as you say — would be impossible in general. It is just choosing (for the purpose of the proof in question) points whose existence is guaranteed by the assumption that $U \cup V$ is dense.

• @ValerySaharov: in Lemma 7 of B–R–Y, they first (at each stage) take some point $w$ as provided by the density assumption on $U \cup V$ (this is directly a hypothesis of the lemma, there is no intermediate argument needed), and then depending on what $w$ is, they give specific choices of $u_n$, $v_n$. (This is at the top of p.8.) So each individual stage of the sequence is unproblematic. Getting from this to the whole sequence uses the principle of dependent choice, which some constructivists reject but others accept. Jul 27 '17 at 15:04
• Meanwhile, in Lemma 9 of Wang’s thesis, the step “Choosing $x_{n+1}$…” is justified by the existence result “Lemma 5 of [?]”, recalled in the preceding sentence. Since the citation reference is missing, we can’t see how it works — but it doesn’t seem at all surprising, since the statement of Lemma 9 has several hypotheses which give us some points, and allow us to construct or conclude the existence of more points (specifically, the hypotheses of Lemma 9 include the points $x_0$ and $y_0$, locatedness of $\Omega$, and the ambient Banach space operations). Jul 27 '17 at 15:16
• Because we know $w \in U \cup V$, and by definition, $U \cup V = \{ x\ |\ x \in U \lor x \in V\}$. Jul 27 '17 at 19:12
• @ValerySaharov: The union $[0,\frac{1}{2}] \cup [\frac{1}{2},1]$ is dense in the unit interval, as you say; what you can’t show constructively is that it’s equal to the unit interval, which is what would be equivalent to “every number in the interval is $\leq \frac{1}{2}$ or $\geq \frac{1}{2}$”. If you can establish $x \in [0,\frac{1}{2}] \cup [\frac{1}{2},1]$, then you do indeed get that either $x \leq \frac{1}{2}$ or $x \geq \frac{1}{2}$. Jul 27 '17 at 21:41

Suppose we know that there exists $x \in A$ such that $\phi(x)$, and we want to prove $\psi$. Then the elimination rule for existential quantifiers allows us to argue as follows:

We know that $\exists x \in A . \phi(x)$, and so we may assume to have $a \in A$ such that $\phi(a)$. [Insert argument using $a$ and the fact that $\phi(a)$ here.] Therefore $\psi$, as required.

There is a technical condition, namely that $a$ must not appear in $\psi$. This is precisely how we always use knowledge that something exists. Many authors use the word "choose", as follows:

We know that $\exists x \in A . \phi(x)$, and so choose $a \in A$ such that $\phi(a)$. [Insert argument using $a$ and the fact that $\phi(a)$ here.] Therefore $\psi$, as required.

This has nothing to do with choice! It is still just elimination of existential quantifiers, but the word "choose" confuses many into thinking we're applying the axiom of choice.

All of the above holds equally well classically and constructively. But people worry about constructive math, as if somehow there existence is more special, so let me address this as well. If we have the assumption $\exists x \in A . \phi(x)$ then we need not "construct" an element $a \in A$ such that $\phi(x)$. The assumption gives us some $a \in A$ such that $\phi(a)$. We do not know which $a$ it gives us, but it gives us one. We are thus allowed to use such an $a \in A$, keeping in mind that all we know about it is $\phi(a)$.

Let us apply this to density. Suppose you know that $U \cup V$ is dense in $A$. The definition of density is: for every $\epsilon > 0$ and $x \in A$ there exists $y \in U \cup V$ such that $d(x,y) < \epsilon$. So, given $x_0 \in A$ and $\epsilon_0 > 0$, we may conclude that there exists $y \in U \cup V$ such that $d(x_0, y) < \epsilon_0$. Therefore, we may say: there is $a \in U \cup V$ such that $d(x_0, a) < \epsilon_0$. There is no need to "construct" $a$. The fact that $a$ is there is precisely the existential assumption!

• @Andej: I don’t think your P.S. is quite fair — “passing as research-level” is determined only by not getting close-votes, and we are the sort of people who should have been casting those close-votes, if anyone. I would have voted for migration to math.se, but the overlapping close-vote reasons mean that questions usually end up getting just closed not migrated, so I prefer to answer it here instead. Why did you choose not to close-vote? Jul 27 '17 at 15:20
• I deleted the P.S. as it's already attracting -1 votes. I will just weep silently in the privacy of my own browser. Jul 27 '17 at 15:22
• And I did now vote to close. This question is not research-level. Jul 27 '17 at 15:23
• I pointed out the confusion with the axiom of choice because many people do get confused by that. In any case, is your question answered either by Peter or me? Jul 27 '17 at 15:24
• I think logic has always been regarded by most mathematicians as tricky: despite its being studied since antiquity, it was really only in the 20th century that it began to be mathematicized, and constructive logic is not something encountered in the usual curricula. Existence is existence, sure, but how an existential statement is deduced is more restricted in constructive logic than how it is in classical logic. Sep 21 '17 at 13:22