Confusion about disjunction in constructive logic

Question

I just realized I probably totally misunderstand the interpretation of disjunction in constructive logic. My confusion comes from the picture below.

Definition. Let $\mathcal E$ be an elementary topos and $X$ an object. For $U\subset X$, $U$ is said to be an intrinsic open if $\mathcal E$ satisfies $$\forall x,y\in X \; x\in U\implies (x\neq y\vee y\in U).$$

Here's an illustration of this definition.

(Here $\neg \left\{ x \right\}= \left\{ y\in X\mid y\neq x\right\} $ and $\neg\neg \left\{ x \right\}= \left\{ y\in X\mid \neg(y\neq x) \right\}$.)

I find this picture confusing; to me, it seems the disjunction $$x\neq y\vee y\in U$$ should be interpreted as follows:

• $x\neq y$, i.e $x,y$ are distinguishable.

or

• $x\neq y$ is not known, and in this case, $y\in U$.

Thus, the white zone should also be within $U$, since it's also inhabited by points $y$ for which we don't know that $x\neq y$.

---

What is my mistake, and why is the picture above correct?

Answer 1

Elaborating on my comment, in general for understanding constructive logic I usually recommend thinking in terms of the BHK interpretation. (Look to the Curry-Howard correspondence for more precision and extensions. Personally, as a programmer, I find it more meaningful than BHK on its own.)

Under the BHK interpretation, the whole definition of intrinsic open is a $U \subset X$ for which we have a function that takes two elements of $X$, $x$ and $y$, a proof that $x \in U$, and produces either a proof that $x \neq y$ or a proof that $y \in U$. In Agda, it would look like:

is_intrinsic_open : (X : Set) → (U : X → Set) → (x y : X) → U x → (¬ (x ≡ y)) ⊎ (U y)

In terms of the Agda code, $U$ is an intrinsic open of $X$ if the type (set) is_intrinsic_open X U is inhabited.

Constructively, there are two types of elements of the set of proofs of $x \neq y \lor y \in U$, either $\mathtt{inl}(p)$ where $p$ is a proof of $x \neq y$ or $\mathtt{inr}(q)$ where $q$ is a proof of $y \in U$. If we're unable to produce a proof of $x \neq y$, even if we are also unable to produce a proof $\lnot (x \neq y)$, then we are forced into producing a proof of $y \in U$. If we can't do that either, then $U$ is not an intrinsic open, i.e. we aren't actually able to create this function. The fact that we can fail to be able to produce a proof of a proposition $P$ and fail to be able to produce a proof of $\lnot P$ is why the Law of Excluded Middle needn't hold.

Giving the authors the benefit of the doubt, perhaps they didn't intend the white area as anything more than visual separator between the two shaded areas. This seems unlikely, though, as that white area is pretty important. More likely, it was a careless mistake. In a comment to another question, you referenced the paper Local Concepts in Synthetic Differential Geometry and Germ Representability (which seems pretty good despite it's age) which includes this exact definition of "intrinsic open" and also has a similar, but simpler, diagram without the mistake. In that paper the authors explicitly note the gap between $\lnot\{x\}$ and $\lnot\lnot\{x\}$ describing it as a "no man's land". The authors define a neighborhood of $x$ as "a part $U$ such that it contains $\lnot\{x\}$ and also this 'no man's land'. This is expressed by the formula $\lnot\{x\}\cup U = X$". They then proceed to immediately define the notion of intrinsic open as that formula (for all $x \in U$) and explicitly point out that it logically expands into the formulation given in the question. Incidentally, the diagram is still wrong (by the same logic) even if the authors had meant for $x \neq y$ to stand for an apartness relation which they almost certainly did not.