categorical interpretation of quantification

Question

Many constructions in intuitionistic and classical logic have relatively simple counterparts in category theory. For instance, conjunctions, disjunctions, and conditionals have analogues in products, coproducts, and exponential objects.

More esoteric concepts still permit reasonably simple categorical interpretations. For instance, the modal operator $\Box$ (necessity) can be described as a monoidal endofunctor (see, for instance, Paiva & Ritter's Basic Constructive Modality (PDF)).

What are the similar constructions that are suitable interpretations for universal and existential quantification in first-order logic?

Answer 1

There are two concepts in category theory that correspond to $\land$ and $\lor$:

1. (Binary) categorical products and coproducts, as you mention.
2. Meets and joins as operations on the subobjects of a given object (satisfying the Beck-Chevalley condition).

Similarly, there are two ways to express logical quantifiers as categorical notions. In the following I assume a category $\mathcal{C}$ which has whatever structure is necessary to make sense of what I am saying (I can be more precise if needed).

1. For every arrow $f : A \to B$ there is a pullback functor $f^{*} : \mathcal{C}/B \to \mathcal{C}/A$ which takes an arrow $g : D \to B$ to its pullback $f^{*}(g) : f^{*}(D) \to A$ along $f$. Here $\mathcal{C}/X$ is the slice category over $X$. There is another functor $\Sigma_f : \mathcal{C}/A \to \mathcal{C}/B$ defined on an object $h : E \to A$ as $\Sigma_f(h) = f \circ h$. Then $\Sigma_f$ is left adjoint to $f^{*}$. Sometimes $\mathcal{C}$ is such that $f^{*}$ also has a right adjoint $\Pi_f$ of $f^{*}$. When such structure exists, $\mathcal{C}$ is said to be locally cartesian closed. The existential quantifier corresponds to $\Sigma_f$ and the universal one to $\Pi_f$. More precisely, universal quantification $\forall x \in X . \phi(x, y)$ corresponds to $\Pi_{\pi_1}(\phi)$ where $\pi_1 : X \times Y \to Y$ is the first projection and $\phi : Z \to X \times Y$.

2. There is a subobject functor $\mathsf{Sub} : \mathcal{C}^{\mathrm{op}} \to \mathsf{Poset}$ which takes an object $A$ to the poset of its subobjects and an arrow $f : A \to B$ to the monotone map $f^{*} : \mathsf{Sub}(B) \to \mathsf{Sub}(A)$ which takes a subobject represented by a mono $m : X \to B$ to the subobject represented by $f^{*}(m) : f^{*}(X) \to A$, the pullback of $m$ along $f$. When the posets $\mathsf{Sub}(A)$ are (distributive) lattices, we can interpret $\land$ and $\lor$ as meets and joins. To interpret the quantifiers we again ask for the left and right adjoints of $f^{*}$. The left adjoints exist when $\mathcal{C}$ has stable image factorizations, and these give the existential quantifiers. The right adjoints give the universal quantifiers. There is a little detail called the Beck-Chevalley condition which requires that the adjoints are stable under pullbacks. (In logic the condition corresponds to the fact that substitution commutes with quantifiers.)

We can also express the inference rules for quantifiers in a form that makes it obvious that they are adjoints. Consider the following rule: $$\frac{x : X, y : Y \mid \phi \vdash \psi}{y : Y \mid \phi \vdash \forall x : X . \psi}$$ This says: "if $\phi$ entails $\psi$, where $x$ and $y$ are free variables of type $X$ and $Y$ respectively, then $\phi$ entails $\forall x : X . \psi$ with free variable $y : Y$." (Note that $x$ cannot occur free in $\phi$ because $\phi$ appears on the bottom line in a context where only the free variable $y$ is allowed.) This is the introduction rule for $\forall$. But we can turn it around to get the elimination rule: $$\frac{y : Y \mid \phi \vdash \forall x : X . \psi}{x : X, y : Y \mid \phi \vdash \psi}$$ This is not the elimination rule as usually stated, which is $$\frac{y : Y \mid \phi \vdash \forall x : X . \psi \qquad a : X}{y : Y \mid \phi \vdash \psi[a/x]},$$ but we can obtain this one from ours by using the rule of substitution: from $\forall x : X . \psi$ first derive $\psi$, and then substiute $a$ for $x$.

Now to be completely precise, we should consider $\phi$ above the line to be different from the one below the line because one appears in the context with variables $x : X$ and $y : Y$, and the other in the context with just $y : Y$. So let us write $[x]^{*}(\phi)$ for the formula $\phi$ considered in the context with the variable $x$ added to it (this is known as weakening in logic, although here we are adding stuff to the typing context, whereas in logic there is also weakening that adds hypotheses). With this notation our rules read as $$\frac{x : X, y : Y \mid [x]^{*}(\phi) \vdash \psi}{y : Y \mid \phi \vdash \forall x : X . \psi}$$ and $$\frac{y : Y \mid \phi \vdash \forall x : X . \psi}{x : X, y : Y \mid [x]^{*}(\phi) \vdash \psi}.$$ But this has the form of an adjunction between $[x]^{*}$ and $\forall x : X$! We also see the correspondence between logic and categories clearly now: weakening $[x]^{*}$ corresponds to pullback along the projection $\pi_1 : X \times Y \to X$, and $\forall x : X$ corresponds the functor $\Pi_{\pi_1}$.

I leave it as an exercise for you to figure out how the existential is a left adjoint to weakening. So the moral of the story is that universal and existential quantifiers are rigth and left adjoints of weakening.

References:

• Steve Awodey: Category theory, Oxford University Press. This has a nice and easy explanation of what I wrote above.
• Bart Jacobs: Categorical Logic and Type Theory. This is nuclear weapons, it contains everything and more about the subject, including generalizations that unify the above two views.

Answer 2

The analogue of existential quantification is the dependent sum, and the analogue of universal quantification is the dependent product. The analogy itself passes through the Curry-Howard correspondence.

A simple categorical description of quantification is the following. In a category with pullbacks, any morphism $f : x \to y$ induces a functor $f^{\ast} : \text{Sub}(y) \to \text{Sub}(x)$ from the category of subobjects of $y$ to the category of subobjects of $x$ by taking pullbacks. In a category with finite products, and when they exist, the existential quantifier is the left adjoint to the functor $\text{Sub}(x) \to \text{Sub}(x \times y)$ induced by a projection map $\pi_x : x \times y \to x$, and the universal quantifier is the right adjoint, thinking of $\text{Sub}(x)$ as being described by predicates over $x$ (although strictly speaking we need a subobject classifier to do this).

See also Heyting category and dependent type theory.

Answer 3

Here's a simple-minded version of the basic point here, put in terms of Galois connections.

Let $L$ be a first-order language, and $\mathit{Form}(\vec{x})$ be the set of $L$-wffs with at most the variables $\vec{x}$ free.

Write $\phi(\vec{x})$ for a formula in $Form(\vec{x})$, $|\phi(\vec{x})|$ for the class of formulae logically interderivable with $\phi(\vec{x})$, and $E_{\vec{x}}$ for the set of such equivalence classes of formulae from $\mathit{Form}(\vec{x})$.

Put $|\phi(\vec{x})| \Rightarrow |\psi(\vec{x})|$ iff $|\phi(\vec{x})| \vdash |\psi(\vec{x})|$. Then $\Rightarrow$ is a partial order on $E_{\vec{x}}$.

Now we'll consider two maps between the posets $(E_{\vec{x}}, \Rightarrow)$ and $(E_{\vec{x}, y}, \Rightarrow)$. In other words, we are going to be moving between (classes of) formulae with at most $\vec{x}$ free, and formulae with at most $\vec{x}, y$ free (where $y$ isn't among the $\vec{x}$).

First, since every wff with at most the variables $\vec{x}$ free also has at most the variables $\vec{x}, y$ free, there is a trivial map $f_*$ that sends $|\phi(\vec{x})| \in E_{\vec{x}}$ to the same element $|\phi(\vec{x})| \in E_{\vec{x}, y}$.

Second, we define the companion map $f^*$ that sends $|\phi(\vec{x}, y)| \in E_{\vec{x}, y}$ to $|\forall y\,\phi(\vec{x}, y)| \in E_{\vec{x}}$.

Then $(f_*, f^*)$ is a Galois connection between $E_{\vec{x}}$ and $E_{\vec{x}, y}$. That is to say

$f_*(|\phi(\vec{x})|) = |\psi(\vec{x},y)|\quad$ if and only if $\quad|\,\phi(\vec{x})\,| = f^*(|\psi(\vec{x},y)|)$

For that just restates the familiar logical rule

$\phi(\vec{x}) \vdash \psi(\vec{x},y)\quad$ iff $\quad\phi(\vec{x}) \vdash \forall y\,\psi(\vec{x},y)$

Hence universal quantification is right-adjoint to a certain quite trivial operation. (There's an analogous result for existentials.)

Answer 4

I've accepted Andrej Bauer's answer as it is the most thorough, provides references, and, especially with the explanations in the comments, has made this topic much clearer. Different references have been provided in the various answers, and in case future users have additional references, I though it would be useful add a community wiki answer listing the various references.

• Steve Awodey: Category theory, Oxford University Press. This has a nice and easy explanation of the material in Andrej Bauer's answer.
• Bart Jacobs: Categorical Logic and Type Theory. This is nuclear weapons, it contains everything and more about the subject, including generalizations that unify the above two views.
• Goldblatt, R. (2006). Topoi: the categorial analysis of logic (Vol. 98). Courier Dover Publications. Goldblatt approaches category theory from the standpoint of logic, so those more acquainted with logic than category theory may appreciate this text. (Additionally, the same might do well to read Peter Smith's answer before reading Andrej Bauer's answer; it will provide some intuition for the categorical generalization.)

Answer 5

There's a detailed discussion of quantifiers-as-adjunctions in Chapter 15 ("Adjointness and Quantifiers") of Goldblatt's book Topoi: the Categorial Analysis of Logic.

The earlier part of the book contains an explanation of category theory from the ground up, with particular attention to how it relates to logic, so might be a good thing to read if you are interested in logic and trying to understand how category theory relates to it, or are learning about adjunctions for the first time for the purpose of understanding the category-theoretic modeling of quantifiers.

Answer 6

The simplest, and most direct, way to include quantifiers that stays within the bounds of first-order logic (as you wish for), while avoiding the better-known constructions seen in higher-order type theory, is to expand the treatment used for finite conjunctions to handle conjunctions indexed by sets $T$. Taking $T$ to be finite, this subsumes both the ‟true” predicate $⊤$ (by taking $T = ∅$), and the ‟and” connective ∧ (by taking $T = 2$), as well as the universal quantifier $∀$ for a single-sorted logic (taking $T$ to be the set of all terms) or for a multi-sorted logic, (where we may have different instances of $T$, one for each type of term). In the last case, we get an algebra for bounded quantifiers that avoids the need for any excursion into dependent types or higher-order type theory / logic and stays strictly first-order.

The key observation is this: if all of the inferences hold $f(t): C ⊢ A(t)$, for every $t∈T$ - in particular, if we have any inference $f(c): C ⊢ A(c)$, where $c$ is a free variable not present in either $C$ or $(∀x)A(x)$ - then we may apply generalization to $f(c)$ to produce the inference $‹x¦f(x)› ≡ {Gen}_c^x f(c): C ⊢ (∀x)A(x)$. We can make this independent of $c$ by imposing an identity ${Gen}_c'^x f(c') = {Gen}_c^x f(c)$, where $c'$ is any other free variable satisfying the same requirement.

Conversely, if we have the inference $h: C ⊢ (∀x)A(x)$, then we may combine it with the instantiation rule $π_At: (∀x)A(x) ⊢ A(t)$ to produce the result $(Πt)h ≡ π_At∘h: C ⊢ A(t)$. It is understood that the usual convention is adopted to take everything modulo α-equivalence to avoid any issues with free-bound capture.

If the categorical algebra is suitably-defined, then these two processes should be inverses, i.e. $‹x¦(Πx)h› = h$ and $(Πt)‹x¦f(x)› = f(t)$ for every $t∈T$, and certain naturality conditions should also hold true. Natural bijections, alone, entail an underlying infrastructure which provides a bundle of rules/operators and related proof algebra sufficient to capture all of what we need.

In the following, I will use the conventions that for a category $𝐗$:

• $|𝐗|$ = the objects of $𝐗$,
• for $X, X' ∈ |𝐗|$, $𝐗(X,X')$ = the set of arrows/morphisms $X → X'$,

along with the definitions

• $𝐗^+$ is the dual category:
  • $|𝐗^+| = |𝐗|$,
  • for $X, X' ∈ |𝐗|$, $𝐗^+(X,X') = 𝐗(X',X)$,
  • identities in $𝐗^+$ are the same as those in $𝐗$,
  • compositions in $𝐗^+$ are the reverse of those in $𝐗$.
• $𝐗×𝐘$ is the direct product category:
  • $|𝐗×𝐘| = |𝐗|×|𝐘|$,
  • for $(X,Y),(X',Y') ∈ |𝐗×𝐘|$, $(𝐗×𝐘)((X,Y),(X',Y')) = 𝐗(X,X')×𝐘(Y,Y')$.
• $1$ is the unit category:
  • $|1| = \left\{0\right\}$,
  • $1(0,0) = \left\{1_0\right\}$,
• $𝐗^T$ is the indexed product category, with indexing set $T$:
  • $|𝐗^T| = |𝐗|^T$,
  • for $A,B ∈ |𝐗|^T$, $𝐗^T(A,B) = ⨅_{t∈T} 𝐗(A(t),B(t))$
  • for $A ∈ |𝐗|^T$, $1_A = [t∈T ↦ A(t)] ∈ 𝐗^T(A,A)$,
  • for $A,B,C ∈ |𝐗|^T$, $f: B → C$, $g: A → B$, $f∘g ≡ [t∈T ↦ f(t)∘g(t)] ∈ 𝐗^T(A,C)$

In a category $𝐋$ for logic, objects are predicates, arrows $A → B$ are inference relations $A ⊢ B$ between predicates $A$ and $B$, while morphisms $f: A → B$ are proofs that bear witness to the respective inference, the relation which we may also write $f: A ⊢ B$.

Within this framework, the distinguished object $⊤$ (for ‟true”), and connective $∧$ (for ‟and”) may be directly implemented by functors

• True (‟terminal object”) ― $⊤: 1 → 𝐋$,
• And (‟product”) ― $∧: 𝐋×𝐋 → 𝐋$,

and proof rules *all* implemented via *natural bijections*, as follows: $$𝐋(C,⊤) ⇔ 1(0,0) = \{1_0\},$$ $$𝐋(C,A∧B) ⇔ 𝐋(C,A)×𝐋(C,B),$$

To extend this to the universal quantifier - treating it as an indexed product - we add in another functor

• All (‟indexed product” indexed by a set $T$) ― $∀: 𝐋^T → 𝐋$,

and another natural bijection: $$𝐋(C,∀A) ⇔ 𝐋^T(C,A).$$

For True, the bijection is trivial and is given by $$h: C ⊢ ⊤ ⇔ 1_0: 0 → 0.$$ For And (conjunctions), the bijection is given by $$h: C ⊢ A∧B ⇔ f: C ⊢ A, g: C ⊢ B.$$ For All (universal quantifiers), it is given by $$h: C ⊢ (∀x)A(x) ⇔ [t∈T ↦ f(t): C ⊢ A(t)].$$

So, let's see how this works for conjunctions, first, and then more generally for indexed conjunctions - subsuming $⊤$, $∧$ and $∀$ within this treatment as special cases.

The Natural Bijection for Conjunctions

For conjunctions, the bijection is given by $$f: C ⊢ A, g: C ⊢ B ⇔ h: C ⊢ A∧B$$ this works as follows:

1. There is a functor $$∧: 𝐋 × 𝐋 → 𝐋$$ such that
   • Objects: $A,B∈|𝐋| ↦ A∧B∈|𝐋|$,
   • Morphisms: for $A,A',B,B'∈|𝐋|$, $f: A ⊢ A', g: B ⊢ B' ↦ f∧g: A∧A' ⊢ B∧B'$.
   The defining properties of a functor, when applied here, entail the identities:
   • for $A,B ∈ |𝐋|$, $1_A∧1_B = 1_{A∧B}$,
   • for $A,A',A'',B,B',B'' ∈ |𝐋|$, and for $f:A⊢A', f':A'⊢A'', g:B⊢B', g':B'⊢B''$, $(f'∘f)∧(g'∘g) = (f'∧g')∘(f∧g)$.
2. There is a bijective natural transform
   • for $A,B,C∈|𝐋|$, $(f: C ⊢ A, g: C ⊢ B) ↦ ‹f,g›: C ⊢ A∧B$,
   • for $A,B,C∈|𝐋|$, $(h: C ⊢ A∧B) ↦ (⊤h: C ⊢ A, ⊥h: C ⊢ B)$,
   with inverse relations: $$⊤‹f,g› = f, ⊥‹f,g› = g, ‹⊤h,⊥h› = h,$$ and naturality conditions described equivalently either as: $$‹k∘f∘m,l∘g∘m› = k∧l∘‹f,g›∘m$$ or $$⊤(k∧l∘h∘m) = k∘⊤h∘m, ⊥(k∧l∘h∘m) = l∘⊥h∘m$$
3. More precisely:
   • $‹⋯,⋯›: 𝐅 → 𝐆$ and $(⊤⋯,⊥⋯): 𝐆 → 𝐅$ are natural transforms between the functors $𝐅$ and $𝐆$ given by
   • $𝐅: 𝐋×𝐋×𝐋^+ → 𝐒𝐞𝐭$, with
     • Objects: $𝐅: A,B,C∈|𝐋| ↦ 𝐋(C,A) × 𝐋(C,B)$,
     • Morphisms: $𝐅: (k:A⊢A',l:B⊢B',m:C'⊢C) ↦ (𝐅(k,l,m): (f,g) ∈ 𝐋(C,A) × 𝐋(C,B) ↦ (k∘f∘m, l∘g∘m) ∈ 𝐋(C',A') × 𝐋(C',B'))$,
   • $𝐆: 𝐋×𝐋×𝐋^+ → 𝐒𝐞𝐭$, with
     • Objects: $𝐆: A,B,C∈|𝐋| ↦ 𝐋(C,A∧B)$,
     • Morphisms: $𝐆: (k:A⊢A',l:B⊢B',m:C'⊢C) ↦ (𝐆(k,l,m): h ∈ 𝐋(C,A∧B) ↦ k∧l∘h∘m ∈ 𝐋(C',A'∧B'))$,
   • 𝐆iven by
     • For $A,B,C∈|𝐋|$, $‹⋯,⋯›_{A,B,C}: (f,g) ∈ 𝐅(A,B,C) ↦ ‹f,g› ∈ 𝐆(A,B,C),$
     • For $A,B,C∈|𝐋|$, $(⊤⋯,⊥⋯)_{A,B,C}: h ∈ 𝐆(A,B,C) ↦ (⊤h,⊥h) ∈ 𝐅(A,B,C),$
   • which satisfies the requisite properties for natural transforms that for $$(k,l,m) ∈ 𝐋×𝐋×𝐋^+((A,B,C),(A',B',C'))$$ (i.e. for $k: A⊢A'$, $l: B⊢B'$, $m: C'⊢C$), $$‹⋯,⋯›_{A',B',C'}∘𝐅(k,l,m) = 𝐆(k,l,m)∘‹⋯,⋯›_{A,B,C}$$ (i.e. $‹k∘f∘m,l∘g∘m› = k∧l∘‹f,g›∘m$, for $(f,g) ∈ 𝐅(A,B,C)$), and $$(⊤⋯,⊥⋯)_{A',B',C'}∘𝐆(k,l,m) = 𝐅(k,l,m)∘(⊤⋯,⊥⋯)_{A,B,C}$$ (i.e. $(⊤(k∧l∘h∘m),⊥(k∧l∘h∘m))$ = $(k∘⊤h∘m,l∘⊥h∘m)$ for $h ∈ 𝐆(A,B,C)$)

The operators $‹⋯,⋯›$, $⊤(⋯)$, $⊥(⋯)$ are equivalently described as ‟polymorphic operators” with polymorphism parametrized by $A,B,C∈|𝐋|$. On account of these identities, each of the operators, as well as the functor $∧$ can be reduced to a small set of primitives, given by $$L_{A,B} ≡ ⊤ 1_{A∧B}: A∧B ⊢ A,$$ $$R_{A,B} ≡ ⊥ 1_{A∧B}: A∧B ⊢ B,$$ as follows:

• for $A,B,C∈|𝐋|$ and $h: C⊢A∧B$, $$⊤h = ⊤(1_{A∧B}∘h) = ⊤1_{A∧B}∘h = L_{A,B}∘h,$$ $$⊥h = ⊥(1_{A∧B}∘h) = ⊥1_{A∧B}∘h = R_{A,B}∘h,$$
• for $A,A',B,B'∈|𝐋|$, and $k:A⊢A'$, $l:B⊢B'$, $$k∧l = k∧l∘‹⊤1_{A∧B},⊥1_{A∧B}›∘1_{A∧B} = ‹k∘L_{A,B},l∘R_{A,B}›$$

with the smaller set of identities:

• for $A,B,C∈|𝐋|$ and $f:C⊢A, g:C⊢B$, $L_{A,B}∘‹f,g› = f$ and $R_{A,B}∘‹f,g› = g$,
• for $A,B,C.C'∈|𝐋|$ and $f:C⊢A, g:C⊢B, m:C'⊢C$, $‹f∘m,g∘m› = ‹f,g›∘m$,
• for $A,B∈|𝐋|$, $‹L_{A,B},R_{A,B}› = 1_{A∧B}$

from which *all* of the previously stated identities follow (which are all well-known, by the way, seen for instance in Girard's formalism).

These, too, are polymorphic operators, and it is generally the case that all of the above relations can be stated more succinctly without the extra parametrization made explicit, without any loss of relevant context, like so: $$⊤h = L∘h, ⊥h = R∘h,$$ $$L = ⊤1, R = ⊥1,$$ $$L∘‹f,g› = f, R∘‹f,g› = g,$$ $$‹L,R› = 1, k∧l = ‹k∘L,l∘R›.$$

The Natural Bijections for Indexed Conjunctions and Universal Quantifiers

For the universal quantifier, this works as follows:

1. There is a functor $$∀: 𝐋^T → 𝐋$$ such that
   • Objects: $A∈|𝐋^T| ↦ (∀x)A(x) ≡ ∀A∈|𝐋|$,
   • Morphisms: for $A,A'∈|𝐋^T|$, $(∀x)f(x) ≡ ∀f: ∀A ⊢ ∀A'$ in $𝐋$
   The key defining properties, for $∀$ to be a functor, are
   • for $A∈|𝐋^T|$, $(∀x)1_{A(x)} = 1_{(∀x)A(x)}$,
   • for $A,A',A''∈|𝐋^T|$ and for $f:A⊢A'$, $f':A'⊢A''$, $∀(f'∘f) = ∀f'∘∀f$, i.e. $(∀x)(f'(x)∘f(x)) = (∀x)f'(x)∘(∀x)f(x)$
   By taking $T$, to be finite sets or natural numbers, we can use the same formalism described here to formulate the natural bijections for finitely-indexed conjunctions. That subsumes the treatments for both the conjunction $A∧B = ⋀(A,B)$ for $T = 2$ and $(A,B) ∈ |𝐋|²$ and $⊤ = ⋀()$ for $T = 0$, for $() ∈ |𝐋|⁰ ≅ 1$, as special cases.
2. A bijective natural transform is given by
   • for $A∈|𝐋^T|$, $C∈|𝐋|$, $[t∈T ↦ f(t): C ⊢ A(t)] ↦ ‹x¦f(x)›: C ⊢ ∀A$,
   • for $A∈|𝐋^T|$, $C∈|𝐋|$, $h: C ⊢ ∀A ↦ [t∈T ↦ (Πt)h: C ⊢ A(t)]$,
   with inverse relations $(Πt)‹x¦f(x)› = f(t)$, for $t∈T$ and $‹x¦(Πx)h› = h$, and naturality conditions described equivalently as: $$‹x¦k(x)∘f(x)∘m› = (∀x)k(x)∘‹x¦f(x)›∘m$$ or $$(Πt)((∀x)k(x)∘h∘m) = k(t)∘(Πt)h∘m$$ for $t∈T$.
3. More precisely:
   • $‹⋯¦⋯›: 𝐅 → 𝐆$ and $((Πt)⋯¦t∈T): 𝐆 → 𝐅$ are natural transforms between the functors $𝐅$ and $𝐆$ given by
   • $𝐅: 𝐋^T×𝐋^+ → 𝐒𝐞𝐭$
     • Objects: $𝐅: A∈|𝐋^T|, C∈|𝐋| ↦ 𝐋^T(C,A)$,
     • Morphisms: for $A,A'∈|𝐋^T|, C,C'∈|𝐋|$, $𝐅: (k:A⊢A',m:C'⊢C) ↦ (𝐅(k,m): f ∈ 𝐋^T(C,A) ↦ (t∈T ↦ k(t)∘f(t)∘m) ∈ 𝐋^T(C',A'))$
   • $𝐆: 𝐋^T×𝐋^+ → 𝐒𝐞𝐭$
     • Objects: $𝐆: A∈|𝐋^T|, C∈|𝐋| ↦ 𝐋(C,∀A)$,
     • Morphisms: for $A,A'∈|𝐋^T|, C,C'∈|𝐋|$, $𝐆: (k:A⊢A',m:C'⊢C) ↦ (𝐆(k,m): h ∈ 𝐋(C,∀A) ↦ ∀k∘h∘m ∈ 𝐋(C',∀A'))$,
   • 𝐆iven by
     • for $A∈|𝐋^T|, C∈|𝐋|$, $‹⋯¦⋯›_{A,C}: f ∈ 𝐅(A,C) ↦ ‹x¦f(x)› ∈ 𝐆(A,C)$,
     • for $A∈|𝐋^T|, C∈|𝐋|$, $((Πt)⋯¦t∈T)_{A,C}: h ∈ 𝐆(A,C) ↦ ((Πt)h:t∈T) ∈ 𝐅(A,C),$
   • which satisfies the requisite properties for natural transforms that for $$(k,m) ∈ 𝐋^T×𝐋^+((A,C),(A',C')),$$ i.e. $k: A⊢A', m: C'⊢C$, $$‹⋯¦⋯›_{A',C'}∘𝐅(k,m) = 𝐆(k,m)∘‹⋯,⋯›_{A,C}$$ i.e. $‹x¦k(x)∘f(x)∘m› = (∀x)k(x)∘‹x¦f(x)›∘m$, for $f ∈ 𝐅(A,C)$, and $$((Πt)⋯:t∈T)_{A',C'}∘𝐆(k,m) = 𝐅(k,m)∘((Πt)⋯:t∈T)_{A,C}$$ i.e. $(Πt)((∀x)k(x)∘h∘m) = (k(t)∘(Πt)h∘m)$ for $h ∈ 𝐆(A,C)$ and $t∈T$.

The operators $‹⋯¦⋯›$, $(Πt)(⋯)$ are, likewise, described equivalently as ‟polymorphic operators” with polymorphism parametrized by $A∈|𝐋^T|$ and $C∈|𝐋|$.

A reduction similar to that for conjunctions yields, equivalently, the following reduced set of operators and identities: $$π_A(t) ≡ (Πt)1_{∀A}: (∀x)A(x) ⊢ A(t)$$ for $t∈T$ as follows:

• for $A∈|𝐋^T|$, $C∈|𝐋|$ and $h: C⊢∀A$, $t∈T$, $(Πt)h = π_A(t)∘h$,
• for $A,A'∈|𝐋^T|$, and $k:A⊢A'$, $∀k = ‹x¦k(x)∘π_A(x)›$

with the smaller set of identities:

• for $A∈|𝐋^T|$, $C∈|𝐋|$, $[t∈T ↦ f(t):C⊢A(t)]$, $π_A(t)∘‹x¦f(x)› = f(t)$,
• for $A∈|𝐋^T|$, $C,C'∈|𝐋|$, $[t∈T ↦ f(t):C⊢A(t)]$, $m:C'⊢C$, $‹x¦f(x)∘m› = ‹x¦f(x)›∘m$,
• for $A∈|𝐋^T|$, $‹x¦π_A(x)› = 1_{∀A}$

from which *all* of the previously stated identities follow.

These, too, can be written more succinctly, without loss of context, by omitting the extra parametrization of the polymorphic operators as: $$(Πt)h = π(t)∘h, π(t) = (Πt)1, π(t)∘‹x¦f(x)› = f(t)$$ for $t∈T$ and $$‹x¦π(x)› = 1, ∀k = ‹x¦k(x)∘π(x)›.$$

By dualizing everything, the treatments for $⊤$, $∧$ and $∀$ can be transformed into treatments respectively for their duals False ($⊥$), Or ($∨$) and Some ($∃$), the existential quantifier, as well as indexed disjunctions.

Answer 7

It's a good exercise to see the natural bijections worked out in some detail, but as I noted in your other reply (Categorical semantics explained – what is an interpretation?), padawan, there is an additional minor detail that you left out, which should be made clear.

While the natural bijection for the $∧$ instantiates to bijections between the hom sets $𝐋(C,A∧B)$ and $𝐋(C,A)×𝐋(C,B)$ for $A,B,C ∈ |𝐋×𝐋×𝐋^+|$, for consistency the natural bijection for $∀$ can't instantiate to bijections between $𝐋(C,∀A)$ and $𝐋^T(C,A)$ for $A ∈ |𝐋^T| = |𝐋|^T$ and $C ∈ |𝐋^+| = |𝐋|$: the $C$ on the right has to be lifted to $|𝐋|^T$ as a constant function. This is implemented by Curry's $K$ combinator, represented here as a functor $𝐊_T: 𝐋 → 𝐋^T$ that embeds the objects and morphisms of $𝐋$ as constant functions in $𝐋^T$ (i.e. $𝐊_T C: t∈T ↦ C$ for $C∈|𝐋|$ and $𝐊_T f: t∈T ↦ f$ for $f ∈ 𝐋(A,B)$ and $A,B ∈ |𝐋|$.

Therefore, the correct statement of the natural bijection ... which produces the details you spelled out ... is actually $𝐋(C,∀A) ⇔ 𝐋^T(𝐊_TC,A)$, for $C ∈ |𝐋|$ and $A ∈ |𝐋^T|$. This forms an adjunction pair $(∀_T,𝐊_T)$ for each set $T$ that is being considered: be they the finite sets $T = ∅$ or $T = 2 = \{0,1\}$ or the infinite sets $T$ of terms in a language or families of such sets if the language is multi-sorted.

This is a natural launching point for considering possible generalizations, where the set $T$, or family of such sets, is replaced by other kinds of objects, perhaps even by categories.