Proving that Ban is a Pre-Abelian Category via Cauchy Completion Functor

We are working over $\mathbb{C}$$\mathbb{C}$.

Let $\mathsf{Ban}$$\mathsf{Ban}$ be the category of Banach spaces. Let $X$$X$ be a Banach space, a sub vector space $V\subseteq X$$V\subseteq X$ is a subobject if $V$$V$ is closed. Otherwise $V$$V$ is not a Banach space. It is easy to see that $\mathsf{Ban}$$\mathsf{Ban}$ is an additive category. Similarly, denote $\mathsf{Norm}$$\mathsf{Norm}$ as the category of normed vector spaces, which is a pre-abelian category.

We would like to prove that $\mathsf{Ban}$$\mathsf{Ban}$ is a pre-abelian category.

It is easy to see that the kernel exists in $\mathsf{Ban}$$\mathsf{Ban}$. For cokernel, we have the following adjoint pair between $\mathsf{Norm}$$\mathsf{Norm}$ and $\mathsf{Ban}$$\mathsf{Ban}$:

$U⊣F$$U \dashv F$

Here $U$$U$ is the Cauchy completion functor, and $F$$F$ is the forgetful/embedding functor. Then both $U,F$$U, F$ are additive functors.

Proposition. Let $X$$X$ be a Banach space and $K$$K$ is a closed subspace of $X$$X$. Then the cokernel of $K\hookrightarrow X$$K\hookrightarrow X$ exists.

Proof. Consider the following short exact sequence in $\mathsf{Norm}$$\mathsf{Norm}$:

$$0⟶K⟶X\stackrel{\pi }{\to }X/K⟶0$$

The Cauchy completion functor preserves cokernels:

$$U(\mathrm{coker}(K\hookrightarrow X))\cong \mathrm{coker}(U(K)\hookrightarrow U(X))\cong \mathrm{coker}(K\hookrightarrow X)$$

Hence $U(X/K)\cong X/K$$U(X/K)\cong X/K$. $◻$$\square$

 

Categorical Logic Primer: Connectives and Quantifiers

Categorical review of logic in $\mathsf{Set}$.Conjunction $\wedge$:Intersection:The partial order $\le$ in $\Omega$.The $\Rightarrow$.The false arrowNegationComplementDisjunctionUnionQuantifier as adjoint.Negation of quantifiers in $\mathsf{Set}$, perspective from adjoint functor.Local QuantifiersExample.Local truth value explanationComposition of quantifiers

Categorical review of logic in $\mathsf{Set}$$\mathsf{Set}$.

We know in $\mathsf{Set}$$\mathsf{Set}$, the subobject classifier is $2=\{\mathrm{\perp },\mathrm{\top }\}\cong \{0,1\}$$2=\{\bot,\top\}\cong\{0,1\}$.

We have $\mathrm{\top },\mathrm{\perp },\wedge ,\vee ,\Rightarrow ,\mathrm{\neg }$$\top,\bot,\wedge,\vee,\Rightarrow,\neg$ for $2$$2$. Let us define them categorically. The point of studying them categorically is that we need to generalize them to any topos.

Conjunction $\wedge$$\wedge$:

The conjunction $\wedge :\mathrm{\Omega }\times \mathrm{\Omega }\to \mathrm{\Omega }$$\wedge:\Omega\times\Omega\to\Omega$ is the characteristic function of $⟨\mathrm{\top },\mathrm{\top }⟩$$\langle\top,\top\rangle$

When $\mathrm{\Omega }=2$$\Omega=2$, $⟨\mathrm{\top },\mathrm{\top }⟩:1⟼(\mathrm{\top },\mathrm{\top })$$\langle\top,\top\rangle:1\longmapsto(\top,\top)$. Then the characteristic function of this subobject is just

$$x\wedge y:=\wedge (x,y)=\mathrm{\top }⟺x=y=\mathrm{\top }$$

Intersection:

It is not hard to see that the intersection of two subobjects ${\chi }_A,{\chi }_B\subseteq X$$\chi_A,\chi_B\subseteq X$ is given by $\wedge \circ ⟨{\chi }_A,{\chi }_B⟩:X\to \mathrm{\Omega }$$\wedge\circ\langle\chi_A,\chi_B\rangle: X\to\Omega$.

The partial order $\le$$\le$ in $\mathrm{\Omega }$$\Omega$.

With $\wedge :\mathrm{\Omega }\times \mathrm{\Omega }\to \mathrm{\Omega }$$\wedge:\Omega\times\Omega\to\Omega$, we have a semilattice structure on $\mathrm{\Omega }$$\Omega$. The following equalizer diagram is the standard way to define the order of a semilattice:

i.e. $x\le y⟺x\wedge y=x$$x\le y\iff x\wedge y=x$.

It is not hard to see that when $\mathrm{\Omega }=2$$\Omega=2$, the order is just $\mathrm{\perp }\le \mathrm{\top }$$\bot\le\top$.

The $\Rightarrow$$\Rightarrow$.

With $\le$$\le$, we could define $\Rightarrow :\mathrm{\Omega }\times \mathrm{\Omega }\to \mathrm{\Omega }$$\Rightarrow:\Omega\times\Omega\to\Omega$ as follows:

That is, $\Rightarrow$$\Rightarrow$ is just the characteristic function of $\le$$\le$.

It is not hard to see that $(p\Rightarrow q)=\mathrm{\top }⟺(p,q)\in \le =\{(\mathrm{\perp },\mathrm{\perp }),(\mathrm{\perp },\mathrm{\top }),(\mathrm{\top },\mathrm{\top })\}$$(p\Rightarrow q)=\top\iff (p,q)\in\le=\{(\bot,\bot),(\bot,\top),(\top,\top)\}$

We could induce the partial order on $\mathrm{Hom}(X,\mathrm{\Omega })$$\mathrm{Hom}(X,\Omega)$ by considering ${\chi }_A\le {\chi }_B⟺\Rightarrow ({\chi }_A,{\chi }_B)=\mathrm{\top }$$\chi_A\le\chi_B\iff\Rightarrow(\chi_A,\chi_B)=\top$.

The false arrow

The false arrow is the characteristic arrow of the initial object.

In $\mathsf{Set}$$\mathsf{Set}$, $0=\mathrm{\varnothing }$$0=\emptyset$, hence $\mathrm{\perp }:1⟼\mathrm{\perp }$$\bot:1\longmapsto\bot$.

Negation

Once we have $\mathrm{\perp }:1\to \mathrm{\Omega }$$\bot:1\to\Omega$, we could define the negation as the characteristic function:

For $\mathrm{\Omega }=2$$\Omega=2$, we have $\mathrm{\neg }\circ \mathrm{\perp }=\mathrm{\top },\mathrm{\neg }\circ \mathrm{\top }=\mathrm{\perp }$$\neg\circ\bot=\top,\neg\circ\top=\bot$.

Complement

With the negation arrow, we could define the complement of a subobject as follows:

$$\mathrm{\neg }\circ {\chi }_A$$

It's easy to see that when $A\subseteq X$$A\subseteq X$ is a subset of $X$$X$, $\mathrm{\neg }\circ {\chi }_A={\chi }_{A^c}$$\neg\circ\chi_A=\chi_{A^c}$ gives us the complement of $A$$A$.

Disjunction

It is not easy to define the disjunction arrow.

Firstly, we need to define the arrow $⟨⟨\mathrm{\top },\mathrm{id}⟩,⟨\mathrm{id},\mathrm{\top }⟩⟩$$\langle\langle \top,\mathrm{id}\rangle,\langle\mathrm{id,\top\rangle}\rangle$.

Consider $⟨\mathrm{\top },\mathrm{id}⟩,⟨\mathrm{id},\mathrm{\top }⟩:\mathrm{\Omega }\to \mathrm{\Omega }\times \mathrm{\Omega }$$\langle\top,\mathrm{id}\rangle,\langle\mathrm{id},\top\rangle:\Omega\to\Omega\times\Omega$, here $\mathrm{\top }$$\top$ is the constant function.

It universally passes through the coproduct $\mathrm{\Omega }+\mathrm{\Omega }$$\Omega+\Omega$. We define the universal map to be:

$$⟨⟨\mathrm{\top },\mathrm{id}⟩,⟨\mathrm{id},\mathrm{\top }⟩⟩$$

Let $U$$U$ be the image of the universal arrow via epi-mono decomposition:

When $\mathrm{\Omega }=2$$\Omega=2$, we get $U=\{(\mathrm{\perp },\mathrm{\top }),(\mathrm{\top },\mathrm{\perp }),(\mathrm{\top },\mathrm{\top })\}$$U=\{(\bot,\top),(\top,\bot),(\top,\top)\}$.

Then we define $\vee$$\vee$ as the characteristic function of $U$$U$.

Union

We could define the union of two subobjects via:

$$\vee \circ ⟨{\chi }_A,{\chi }_B⟩$$

In $\mathsf{Set}$$\mathsf{Set}$, we have $\vee \circ ⟨{\chi }_A,{\chi }_B⟩={\chi }_{A\cup B}$$\vee\circ\langle\chi_A,\chi_B\rangle=\chi_{A\cup B}$.

Quantifier as adjoint.

In $\mathbf{Set}$$\mathbf{Set}$, we could talk about $\mathrm{\forall },\mathrm{\exists }$$\forall,\exists$.

For example, $\mathrm{\forall }x\in X,P(x)$$\forall x\in X,P(x)$ or $\mathrm{\exists }x\in X,P(x)$$\exists x\in X,P(x)$. This sentence is either true or false.

Here $P:X\to 2$$P:X\to 2$ is a predicate about $X$$X$, hence uniquely corresponds to a subset of $X$$X$.

For example, "all people on Earth feel happy" is false. "There exists some people on Earth who feel happy" is true.

Here $x\in X$$x\in X$ represents people on Earth and $p:X\to 2$$p:X\to 2$ indicates whether this person is happy or not. $\mathrm{\forall }x\in X:={\mathrm{\forall }}_X:P(X)\to 2$$\forall x\in X:=\forall_X:P(X)\to 2$.

Indeed，$\mathrm{\exists }x\in X,P$$\exists x\in X,P$ is true iff $P\ne \mathrm{\varnothing }$$P\ne\empty$, $\mathrm{\forall }x\in X,P$$\forall x\in X,P$ is true iff $P=X$$P=X$.

Consider the universal map $!:X\to 1$$!:X\to 1$ in $\mathsf{Set}$$\mathsf{Set}$. Applying the subobject functor, we get $\mathrm{Sub}(!)={!}^{-1}(-):2\to \mathrm{Sub}(X)$$\mathrm{Sub}(!)=!^{-1}(-):2\to\mathrm{Sub}(X)$.

We know that ${!}^{-1}$$!^{-1}$ is an order preserving map, hence a functor.

Proposition. (actually it is the definition)

${\mathrm{\exists }}_{!}⊣{!}^{-1}⊣{\mathrm{\forall }}_{!}$$\exists_!\dashv\,\, !^{-1}\dashv\forall_!$. Here ${\mathrm{\exists }}_{!}$$\exists_!$ means there exists $x\in X$$x\in X$, the input is a predicate(subset of $X$$X$) and the out put is true or false.

We need to show that:

$${\mathrm{\exists }}_{!}(P)\le ?⟺P\le {!}^{-1}(?)$$

and

$${!}^{-1}(?)\le Q⟺?\le {\mathrm{\forall }}_{!}(Q)$$

It is pretty easy to see since $?\in 2$$?\in 2$.

We prove ${\mathrm{\exists }}_{!}$$\exists_!$ first.

If $?=\mathrm{\perp }$$?=\bot$, then we have ${\mathrm{\exists }}_{!}(U)\le \mathrm{\perp }⟹U=\mathrm{\varnothing }$$\exists_!(U)\le \bot\implies U=\emptyset$. Then both sides are tautologies.

If $?=\mathrm{\top }$$?=\top$, then we have ${!}^{-1}(?)=X$$!^{-1}(?)=X$. Both sides are tautologies as well.

Now we prove ${\mathrm{\forall }}_{!}$$\forall_!$.

If $?=\mathrm{\perp }$$?=\bot$, then ${!}^{-1}(?)=\mathrm{\varnothing }$$!^{-1}(?)=\emptyset$ and both sides are tautologies.

If $?=\mathrm{\top }$$?=\top$, then $V=X,{\mathrm{\forall }}_{!}(V)=\mathrm{\top }$$V=X,\forall_!(V)=\top$, and both sides are tautologies.

Corollary. ${\mathrm{\exists }}_{!}(p\vee q)={\mathrm{\exists }}_{!}(p)\vee {\mathrm{\exists }}_{!}(q),{\mathrm{\forall }}_{!}(p\wedge q)={\mathrm{\forall }}_{!}(p)\wedge {\mathrm{\forall }}_{!}(q)$$\exists_!(p\vee q)=\exists_! (p)\vee\exists_! (q),\forall_!(p\wedge q)=\forall_!(p)\wedge\forall_!(q)$.

Proof. Left adjoint preserve colimit and right adjoint preserve limit. $◻$$\square$

Corollary. Let $X=\mathrm{\varnothing }$$X=\empty$ and $P$$P$ is a predicate of $\mathrm{\varnothing }$$\empty$ (hence it has to be $\mathrm{\varnothing }$$\empty$) and consider $!:X\to 1$$!:X\to1$. Then ${\mathrm{\exists }}_{!}(P)=\mathrm{\perp },{\mathrm{\forall }}_{!}(P)=\mathrm{\top }$$\exists_!(P)=\bot,\forall_!(P)=\top$.

Proof. Let $?=\mathrm{\perp }$$?=\bot$, then we have $\mathrm{\varnothing }=P\le {!}^{-1}(\mathrm{\perp })⟺{\mathrm{\exists }}_{!}(P)\le \mathrm{\perp }⟺{\mathrm{\exists }}_{!}(P)=\mathrm{\perp }$$\empty=P\le!^{-1}(\bot)\iff\exists_!(P)\le\bot\iff\exists_!(P)=\bot$.

Now let $?=\mathrm{\top }$$?=\top$, we have $\mathrm{\varnothing }={!}^{-1}(\mathrm{\top })\le P⟺\mathrm{\top }\le {\mathrm{\forall }}_{!}(P).⟺{\mathrm{\forall }}_{!}(P)=\mathrm{\top }$$\empty=!^{-1}(\top)\le P\iff\top\le\forall_!(P).\iff\forall_!(P)=\top$. $◻$$\square$

Example. For all $x\in \mathrm{\varnothing },x$$x\in\empty,x$ is a natural number $={\mathrm{\forall }}_{!}(P)$$=\forall_!(P)$ is true, but there exists $x\in \mathrm{\varnothing },x$$x\in\empty,x$ is natural number $={\mathrm{\exists }}_{!}(P)$$=\exists_!(P)$ is false.

Negation of quantifiers in $\mathsf{Set}$$\mathsf{Set}$, perspective from adjoint functor.

Now let us see why we have $\mathrm{\neg }(\mathrm{\forall }x\in X,P)=\mathrm{\exists }x\in X,\mathrm{\neg }P$$\neg(\forall x\in X,P)=\exists x\in X,\neg P$.

Consider

$${\mathrm{\exists }}_{!}(P)\le ?⟺P\le {!}^{-1}(?),{!}^{-1}(?)\le Q⟺?\le {\mathrm{\forall }}_{!}(Q)$$

For

$${\mathrm{\exists }}_{!}(P)\le ?⟺P\le {!}^{-1}(?)$$

Apply negation both side, we have

$${!}^{-1}(\mathrm{\neg }?)\le \mathrm{\neg }P⟺\mathrm{\neg }?\le \mathrm{\neg }{\mathrm{\exists }}_{!}(P)$$

Hence $\mathrm{\neg }{\mathrm{\exists }}_{!}(P)={\mathrm{\forall }}_{!}(\mathrm{\neg }P)$$\neg\exists_!(P)=\forall_!(\neg P)$, since the right adjoint is unique! Amazing right!

Similarly, for

$${!}^{-1}(?)\le Q⟺?\le {\mathrm{\forall }}_{!}(Q)$$

Apply negation both sides we have:

$$\mathrm{\neg }{\mathrm{\forall }}_{!}(Q)\le \mathrm{\neg }?⟺\mathrm{\neg }Q\le {!}^{-1}(\mathrm{\neg }?)$$

Hence $\mathrm{\neg }{\mathrm{\forall }}_{!}(Q)={\mathrm{\exists }}_{!}(\mathrm{\neg }Q)$$\neg\forall_!(Q)=\exists_!(\neg Q)$ !

Indeed, what we have is $\mathrm{\neg }{\mathrm{\forall }}_{!}\mathrm{\neg }={\mathrm{\exists }}_{!}$$\neg\forall_!\neg=\exists_!$ and $\mathrm{\neg }{\mathrm{\exists }}_{!}\mathrm{\neg }={\mathrm{\forall }}_{!}$$\neg\exists_!\neg=\forall_!$.

Since once we have two involution($F^2=\mathrm{id}$$F^2=\mathrm{id}$) functors $N_{\mathcal{C}}:{\mathcal{C}}^{\mathrm{op}}\to \mathcal{C},N_{\mathcal{D}}:{\mathcal{D}}^{\mathrm{op}}\to \mathcal{D}$$N_{\mathcal C}:\mathcal {C}^{\mathrm{op}}\to\mathcal C,N_{\mathcal D}:\mathcal D^{\mathrm{op}}\to\mathcal D$ and a pair of adjoints

$$L⊣R$$

We have

$$N_{\mathcal{D}}\circ R\circ N_{\mathcal{C}}⊣N_{\mathcal{C}}\circ L\circ N_{\mathcal{D}}$$

 

Since

$$\begin{array}{rl}{\mathrm{Hom}}_{\mathcal{D}}(N_{\mathcal{D}}R{N}_{\mathcal{C}}(X),V)& \cong {\mathrm{Hom}}_{\mathcal{D}}(N_{\mathcal{D}}V,R{N}_{\mathcal{C}}(X))\\ & \cong {\mathrm{Hom}}_{\mathcal{C}}(L{N}_{\mathcal{D}}(V),N_{\mathcal{C}}(X))\\ & \cong {\mathrm{Hom}}_{\mathcal{C}}(X,N_{\mathcal{C}}L{N}_{\mathcal{D}}(V)),\end{array}$$

Now apply this general result to our adjoint triples

Notice that we have ${!}^{-1}\circ \mathrm{\neg }=\mathrm{\neg }\circ {!}^{-1}$$!^{-1}\circ\neg=\neg\circ !^{-1}$, hence $\mathrm{\neg }\circ {!}^{-1}\circ \mathrm{\neg }={!}^{-1}$$\neg\circ!^{-1}\circ\neg=!^{-1}$.

Therefore we have

$$\mathrm{\neg }\circ {\mathrm{\forall }}_{!}\circ \mathrm{\neg }⊣{!}^{-1}⊣\mathrm{\neg }\circ {\mathrm{\exists }}_{!}\circ \mathrm{\neg }$$

i.e. $\mathrm{\neg }{\mathrm{\forall }}_{!}\mathrm{\neg }={\mathrm{\exists }}_{!}$$\neg\forall_!\neg=\exists_!$ and $\mathrm{\neg }{\mathrm{\exists }}_{!}\mathrm{\neg }={\mathrm{\forall }}_{!}$$\neg\exists_!\neg=\forall_!$.

Local Quantifiers

But then you may ask me, how do I write something like $\mathrm{\forall }\epsilon \in \mathbb{R},\mathrm{\exists }N\in \mathbb{N},P(\epsilon ,N)$$\forall\varepsilon\in\mathbb R,\exists N\in\mathbb N,P(\varepsilon,N)$?

Well, we need to generalize the quantifier above first.

Definition.

Let $f:X\to Y$$f:X\to Y$ be a function, then we define ${\mathrm{\exists }}_f$$\exists_f$ and ${\mathrm{\forall }}_f$$\forall_f$ to be the left and right adjoint of $f^{-1}$$f^{-1}$.

Indeed, we have:

${\mathrm{\exists }}_f:P(X)\to P(Y)$$\exists_f:P(X)\to P(Y)$ is given by ${\mathrm{\exists }}_f(U):=\{y\in Y:\mathrm{\exists }x\in U,f(x)=y\}=f(U)$$\exists_f(U):=\{y\in Y:\exists x\in U, f(x)=y\}=f(U)$.

and

${\mathrm{\forall }}_f:P(X)\to P(Y)$$\forall_f:P(X)\to P(Y)$ is given by ${\mathrm{\forall }}_f(U):=\{y\in Y:\mathrm{\forall }x\in X,f(x)=y⟹x\in U\}=\{y\in Y:f^{-1}(y)\subseteq U\}$$\forall_f(U):=\{y\in Y:\forall x\in X,f(x)=y\implies x\in U \}=\{y\in Y:f^{-1}(y)\subseteq U\}$

You should check that when $f=!$$f=!$, this gives us ${\mathrm{\exists }}_{!}$$\exists_!$ and ${\mathrm{\forall }}_{!}$$\forall_!$ and the following adjoint:

$${\mathrm{\exists }}_f(U)=f(U)\subseteq V⟺U\subseteq f^{-1}(V),f^{-1}(U)\subseteq V⟺U\subseteq {\mathrm{\forall }}_f(V)$$

The way to understand ${\mathrm{\exists }}_f,{\mathrm{\forall }}_f$$\exists_f,\forall_f$ is to view $\mathrm{Sub}(Y)$$\mathrm{Sub}(Y)$ as a set of local truth values.

Similarly, we have, if $X=\mathrm{\varnothing },f:\mathrm{\varnothing }\to Y$$X=\empty,f:\empty\to Y$ is the unique map, we have

$${\mathrm{\exists }}_f(P)=f(P)=\mathrm{\varnothing },{\mathrm{\forall }}_f(P)=\{y\in Y:f^{-1}(y)\subseteq P\}=Y$$

I would like to give some examples here to help readers understand ${\mathrm{\exists }}_f,{\mathrm{\forall }}_f$$\exists_f,\forall_f$.

Example.

• Let $X$$X$ be the set of all tasks.

• Let $Y$$Y$ be the set of all employees.

• Let $f:X\to Y$$f: X \to Y$ assign each task to its responsible employee (i.e., $f(x)$$f(x)$ is the employee in charge of task $x$$x$).

Now suppose on $X$$X$ we have a predicate $\phi (x)$$\varphi(x)$: “task $x$$x$ is urgent.” Let $A\subseteq X$$A \subseteq X$ be the subset of urgent tasks, so $\phi$$\varphi$ is represented by the characteristic function ${\chi }_{\phi }:X\to \{0,1\}$$\chi_\varphi: X \to \{0,1\}$.

• Existential quantification along $f$$f$, ${\mathrm{\exists }}_f\phi$$\exists_f \varphi$: For an employee $y\in Y$$y \in Y$, $({\mathrm{\exists }}_f\phi )(y)$$(\exists_f \varphi)(y)$ is true if and only if this employee has at least one assigned urgent task. Intuition: “This employee has some urgent task.”

• Universal quantification along $f$$f$, ${\mathrm{\forall }}_f\phi$$\forall_f \varphi$: For an employee $y$$y$, $({\mathrm{\forall }}_f\phi )(y)$$(\forall_f \varphi)(y)$ is true if and only if all tasks assigned to this employee are urgent. (If the employee has no tasks, one usually treats this as true by convention, depending on the ambient context.) Intuition: “Every task of this employee is urgent.”

Local truth value explanation

Fix a map $f:X\to Y$$f: X \to Y$. Think of a point $y\in Y$$y \in Y$ (e.g., an employee) as a local context. The quantifications along $f$$f$ evaluate a predicate upstairs by aggregating over the fiber $f^{-1}(y)$$f^{-1}(y)$:

• ${\mathrm{\exists }}_f$$\exists_f$ does OR over the fiber $f^{-1}(y)$$f^{-1}(y)$:
  It asks whether there exists some element in the fiber that satisfies the predicate. Intuition: “Does employee $y$$y$ have some urgent task?”

• ${\mathrm{\forall }}_f$$\forall_f$ does AND over the fiber $f^{-1}(y)$$f^{-1}(y)$:
  It asks whether every element in the fiber satisfies the predicate. Intuition: “Are all tasks assigned to employee $y$$y$ urgent?” (If the fiber is empty, then ${\mathrm{\exists }}_f$$\exists_f$ is false and ${\mathrm{\forall }}_f$$\forall_f$ is true by vacuous truth.)

So for each $y\in Y$$y \in Y$ we get two local truth values:

• “Employee $y$$y$ has an urgent task?” is $({\mathrm{\exists }}_f\phi )(y)$$(\exists_f \varphi)(y)$.

• “All tasks of employee $y$$y$ are urgent?” is $({\mathrm{\forall }}_f\phi )(y)$$(\forall_f \varphi)(y)$.

More formally: if $\phi$$\varphi$ is a predicate on $X$$X$ (represented by a subobject $A\subseteq X$$A \subseteq X$ or its characteristic map ${\chi }_{\phi }:X\to \mathrm{\Omega }$$\chi_\varphi: X \to \Omega$), then

$$({\mathrm{\exists }}_f\phi )(y)=\text{true}⟺\mathrm{\exists }x\in X,f(x)=y\text{ and }\phi (x)\text{ holds},$$

$$({\mathrm{\forall }}_f\phi )(y)=\text{true}⟺\text{for all }x\in X\text{ with }f(x)=y,\phi (x)\text{ holds},$$

with the convention that $({\mathrm{\forall }}_f\phi )(y)$$(\forall_f \varphi)(y)$ is true when $f^{-1}(y)=\mathrm{\varnothing }$$f^{-1}(y)=\emptyset$.

Composition of quantifiers

Now we consider the map ${\pi }_X:X\times Y\to X$$\pi_X:X\times Y\to X$, then:

Let $P:X\times Y\to 2$$P:X\times Y\to 2$ be a predicate. ${\mathrm{\exists }}_{{\pi }_X}(P)={\pi }_X(P)=\{x\in X:\mathrm{\exists }y\in Y,P(x,y)=\mathrm{\top }\}$$\exists_{\pi_X}(P)=\pi_X(P)=\{x\in X:\exists y\in Y,P(x,y)=\top\}$.

Here ${\mathrm{\exists }}_{{\pi }_X}$$\exists_{\pi_{X}}$ is all the $x\in X$$x\in X$ that make $P(x,y)=\mathrm{\top }$$P(x,y)=\top$. Similarly, we have ${\mathrm{\forall }}_{{\pi }_X}(P)=\{x\in X:\mathrm{\forall }y\in Y,P(x,y)=\mathrm{\top }\}$$\forall_{\pi_{X}}(P)=\{x\in X:\forall y\in Y,P(x,y)=\top\}$.

Now we could talk about something like $\mathrm{\forall }x\in X,\mathrm{\exists }y\in Y,P(x,y)$$\forall x\in X,\exists y\in Y,P(x,y)$.

That is:

$${\mathrm{\forall }}_{!}\circ {\mathrm{\exists }}_{{\pi }_X}:P(X\times Y)\to 2$$

It is easy to verify. For a fixed $x\in X$$x\in X$, $\mathrm{\exists }y\in Y,P(x,y)=\mathrm{\top }⟺x\in {\pi }_X(P)$$\exists y\in Y,P(x,y)=\top\iff x\in\pi_X(P)$. Hence $\mathrm{\forall }x\in X,\mathrm{\exists }y\in Y,P(x,y)$$\forall x\in X,\exists y\in Y,P(x,y)$ is true iff

${\mathrm{\forall }}_{!}\circ {\mathrm{\exists }}_{{\pi }_X}(P)=\mathrm{\top }⟺{\mathrm{\exists }}_{{\pi }_X}(P)=X$$\forall_{!}\circ \exists_{\pi_X}(P)=\top\iff\exists_{\pi_X}(P)=X$.

For example, let $X=\mathbb{R},Y=\mathbb{N}$$X=\mathbb R,Y=\mathbb N$. Then $\mathrm{\forall }\epsilon \in \mathbb{R},\mathrm{\exists }n\in \mathbb{N},f(n)\le \epsilon$$\forall \varepsilon\in \mathbb R,\exists n\in\mathbb N,f(n)\le\varepsilon$ is given by:

$${\mathrm{\forall }}_{!}\circ {\mathrm{\exists }}_{{\pi }_{\mathbb{R}}}(\{(\epsilon ,n):f(n)\le \epsilon \})$$

It is true means:

$${\mathrm{\exists }}_{{\pi }_{\mathbb{R}}}(\{(\epsilon ,n):f(n)\le \epsilon \})=\{\epsilon \in \mathbb{R}:\mathrm{\exists }n\in \mathbb{N},f(n)\le \epsilon \}=\mathbb{R}$$

We also could talk about something like $\mathrm{\exists }x\in X,\mathrm{\forall }y\in Y,P(x,y)$$\exists x\in X,\forall y\in Y,P(x,y)$.

Which is given by:

$${\mathrm{\exists }}_{!}\circ {\mathrm{\forall }}_{{\pi }_X}(P)$$

For example, $\mathrm{\exists }n\in \{1,2,3\},\mathrm{\forall }m\in \{-1,0\},n\ge m$$\exists n\in\{1,2,3\},\forall m\in\{-1,0\},n\ge m$.

Hence consider ${\mathrm{\exists }}_{!}\circ {\mathrm{\forall }}_{{\pi }_{\{1,2,3\}}}(\{(n,m)\in \{1,2,3\}\times \{-1,0\},n\ge m\})={\mathrm{\exists }}_{!}(X)=\mathrm{\top }$$\exists_{!}\circ\forall_{\pi_{\{1,2,3\}}}(\{(n,m)\in\{1,2,3\}\times\{-1,0\},n\ge m\})=\exists_!(X)=\top$

If we consider $\mathrm{\exists }n\in \{1,2,3\},\mathrm{\forall }m\in \{-1,0\},n\le m$$\exists n\in\{1,2,3\},\forall m\in\{-1,0\},n\le m$, then what we will get is just:

$${\mathrm{\exists }}_{!}\circ {\mathrm{\forall }}_{{\pi }_{\{1,2,3\}}}(\mathrm{\varnothing })=\mathrm{\perp }$$