Commuting Quantifiers

When does the universal quantifier commute with the existential quantifier? That is, when does $\forall x \in A. \exists y \in B. P(x, y)$ imply $\exists y \in B. \forall x \in A. P(x, y)$? Obviously, this is not always the case. There are many counter examples — every house in Aarhus has an owner but there is no person that owns all houses in Aarhus. Here, we will see two criteria where the universal quantifier commutes with the existential quantifier.

Introduction

Working internally in a (pre)sheaf category is quite useful. One particular useful class of these (pre)sheaf categories is (pre)sheaf categories over ordinal numbers (seen as preorder categories), e.g., the topos of trees, $\mathbf{Set}^{\omega^\mathrm{op}}$, which is useful for constructing synthetic domains for studying programming languages¹. In such semantics the meaning of the existential quantifier is defined as follows: $$ \llbracket \exists x : A. \varphi \rrbracket_{\gamma}(c) \overset{\Delta}{=} \exists a \in \llbracket A \rrbracket_{\gamma}(c). \llbracket \varphi \rrbracket_{\gamma[x \mapsto a]}(c) $$ where $\gamma$ maps free variables to their interpretation and $c$ is an object in the base category $C$ of the (pre)sheaf category. In these settings we say that a (closed) formula $\psi$ holds, written $\vdash \psi$, when essentially we have that $\forall c \in \mathit{Obj}(C). \llbracket \psi \rrbracket(c)$. That is, when proving an object exists internally, $\exists x : A. \varphi$, we are proving that for any object $c$ of $C$ there exists an object at the same state $c$ that satisfies $\varphi$ at stage $c$. Hence, if we want to obtain an object in the meta level that satisfies $\varphi$ (i.e., satisfies $\varphi$ for all $c$’s), we need to show that quantifiers commute.

When Do Quantifiers Commute?

It is instructive to look at the situation in the counter example above where quantifiers fail to commute before we discuss situations where they do commute. The problem is rooted in the fact that for each $x$ there is a (possibly) different $y$ for which $P(x, y)$ holds — each house in Aarhus could have a different owner. However, there are situations where this cannot occur. The two situations that we present below for allowing quantifiers to commute consist of imposing some structure and properties over the quantified sets so as to make sure that either: (1) there are so few $y$’s compared to $x$’s that we can always find a $y$ that works for all $x$’s, or (2) there are so many $y$’s for each $x$ that there is always one that works for all $x$’s. The first approach is particularly useful for working with the internally in a (pre)sheaf category when the base category is a regular ordinal (see below). The second approach is another very simple criterion for quantifiers commuting that is useful when the object existentially quantified over satisfies particular properties.

Downwards Closure and Cardinality Restriction

Here, we assume that set universally quantified over has a relation on it and that $P$ is downwards closed with respect to this relation (this is always the case when working with (pre)sheaf categories over ordinal numbers): $$ \forall n \in A, m \in A, y \in B. n \preceq m \land P(m, y) \Rightarrow P(n, y) $$ where the binary relation $\preceq\; \subseteq A \times A$ is reflexive, transitive, and total. Moreover, we assume that the cardinality of the set $B$ is strictly smaller than the cardinality of $A$. We formally represent having a smaller cardinality as the following: $$ \mathit{smaller\_card}(B, A) \overset{\Delta}{=} \forall f : A \to B. \lnot \mathit{injective}(f) $$ That is, we say that $B$ has a smaller cardinality than $A$ if any function from $A$ to $B$ is not injective. In other words, there are fewer elements of $B$ than elements of $A$. Hence, any function mapping elements of $A$ to $B$ must be mapping multiple elements of $A$ to the same element in $B$. We define injectivity as follows: $$ \mathit{injective}(f) \overset{\Delta}{=} \forall x, y. f(x) = f(y) \Rightarrow x = y $$ The last restriction that we impose is that the set $A$ together with the $\preceq$ relation forms a regular ordinal. (This is not precisely true. Strictly speaking we do not require anything about the structure elements of $A$ or about $\preceq$ being well-founded.) There are different equivalent definitions of when an ordinal number is regular. Here, we define it as follows: “any cofinal subset of $A$ must have a cardinality bigger than or equal to that of $A$.” We say that a subset $X$ of $A$ is cofinal if it is not bounded in $A$: $$ \mathit{cofinal}(X) \overset{\Delta}{=} \forall x \in A, \exists y \in X. x \preceq y $$ Since the relation $\preceq$ is reflexive the entire set $A$ itself, as a subset of $A$, is a cofinal subset. Also note that if $A$ has a maximum with respect to $\preceq$, i.e., some $M \in A$ such that $\forall x \in A. x \preceq M$, then the singleton set $\{M\}$ is a cofinal subset of $A$.

We define regularity as follows: $$ \mathit{regular}(A) \overset{\Delta}{=} \forall X \subseteq A. \mathit{cofinal}(X) \Rightarrow \exists f : A \to X. \mathit{injective}(f) $$ The quintessential example of a regular ordinal is the first infinite cardinal $\aleph_0 = \omega$, i.e., the set of natural numbers with the $\preceq$ relation being the $\le$ relation on natural numbers. That is to say that any cofinal (unbounded) subset of the set of natural numbers is necessarily a countable set; hence there is an injection from the set of natural numbers to this subset. Hence, the arguments presented here are valid for extracting witnesses of existential quantification out of closed proofs when working internally in the topos of trees, $\mathbf{Set}^{\omega^\mathrm{op}}$. Moreover, all successor cardinals, i.e., $\aleph_{\alpha + 1}$ for any ordinal number $\alpha$, are examples of regular ordinals. Therefore, our arguments also apply to (pre)sheaf categories where the base is a successor cardinal number.

Given the definitions above, we state the main theorem that we prove in this section.

In the rest of this section we prove the theorem above. We first define the simple notion a fiber for elements of $B$: $$ \mathit{fiber}_P(b) \overset{\Delta}{=} \left\{x \in A \middle| P(x, b) \right\} $$ Notice that if an element $b \in B$ has a cofinal fiber, i.e., $\mathit{cofinal}(\mathit{fiber}(b))$, then for any $x \in A$ we have $P(x, b)$. That is, $$ \begin{align} \mathit{cofinal}\left(\mathit{fiber}_P(b)\right) \Rightarrow \forall x \in A. P(x, b) \end{align} $$ This simply follows from downwards closure of $P$ with respect to $\preceq$ and cofinality of the fiber: for any $n \in A$ there is an element $m \in \mathit{fiber}_P(b)$ such that $n \preceq m$. On the other hand, since $m \in \mathit{fiber}_P(b)$ we must have $P(m, b)$ and by downwards closure also $P(n, b)$. This means that if under the assumption that $(\forall x \in A. \exists y \in B. P(x, y))$ we can find an element in $B$ whose fiber is cofinal, then we have established Theorem 1 above.

The following lemma is the reason why we need $A$ to be a regular ordinal. This lemma says that the union of a non-cofinal family of subsets of a regular ordinal is not cofinal as long as the family is indexed by a set whose cardinality is strictly smaller than that of $A$. Intuitively, regularity of the set $A$ can be understood as $A$ being so large that the union of any family of sets smaller than $A$ indexed by a set that is itself also smaller than $A$ is necessarily smaller than $A$. When applied to the set of natural numbers, which as we said is regular, the following lemma says that the union of finitely many bounded subsets of natural numbers is a bounded subset of natural numbers.

As a corollary of Lemma 2 above we get the following:

Finally, the proof of Theorem 1 is as follows:

Monotonicity and Upper Bounds

Here we assume that the set we existentially quantify over has a relation on it and $P$ is monotone with respect to this relation: $$ \forall n \in B, m \in B, x \in A. n \sqsubseteq m \land P(x, n) \Rightarrow P(x, m) $$ where $\sqsubseteq\; \subseteq B \times B$ is an arbitrary binary relation. Furthermore, we require that for any function from $A$ to $B$ has an upper bound. That is, $$ \forall f : A \to B. \exists u \in B. \forall x \in A.\; f(x) \sqsubseteq u $$ Given this, we prove that $\forall x \in A. \exists y \in B. P(x, y)$ implies $\exists y \in B. \forall x \in A. P(x, y)$. Given that $\forall x \in A. \exists y \in B. P(x, y)$ holds, by axiom of choice we get a function $f : A \to B$ such that $\forall x \in A. P(x, f(x))$. On the other hand, by our assumption every such function has an upper bound $u$ for which $\forall x \in A, f(x) \sqsubseteq u$. Hence, by monotonicity of $P$ we have that $\forall x \in A. P(x, u)$ which concludes the proof.

Bibliography