2 Typed Full Lambek calculus

In this section we introduce the Typed Full Lambek calculus with quantifiers, denoted $\mathrm {TFL}$ , which is basically a typed or many-sorted version of the first-order Full Lambek calculus $\mathrm {FL}$ as in Ono [Reference Ono34]; we follow the typing style of Pitts [Reference Pitts, Abramsky, Gabbay and Maibaum35], and so this is basically the combination of Pitts [Reference Pitts, Abramsky, Gabbay and Maibaum35] and Ono [Reference Ono34].

Standard categorical logic discusses a typed version of intuitionistic (or coherent or regular) logic, as seen, for example, in Pitts [Reference Pitts, Abramsky, Gabbay and Maibaum35], Lambek–Scott [Reference Lambek and Scott21], Jacobs [Reference Jacobs16], and Johnstone [Reference Johnstone18]. Typed logic is more natural than single-sorted one from a categorical point of view, and is more expressive in general, since it can be equipped with various type constructors, which make the logic more powerful (if they do not make it inconsistent). If one prefers single-sorted logic to typed logic, the latter can be reduced to the former by allowing for one type (or sort) only.

To put it differently, typed logic is the combination of logic and type theory, and has not only a logic structure but also a type structure, and the latter itself has a rich structure as well as the former. For this reason, syntactic hyperdoctrines constructed from typed systems of logic (which are discussed in relation to completeness in the next section) are amalgamations of syntactic categories obtained from their type theories on the one hand, and Lindenbaum–Tarski algebras obtained from their logic parts on the other; in a nutshell, syntactic hyperdoctrines are type-fibred Lindenbaum–Tarski algebras.

Another merit of typed logic is that the problem of empty domains is resolved because it allows us to have explicit control on type contexts. This was discovered by Joyal, according to Marquis and Reyes [Reference Marquis, Reyes, Gabbay, Kanamori and Woods24], and shall be touched upon later in more detail.

$\mathrm {TFL}$ has the following logical connectives:

$$ \begin{align*}\otimes, \wedge, \vee, \backslash, /, 1, 0, \top, \bot, \forall, \exists.\end{align*} $$

Note that there are two kinds of implication connectives $\backslash $ and $/$ , owing to the non-commutative nature of $\mathrm {TFL}$ .

In $\mathrm {TFL}$ , every variable x comes with its type $\sigma $ . That is, $\mathrm {TFL}$ has basic types, which are denoted by letters like $\sigma ,\tau $ , and

$$ \begin{align*}x:\sigma\end{align*} $$

is a formal expression meaning that a variable x is of type $\sigma $ . Then, a (type) context is a finite list of type declarations on variables:

$$ \begin{align*}x_1:\sigma_1,\ldots,x_n:\sigma_n.\end{align*} $$

A context is often denoted $\Gamma $ .

Accordingly, $\mathrm {TFL}$ has typed predicate symbols (aka. predicates in context) and typed function symbols (aka. function symbols in context):

$$ \begin{align*}R(x_1,\ldots,x_n) \ [x_1:\sigma_1,\ldots,x_n:\sigma_n]\end{align*} $$

is a formal expression meaning that R is a predicate with n variables $x_1,\ldots ,x_n$ of types $\sigma _1,\ldots ,\sigma _n$ respectively; likewise,

$$ \begin{align*}f:\tau \ [x_1:\sigma_1,\ldots,x_n:\sigma_n]\end{align*} $$

is a formal expression meaning that f is a function symbol with n variables $x_1,\ldots ,x_n$ of types $\sigma _1,\ldots ,\sigma _n$ and with its values in $\tau $ . Then, formulae-in-context $\varphi \ [\Gamma ]$ and terms-in-context $t:\tau \ [\Gamma ]$ are defined in the usual, inductive way.

In the present paper, we do not consider any specific type constructor, but even if type constructors such as products, sums, and function spaces are added, they just make the syntactic category construction below more complex (since they do not affect the propositional structure), and all proofs below can be directly adapted to such cases in a modular manner. Note that if type constructors affect the propositional structure, then proofs get essentially more difficult; this is the case in higher-order logic with the proposition type $\mathrm {Prop}$ (aka. truth value type $\Omega $ ), which interlace the term structure with the propositional structure. Although we focus upon plainly typed predicate logic with no complicated type structure, still, products (not as types but as categorical structures) shall be used in categorical semantics in the next section, to the end of interpreting predicate and function symbols (of arity greater than one).

$\mathrm {TFL}$ thus has both a type structure and a logic structure, dealing with sequents-in-contexts:

$$ \begin{align*}\Phi \vdash \varphi \ [\Gamma],\end{align*} $$

where $\Gamma $ is a type context, and $\Phi $ is a finite list of formulae: $\varphi _1,\ldots ,\varphi _n$ . Although it is common to write $\Gamma \ | \ \Phi \vdash \varphi $ rather than $\Phi \vdash \varphi \ [\Gamma ]$ , we employ the latter notation in this paper, following Pitts [Reference Pitts, Abramsky, Gabbay and Maibaum35], since $\mathrm {TFL}$ is an adaptation of Pitts’ typed system for intuitionistic logic to the system of the Full Lambek calculus.

The syntax of type contexts $\Gamma $ in $\mathrm {TFL}$ is the same as that of typed intuitionistic logic in Pitts [Reference Pitts, Abramsky, Gabbay and Maibaum35]. Note that it is allowed to add a fresh $x:\sigma $ to a context $\Gamma $ : e.g.,

$$ \begin{align*}\Phi \vdash \varphi \ [\Gamma,x:\sigma]\end{align*} $$

whenever $\Phi \vdash \varphi \ [\Gamma ]$ . On the other hand, it is not permitted to delete redundant variables; the reason becomes clear in latter discussion on empty domains. It is allowed to change the order of contexts (e.g., $[\Gamma ,\Gamma ']$ into $[\Gamma ',\Gamma ]$ ). Now, in the following, we explain logical rules of inference.

$\mathrm {TFL}$ has no structural rule other than the following cut rule:

where $\psi $ may be empty; this is allowed in the following L (left) rules as well. As usual, we have the rule of identity

In the following, we list the rules of inference for the logical connectives of $\mathrm {TFL}$ . The following formulation is intuitionistic in the sense that only one formula is allowed to appear on the right-hand side of sequents; nevertheless, we can treat classical logic as an axiomatic extension of $\mathrm {TFL}$ , by adding to $\mathrm {TFL}$ exchange, weakening, contraction, and the excluded middle (note that structural rules can be expressed as axioms). There are two kinds of conjunction in $\mathrm {TFL}$ : multiplicative or monoidal $\otimes $ and additive or Cartesian $\wedge $ :

There is only one disjunction in $\mathrm {TFL}$ , which is additive, since $\mathrm {TFL}$ is intuitionistic in the aforementioned sense.

Due to non-commutativity, there are two kinds of implication in $\mathrm {TFL}$ , $\backslash $ and $/$ , which are a right adjoint of $\varphi \otimes (\mbox {-})$ and a right adjoint of $(\mbox {-})\otimes \psi $ respectively.

There are two kinds of truth and falsity constants, monoidal and Cartesian ones.

Finally, we have the following rules for quantifiers $\forall $ and $\exists $ , in which type contexts explicitly change; notice that type contexts do not change in the rest of the rules presented above.

As usual, there are eigenvariable conditions on the rules above: x does not appear as a free variable in the bottom sequent of Rule $\forall R$ ; likewise, x does not appear as a free variable in the bottom sequent of Rule $\exists L$ . The other two rules do not have eigenvariable conditions, and this is why contexts do not change in them.

The deducibility of sequents-in-context in $\mathrm {TFL}$ is defined in the usual way. In this paper, we denote by $\mathrm {FL}$ the propositional (and hence no contextual) part of $\mathrm {TFL}$ . Note that what is called $\mathrm {FL}$ in the literature often lacks $\bot $ and $\top $ .

As is well known, the following propositional (resp. predicate) logics can be represented as axiomatic (to be precise, axiom-schematic) extensions of $\mathrm {FL}$ (resp. $\mathrm {TFL}$ ): classical logic, intuitionistic logic, linear logic (without exponentials), relevance logics, and fuzzy logics such as Gödel–Dummett logic (see, e.g., Galatos–Jipsen–Kowalski–Ono [Reference Galatos, Jipsen, Kowalski and Ono10]). Given a set of axioms (to be precise, axiom schemata), say X, we denote by $\mathrm {FL}_X$ (resp. $\mathrm {TFL}_X$ ) the corresponding extension of $\mathrm {FL}$ (resp. $\mathrm {TFL}$ ) via X.

A striking feature of typed predicate logic is that domains of discourse in semantics can be empty; they are assumed to be non-empty in the usual Tarski semantics of predicate logic. We therefore need no ad hoc condition on domains of discourse if we work with typed predicate logic. This resolution of the problem of empty domains is due to Joyal as noted in Marquis and Reyes [Reference Marquis, Reyes, Gabbay, Kanamori and Woods24].

A proof-theoretic manifestation of this feature is that the following sequent-in-context is not necessarily deducible in $\mathrm {TFL}$ :

$$ \begin{align*}\forall x \varphi \vdash \exists x \varphi \ [\mbox{ }],\end{align*} $$

where the context is empty. Nonetheless, the following is deducible in $\mathrm {TFL}$ :

$$ \begin{align*}\forall x \varphi \vdash \exists x \varphi \ [x:\sigma,\Gamma],\end{align*} $$

where $\Gamma $ is an appropriate context including type declarations on free variables in $\varphi $ . This means that we can prove the sequent above when a type $\sigma $ is inhabited. Here, it is crucial that it is not allowed to delete redundant free variables (e.g., $[x:\sigma ,\Gamma ]$ cannot be reduced into $[\Gamma ]$ even if x does not appear as a free variable in formulae involved); however, it is allowed to add fresh free variables to a context.

3 Full Lambek hyperdoctrine

It is well known that $\mathrm {FL}$ algebras (defined below) provide sound and complete semantics for propositional logic $\mathrm {FL}$ (see, e.g., Galatos–Jipsen–Kowalski–Ono [Reference Galatos, Jipsen, Kowalski and Ono10]). In this section we show that fibred $\mathrm {FL}$ algebras, or $\mathrm {FL}$ hyperdoctrines (defined below), yield sound and complete semantics for typed (or many-sorted) predicate logic $\mathrm {TFL}$ .

We emphasise the simple, algebro-logical idea that single algebras (symbolically, A with no indexing) correspond to propositional logic, and fibred algebras (symbolically, $(A_C)_{C\in {\textbf{C}}}$ indexed by a category ${\textbf{C}}$ ) correspond to predicate logic. As universal algebra gives foundations for algebraic propositional logic, so fibred universal algebra lays a foundation for algebraic predicate logic.

Definition 2 [Reference Galatos, Jipsen, Kowalski and Ono10]

$$ \begin{align*}(A,\otimes,\wedge,\vee,\backslash,/,1,0,\top,\bot)\end{align*} $$

is called an $\mathrm {FL}$ algebra iff

• • $(A,\otimes ,1)$ is a monoid $; 0$ is a (distinguished) element of $A;$

• • $(A,\wedge ,\vee ,\top ,\bot )$ is a bounded lattice, which induces a partial order $\leq $ on $A;$

• • for any $a\in A$ , $a\backslash (\mbox {-}):A\to A$ is a right adjoint of $a\otimes (\mbox {-}):A\to A:$ i.e., $a\otimes b \leq c \mbox { iff } b\leq a\backslash c$ for any $a,b,c\in A;$

• • for any $b\in A$ , $(\mbox {-})/ b:A\to A$ is a right adjoint of $(\mbox {-})\otimes b:A\to A:$ i.e., $a\otimes b \leq c \mbox { iff } a\leq c/ b$ for any $a,b,c\in A$ .

A homomorphism of $\mathrm {FL}$ algebras is defined as a map preserving all the operations $(\otimes ,\wedge ,\vee ,\backslash ,/,1,0,\top ,\bot )$ . ${\textbf{FL}}$ denotes the category of $\mathrm {FL}$ algebras and their homomorphisms.

Although $0$ is just a neutral element of A with no axiom, the rules for $0$ are automatically valid by the definition of interpretations defined below.

${\textbf{FL}}$ is an algebraic category (i.e., a category monadic over ${\textbf{Set}}$ ), or a variety in terms of universal algebra, since the two adjointness conditions can be rephrased by equations (see, e.g., Galatos–Jipsen–Kowalski–Ono [Reference Galatos, Jipsen, Kowalski and Ono10]). An axiomatic extension $\mathrm {FL}_X$ of $\mathrm {FL}$ corresponds to an algebraic full subcategory (or sub-variety) of ${\textbf{FL}}$ , denoted ${\textbf{FL}}_X$ (algebraicity follows from definability by axioms); this is the well-known, logic-variety correspondence for logics over $\mathrm {FL}$ (see Galatos–Jipsen–Kowalski–Ono [Reference Galatos, Jipsen, Kowalski and Ono10]).

Definition 3. An $\mathrm {FL}$ (Full Lambek) hyperdoctrine is an ${\textbf{FL}}$ -valued presheaf

$$ \begin{align*}P:{\textbf{ C}}^{\mathrm{op}}\to {\textbf{ FL}}\end{align*} $$

such that ${\textbf{C}}$ is a category with finite products, and the following conditions on quantifiers hold:

• • For any projection $\pi :X\times Y\to Y$ in ${\textbf{C}}$ , $P(\pi ):P(Y)\to P(X\times Y)$ has a right adjoint, denoted

  $$ \begin{align*}\forall_{\pi}:P(X\times Y)\to P(Y).\end{align*} $$
  And the corresponding Beck–Chevalley condition holds, i.e., the following diagram commutes for any arrow $f:Z\to Y$ in ${\textbf{C}} (\pi ':X\times Z\to Z$ below denotes a projection):
  

• • For any projection $\pi :X\times Y\to Y$ in ${\textbf{C}}$ , $P(\pi ):P(Y)\to P(X\times Y)$ has a left adjoint, denoted

  $$ \begin{align*}\exists_{\pi}:P(X\times Y)\to P(Y).\end{align*} $$
  The corresponding Beck–Chevalley condition holds:
  
  Furthermore, the Frobenius Reciprocity conditions hold: for any projection $\pi :X\times Y\to Y$ in ${\textbf{C}}$ , any $a\in P(Y)$ , and any $b\in P(X\times Y)$ ,
  $$ \begin{align*} a\otimes (\exists_{\pi}b) &= \exists_{\pi}(P(\pi)(a)\otimes b), \\ (\exists_{\pi}b)\otimes a &= \exists_{\pi}(b\otimes P(\pi)(a)). \end{align*} $$

For an axiomatic extension $\mathrm {FL}_X$ of $\mathrm {FL}$ , an $\mathrm {FL}_X$ hyperdoctrine is defined by restricting the value category ${\textbf{FL}}$ into ${\textbf{FL}}_X$ . An $\mathrm {FL} ($ resp. $\mathrm {FL}_X)$ hyperdoctrine is also called a fibred $\mathrm {FL} ($ resp. $\mathrm {FL}_X)$ algebra.

The category ${\textbf{C}}$ of an $\mathrm {FL}$ hyperdoctrine $P:{\textbf{C}}^{\mathrm {op}} \to {\textbf{FL}}$ is called its base category or type category, and P is also called its predicate functor; intuitively, $P(C)$ is the algebra of predicates on a type, or domain of discourse, C.

Note that, in the definition above, we need two Frobenius Reciprocity conditions due to the non-commutativity of $\mathrm {FL}$ algebras.

An $\mathrm {FL}$ hyperdoctrine may be seen as an indexed category, and thus as a fibration via the Grothendieck construction. Although we formulate everything in terms of indexed categories in this paper, we can do the same in terms of fibrations as well (working with indexed categories would probably be simpler to those who are not familiar with category theory). From a fibrational point of view, each $P(C)$ is called a fibre of an $\mathrm {FL}$ hyperdoctrine P.

The $\mathrm {FL}$ (resp. $\mathrm {FL}_X$ ) hyperdoctrine semantics for $\mathrm {TFL}$ (resp. $\mathrm {TFL}_X$ ) is defined as follows.

In the following, we show that the $\mathrm {FL}$ (resp. $\mathrm {FL}_X$ ) hyperdoctrine semantics is sound and complete for $\mathrm {TFL}$ (resp. $\mathrm {TFL}_X$ ). Let $[\kern -0.35pt[ \Phi \ [\Gamma ] ]\kern -0.35pt]$ denote

$$ \begin{align*}[\kern-0.35pt[ \varphi_1 \ [\Gamma] ]\kern-0.35pt] \otimes\cdots\otimes [\kern-0.35pt[ \varphi_n \ [\Gamma] ]\kern-0.35pt]\end{align*} $$

when $\Phi $ is $\varphi _1,\ldots ,\varphi _n$ .

Intuitively, an arrow f in ${\textbf{C}}$ is a term, and $P(f)$ is a substitution operation (this is exactly true in syntactic hyperdoctrines defined later); then, the Beck–Chevalley conditions and the functoriality of P tell us that substitution commutes with all the logical operations (namely, both propositional connectives and quantifiers). From such a logical point of view, the meaning of the Beck–Chevalley conditions is transparent; they just say that substitution after quantification is the same as quantification after substitution.

Proof Fix an $\mathrm {FL}$ or $\mathrm {FL}_X$ hyperdoctrine P and an interpretation $[\kern -0.35pt[ \mbox {-} ]\kern -0.35pt]$ in P. Initial sequents in context are satisfied because $a \leq a$ in any fibre $P(C)$ . The cut rule preserves satisfaction, since tensoring preserves $\leq $ and $\leq $ has transitivity. It is easy to verify that all the rules for the logical connectives preserve satisfaction.

Let us consider universal quantifier $\forall $ . To show the case of Rule $\forall R$ , assume that

$$ \begin{align*}[\kern-0.35pt[ \Phi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \leq [\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt]\end{align*} $$

in $P([\kern -0.35pt[ \sigma ]\kern -0.35pt] \times [\kern -0.35pt[ \Gamma ]\kern -0.35pt])$ . It then follows that

$$ \begin{align*}[\kern-0.35pt[ \Phi \ [x:\sigma,\Gamma] ]\kern-0.35pt] = P(\pi:[\kern-0.35pt[ \sigma ]\kern-0.35pt] \times [\kern-0.35pt[ \Gamma ]\kern-0.35pt] \to [\kern-0.35pt[ \Gamma ]\kern-0.35pt]) ([\kern-0.35pt[ \Phi \ [\Gamma] ]\kern-0.35pt]),\end{align*} $$

where $\pi $ is a projection in ${\textbf{C}}$ , and note that $\Phi $ does not include x among its free variables by the eigenvariable condition. We thus have

$$ \begin{align*}P(\pi)([\kern-0.35pt[ \Phi \ [\Gamma] ]\kern-0.35pt]) \leq [\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt].\end{align*} $$

Since $\forall _{\pi }:P([\kern -0.35pt[ \sigma ]\kern -0.35pt] \times [\kern -0.35pt[ \Gamma ]\kern -0.35pt] )\to P([\kern -0.35pt[ \Gamma ]\kern -0.35pt])$ is a right adjoint of $P(\pi )$ , it follows that

$$ \begin{align*}[\kern-0.35pt[ \Phi \ [\Gamma] ]\kern-0.35pt] \leq \forall_{\pi}([\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt]) =[\kern-0.35pt[ \forall x \varphi \ [\Gamma] ]\kern-0.35pt].\end{align*} $$

We next show the case of $\forall L$ . Assume that

$$ \begin{align*}[\kern-0.35pt[ \Phi_1 \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \Phi_2 \ [x:\sigma,\Gamma] ]\kern-0.35pt] \leq [\kern-0.35pt[ \psi \ [x:\sigma,\Gamma] ]\kern-0.35pt].\end{align*} $$

The adjunction condition for universal quantifier gives us

$$ \begin{align*}P(\pi)(\forall_{\pi}([\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt])) \leq [\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt],\end{align*} $$

where $\pi :[\kern -0.35pt[ \sigma ]\kern -0.35pt] \times [\kern -0.35pt[ \Gamma ]\kern -0.35pt] \to [\kern -0.35pt[ \Gamma ]\kern -0.35pt]$ is a projection. Yet we also have

$$ \begin{align*}P(\pi)(\forall_{\pi}([\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt])) =P(\pi)([\kern-0.35pt[ \forall x \varphi \ [\Gamma] ]\kern-0.35pt]) =[\kern-0.35pt[ \forall x \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt].\end{align*} $$

Since tensoring respects $\leq $ , these together imply that

$$ \begin{align*}[\kern-0.35pt[ \Phi_1 \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \forall x \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \Phi_2 \ [x:\sigma,\Gamma] ]\kern-0.35pt] \leq [\kern-0.35pt[ \psi \ [x:\sigma,\Gamma] ]\kern-0.35pt].\end{align*} $$

It remains to show the case of existential quantifier $\exists $ . In order to prove that Rule $\exists L$ preserves satisfaction, assume that

$$ \begin{align*}[\kern-0.35pt[ \Phi_1 \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \Phi_2 \ [x:\sigma,\Gamma] ]\kern-0.35pt] \leq [\kern-0.35pt[ \psi \ [x:\sigma,\Gamma] ]\kern-0.35pt].\end{align*} $$

This is equivalent to the following:

$$ \begin{align*}[\kern-0.35pt[ \Phi_1 \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \Phi_2 \ [x:\sigma,\Gamma] ]\kern-0.35pt] \leq P(\pi)([\kern-0.35pt[ \psi \ [\Gamma] ]\kern-0.35pt]),\end{align*} $$

where $\pi :[\kern -0.35pt[ \sigma ]\kern -0.35pt] \times [\kern -0.35pt[ \Gamma ]\kern -0.35pt] \to [\kern -0.35pt[ \Gamma ]\kern -0.35pt]$ is a projection. Since

$$ \begin{align*}\exists_{\pi}:P([\kern-0.35pt[ \sigma ]\kern-0.35pt] \times [\kern-0.35pt[ \Gamma ]\kern-0.35pt] )\to P([\kern-0.35pt[ \Gamma ]\kern-0.35pt])\end{align*} $$

is left adjoint to $P(\pi )$ , it follows that

$$ \begin{align*}\exists_{\pi}([\kern-0.35pt[ \Phi_1 \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \Phi_2 \ [x:\sigma,\Gamma] ]\kern-0.35pt]) \leq [\kern-0.35pt[ \psi \ [\Gamma] ]\kern-0.35pt].\end{align*} $$

This is equivalent to the following:

$$ \begin{align*}\exists_{\pi}(\ P(\pi)([\kern-0.35pt[ \Phi_1 \ [\Gamma] ]\kern-0.35pt]) \otimes [\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \otimes P(\pi)([\kern-0.35pt[ \Phi_2 \ [\Gamma] ]\kern-0.35pt])\ ) \leq [\kern-0.35pt[ \psi \ [\Gamma] ]\kern-0.35pt].\end{align*} $$

Repeated applications of the two Frobenius Reciprocity conditions give us

$$ \begin{align*}[\kern-0.35pt[ \Phi_1 \ [\Gamma] ]\kern-0.35pt] \otimes \exists_{\pi}([\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt]) \otimes [\kern-0.35pt[ \Phi_2 \ [\Gamma] ]\kern-0.35pt] \leq [\kern-0.35pt[ \psi \ [\Gamma] ]\kern-0.35pt].\end{align*} $$

Then we finally have the following:

$$ \begin{align*}[\kern-0.35pt[ \Phi_1 \ [\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \exists x \varphi \ [\Gamma] ]\kern-0.35pt] \otimes [\kern-0.35pt[ \Phi_2 \ [\Gamma] ]\kern-0.35pt] \leq [\kern-0.35pt[ \psi \ [\Gamma] ]\kern-0.35pt].\end{align*} $$

To show the case of $\exists R$ , assume that

$$ \begin{align*}[\kern-0.35pt[ \Phi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \leq [\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt].\end{align*} $$

The adjunction condition for existential quantifier tells us that

$$ \begin{align*}[\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \leq P(\pi)(\exists_{\pi}([\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt])),\end{align*} $$

where $\pi :[\kern -0.35pt[ \sigma ]\kern -0.35pt] \times [\kern -0.35pt[ \Gamma ]\kern -0.35pt] \to [\kern -0.35pt[ \Gamma ]\kern -0.35pt]$ is a projection. We thus have the following:

$$ \begin{align*}[\kern-0.35pt[ \Phi \ [x:\sigma,\Gamma] ]\kern-0.35pt] \leq P(\pi)(\exists_{\pi}([\kern-0.35pt[ \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt])) =[\kern-0.35pt[ \exists x \varphi \ [x:\sigma,\Gamma] ]\kern-0.35pt].\end{align*} $$

This completes the proof.⊣

Syntactic hyperdoctrines are then defined as follows towards the goal of proving completeness. They are the hyperdoctrinal categorificaton of Lindenbaum–Tarski algebras.

Definition 6. The syntactic hyperdoctrine of $\mathrm {TFL}$ is defined as follows $;$ that of $\mathrm {TFL}_X$ is defined by replacing ${\textbf{FL}}$ and $\mathrm {TFL}$ below with ${\textbf{FL}}_X$ and $\mathrm {TFL}_X$ .

We first define the base category ${\textbf{C}}$ . An object in ${\textbf{C}}$ is a context $\Gamma $ up to $\alpha $ -equivalence (i.e., the naming of variables does not matter). An arrow in ${\textbf{C}}$ from an object $\Gamma $ to another $\Gamma ' $ is a list of terms $[t_1,\ldots ,t_n]$ (up to equivalence) such that $t_1:\sigma _1\ [\Gamma ],\ldots ,t_n:\sigma _n\ [\Gamma ]$ where $\Gamma '$ is supposed to be $x_1:\sigma _1,\ldots ,x_n:\sigma _n$ .

The syntactic hyperdoctrine $P:{\textbf{C}}^{\mathrm {op}}\to {\textbf{FL}}$ is then defined in the following way. For an object $\Gamma $ in ${\textbf{C}}$ , let

$$ \begin{align*}\mathrm{Form}_{\Gamma} = \{ \varphi \ | \ \varphi \mbox{ is a formula in context } \Gamma \}.\end{align*} $$

Define an equivalence relation $\sim $ on $\mathrm {Form}_{\Gamma }$ as follows: for $\varphi ,\psi \in \mathrm {Form}_{\Gamma }$ , $\varphi \sim \psi $ iff both $\varphi \vdash \psi \ [\Gamma ]$ and $\psi \vdash \varphi \ [\Gamma ]$ are deducible in $\mathrm {TFL}$ . We then define

$$ \begin{align*}P(\Gamma)=\mathrm{Form}_{\Gamma}{/}{\sim}\end{align*} $$

with an $\mathrm {FL}$ algebra structure induced by the logical connectives.

The arrow part of P is defined as follows. Let $[t_1,\ldots ,t_n]:\Gamma \to \Gamma '$ be an arrow in ${\textbf{C}}$ where $\Gamma '$ is $x_1:\sigma _1,\ldots ,x_n:\sigma _n$ . Then we define $P([t_1,\ldots ,t_n]):P(\Gamma ')\to P(\Gamma )$ by

$$ \begin{align*}P([t_1,\ldots,t_n])(\varphi)=\varphi[t_1/x_1,\ldots,t_n/x_n],\end{align*} $$

where it is supposed that $t_1:\sigma _1 \ [\Gamma ],\ldots ,t_n:\sigma _n \ [\Gamma ]$ , and that $\varphi $ is a formula in context $x_1:\sigma _1,\ldots ,x_n:\sigma _n$ .

Intuitively, $P(\Gamma )$ above is a Lindenbaum–Tarski algebra sliced with respect to each $\Gamma $ . It is straightforward to verify that the operations of $P(\Gamma )$ above are well defined, and $P(\Gamma )$ forms an $\mathrm {FL}$ algebra. We still have to check that P defined above is a hyperdoctrine; this is done in the following lemma.

Proof Since substitution commutes with all the logical connectives, $P([t_1,\ldots ,t_n])$ defined above is always a homomorphism of $\mathrm {FL}$ algebras. Thus, P is a contravariant functor.

We have to verify that the base category ${\textbf{C}}$ has finite products, or equivalently, binary products. For objects $\Gamma ,\Gamma '$ in ${\textbf{C}}$ , we define their product $\Gamma \times \Gamma '$ as follows. Suppose that $\Gamma $ is $x_1:\sigma _1,\ldots ,x_n:\sigma _n$ , and $\Gamma '$ is $y_1:\tau _1,\ldots ,y_m:\tau _m$ . Then, $\Gamma \times \Gamma '$ is defined as

$$ \begin{align*}x_1:\sigma_1,\ldots,x_n:\sigma_n,y_1:\tau_1,\ldots,y_m:\tau_m.\end{align*} $$

An associated projection $\pi :\Gamma \times \Gamma '\to \Gamma '$ is defined as

$$ \begin{align*}[y_1,\ldots,y_m]:\Gamma\times \Gamma'\to \Gamma',\end{align*} $$

where the context of each $y_i$ is taken to be $x_1:\sigma _1,\ldots ,x_n:\sigma _n,y_1:\tau _1,\ldots ,y_m:\tau _m$ (rather than $y_1:\tau _1,\ldots ,y_m:\tau _m$ ). The other projection is defined in a similar way. It is easily verified that these indeed form a categorical product in ${\textbf{C}}$ .

In order to show that P has quantifier structures, let $\pi :\Gamma \times \Gamma ' \to \Gamma '$ denote the projection in ${\textbf{C}}$ defined above, and then consider $P(\pi )$ , which we have to show has right and left adjoints. The right and left adjoints of $P(\pi )$ can be constructed as follows. Recall $\Gamma $ is $x:\sigma _1,\ldots ,x_n:\sigma _n$ . Let $\varphi \in P(\Gamma \times \Gamma ' )$ ; here we are identifying $\varphi $ with the equivalence class to which $\varphi $ belongs, since every argument below respects the equivalence. Then define $\forall _{\pi }:P(\Gamma \times \Gamma ' )\to P(\Gamma ' )$ by

$$ \begin{align*}\forall_{\pi}(\varphi)=\forall x_1 ... \forall x_n \varphi,\end{align*} $$

where the formula on the right-hand side actually denotes the corresponding equivalence class. Similarly, we define $\exists _{\pi }:P(\Gamma \times \Gamma ' )\to P(\Gamma ' )$ by

$$ \begin{align*}\exists_{\pi}(\varphi)=\exists x_1 ... \exists x_n \varphi.\end{align*} $$

Let us show that $\forall _{\pi }$ is the right adjoint of $P(\pi )$ . We first assume $P(\pi )(\psi ) \leq \varphi $ in $P(\Gamma \times \Gamma ' )$ for $\psi \in P(\Gamma ')$ and $\varphi \in P(\Gamma \times \Gamma ' )$ . Then it follows from the definition of P and $\pi $ that

$$ \begin{align*}P(\pi)(\psi \ [\Gamma]) = \psi \ [\Gamma,\Gamma'],\end{align*} $$

where we are making explicit the two different contexts of $\psi $ ; the role of $P(\pi )$ just lies in changing contexts. Since the $\leq $ of $P(\Gamma \times \Gamma ' )$ is induced by its lattice structure, we have $\varphi \wedge \psi = \psi $ . It follows from the definition of $P(\Gamma \times \Gamma ' )$ that $\varphi \wedge \psi \vdash \psi \ [\Gamma ,\Gamma ']$ and $\psi \vdash \varphi \wedge \psi \ [\Gamma ,\Gamma ']$ are deducible in $\mathrm {TFL}$ (resp. $\mathrm {TFL}_X$ ), whence $\psi \vdash \varphi \ [\Gamma ,\Gamma ']$ is deducible as well. By repeated applications of rule $\forall R$ , it follows that

$$ \begin{align*}\psi \vdash \forall x_1...\forall x_n\varphi \ [\Gamma']\end{align*} $$

is deducible. This implies that both $\psi \vdash \psi \wedge \forall x_1...\forall x_n\varphi \ [\Gamma ']$ and $\psi \wedge \forall x_1...\forall x_n\varphi \vdash \psi \ [\Gamma ']$ are deducible, whence $\psi \leq \forall x_1...\forall x_n\varphi $ in $P(\Gamma ')$ .

We show the converse. Assume that $\psi \leq \forall x_1...\forall x_n\varphi $ in $P(\Gamma ')$ . By arguing as in the above,

$$ \begin{align*}\psi \vdash \forall x_1...\forall x_n\varphi \ [\Gamma']\end{align*} $$

is deducible. By enriching the context,

$$ \begin{align*}\psi \vdash \forall x_1...\forall x_n\varphi \ [\Gamma,\Gamma']\end{align*} $$

is deducible. Since

$$ \begin{align*}\forall x_1...\forall x_n\varphi \vdash \varphi \ [\Gamma,\Gamma']\end{align*} $$

is deducible by rule $\forall L$ , the cut rule tells us that $\psi \vdash \varphi \ [\Gamma ,\Gamma ']$ is deducible; note that the contexts of two sequents-in-context must be the same when applying the cut rule to them. It finally follows that $P(\pi )(\psi ) \leq \varphi $ in $P(\Gamma \times \Gamma ' )$ . Thus, $\forall _{\pi }$ is the right adjoint of $P(\pi )$ . Similarly, $\exists _{\pi }$ can be shown to be the left adjoint of $P(\pi )$ .

The Beck–Chevalley condition for $\forall $ can be verified as follows. Let $\varphi \in P(\Gamma \times \Gamma ')$ , $\pi :\Gamma \times \Gamma '\to \Gamma '$ a projection in ${\textbf{C}}$ , and $\pi ':\Gamma \times \Gamma ''\to \Gamma ''$ another projection in ${\textbf{C}}$ for objects $\Gamma ,\Gamma ',\Gamma ''$ in ${\textbf{C}}$ . Then, we have

$$ \begin{align*}P([t_1,\ldots,t_n])\circ \forall_{\pi}(\varphi)=(\forall x_1...\forall x_n \varphi) [t_1/y_1,\ldots,t_n/y_m],\end{align*} $$

where it is supposed that $\Gamma $ is $x_1:\sigma _1,\ldots ,x_n:\sigma _n$ , $\Gamma '$ is $y_1:\tau _1,\ldots ,y_m:\tau _m$ , and $t_1:\tau _1\ [\Gamma ''], ..., t_m:\tau _m \ [\Gamma '']$ . We also have the following:

$$ \begin{align*}\forall_{\pi'}\circ P( [t_1,\ldots,t_n])(\varphi)= \forall x_1...\forall x_n (\varphi [t_1/y_1,\ldots,t_n/y_m]).\end{align*} $$

The Beck–Chevalley condition for $\forall $ thus follows. The Beck–Chevalley condition for $\exists $ can be verified in a similar way. The two Frobenius Reciprocity conditions for $\exists $ follow immediately from Lemma 1.⊣

The syntactic hyperdoctrine is a free or classifying hyperdoctrine; it is the combination of the classifying category ${\textbf{C}}$ and the free algebras $P(\Gamma )$ ’s.

Now, there is the obvious, canonical interpretation of $\mathrm {TFL}$ (resp. $\mathrm {TFL}_X$ ) in the syntactic hyperdoctrine of $\mathrm {TFL}$ (resp. $\mathrm {TFL}_X$ ); it is straightforward to see:

The lemmata above give us the completeness result: If $\Phi \vdash \psi \ [\Gamma ]$ is satisfied in any interpretation in any $\mathrm {FL}$ (resp. $\mathrm {FL}_X$ ) hyperdoctrine, then it is deducible in $\mathrm {TFL}$ (resp. $\mathrm {TFL}_X$ ). Combining soundness and completeness, we obtain:

Let us finally give set-theoretical examples of hyperdoctrines and remark on what set-theoretical semantics look like in light of the hyperdoctrinal approach to semantics.

Any complete $\mathrm {FL}$ algebra yields an $\mathrm {FL}$ hyperdoctrine as a contravariant $\mathrm {Hom}$ functor into the algebra in the following way:

Proposition 10. Let $\Omega \in {\mathbf{FL}}$ with $\Omega $ being complete. Then,

$$ \begin{align*}\mathrm{Hom}_{\mathbf{Set}}(\mbox{-},\Omega):{\mathbf{Set}}^{\mathrm{op}}\to {\mathbf{FL}} \mbox{(resp.}\ {\mathbf{FL}}_X\mbox{)}\end{align*} $$

is an $\mathrm {FL} ($ resp. $\mathrm {FL}_X)$ hyperdoctrine.

Proof Let $\pi :X\times Y\to Y$ be a projection in ${\textbf{Set}}$ . We define $\forall _{\pi }$ and $\exists _{\pi }$ as follows: given $v\in \mathrm {Hom}(X\times Y,\Omega )$ and $y\in Y$ , let

$$ \begin{align*}\forall_{\pi}(v)(y) := \bigwedge \{ v(x,y) \ | \ x\in X \}\end{align*} $$

and

$$ \begin{align*}\exists_{\pi}(v)(y) := \bigvee \{ v(x,y) \ | \ x\in X \}.\end{align*} $$

These morphisms give the required quantifier structures satisfying the Beck–Chevalley and Frobenius Reciprocity properties.⊣

If $\Omega $ is the two element Boolean algebra, the functor above comes down to the contravariant powerset functor, the hyperdoctrinal interpretation with which amounts to the standard Tarski semantics of classical logic. So the hyperdoctrinal semantics may be seen as a vast generalisation of the classic Tarski semantics.

The above hyperdoctrine and corresponding semantics may be regarded as the $\Omega $ -valued powerset functor and $\Omega $ -valued semantics, respectively; this is related to algebra-valued models of set theory as we shall remark in the concluding section below. The $\Omega $ -valued semantics of substructural logic have been developed essentially in the context of algebraic substructural logic, independently of any categorical semantics (see, e.g., Ono [Reference Ono33, Reference Ono34]); yet the hyperdoctrinal semantics even encompass those semantics.

The algebraic completeness of algebras $\Omega $ actually prevents us from proving the logical completeness of the semantics with respect to those complete algebras. To be precise, assuming completeness prevents us from obtaining completeness for any axiomatic extension $\mathrm {TFL}_X$ of $\mathrm {TFL}$ ; such incompleteness phenomena have been observed in various settings (see, e.g., Ono [Reference Ono33]). Yet at the same time, if $\Omega $ is not complete, in general, $\mathrm {Hom}_{\textbf{Set}}(\mbox {-},\Omega )$ cannot interpret quantifiers; this is because $\forall $ and $\exists $ in $\mathrm {Hom}_{\textbf{Set}}(\mbox {-},\Omega )$ are actually infinitary meets and joins in $\Omega $ . In algebraic predicate logic, thus, the notion of safe valuations has been applied in order to address this issue; yet they require ad hoc constraints to interpret quantifiers in non-complete algebras (see, e.g., Ono [Reference Ono34]). If we restrict the hyperdoctrine semantics to the $\Omega $ -valued models $\mathrm {Hom}_{\textbf{Set}}(\mbox {-},\Omega )$ , we can encounter the same problem, and we do need the same, safe valuation technique to show the completeness theorem with respect to those models. Yet from a categorical point of view, there is no a priori reason to stick to set-theoretical models, and in the general hyperdoctrinal setting as above, completeness comes for free (i.e., without any cost of ad hoc manipulations) via the syntactic hyperdoctrine construction, just as completeness holds for free in algebraic propositional logic via the Lindenbaum–Tarski algebra construction. This would suggest that hyperdoctrines or fibred algebras give the right notion of algebras of predicate logic that directly extend the salient features of algebraic propositional logic; there is, to the best of the author’s knowledge, no other such concept of algebras of predicate logic that works for a broad variety of logical systems in a uniform and modular manner.

The above functor is actually part of a dual adjunction: given $\Omega \in {\textbf{FL}}$ , the following dual adjunction holds between ${\textbf{Set}}$ and ${\textbf{FL}}$ , induced by $\Omega $ as a dualising object:

$$ \begin{align*}\mathrm{Hom}_{\textbf{ FL}}(\mbox{-},\Omega)^{\mathrm{op}} \dashv \mathrm{Hom}_{\textbf{ Set}}(\mbox{-},\Omega):{\textbf{ Set}}^{\mathrm{op}}\to {\textbf{ FL}}.\end{align*} $$

As this example suggests, hyperdoctrines tend to arise from the predicate functor parts of dual adjunctions induced by dualising objects. The dual adjunction between frames and topological spaces (see Johnstone [Reference Johnstone17]) gives a hyperdoctrine for geometric predicate logic; likewise, the dual adjunction between convex algebras and convex spaces as in [Reference Maruyama25] gives a hyperdoctrine for convex geometric logic. Coalgebraic dualities as in [Reference Kupke, Kurz and Venema19, Reference Maruyama26] give hyperdoctrines for modal predicate logics. There could be a systematic study of these phenomena at the interface of duality theory and categorical logic. In general, categorical dualities for propositional logics (see, e.g., [Reference Maruyama27, Reference Maruyama30]) often give hyperdoctrinal models of the predicate logics that extend them with typed quantifiers (as studied in [Reference Maruyama29]).

4 Hyperdoctrinal Lawvere–Tierney topology as Girard and Kolmogorov translation

In the hyerdoctrinal setting, type theories are categories, logics over them are functors, and logical translations between them are natural transformations; we elaborate on this idea in the present section, introducing the generalised notion of Lawvere–Tierney topologies and cotopologies on hyperdoctrines (rather than toposes), which allow for a uniform treatment of logical translations, such as the Kolmogorov’s double negation translation and the Girard’s exponential translation as we shall see below.

In the following, HA and BA denote the category of Heyting algebras and the category of Boolean algebras, respectively. $\mathrm {IL}$ and $\mathrm {CL}$ hyperdoctrines are defined as $\mathrm {FL}$ hyperdoctrines with values in HA and BA, respectively. Note that both $\mathrm {IL}$ and $\mathrm {CL}$ hyperdoctrines are $\mathrm {FL}_X$ hyperdoctrines for suitable sets of axioms X.

Given a Heyting algebra, the fixpoints of double negation, namely those elements that validate the double negation elimination, form a Boolean algebra; this is an algebraic version of the Kolmogorov translation between intuitionistic and classical propositional logics. In the following, we explore how this extends to predicate logics and hyperdoctrines through the concept of Lawvere–Tierney topologies and cotopologies, which give a unifying perspective on different logical translations. In particular, exponential ! is understood as a Lawvere–Tierney cotopology on substructural hyperdoctrines.

Lawvere–Tierney topologies originally come from topos theory, and they induce topologies on hyperdoctrines (this is just for motivating the following discussion, which itself does not require any substantial knowledge of topos theory): given a topos ${\textbf{C}}$ with a subobject classifier $\Omega $ , a Lawvere–Tierney topology on $\Omega $ corresponds to a natural transformation on the subobject hyperdoctrine $\mathrm {Sub}: {\textbf{C}}\to {\textbf{HA}}$

$$ \begin{align*}j:\mathrm{Sub}_{\textbf{ C}}(\mbox{-})\to \mathrm{Sub}_{\textbf{ C}}(\mbox{-})\end{align*} $$

such that $j_C$ is a closure operator on $\mathrm {Sub}_{\textbf{C}}(C)$ for every $C\in {\textbf{C}}$ (see, e.g., Jacobs [Reference Jacobs16]). Having this correspondence in mind, let us define the concept of Lawvere–Tierney topologies and cotopologies on hyperdoctrines in the following manner, which allow us to capture different logical translations uniformly in the general hyperdoctrinal setting.

Definition 11. For an $\mathrm {FL}$ hyperdoctrine $P:{\textbf{C}}^{\mathrm {op}}\to {\textbf{FL}}$ , a Lawvere–Tierney topology on P is a natural transformation

$$ \begin{align*}j:P \to P\end{align*} $$

such that

$$ \begin{align*}j_C:P(C)\to P(C)\end{align*} $$

is a closure operator on $P(C)$ for each $C\in {\textbf{C}}$ . We also call a Lawvere–Tierney topology a Lawvere–Tierney operator.

Dually, a Lawvere–Tierney cotopology (or co-operator) for P is a natural transformation

$$ \begin{align*}j:P \to P\end{align*} $$

such that

$$ \begin{align*}j_C:P(C)\to P(C)\end{align*} $$

is an interior operator on $P(C)$ for each $C\in {\textbf{C}}$ .

Examples we are going to discuss below would clarify what the definition above means in logical contexts. The above transformation j on the subobject hyperdoctrine $\mathrm {Sub}: {\textbf{C}}\to {\textbf{HA}}$ of a topos, of course, forms a Lawvere–Tierney topology on $\mathrm {Sub}$ .

Let us introduce intuitionistic linear logic with exponential $!$ , which allows us to have control over structural rules and simulate intuitionistic logic within linear logic. An exponential $!$ on an $\mathrm {FL}$ algebra A is defined in algebraic terms as follows (see Coumans–Gehrke–Rooijen [Reference Coumans, Gehrke and van Rooijen7]):

Note that the above definition of Lawvere–Tierney topologies and cotopologies obviously generalises to $\mathrm {ILL}$ hyperdoctrines, i.e., just by replacing ${\textbf{FL}}$ with ${\textbf{FL}}^{!}_e$ in the above definition.

The exponential operation ! induces a Lawvere–Tierney cotopology on an $\mathrm {ILL}$ hyperdoctrine $P:{\textbf{C}}^{\mathrm {op}}\to {\textbf{FL}}^!_e$ : that is, ! can naturally be considered as a natural transformation

$$ \begin{align*}!:P \to P\end{align*} $$

such that

$$ \begin{align*}!_C(a)=!a\end{align*} $$

for any $C\in {\textbf{C}}$ and $a\in P(C)$ . The naturality condition in the definition of Lawvere–Tierney cotopologies means that the following diagram commutes: given $f:C\to D$ ,

The diagram above indeed commutes because the following hold:

$$ \begin{align*}!P(f)(x)=P(f)(!x),\end{align*} $$

where note that $P(f)$ is a homomorphism. In addition to this,

$$ \begin{align*}!_C:P(C)\to P(C)\end{align*} $$

is an interior operator on $P(C)$ , and thus we have verified the following:

Another example of Lawvere–Tierney topology is the double negation topology. Just in the same way as above, the double negation operation $\neg \neg $ in Heyting algebras yields a Lawvere–Tierney topology $\neg \neg : P\to P$ on an intuitionistic hyperdoctrine $P:{\textbf{C}}^{\mathrm {op}}\to {\textbf{HA}}$ .

Given a Lawvere–Tierney (co)topology j on a hyperdoctrine, we can construct another functor $P_j$ in the following manner:

Proposition 14. A Lawvere–Tierney (co)topology j on a given ${\mathbf{FL}}$ or ${\mathbf{FL}}^!_e$ hyperdoctrine P induces another functor $P_j$ such that

$$ \begin{align*}P_j(C)=\{ j_C(x) \ | \ x \in P(C) \}\end{align*} $$

and

$$ \begin{align*}P_j(f:C\to D)(x)=P(f)(x),\end{align*} $$

which is well defined as a functor. In particular, $P(f)(x)$ is an element of $P_j(C)$ .

Proof This follows from the naturality of the Lawvere–Tierney (co)topology j: there is some $y\in P(D)$ such that $x=j_D(y)$ , and the naturality of transformation j gives us

$$ \begin{align*}P(f)(x)=P(f)(j_D(y))=j_C(P(f)(y)),\end{align*} $$

and $j_C(P(f)(y))$ is an element of $P_j(C)$ .⊣

Note that $P_j$ amounts to taking the fixpoints of j with respect to each C, since $j_C$ is a closure or interior operator, and therefore idempotent in either case.

By the proposition above, the double negation Lawvere–Tierney topology $\neg \neg $ on an intuitionistic hyperdoctrine $P:{\textbf{C}}^{\mathrm {op}}\to {\textbf{HA}}$ induces a functor

$$ \begin{align*}P_{\neg \neg}: {\textbf{ C}}^{\mathrm{op}}\to {\textbf{ BA}},\end{align*} $$

where note that $P_{\neg \neg }(C)$ forms a Boolean algebra because the elements of $P_{\neg \neg }(C)$ are classical propositions, i.e., those elements that validate the double negation elimination. Likewise, the exponential Lawvere–Tierney cotopology $!$ on a substructural hyperdoctrine $P:{\textbf{C}}^{\mathrm {op}}\to {\textbf{FL}}^!_e$ induces a functor

$$ \begin{align*}P_!: {\textbf{ C}}^{\mathrm{op}}\to {\textbf{ HA}},\end{align*} $$

where note that $P_!(C)$ forms a Heyting algebra because the elements of $P_!(C)$ are structural propositions, i.e., those admitting the structural rules. Furthermore, in the following, we show that $P_{\neg \neg }$ and $P_!$ are actually intuitionistic and classical hyperdoctrines, respectively.

Theorem 15. Let $P:{\mathbf{C}}^{\mathrm {op}}\to {\mathbf{FL}}^{!}_e$ be an $\mathrm {ILL}$ hyperdoctrine. Then, the following functor induced by the exponential Lawvere–Tierney cotopology $!$ on P

$$ \begin{align*}P_!:{\mathbf{C}}^{\mathrm{op}}\to {\mathbf{HA}}\end{align*} $$

forms an $\mathrm {IL}$ hyperdoctrine: i.e., it has the quantifier structure as required.

Proof Let us fix a projection $\pi :C\times D\to D$ . We have to prove that

$$ \begin{align*}P_!(\pi):P_!(D)\to P_!(C\times D)\end{align*} $$

has both right and left adjoints. By the adjoint functor theorem, it suffices to show that $P_!(\pi )$ preserves limits and colimits, namely infimums and supremums in the present case. Let us first prove that it preserves infimums. To show this, suppose that

$$ \begin{align*}\bigwedge \{ x_i \ | \ i\in I \} \in P_!(D),\end{align*} $$

for $x_i\in P_!(D)$ . It then holds that $!x_i=x_i$ and $!\bigwedge \{ x_i \ | \ i\in I \}=\bigwedge \{ x_i \ | \ i\in I \},$ since any element of $P_!(D)$ is a fixpoint of the exponential operation $!$ . We then have

$$ \begin{align*} P_!(\pi)(\bigwedge \{ x_i \ | \ i\in I \} ) &= P_!(\pi)(!\bigwedge \{ x_i \ | \ i\in I \} ) \\ &= P(\pi)(!\bigwedge \{ x_i \ | \ i\in I \} ) \\ &=\ !\bigwedge \{ P(\pi)(x_i) \ | \ i\in I \} \\ &=\ !\bigwedge \{ P_!(\pi)(x_i) \ | \ i\in I \} \\ &= \bigwedge \{ P_!(\pi)(x_i) \ | \ i\in I \}. \end{align*} $$

The last equality holds because $!\bigwedge ( \{ P_!(\pi )(x_i) \ | \ i\in I \} )$ is actually the infimum of $P_!(\pi )(x_i)$ ’s in $P_!(C\times D)$ , which can be verified in the following way. We first have

$$ \begin{align*}!\bigwedge \{ P_!(\pi)(x_i) \ | \ i\in I \} \leq P_!(\pi)(x_i),\end{align*} $$

for any $i\in I$ , since $!x_i=x_i$ and $P_!(\pi )$ preserves $!$ . Suppose that there is some $z\in P_!(C\times D)$ such that $z\leq P_!(\pi )(x_i)$ for any $i\in I$ . Then we have got $!z=z$ and

$$ \begin{align*}z\leq \bigwedge \{ P_!(\pi)(x_i) \ | \ i\in I \},\end{align*} $$

which implies that

$$ \begin{align*}z=!z\leq ! \bigwedge \{ P_!(\pi)(x_i) \ | \ i\in I \}.\end{align*} $$

This means that $!\bigwedge ( \{ P_!(\pi )(x_i) \ | \ i\in I \} )$ is the infimum of $P_!(\pi )(x_i)$ ’s. We have thus shown that $P_!(\pi )$ preserves limits. The case of colimits can be verified in the same way.⊣

This is an analogue of the Girard translation formulated in terms of hyperdoctrines and Lawvere–Tierney (co)topology. The above theorem is more general than Girard’s translation theorem in the sense that the latter corresponds to the case of syntactic hyperdoctrines in the former. Although in this paper we do not explicitly discuss substructural logics enriched with modalities and their hyperdoctrinal semantics, nevertheless, our methods work for them as well, yielding the corresponding soundness and completeness results in terms of hyperdoctrines with values in $\mathrm {FL}$ algebras with modalities; Girard’s exponential $!$ is just a special case.

Now, the double negation translation version is as follows.

Theorem 16. Let $P:{\mathbf{C}}^{\mathrm {op}}\to {\mathbf{HA}}$ be an $\mathrm {IL}$ hyperdoctrine. Then, the following functor induced by the double negation Lawvere–Tierney topology $\neg \neg $ on P

$$ \begin{align*}P_{\neg\neg}:{\mathbf{C}}^{\mathrm{op}}\to {\mathbf{HA}}\end{align*} $$

forms an $\mathrm {CL}$ hyperdoctrine: i.e., it has the quantifier structure as required.

Proof The argument to show this is mostly the same as above. Fix a projection $\pi :C\times D\to D$ . We prove that

$$ \begin{align*}P_{\neg\neg}(\pi):P_{\neg\neg}(D)\to P_{\neg\neg}(C\times D)\end{align*} $$

has both right and left adjoints. It suffices to show that $P_{\neg \neg }(\pi )$ preserves limits and colimits. To show that it preserves limits, suppose

$$ \begin{align*}\bigwedge \{ x_i \ | \ i\in I \} \in P_{\neg\neg}(D),\end{align*} $$

for $x_i\in P_{\neg \neg }(D)$ . It then holds that $\neg \neg x_i=x_i$ and ${\neg \neg }\bigwedge \{ x_i \ | \ i\in I \}=\bigwedge \{ x_i \ | \ i\in I \}$ . We then have

$$ \begin{align*} P_{\neg\neg}(\pi)(\bigwedge \{ x_i \ | \ i\in I \} ) &= P(\pi)(\neg\neg \bigwedge \{ x_i \ | \ i\in I \} ) \\ &= \neg\neg \bigwedge \{ P(\pi)(x_i) \ | \ i\in I \} \\ &= \bigwedge \{ P_{\neg\neg}(\pi)(x_i) \ | \ i\in I \}. \end{align*} $$

The preservation of colimits can be shown in the same way.⊣

While the double negation topology in topos theory is concerned with (theories over) higher-order logic, the above translation theorem is for (theories over) first-order logic in general; there is no similar result known for Heyting categories or logoses, the first-order version of toposes. Note that intuitionistic hyperdoctrines and Heyting categories are linked with each other via the subobject hyperdoctrine functor and the partial equivalence category functor (which is the first-order version of the tripos-to-topos construction); the above theorem, thus, can be recast in terms of Heyting categories, though the hyperdoctrinal formulation appears more natural.

Let us finally remark on the naturality condition of Lawvere–Tierney topology on hyperdoctrines. From a logical point of view, the naturality condition means that the operator j commutes with substitution of terms for variables. Let us, for example, consider the syntactic hyperdoctrine for intuitionistic predicate logic

$$ \begin{align*}P:{\textbf{ C}}^{\mathrm{op}}\to {\textbf{ HA}}.\end{align*} $$

Recall that an object of ${\textbf{C}}$ is a collection of typed variables, and an arrow of ${\textbf{C}}$ is a term. Then, P maps a collection of variables $x_1,\ldots ,x_n$ to the Heyting algebra of formulas $\varphi (x_1,\ldots ,x_n)$ with those variables, and $P(t)$ is the substitution of t for variables concerned. The double negation Lawvere–Tierney topology on the hyperdoctrine P is indeed a natural transformation because substitution commutes with double negation:

$$ \begin{align*}(\neg \neg \varphi)[t/x]=\neg \neg (\varphi [t/x]).\end{align*} $$

Extending Lawvere hyperdoctrines to a substructural setting, thus, we can give a uniform treatment of different logical translations through the concept of Lawvere–Tierney topologies and cotopologies on hyperdoctrines.

5 Concluding remarks

We have developed the hyperdoctrinal or fibred algebraic theory of substructural predicate logics, and given a uniform understanding of logical translation theorems on the basis of Lawvere–Tierney topologies and cotopologies on them. Let us finally comment upon further directions of research.

5.2 Algebra-valued models of set theory and consistency problems on substructural set theory

Another potential application could be found in set theory, just as intuitionistic hyperdoctrines yield Heyting-valued models of set theory via the tripos-to-topos construction originally due to Hyland–Johnstone–Pitts [Reference Hyland, Johnstone and Pitts14]. We can reformulate it in the present context of $\mathrm {FL}$ hyperdoctrines. To do this, we work in the internal logic of $\mathrm {FL}$ hyperdoctrines $P:{\textbf{C}}^{\mathrm {op}}\to {\textbf{FL}}$ : i.e., we have types X and function symbols f corresponding to objects X and arrows f in ${\textbf{C}}$ respectively, and also those predicate symbols R on a type $C \in {\textbf{C}}$ that correspond to elements $R\in P(C)$ .

We can then define a category ${\textbf{T}}[P]$ as follows. An object of ${\textbf{T}}[P]$ is a partial equivalence relation, i.e., a pair

$$ \begin{align*}(X,E_X)\end{align*} $$

such that X is an object in the base category ${\textbf{C}}$ , and $E_X$ is an element of $P(X\times X)$ and is symmetric and transitive in the internal logic of P:

$$ \begin{align*}E_X(x,y)\vdash E_X(y,x) \ [x,y:X]\end{align*} $$

and

$$ \begin{align*}E_X(x,y),E_X(y,z) \vdash E_X(x,z) \ [x,y,z:X].\end{align*} $$

An arrow from $(X,E_X)$ to $(Y,E_Y)$ is then defined as $F\in P(X\times Y)$ such that (i) extensionality:

$$ \begin{align*}E_X(x_1,x_2), E_Y(y_1,y_2), F(x_1,y_1)\vdash F(x_2,y_2) \ [x_1,x_2:X,y_1,y_2:Y];\end{align*} $$

(ii) strictness:

$$ \begin{align*}F(x,y)\vdash E_X(x,x) \wedge E_Y(y,y) \ [x:X,y:Y];\end{align*} $$

(iii) single-valuedness:

$$ \begin{align*}F(x,y_1), F(x,y_2)\vdash E_Y(y_1,y_2) \ [x:X,y_1,y_2:Y];\end{align*} $$

(iv) totality:

$$ \begin{align*}E_X(x,x)\vdash \exists y \ F(x,y) \ [x:X].\end{align*} $$

Such an F is called a functional relation.

Now, if $\Omega $ is a locale,

$$ \begin{align*}{\textbf{ T}}[\mathrm{Hom}_{\textbf{ Set}}(\mbox{-},\Omega)]\end{align*} $$

is the Higgs topos of $\Omega $ -valued sets, which is in turn equivalent to the category of sheaves on $\Omega $ ; it has given a number of applications to consistency and independence problems in both classical and intuitionistic set theories. For a complete $\mathrm {FL}$ algebra $\Omega $ , which is a quantale with additional operations, ${\textbf{T}}[\mathrm {Hom}_{\textbf{Set}}(\mbox {-},\Omega )]$ may be seen as the category of $\Omega $ -valued sets. Quantale sets in the sense of Höhle-Kubiak [Reference Höhle and Kubiak13] can be regarded as objects in ${\textbf{T}}[\mathrm {Hom}_{\textbf{Set}}(\mbox {-},\Omega )]$ . We could interpret substructural set theories in the category of $\Omega $ -valued sets, and thereby might be able to solve consistency and independence problems in them. Presumably the most challenging problem in this context is the consistency of Łukasiewicz predicate logic with the naive comprehension principle, which White [Reference White38] claimed to have proven, yet generally considered to be an open problem even now.