Categorical Logic 1. disjuction, conjuction, implies, quantifer as adjoint.

 

Readers should be farmilar with category theory.

In the previous blog, we already know that coproduct and product is the left and right adjoint of $\mathrm{\Delta }$$\Delta$​.

Consider the category of a propositiaonal logic over a formal language $L$$L$, the object is proposition and morphism is implies. Hence $\vee ⊣\mathrm{\Delta }⊣\wedge$$\vee\dashv\Delta\dashv\wedge$. Moreover, we have product-exponential adjoint(or tensor-hom adjoint)

$$\begin{array}{}\text{(1)}& p\wedge q⊢r⟺p⊢(q\to r)\end{array}$$

Or, using the language of tensor category, we get that:

$$\begin{array}{}\text{(2)}& ({\mathrm{hom}}_{\mathcal{L}}(p\otimes q),r)\cong {\mathrm{hom}}_{\mathcal{L}}(p,{\mathrm{hom}}_{\mathcal{L}}(q,r))\end{array}$$

Consider a function $f:X\to Y$$f:X\to Y$, and the power set functor, which is natural isomorphic to $\mathrm{Set}(-,2)$$\mathrm{Set}(-,2)$, induced the Boolean ring homomorphism $f^{-1}:P(Y)\to P(X)$$f^{-1}:P(Y)\to P(X)$, can be viewed as a functor, if you view the poset as a category.

This blog introduce the left and right adjoint of $f^{-1}$$f^{-1}$​, whcih is known as quantifer as adjoint.

$$\begin{array}{}\text{(3)}& {\mathrm{\exists }}_f⊣f^{-1}⊣{\mathrm{\forall }}_f\end{array}$$

Let us define two functor ${\mathrm{\exists }}_f$$\exists_f$ and ${\mathrm{\forall }}_f$$\forall_f$ as follows.

$$\begin{array}{}\text{(4)}& {\mathrm{\exists }}_f:P(X)\to P(Y),{\mathrm{\exists }}_f(U)=\{y\in Y|\mathrm{\exists }x,f(x)=y\wedge x\in U\}\end{array}$$

That is, actually, the $f(S)$$f(S)$. Readers may already see this adjoint $f(S)\subseteq U⟺S\subseteq f^{-1}(U)$$f(S)\subseteq U\iff S\subseteq f^{-1}(U)$ in the blog about Galois Connection: Math Essays: Galois Connection in various branches (marco-yuze-zheng.blogspot.com).

The forall $f$$f$ is defined as

$$\begin{array}{}\text{(5)}& {\mathrm{\forall }}_f:P(X)\to P(Y),{\mathrm{\forall }}_f(U)=\{y\in Y|\mathrm{\forall }x,f(x)=y⟹x\in U\}\end{array}$$

i.e. for each $y\in {\mathrm{\forall }}_f(U)$$y\in\forall_f(U)$, we need that $f^{-1}(y)\subseteq U$$f^{-1}(y)\subseteq U$. In other word, ${\mathrm{\forall }}_f(U)=\{y\in Y|f^{-1}(y)\subseteq U\}$$\forall_f(U)=\{y\in Y|f^{-1}(y)\subseteq U\}$

Hence we have

$$\begin{array}{}\text{(6)}& f^{-1}(S)\subseteq U⟺S\subseteq {\mathrm{\forall }}_{f}f(U)\end{array}$$

If you consider a particular case, i.e. $p:X\times Y\to Y$$p:X\times Y\to Y$ and $p$$p$ is the canonical projection.

Then the adjoint triple will give you the classic quantifer:

$$\begin{array}{}\text{(7)}& {\mathrm{\exists }}_y⊣p^{-1}⊣{\mathrm{\forall }}_y\end{array}$$

Let me explain more details.

The subset of $X\times Y$$X\times Y$ can be realized as the subset satisfies $S:X\times Y\to 2,S(x,y)=1$$S:X\times Y\to 2,S(x,y)=1$. Here $S$$S$​ is a predicate.

Remark.You will see the pull back diagram in Topos theory, the $2={\mathbb{F}}_2$$2=\mathbb F_2$ is the subobject classifier in $\mathrm{S}\mathrm{e}\mathrm{t}$$\rm Set$​.

Hence in this case, we could consider ${\mathrm{\exists }}_{y}S(x,y)$$\exists_y S(x,y)$ and ${\mathrm{\forall }}_{y}S(x,y)$$\forall_y S(x,y)$ instead of $\mathrm{\exists }(U)$$\exists (U)$ and $\mathrm{\forall }(U)$$\forall(U)$.

Let us consider

$$\begin{array}{}\text{(8)}& {\mathrm{\exists }}_y:P(X\times Y)\to P(Y),{\mathrm{\exists }}_{y}S(x,y)=\{y\in Y|\mathrm{\exists }(x,y),p(x,y)=y\wedge S(x,y)=1\}\end{array}$$

Hence ${\mathrm{\exists }}_{y}S(x,y)\ne \mathrm{\varnothing }$$\exist_y S(x,y)\ne\empty$ means $\mathrm{\exists }y,S(x,y)$$\exists y,S(x,y)$ is true! Moreover, ${\mathrm{\exists }}_{y}S(x,y)$$\exists_y S(x,y)$ is the elements in $Y$$Y$ makes $S(x,y)$$S(x,y)$ ture.

Similarly,

$$\begin{array}{}\text{(9)}& {\mathrm{\forall }}_y:P(X\times Y)\to P(Y),{\mathrm{\forall }}_{y}S(x,y)=\{y\in Y|\mathrm{\forall }(x,y),p(x,y)=y⟹S(x,y)=1\}\end{array}$$

Hence ${\mathrm{\forall }}_{y}S(x,y)$$\forall_y S(x,y)$ means $\mathrm{\forall }y\in {\mathrm{\forall }}_{y}S(x,y),S(x,y)$$\forall y\in\forall_y S(x,y),S(x,y)$ is true!

Remark. If you compare the definition of ${\mathrm{\exists }}_f$$\exists_f$ and ${\mathrm{\forall }}_f$$\forall_f$ , you will see the product-exponential( $\wedge ,⟹$$\wedge,\implies$). I do not fully understand it.