tl;dr The notion of two sets overlapping is very common. Often it is expressed
via |A \cap B \neq \varnothing|. Constructively, this is not the best definition
as it does not imply |\exists x. x \in A \land x \in B|. Even classically, this
second-class treatment of overlapping obscures important and useful connections.
In particular, writing |U \between A| for “|U| overlaps |A|”, we have a De Morgan-like
duality situation with |\between| being dual to |\subseteq|. Recognizing and
exploiting this duality, in part by using more appropriate notation for “overlaps”,
can lead to new concepts and connections.
Introduction
The most common way I’ve seen the statement “|A| overlaps |B|” formalized
is |A \cap B \neq \varnothing|. To a constructivist, this definition isn’t
very satisfying. In particular, this definition of overlaps does not allow
us to constructively conclude that there exists an element contained in both
|A| and |B|. That is, |A \cap B \neq \varnothing| does not imply
|\exists x. x \in A \land x \in B| constructively.
As is usually the case, even if you are not philosophically a constructivist,
taking a constructivist perspective can often lead to better definitions and
easier to see connections. In this case, constructivism suggests the more positive
statement |\exists x. x \in A \land x \in B| be the definition of “overlaps”.
However, given that we now have two (constructively) non-equivalent definitions,
it is better to introduce notation to abstract from the particular definition. In
many cases, it makes sense to have a primitive notion of “overlaps”. Here I will
use the notation |A \between B| which is the most common option I’ve seen.
Properties
We can more compactly write the quantifier-based definition as |\exists x \in A.x \in B|
using a common set-theoretic abbreviation. This presentation suggests a perhaps surprising
connection. If we swap the quantifier, we get |\forall x\in A.x \in B| which is commonly
abbreviated |A \subseteq B|. This leads to a duality between |\subseteq| and |\between|,
particularly in topological contexts. In particular, if we pick a containing set |X|,
then |\neg(U \between A) \iff U \subseteq A^c| where the complement is relative to |X|,
and |A| is assumed to be a subset of |X|. This is a De Morgan-like duality.
If we want to characterize these operations via an adjunction, or, more precisely, a Galois
connection, we have a slight awkwardness arising from |\subseteq| and |\between| being
binary predicates on sets. So, as a first step we’ll identify sets with predicates via, for
a set |A|, |\underline A(x) \equiv x \in A|. In terms of predicates, the adjunctions we
want are just a special case of the adjunctions characterizing the quantifiers.
\[\underline U(x) \land P \to \underline A(x) \iff P \to U \subseteq A\]
\[U \between B \to Q \iff \underline B(x) \to (\underline U(x) \to Q)\]
What we actually want is a formula of the form |U \between B \to Q \iff B \subseteq (\dots)|.
To do this, we need an operation that will allow us to produce a set from a predicate. This is
exactly what set comprehension does. For reasons that will become increasingly clear, we’ll
assume that |A| and |B| are subsets of a set |X|. We will then consider quantification relative
to |X|. The result we get is:
\[\{x \in U \mid P\} \subseteq A \iff \{x \in X \mid x \in U \land P\} \subseteq A \iff P \to U \subseteq A\]
\[U \between B \to Q \iff B \subseteq \{x \in X \mid x \in U \to Q\} \iff B \subseteq \{x \in U \mid \neg Q\}^c\]
The first and last equivalences require additionally assuming |U \subseteq X|.
The last equivalence requires classical reasoning. You can already see motivation to
limit to subsets of |X| here. First, set complementation, the |(-)^c|, only makes sense relative to
some containing set. Next, if we choose |Q \equiv \top|, then the latter formulas
state that no matter what |B| is it should be a subset of the expression that
follows it. Without constraining to subsets of |X|, this would require a universal
set which doesn’t exist in typical set theories.
Choosing |P| as |\top|, |Q| as |\bot|, and |B| as |A^c| leads to the
familiar |\neg (U \between A^c) \iff U \subseteq A|, i.e. |U| is a
subset of |A| if and only if it doesn’t overlap |A|’s complement.
Incidentally, characterizing |\subseteq| and |\between| in terms of Galois
connections, i.e. adjunctions, immediately gives us some properties for free via continuity.
We have |U \subseteq \bigcap_{i \in I}A_i \iff \forall i\in I.U \subseteq A_i|
and |U \between \bigcup_{i \in I}A_i \iff \exists i \in I.U \between A_i|. This
is relative to a containing set |X|, so |\bigcap_{i \in \varnothing}A_i = X|, and |U|
and each |A_i| are assumed to be subsets of |X|.
Categorical Perspective
Below I’ll perform a categorical analysis of the situation. I’ll mostly be using categorical
notation and perspectives to manipulate normal sets. That said, almost all of what I say will
be able to be generalized immediately just by reinterpreting the symbols.
To make things a bit cleaner in the future, and to make it easier to apply these ideas
beyond sets, I’ll introduce the concept of a Heyting algebra.
A Heyting algebra is a partially ordered set |H| satisfying the following:
- |H| has two elements called |\top| and |\bot| satisfying for all |x| in |H|, |\bot \leq x \leq \top|.
- We have operations |\land| and |\lor| satisfying for all |x|, |y|, |z| in |H|,
|x \leq y \land z| if and only |x \leq y| and |x \leq z|, and similarly for |\lor|,
|x \lor y \leq z| if and only |x \leq z| and |y \leq z|.
- We have an operation |\to| satisfying for all |x|, |y|, and |z| in |H|,
|x \land y \leq z| if and only if |x \leq y \to z|.
For those familiar with category theory, you might recognize this as simply the decategorification
of the notion of a bicartesian closed category.
We can define the pseudo-complement, |\neg x \equiv x \to \bot|.
Any Boolean algebra is an
example of a Heyting algebra where we can define |x \to y| via |\neg x \lor y| where
here |\neg| is taken as primitive. In particular, subsets of a given set ordered by
inclusion form a Boolean algebra, and thus a Heyting algebra. The |\to| operation can also
be characterized by |x \leq y \iff (x \to y) = \top|. This lets us immediately see
that for subsets of |X|, |(A \to B) = \{x \in X \mid x \in A \to x \in B\}|. All
this can be generalized to the subobjects in any Heyting category.
As the notation suggests, intuitionistic logic (and thus classical logic) is another
example of a Heyting algebra.
We’ll write |\mathsf{Sub}(X)| for the partially ordered set of subsets of |X| ordered
by inclusion. As mentioned above, this is (classically) a Boolean algebra and thus a
Heyting algebra. Any function |f : X \to Y| gives a monotonic function
|f^* : \mathsf{Sub}(Y) \to \mathsf{Sub}(X)|. Note the swap. |f^*(U) \equiv f^{-1}(U)|.
(Alternatively, if we think of subsets in terms of characteristic functions, |f^*(U) \equiv U \circ f|.)
Earlier, we needed a way to turn predicates into sets. In this case, we’ll go the other way
and identify truth values with subsets of |1| where |1| stands for an arbitrary singleton set.
That is, |\mathsf{Sub}(1)| is the poset of truth values. |1| being the terminal object of |\mathbf{Set}|
induces the (unique) function |!_U : U \to 1| for any set |U|. This leads to the important
monotonic function |!_U^* : \mathsf{Sub}(1) \to \mathsf{Sub}(U)|. This can be described
as |!_U^*(P) = \{x \in U \mid P\}|. Note, |P| cannot contain |x| as a free variable.
In particular |!_U^*(\bot) = \varnothing| and |!_U^*(\top) = U|. This monotonic function
has left and right adjoints:
\[\exists_U \dashv {!_U^*} \dashv \forall_U : \mathsf{Sub}(U) \to \mathsf{Sub}(1)\]
|F \dashv G| for monotonic functions |F : X \to Y| and |G : Y \to X|
means |\forall x \in X. \forall y \in Y.F(x) \leq_Y y \iff x \leq_X G(y)|.
|\exists_U(A) \equiv \exists x \in U. x \in A| and |\forall_U(A) \equiv \forall x \in U. x \in A|.
It’s easily verified that each of these functions are monotonic.
It seems like we should be done. These formulas are the formulas I originally gave for
|\between| and |\subseteq| in terms of quantifiers. The problem here is that these functions
are only defined for subsets of |U|. This is especially bad for interpreting |U \between A|
as |\exists_U(A)| as it excludes most of the interesting cases where |U| partially overlaps |A|.
What we need is a way to extend |\exists_U| / |\forall_U| beyond subsets of |U|. That is,
we need a suitable monotonic function |\mathsf{Sub}(X) \to \mathsf{Sub}(U)|.
Assume |U \subseteq X| and that we have an inclusion |\iota_U : U \hookrightarrow X|.
Then |\iota_U^* : \mathsf{Sub}(X) \to \mathsf{Sub}(U)| and |\iota_U^*(A) = U \cap A|.
This will indeed allow us to define |\subseteq| and |\between| as |U \subseteq A \equiv \forall_U(\iota_U^*(A))|
and |U \between A \equiv \exists_U(\iota_U^*(A))|. We have:
\[\iota_U[-] \dashv \iota_U^* \dashv U \to \iota_U[-] : \mathsf{Sub}(U) \to \mathsf{Sub}(X)\]
Here, |\iota_U[-]| is the direct image of |\iota_U|. This doesn’t really do anything in this case
except witness that if |A \subseteq U| then |A \subseteq X| because |U \subseteq X|.
We can recover the earlier adjunctions by simply using these two pairs of adjunctions.
\[\begin{align}
U \between B \to Q
& \iff \exists_U(\iota_U^*(B)) \to Q \\
& \iff \iota_U^*(B) \subseteq {!}_U^*(Q) \\
& \iff B \subseteq U \to \iota_U[{!}_U^*(Q)] \\
& \iff B \subseteq \{x \in X \mid x \in U \to Q\}
\end{align}\]
Here the |\iota_U[-]| is crucial so that we use the |\to| of |\mathsf{Sub}(X)|
and not |\mathsf{Sub}(U)|.
\[\begin{align}
P \to U \subseteq A
& \iff P \to \forall_U(\iota_U^*(A)) \\
& \iff {!}_U^*(P) \subseteq \iota_U^*(A) \\
& \iff \iota_U[{!}_U^*(P)] \subseteq A \\
& \iff \{x \in X \mid x \in U \land P\} \subseteq A
\end{align}\]
In this case, the |\iota_U[-]| is truly doing nothing because |\{x \in X \mid x \in U \land P\}|
is the same as |\{x \in U \mid P\}|.
While we have |{!}_U^* \circ \exists_U \dashv {!}_U^* \circ \forall_U|, we
see that the inclusion of |\iota_U^*| is what breaks the direct connection between
|U \between A| and |U \subseteq A|.
Examples
As a first example, write |\mathsf{Int}A| for the interior of |A| and |\bar A| for the closure of |A|
each with respect to some topology
on a containing set |X|.
One way to define |\mathsf{Int}A| is |x \in \mathsf{Int}A| if and only if there exists an open set
containing |x| that’s a subset of |A|. Writing |\mathcal O(X)| for the set of open sets, we
can express this definition in symbols:
\[x \in \mathsf{Int}A \iff \exists U \in \mathcal O(X). x \in U \land U \subseteq A\]
We have a “dual” notion:
\[x \in \bar A \iff \forall U \in \mathcal O(X). x \in U \to U \between A\]
That is, |x| is in the closure of |A| if and only if every open set containing |x| overlaps |A|.
As another example, here is a fairly unusual way of characterizing a compact subset |Q|.
|Q| is compact if and only if |\{U \in \mathcal O(X) \mid Q \subseteq U\}| is open
in |\mathcal O(X)| equipped with the Scott topology.
As before, this suggests a “dual” notion characterized by |\{U \in \mathcal O(X) \mid O \between U\}|
being an open subset. A set |O| satisfying this is called overt.
This concept is never mentioned in traditional presentations of point-set topology because every
subset is overt. However, if we don’t require that arbitrary unions of open sets are open (and only require
finite unions to be open) as happens in synthetic topology
or if we aren’t working in a classical context then overtness becomes a meaningful concept.
One benefit of the intersection-based definition of overlaps is that it is
straightforward to generalize to many sets overlapping, namely |\bigcap_{i\in I} A_i \neq \varnothing|.
This is also readily expressible using quantifiers as: |\exists x.\forall i \in I. x \in A_i|.
As before, having an explicit “universe” set also clarifies this. So,
|\exists x \in X.\forall i \in I. x \in A_i| with |\forall i \in I. A_i \subseteq X| would
be better. The connection of |\between| to |\subseteq| suggests instead of this fully
symmetric presentation, it may still be worthwhile to single out a set producing
|\exists x \in U.\forall i \in I. x \in A_i| where |U \subseteq X|. This can be
read as “there is a point in |U| that touches/meets/overlaps every |A_i|”.
If desired we could notate this as |U \between \bigcap_{i \in I}A_i|. Negating and
complementing the |A_i| leads to the dual notion |\forall x \in U.\exists i \in I.x \in A_i|
which is equivalent to |U \subseteq \bigcup_{i \in I}A_i|. This dual notion could
be read as “the |A_i| (jointly) cover |U|” which is another common and important concept
in mathematics.
Conclusion
Ultimately, the concept of two (or more) sets overlapping comes up quite often. The usual
circumlocution, |A \cap B \neq \varnothing|, is both notationally and conceptually clumsy.
Treating overlapping as a first-class notion via notation and formulating definitions in terms
of it can reveal some common and important patterns.