Stone-Type Dualities for Separation Logics

S. Docherty]Simon Dochertya
aUniversity College London, London, UK

D. Pym]David Pyma, b
bThe Alan Turing Institute, London, UK

Stone-type duality theorems, which relate algebraic and relational/topological models, are
important tools in logic because — in addition to elegant abstraction — they strengthen
soundness and completeness to a categorical equivalence, yielding a framework through
which both algebraic and topological methods can be brought to bear on a logic. We give a
systematic treatment of Stone-type duality for the structures that interpret bunched logics,
starting with the weakest systems, recovering the familiar BI and Boolean BI (BBI), and extending
to both classical and intuitionistic Separation Logic.

We demonstrate the uniformity and modularity of this analysis by additionally capturing the
bunched logics obtained by extending BI and BBI with modalities and multiplicative connectives corresponding
to disjunction, negation and falsum. This includes the logic of separating modalities (LSM), De Morgan BI (DMBI), Classical BI (CBI), and the sub-classical family of logics extending Bi-intuitionistic (B)BI (Bi(B)BI). We additionally obtain as corollaries
soundness and completeness theorems for the specific Kripke-style models of these logics
as presented in the literature: for DMBI, the sub-classical logics extending BiBI and a new bunched logic, Concurrent Kleene BI (connecting our work to Concurrent Separation Logic), this is the first time soundness and completeness theorems have been proved. We thus obtain a comprehensive semantic account of the multiplicative variants of all standard propositional connectives in the bunched logic setting. This approach synthesises a variety of techniques
from modal, substructural and categorical logic and contextualizes the `resource semantics'
interpretation underpinning Separation Logic amongst them.

This enables the application of algebraic and topological methods to both Separation
Logic and the systems of bunched logics it is built upon. Conversely, the new notion of
indexed frame (generalizing the standard memory model of Separation Logic) and its
associated completeness proof can easily be adapted to other non-classical predicate logics.

§ INTRODUCTION

§.§ Background

Bunched logics, beginning with O'Hearn and Pym's BI [68], have
proved to be exceptionally useful tools in modelling and reasoning about
computational and information-theoretic phenomena such as resources, the
structure of complex systems, and access control [20, 21, 35]. Perhaps the most striking example is Separation
Logic [70, 80] (via Pointer Logic [49]), a specific
theory of first-order (Boolean) BI with primitives for mutable data structures.

A layered graph $H \gcomp_\mathcal{E} K$

The weakest bunched systems are the so-called layered graph logics [20, 35].
These logics have a multiplicative conjunction that is
neither associative nor commutative, together with its associated
implications, and additives that may be classical or intuitionistic.
These systems can be used to describe the decomposition of directed graphs into layers (see Fig. <ref>),
with applications such as complex
systems modelling (e.g., [20, 35]) and issues in security concerning the
relationship of policies and the systems to which they are intended to
apply (e.g., [21, 35]). Strengthening the multiplicative conjunction to
be associative and commutative and adding a multiplicative unit yields BI, for intuitionistic additives,
and Boolean BI (BBI), for classical additives. A number of extensions of these logics can also be defined which include multiplicative variants on all of the standard propositional connectives [11, 12, 15]. Further extensions
include additive and multiplicative modalities and, with the addition of
parametrization of modalities on actions, Hennessy–Milner-style process
logics [22, 3]. Yet further extensions include additive and
multiplicative epistemic modalities [29, 43], with applications in
security modelling.

All of the applications of bunched logics to reasoning about
computational and information-theoretic phenomena essentially rely on
the interpretation of the truth-functional models of these systems
known as resource semantics. Truth-functional models of bunched
logics are, essentially, constructed from pre- or partially ordered
partial monoids [45] which, in resource semantics, are interpreted as
describing how resource-elements can be combined (monoid composition)
and compared (order). The program logic known as Separation Logic [49, 70, 80]
is a specific theory of first-order bunched logic based on the partial monoid of elements of
the heap (with the order being simply equality). Separation Logic has
found industrial-strength application to static analysis through
Facebook's Infer tool (<fbinfer.com>).

Stone's representation theorem for Boolean algebras [74]
establishes that every Boolean algebra is isomorphic to a field of sets. Specifically,
every Boolean algebra $\algfont{A}$ is isomorphic to the algebra of
clopen subsets of its associated Stone space [54]
$S(\algfont{A})$. This result generalizes to a
family of Stone-type duality theorems which establish equivalences
between certain categories of topological spaces and categories of
partially ordered sets.  From the point of view of logic, Stone-type
dualities strengthen the semantic equivalence of truth-functional (such
as BI's resource semantics or Kripke's semantics for intuitionistic
logic) and algebraic (such as BI algebras or Heyting
algebras) models to a dual equivalence of categories. This is useful for a number of reasons: on the
one hand, it provides a theoretically convenient abstract characterization of
semantic interpretations and, on the other, it provides a systematic
approach to soundness and completeness theorems, via the close
relationship between the algebraic structures and Hilbert-type proof
systems. Beyond this, Stone-type dualities set up a framework through which techniques
from both algebra and topology can be brought to bear on a logic.

§.§ Contributions

In this paper, we give a systematic account of resource semantics via a family of Stone-type
duality theorems that encompass the range of
systems from the layered graph logics, via BI and BBI, to
Separation Logic. Our analysis is extended to bunched logics featuring multiplicative variants of all of the standard propositional connectives [11, 12, 15] and — through straightforward combination with the analogous results from the modal logic literature — is additionally given for the modal and
epistemic systems extending (B)BI [27, 29, 43]. As corollaries we retrieve the soundness and completeness of the standard Kripke models in the literature as well as several new ones.

Soundness and completeness theorems for bunched logics and their extensions tend to be proved through labelled tableaux countermodel procedures [29, 43, 45, 60] that must be specified on a logic-by-logic basis, or by lengthy translations into auxilliary modal logics axiomatized by Sahlqvist [71] formulae [12, 15, 17]. A notable exception to this (and precursor of the completeness result for (B)BI given in the present work) is Galmiche & Larchey-Wendling's completeness result for what they call relational BBI [44]. We predict our framework will increase the ease with which completeness theorems can be proved for future bunched logics, as the family of duality theorems are modular in the sense that all that need be verified in an extension of a bunched logic is that the additional axioms and structure that define the extension are also witnessed by the duality. In particular, we give an exhaustive treatment of the structure required for every multiplicative propositional connective in the bunched logic setting as well as the correspondence theory for a selection of axioms that includes all those that define known systems. The only remaining ingredient for a comprehensive treatment of bunched logic semantics is the identification of a Sahlqvist-like class of bunched logic formulas from which Kripke completeness can automatically be obtained. However, the results of the present work lay a clear foundation for such a class to be identified, as the duality theoretic techniques Sambin & Vaccaro use in their proof of Sahlqvist's theorem [72] should be adaptable given our duality theorems.

Of particular interest in the present paper are bunched logics with intuitionistic additives. In proving completeness for bunched logics via translations into Sahlqvist-axiomatized modal logics, some connectives must be converted into their `diamond-like' De Morgan dual and back using Boolean negation to apply Sahlqvist's theorem. For example, magic wand $\wand$ must be encoded as septraction — that is, $\varphi \septraction \psi := \neg (\neg \varphi \wand \neg \psi)$
— in a logically equivalent Sahlqvist-axiomatized modal logic. This is not possible on weaker-than-Boolean bases, which necessarily lack Boolean negation. Our direct proof method side steps this issue and as a result we are able to give the first completeness proofs for the intuitionistic variants of bunched logics that were not amenable to the proof method used for their Boolean counterparts. We further demonstrate the viability of this proof technique for bunched logics by specifying a new logic CKBI, derived from the interpretation of Concurrent Separation Logic in concurrent Kleene algebra, and prove it sound and complete via duality. More generally, the notion of indexed frame (generalizing the standard model of Separation Logic) and its associated completeness proof can easily be adapted to other non-classical predicate logics.

All of the structures given in existing algebraic and relational approaches to
Separation Logic — including [13, 18, 31, 38, 39] — are instances of the structures utilized in the present work. Thus these approaches are all proved
sound with respect to the standard semantics on store-heap pairs by the results of this paper.
In particular, we strengthen Biering et al.'s [6] interpretation of Separation Logic in BI hyperdoctrines to a dual equivalence of categories. To do so we synthesise a variety of related work from modal [55, 77, 47], relevant [2, 76], substructural [7] and categorical logic [25], and thus mathematically some of what follows may be familiar, even if the application to Separation Logic is not. Much of the theory these areas enjoy is produced by way of algebraic and topological arguments. We hope that by recontextualizing the resource semantics of bunched logics in this way similar theory can be given for both Separation Logic and its underlying systems. As a preliminary example (which can be found in the first author's PhD thesis [32]), we have used the framework given here to prove a bunched logic variant of the Goldblatt-Thomason theorem, which characterises the classes of model that are definable by bunched logic formulae.

§.§ Structure

The paper proceeds as described below. In Section <ref>, we introduce the core bunched logics: the weakest systems LGL and ILGL, the resource logics BI and BBI, and finally the program logic Separation Logic (in both classical and intuitionistic form). In Section <ref>, we define the algebraic and topological structures suitable for interpreting (I)LGL and give representation and duality theorems relating them. In Section <ref> these results are extended to the logics of bunched implications, (B)BI. In Section <ref>, we consider categorical structure appropriate for giving algebraic and truth-functional semantics for first-order (B)BI (FO(B)BI). We recall how FO(B)BI can be interpreted on (B)BI hyperdoctrines and define new structures called indexed (B)BI frames. Crucially, we show that the standard models of Separation Logic are instantiations of an indexed frames. We then extend (B)BI duality to give a dual equivalence of categories between the category of (B)BI hyperdoctrines and the category of indexed (B)BI frames.

In Section <ref> we extend the theory of the previous sections to bunched logics featuring the full range of multiplicative propositional connectives, as well as normal and separating modal extensions of (B)BI. In doing so we give new completeness theorems for De Morgan BI and the intuitionistic subclassical bunched logics, and specify a new propositional logic connecting our work to Concurrent Separation Logic, CKBI, which also fits into our framework. In Section <ref>, we consider possibilities for further work as a result of the duality theorems.

The present work is an extended and expanded version of a conference
paper presented at MFPS XXXIII [33]. New to this version are the corresponding results for the intuitionistic variants of the logics considered there, as well as the extension to bunched logics with additional modalities and multiplicatives.
Proofs have been included wherever length permits. A further expansion of this work can be found in the first author's PhD thesis [32].

§ PRELIMINARIES

In this section we give an introduction to the core bunched logics we consider in this paper: layered graph logics, logics of bunched implications and Separation Logic. In particular, we focus on the intended models of these logics, which will be generalised to classes of frames amenable to our duality theoretic framework in what follows.

§.§ Layered Graph Logics

We begin by presenting the layered graph logics LGL [20] and ILGL [35].
First, we give a formal, graph-theoretic definition of layered graph that, we claim,
captures the concept as used in modelling complex systems [20, 21, 35].
Informally, two layers in a directed graph are connected by a specified set
of edges, each element of which starts in the upper layer and ends in the lower layer.

Given a directed graph, $\mathcal{G}$, we refer to its vertex set and its edge set by
$V(\mathcal{G})$ and $E(\mathcal{G})$ respectively, while its set of subgraphs is denoted
$S\!g(\mathcal{G})$, with $H \subseteq \mathcal{G} \text{ iff } H \in S\!g(\mathcal{G})$. For a
distinguished edge set $\mathcal{E} \subseteq E(\mathcal{G})$, the reachability relation
$\leadsto_{\mathcal{E}}$ on $S\!g(\mathcal{G})$ is defined $H \leadsto_{\mathcal{E}} K$ iff
a vertex of $K$ can be reached from a vertex of $H$ by an $\mathcal{E}$-edge. This generates a partial composition $@_{\mathcal{E}}$ on subgraphs, with $\gcompE{H}{K} \downarrow$ (where $\downarrow$ denotes definedness) iff
$V(H) \cap V(K) = \emptyset, H \leadsto_{\mathcal{E}} K \text{ and } K \not \leadsto_{\mathcal{E}} H$. Output is given by the graph union of the two subgraphs
and the $\mathcal{E}$-edges between them. We say $G$ is  a layered graph (with
respect to $\mathcal{E}$) if there exist $H$, $K$ such that $\gcompE{H}{K}\downarrow$ and
$G = \gcompE{H}{K}$ (see Fig. <ref>). Layering is evidently neither commutative
nor (because of the definedness condition) associative.

0.     $\cfrac{}{\neg \neg \varphi \vdash \varphi}$       1.     $\cfrac{}{\varphi\vdash\varphi}$     2.     $\cfrac{}{\varphi\vdash\top}$

3.      $\cfrac{}{\bot\vdash\varphi}$      4.     $\cfrac{\eta \vdash \varphi \quad \eta \vdash \psi}{\eta \vdash \varphi \wedge \psi}$      5.     $\cfrac{\varphi \vdash \psi_1 \wedge \psi_2}{\varphi \vdash \psi_i}$

6.      $\cfrac{\varphi \vdash \psi}{\eta \wedge\varphi \vdash \psi }$      7.     $\cfrac{\eta \vdash \psi \quad \varphi \vdash \psi}{\eta \lor \varphi \vdash \psi}$
8.      $\cfrac{\varphi\vdash\psi_i} {\varphi\vdash\psi_1\lor\psi_2}$

9.     $\cfrac{\eta \vdash\varphi\to\psi \quad \eta\vdash\varphi}{\eta\vdash\psi}$
10.      $\cfrac{\eta\wedge\varphi\vdash\psi}{\eta\vdash\varphi\to\psi}$     11.     $\cfrac{\xi\vdash\varphi\quad\eta\vdash\psi}{\xi*\eta\vdash\varphi*\psi}$

12.     $\cfrac{\eta*\varphi\vdash\psi}{\eta\vdash\varphi\wand\psi}$     13.     $\cfrac{\xi\vdash\varphi\wand\psi\quad\eta\vdash\varphi}{\xi*\eta\vdash\psi}$      14.     $\cfrac{\eta*\varphi\vdash\psi}{\varphi\vdash\eta\dnaw\psi}$

15.     $\cfrac{\xi\vdash\varphi\dnaw\psi\quad\eta\vdash\varphi}{\eta*\xi\vdash\psi}$

[Hilbert rules for layered graph logics.]Hilbert rules for layered graph logics. $i=1$ or $2$ for 5. and 8.

$G$     $\vDash$     $\Atom{p}$     iff     l$G \in \Valuation(\Atom{p})$
$G$     $\vDash$     $\top$
$G  \not\vDash \bot$

$G$     $\vDash$     $\varphi \land \psi$     iff     l$G \vDash \varphi$ and $G \vDash \psi$
$G$     $\vDash$     $\varphi \lor \psi$     iff     2l$G \vDash \varphi$ or $G \vDash \psi$

$G$     $\vDash$     $\varphi \rightarrow \psi$     iff     lfor all $H \succcurlyeq G$, $H \vDash\varphi$ implies $H$  $\vDash$ $\psi$

$G$     $\vDash$     $\varphi * \psi$     iff     8lthere exists $H, K$ such that $\gcompE{H}{K}\downarrow$, $\gcompE{H}{K} \preccurlyeq G$, $H \vDash \varphi$ and  $K \vDash \psi$

$G$     $\vDash$     $\varphi \wand \psi$     iff     8lfor all $H, K$ such that $\gcompE{H}{K}\downarrow$ and $G \preccurlyeq H$,  $H \vDash \varphi$ implies $\gcompE{H}{K} \vDash \psi$

$G$     $\vDash$     $\varphi \dnaw \psi$     iff     8lfor all $H, K$ such that $\gcompE{K}{H}\downarrow$ and $G \preccurlyeq H$,  $H \vDash \varphi$ implies $\gcompE{K}{H} \vDash \psi$

Satisfaction on layered graphs for (I)LGL. LGL is the case where $\preccurlyeq$ is $=$.

Let $\Prop$ be a set of atomic propositions, ranged over by $\mathrm{p}$.
The set of all formulae of $\logicfont{LGL}$ and $\logicfont{ILGL}$ is generated by the following grammar:

\[
\varphi::=\mathrm{p}
\mid \top
\mid \bot
\mid \varphi\wedge\varphi
\mid\varphi\lor\varphi
\mid\varphi\to\varphi
\mid\varphi*\varphi
\mid\varphi\wand\varphi
\mid \varphi\dnaw\varphi .
\]

The connectives above are the standard logical connectives,
together with a (non-commutative and non-associative) multiplicative conjunction, $*$, and its associated implications $\wand$ and $\dnaw$, in the spirit of the Lambek calculus [58, 59].
We define $\neg \varphi$ as $\varphi \to \bot$. Hilbert-type systems for the logics are given in Fig. <ref>: ILGL is specified by rules 1–15, whilst LGL is specified by rules 0–15. We note that our notation differs here compared from that found in the work of Collinson et al. [20, 21] and our previous work [35, 36].
There, the multiplicative conjunction is given by $\blacktriangleright$, with the associated implications written $\gimp$ and $\limp$. While this notation has the benefit of directly presenting the non-commutativity of the conjunction, we use the $*$ notation associated with the logic of bunched implications uniformly across all logics we consider. This allows us to uniformly present rules, algebras, and constructions that instantiate the same structure independently of the logic under consideration.

LGL and ILGL are interpreted on  scaffolds: structures $\mathcal{X} = (\mathcal{G}, \mathcal{E}, X, \preccurlyeq)$ where $\mathcal{G}$ is a directed graph, $\mathcal{E}$ is a distinguished edge set, $X \subseteq S\!g(\mathcal{G})$ is such that — if $\gcompE{H}{K}\downarrow$ — $H, K \in X$ iff $\gcompE{H}{K} \in X$ and $\preccurlyeq$ is a preorder on $X$. We note that for any $\mathcal{G}, \mathcal{E}$ and $X$ there are always two “canonical” orders one can consider: the subgraph and the supergraph relations.

To model the logic soundly in the intuitionistic case, valuations $\Valuation: \Prop \rightarrow \pow{X}$ (where $\pow{X}$ is the power set of $X$) must be persistent: for all $G, H \in X$, if $G \in \Valuation(\Atom{p})$ and $G \preccurlyeq H$, then $H \in \Valuation(\Atom{p})$. This has a spatial interpretation when we consider the order to be the subgraph relation: if p designates that a resource is located in the region $G$, it should also hold of the region $H$ containing $G$.

Given a scaffold $\framefont{X}$ and a persistent valuation
$\Valuation$ the satisfaction relation $\vDash_{\Valuation}$ for ILGL is inductively defined in Fig. <ref>; the particular case where $\preccurlyeq$ is equality yields LGL. As is necessary for a sound interpretation of intuitionistic logic, persistence extends to all formulas with respect to the semantics of Fig. <ref>: for all $\varphi$, $G$, $H$, if $G \vDash_{\Valuation} \varphi$ and $G \preccurlyeq H$ then $H \vDash_{\Valuation} \varphi$. We define validity of $\varphi$ in a model defined on $\mathcal{X}$ to mean for all $G \in X, G \vDash_{\Valuation} \varphi$. Validity of $\varphi$ is defined to be validity in all models. Finally, the entailment relation $\varphi \vDash \psi$ holds iff for all models and all $G$, $G \vDash_{\Valuation} \varphi$ implies $G \vDash_{\Valuation} \psi$.

§.§ BI and Boolean BI

Next we present the resource logics BI and BBI [68]. Let $\Prop$ be a set of atomic propositions, ranged over by $\Atom{p}$. The set of all formulae of $\logicfont{(B)BI}$ is generated by the following grammar:

\[
\varphi::=\mathrm{p}
\mid \top
\mid \bot
\mid \mtop
\mid \varphi\wedge\varphi
\mid\varphi\lor\varphi
\mid\varphi\to\varphi
\mid\varphi*\varphi
\mid\varphi\wand\varphi.
\]

Once again we have the standard logical connectives, this time joined by a commutative, associative multiplicative conjunction $*$ together with its associated implication $\wand$, and unit $\mtop$. By extending rules 1–15 of Fig. <ref> with the rules of Fig. <ref> we obtain a system for BI; extending rules 0–15 of Fig. <ref> with the rules of Fig. <ref> yields a system for BBI. These rules can be straightforwardly read as enforcing commutativity and associativity of the multiplicative conjunction $*$, the adjointness between $*$ and its associated implication $\wand$, and the fact that $\mtop$ is a unit for $*$.

16.     $\cfrac{}{(\varphi * \psi) * \xi \vdash \varphi * (\psi * \xi)}$
17.     $\cfrac{}{\varphi * \psi \vdash \psi * \varphi}$
18.     $\cfrac{}{\varphi * \mtop \dashv \vdash \varphi}$

Rules for the (B)BI Hilbert Systems, $\mathrm{(B)BI}_{\mathrm{H}}$.

$r$     $\vDash_{\Valuation}$     $\Atom{p}$     iff     l$r \in \Valuation(\Atom{p})$
$r$     $\vDash_{\Valuation}$     $\top$
$r  \not\vDash_{\Valuation} \bot$

$r$     $\vDash_{\Valuation}$     $\varphi \land \psi$     iff     l$r \vDash_{\Valuation} \varphi$ and $r\vDash_{\Valuation} \psi$
$r$     $\vDash_{\Valuation}$     $\varphi \lor \psi$     iff     2l$r \vDash_{\Valuation} \varphi$ or $r \vDash_{\Valuation} \psi$

$r$     $\vDash_{\Valuation}$     $\varphi \rightarrow \psi$     iff     lfor all $r' \succcurlyeq r$, $r' \vDash_{\Valuation}\varphi$ implies $r'$  $\vDash_{\Valuation}$ $\psi$;        $r$     $\vDash_{\Valuation}$     $\mtop$     iff     l$r \in E$

$r$     $\vDash_{\Valuation}$     $\varphi * \psi$     iff     8lthere exists $r', r''$ such that  $r \in r' \circ r''$, $r' \vDash_{\Valuation} \varphi$ and  $r'' \vDash_{\Valuation} \psi$

$r$     $\vDash_{\Valuation}$     $\varphi \wand \psi$     iff     8lfor all $r', r''$ such that $r'' \in r \circ r'$, $r' \vDash_{\Valuation} \varphi$ implies $r'' \vDash_{\Valuation} \psi$

Satisfaction on UDMFs for (B)BI. BBI is the case where $\preccurlyeq$ is =.

Models of these logics arise from the analysis of the abstract notion of resource first outlined in the original work on BI [68]. There, the principal properties were determined to be composability and comparison, formalized by a commutative and associative composition $\circ$ with unit $e$, and a pre- or partial order $\preccurlyeq$, respectively. The interplay between composition and comparison in this analysis is formalized by a bifunctorality condition: if $a \preccurlyeq a'$ and $b \preccurlyeq b'$ then $a \circ a' \preccurlyeq b \circ b'$. Structures $\mathcal{M} = (M, \preccurlyeq, \circ, e)$ satisfying these conditions are known as resource monoids.

(B)BI is interpreted on ordered monoidal structures that generalize the notion of resource monoid in various ways. For example, $\circ$ can be generalized to be non-deterministic and/or partial, the unit $e$ can be generalized to a set of units $E$, and the bifunctorality condition can be generalized to a number of different coherence conditions between $\circ$ and $\preccurlyeq$. The majority of these choices define the same notion of validity, although there are some sharp boundaries (an analysis of some of these issues can be found in [61]), and all of them can be grouped under the name resource semantics. As an example we give a class of models that corresponds closely to the standard intuitionistic model of Separation Logic. This class will be further generalized in Section <ref> for the purposes of the duality theorem.

A monoidal frame is a structure $\mathcal{X} = (X, \preccurlyeq, \circ, E)$ s.t. $\preccurlyeq$ is a preorder, $\circ: X^2 \rightarrow \mathcal{P}(X)$ is commutative operation satisfying non-deterministic associativity

\[ \forall x, y, z, t, s: s \in x \circ y \text{ and } t\in s \circ z \text{ implies } \exists s'(s' \in y \circ z \text{ and } t \in x \circ s),  \]
and $E$ is a set satisfying, for all $x, y \in X$, the conditions
(Unit Existence) $\exists e \in E(x \in x \circ e)$; (Coherence) $x \in y \circ e \land e \in E \rightarrow y \preccurlyeq x$; and (Closure) $e \in E \land e \preccurlyeq e' \rightarrow e' \in E$.
It is downwards-closed if, whenever $x \in y \circ z$, $y' \preccurlyeq y$ and $z' \preccurlyeq z$, there exists $x' \preccurlyeq x$ such that $x' \in y' \circ z'$. Conversely it is upwards-closed if, whenever $x \in y \circ z$ and $x \preccurlyeq x'$, there exists $y' \succcurlyeq y$ and $z' \succcurlyeq z$ such that $x' \in y' \circ z'$.

The notions of upwards and downwards closure are properties that the majority of models of Separation Logic satisfy. Cao et al. [19] show that when a model satisfies both upwards and downwards closure, the semantic clauses of $*$ and $\wand$ can be given identically in the classical and intuitionistic cases.

Given an upwards and downwards closed monoidal frame (UDMF) $\mathcal{X}$ and a persistent valuation $\mathcal{V}: \Prop \rightarrow \mathcal{P}(\mathrm{X})$, the satisfaction relation $\vDash_{\Valuation}$ is inductively defined in Fig. <ref>. Once again, a semantics for BBI is obtained as the particular case where the order $\preccurlyeq$ is equality $=$. As with $\logicfont{ILGL}$, persistence extends to all formulas of $\logicfont{BI}$, with upwards and downwards closure ensuring that this is the case for formulas of the form $\varphi * \psi$ and $\varphi \wand \psi$. Validity and entailment are defined in much the same way as the case for (I)LGL.

§.§ Separation Logic

Separation Logic [64], introduced by Ishtiaq and O'Hearn [49], and Reynolds [70], is an extension of
Hoare's program logic which addresses reasoning about programs that access and mutate shared data structures. The usual
presentation of Separation Logic is based on Hoare triples — for reasoning about the state of imperative programs —
of the form $ \{ \,\varphi \, \} \, C \, \{ \,\psi \, \}$,
where $C$ is a program command, $\varphi$ is pre-condition for $C$, and $\psi$ is a post-condition for $C$. The formulas $\varphi$ and $\psi$ are given by the following grammar:

\[
\varphi::= E = E'
\mid E \mapsto F
\mid \top
\mid \bot
\mid \mathrm{Emp}
\mid \varphi\wedge\varphi
\mid\varphi\lor\varphi
\mid\varphi\to\varphi
\mid\varphi*\varphi
\mid\varphi\wand\varphi
\mid \exists v. \varphi
\mid \forall v. \varphi.
\]

Reynolds' programming language is a simple language of commands with a Lisp-like set-up for creating and accessing cons
cells: $C \, ::= \, x := E \mid x := E.i \mid E.i := E' \mid x := cons(E_1,E_2) \mid \dots \,$. Here the expressions $E$
of the language are built up using booleans, variables, etc., $cons$ cells, and atomic expressions.
Separation Logic thus facilitates verification procedures for programs that alter the heap.

A key feature of Separation Logic is the local reasoning provided by the Frame Rule,

\[\frac{\{ \,\varphi \, \} \, C \, \{ \,\psi \, \} }{\{ \,\varphi \ast \chi\, \} \, C \, \{ \,\psi \ast \chi\, \} },\]

where $\chi$ does not include any free variables modified by the program $C$. Static analysis procedures based on the
Frame Rule form the basis of Facebook's Infer tool (<fbinfer.com>) that is deployed in its code production. The decomposition of
the analysis that is facilitated by the Frame Rule is critical to the practical deployability of Infer.

Separation Logic can usefully and safely be seen (see [80] for the details) as a presentation of (B)BI Pointer
Logic [49]. The semantics of (B)BI Pointer Logic, a theory of (first-order) (B)BI, is an instance of (B)BI's resource
semantics in which the monoid of resources is constructed from the program's heap. In detail, this model
has two components, the store and the heap. The store is a partial function mapping from variables
to values $a \in \mbox{\rm Val}$ (e.g., integers) and the heap is a partial function from natural numbers to values.
In logic, the store is often called the valuation, and the heap is a possible world.
In programming languages, the store is sometimes called the environment. Within this set-up, the atomic
formulae of (B)BI Pointer Logic include equality between expressions, $E = E'$, and, crucially, the points-to predicate,
$E \mapsto F$.

We use the following additional notation: $dom(h)$ denotes the domain of definition of a heap $h$ and
$dom(s)$ is the domain of  a store $s$; $h \# h'$ denotes that $dom(h) \cap dom(h') = \emptyset$;
$h \cdot h'$ denotes the union of functions with disjoint domains, which is undefined if the domains
overlap; $h \sqsubseteq h'$ denotes that the graph of $h$ is a subgraph of $h'$; $[]$ denotes the empty heap that is nowhere defined; $[ f \mid v \mapsto a ]$ is the partial function that is equal to $f$ except that $v$ maps to $a$;
expressions $E$ are built up from variables and constants, and so determine denotations
$\dbrace{E}s \in {\rm Val}$.

With this basic data we can define the satisfaction relations for BI and BBI pointer logic. BI pointer logic is given by extending the intuitionistic semantic clause for $\mapsto$,

\[ s, h \vDash E \!\mapsto\! F{\ } \mbox{\rm iff } \dbrace{E}s \in dom(h) \mbox{\rm and } h(\dbrace{E}s) = \dbrace{F}s, \]

with those in Fig. <ref>; similarly, BBI pointer logic is given by extending the classical semantic clause for $\mapsto$,

\[ s , h \vDash E \!\mapsto\! F{\  } \mbox{\rm  iff }  \dbrace{E}s = {\rm dom}(h) \mbox{\rm and } h(\dbrace{E}s) = \dbrace{F}s, \]

with those in Fig. <ref>, where $\sqsubseteq$ is replaced for $=$ in the clauses for $\rightarrow$ and $\mathrm{Emp}$. The judgement, $s, h \vDash \varphi$, says that the assertion $\varphi$ holds for a given store and heap, assuming that the free variables of $\varphi$ are contained in the domain of $s$. The classical interpretation of $\mapsto$ requires $E$ to be the only active address in the current
heap, whereas the intuitionistic interpretation is the weaker judgement that $E$ is at least one of the active addresses in the current heap.

$s, h$     $\vDash$     $E = E'$     iff     l$\dbrace{E}s = \dbrace{E'}s$
$s,h$     $\vDash$     $\top$
$s, h  \not\vDash \bot$

$s, h$     $\vDash$     $\varphi \land \psi$     iff     l$s, h \vDash \varphi$ and $s, h \vDash \psi$
$s, h$     $\vDash$     $\varphi \lor \psi$     iff     2l$s, h \vDash \varphi$ or $s, h \vDash \psi$

$s, h$     $\vDash$     $\varphi \rightarrow \psi$     iff     lfor all $h' \sqsupseteq h$, $h'$ $\vDash$ $\varphi$ implies $h'$  $\vDash$ $\psi$        $s, h$     $\vDash$     $\Atom{Emp}$     iff     l$h \sqsupseteq []$

$s, h$     $\vDash$     $\varphi * \psi$     iff     8lthere exists $h', h''$ s.t. $h\# h'$, $h = h' \cdot h''$, $s, h' \vDash \varphi$ and  $s, h'' \vDash \psi$

$s, h$     $\vDash$     $\varphi \wand\psi$     iff     8lfor all $h'$ such that $h \# h',  s, h' \vDash \varphi$ implies $s, h \cdot h' \vDash \psi$

$s, h$     $\vDash$     $\exists v. \varphi$     iff     8lthere exists $a \in \mathrm{Val}$,  $[s \mid v \mapsto a], h \vDash \varphi$

$s, h$     $\vDash$     $\forall v. \varphi$     iff     8lfor all $a \in \mathrm{Val}$,  $[s \mid v \mapsto a], h \vDash \varphi$

Satisfaction for (B)BI Pointer Logic. The BBI variant replaces $\sqsupseteq$ with =.

The technical reason for this difference is the requirement of persistence with respect to the heap extension ordering $\sqsubseteq$ for soundness of the intuitionistic semantics.

This leads to some quirks in the intuitionistic model: for example, the multiplicative unit $\mathrm{Emp}$ collapses to $\top$ as every heap extends the empty heap. Some aspects remain the same: as heaps are upwards and downwards closed (in the sense defined in Section <ref>) the semantic clauses for $*$ and $\wand$ can be given identically. Most importantly, in both cases descriptions of larger heaps can be built up using $\ast$, and this coheres with the local reasoning provided by the Frame Rule.

When Separation Logic is given as BI pointer logic it is known as Intuitionistic Separation Logic, whereas the formulation as BBI pointer logic is known as Classical Separation Logic. Although both were defined in the paper introducing Separation Logic as a theory of bunched logic [49], the classical variant has taken precedence in both theoretical work and practical implementations. A key exception to this is the higher-order Concurrent Separation Logic framework IRIS, which is based on Intuitionistic Separation Logic [56]. IRIS requires an underlying intuitionistic logic as it utilizes the `later' modality $\triangleright$ [63], which collapses to triviality ($\triangleright \varphi \leftrightarrow \top$ for all $\varphi$) in the presence of the law of excluded middle.

§ LAYERED GRAPH LOGICS

§.§ Algebra and Frames for (I)LGL

We begin our analysis with the weakest systems, LGL and ILGL. Each of the logics we consider can be obtained by extending the basic structures associated with these logics and so we are able to systematically extend the theory in each case by accounting for just the extensions to the structure. First, we consider lattice-based algebras suitable for interpreting (I)LGL.

[(I)LGL Algebra]

* An ILGL algebra is an algebra $\mathbb{A} = (A, \land, \lor, \rightarrow, \top, \bot, *, \wand, \dnaw)$
such that $(A, \land, \lor, \rightarrow, \top, \bot)$ is a Heyting algebra and $*, \wand, \dnaw$ are binary operations on $A$ satisfying, for all $a, b, c \in A$,
\[a * b \leq c \text{ iff } a \leq b \wand c \text{ iff } b \leq a \dnaw c.\]

* A LGL algebra is an ILGL algebra $\mathbb{A} = (A, \land, \lor, \rightarrow, \top, \bot, *, \wand, \dnaw)$ for which $(A, \land, \lor, \rightarrow, \top, \bot)$ is a Boolean algebra.

Residuation of $*$, $\wand$ and $\dnaw$ with respect to the underlying lattice order entails a number of useful properties that are utilised in what follows.

Let $\mathbb{A}$ be an (I)LGL algebra. Then, for all $a, b, a', b' \in A$ and $X, Y \subseteq A$,  we have the following:

* If $a \leq a'$ and $b \leq b'$ then $a * b \leq a' * b'$;

* If $\bigvee X$ and $\bigvee Y$ exist then $\bigvee_{x \in X, y \in Y} x * y$ exists and
$(\bigvee X) * (\bigvee Y) =  \bigvee_{x \in X, y \in Y} x * y$;

* If $a = \bot$ or $b = \bot$ then $a * b = \bot$;

* If $\bigvee X$ exists then for any $z \in A$, $\bigwedge_{x \in X} (x \wand z)$ and $\bigwedge_{x \in X} (x 	\dnaw z)$ exist with
\[\bigwedge_{x \in X} (x \wand z) = (\bigvee X) \wand z \text{ and } \bigwedge_{x \in X} (x 			\dnaw z) = (\bigvee X) \dnaw z;\]

* If $\bigwedge X$ exists then for any $z \in A$, $\bigwedge_{x \in X} (z \wand x)$ and
$\bigwedge_{x \in X} (z \dnaw x)$ exist with
\[ \bigwedge_{x \in X} (z \wand x) = z \wand (\bigwedge X)
\text{ and } \bigwedge_{x \in X} (z \dnaw x) = z \dnaw (\bigwedge X); \;\mbox{\rm and}\]

* $a \wand \top = a \dnaw \top = \bot \wand a =  \bot \dnaw a = \top$.

Interpretations of (I)LGL on an (I)LGL algebra work as follows: let $\Valuation: \Prop \rightarrow A$ be an assignment of propositional variables to elements of the algebra; this is uniquely extended to an interpretation $\llbracket - \rrbracket$ of every ILGL formula by induction, with $\Interp{\Atom{p}} = \Valuation(\Atom{p}), \Interp{\top} = \top$ and $\Interp{\bot} = \bot$ as base cases:

\[
\begin{array}{llllllll}
\llbracket \varphi \land \psi \rrbracket &= \llbracket \varphi \rrbracket \land \llbracket \psi \rrbracket  			&\llbracket \varphi \lor \psi \rrbracket &= \llbracket \varphi \rrbracket \lor \llbracket \psi \rrbracket &
\llbracket \varphi \rightarrow \psi \rrbracket & = \llbracket \varphi \rrbracket \rightarrow \llbracket \psi \rrbracket \\
\Interp{\varphi * \psi} & = \Interp{\varphi} * \Interp{\psi}
&\Interp{\varphi \wand \psi} & = \Interp{\varphi} \wand \Interp{\psi}
&\Interp{\varphi \dnaw \psi} & = \Interp{\varphi} \dnaw \Interp{\psi}.\\
\end{array}
\]

An interpretation $\Interp{-}$ on a(n) (I)LGL algebra $\mathbb{A}$ satisfies $\varphi$ iff $\Interp{\varphi} = \top$; $\varphi$ is valid on (I)LGL algebras iff $\varphi$ is satisfied by every interpretation $\Interp{-}$ on every ILGL algebra $\mathbb{A}$. By constructing Lindenbaum-Tarski algebras from the Hilbert systems of Fig. <ref> we obtain the following soundness and completeness theorem for (I)LGL algebras.

For all (I)LGL formulas $\varphi$, $\psi$, $\varphi \vdash \psi$ is provable in $\mathrm{(I)LGL}_{\mathrm{H}}$ iff, for all (I)LGL algebras $\mathbb{A}$ and all interpretations $\Interp{-}$ on $\mathbb{A}$, $\llbracket \varphi \rrbracket \leq \Interp{\psi}$.

Next we generalize the intended model of the logics to a class of relational structures.

[(I)LGL Frame]
An ILGL frame is a triple $\mathcal{X} = (X, \preccurlyeq, \circ)$ where $X$ is a set, $\preccurlyeq$ a preorder on $X$ and $\circ: X^2 \rightarrow \pow{X}$ a binary operation. An LGL frame is an ILGL frame for which the order $\preccurlyeq$ is equality $=$.

Here $\circ$ is a generalization of Section <ref>'s $\mathop{@}\nolimits$. We can therefore reconfigure the semantics given in Fig. <ref> to give a satisfaction relation on (I)LGL frames by straightforward substitutions of $\circ$ (see Fig. <ref>). Partiality is encoded by the fact $\circ$ has codomain $\pow{X}$ and thus $x \circ y = \emptyset$ holds when $\circ$ is undefined for $x, y$. However, $\circ$ is strictly more general as it does not necessarily satisfy the partial determinism that holds of scaffolds: $G =\gcompE{H}{K}$ and $G' = \gcompE{H}{K}$ implies $G = G'$. As $\circ$ is nondeterministic, it can equivalently be seen as a ternary relation, though we maintain the partial function notation to emphasise its interpretation as a composition operator.

$x$     $\vDash_{\mathcal{V}}$     $\mathrm{p}$     iff     l$x \in \mathcal{V}(\mathrm{p})$

$x$     $\vDash_{\mathcal{V}}$     $\top$         always

$x$      $\vDash_{\mathcal{V}}$     $\bot$         never

$x$     $\vDash_{\mathcal{V}}$     $\varphi \land \psi$     iff     l$x \vDash_{\mathcal{V}} \varphi$ and $x \vDash_{\mathcal{V}} \psi$

$x$     $\vDash_{\mathcal{V}}$     $\varphi \lor \psi$     iff     $x \vDash_{\mathcal{V}} \varphi$ or $x \vDash_{\mathcal{V}} \psi$

$x$     $\vDash_{\mathcal{V}}$     $\varphi \rightarrow \psi$     iff     lfor all $y \succcurlyeq x$, $y \vDash_{\mathcal{V}}\varphi$ implies $y$  $\vDash_{\mathcal{V}}$ $\psi$

$x$     $\vDash_{\mathcal{V}}$     $\varphi * \psi$     iff     8lthere exists $x', y, z$ s.t. $x \succcurlyeq x' \in y \circ z$, $y \vDash_{\mathcal{V}} \varphi$ and  $z \vDash_{\mathcal{V}} \psi$

$x$     $\vDash_{\mathcal{V}}$     $\varphi \wand \psi$     iff     8lfor all $x', y, z$ s.t. $x' \succcurlyeq x$ and $z \in x' \circ y$: $y \vDash_{\mathcal{V}} \varphi$ implies $z \vDash_{\mathcal{V}} \psi$

$x$     $\vDash_{\mathcal{V}}$     $\varphi \dnaw \psi$     iff     8lfor all $x', y, z$ s.t. $x' \succcurlyeq x$ and $z \in y \circ x'$:  $y \vDash_{\mathcal{V}} \varphi$ implies $z \vDash_{\mathcal{V}} \psi$

[Satisfaction for (I)LGL.]Satisfaction for (I)LGL. LGL is given by the case where $\succcurlyeq$ is $=$.

The structure of what follows will be reflected across each bunched logic we consider. First, we equip the frames associated with the logic with an appropriate notion of morphism to obtain a category. Next we set up the dual functors $Com$ and $Pr$ for transforming algebras into frames (and vice versa) and homomorphisms into frame morphisms (and vice versa), and prove a representation theorem falls out of this relationship. Finally we add appropriate topological structure to the frames to obtain a category of topological spaces that is dually equivalent to the category of algebras.

(I)LGL frames can be equipped a notion of morphism to obtain categories $\mathrm{ILGLFr}$ and $\mathrm{LGLFr}$. As in modal logic, morphisms have the following connection with the logics: if there exists a surjective (I)LGL morphism $g: \mathcal{X} \rightarrow \mathcal{X}'$ then any (I)LGL formula valid in $\mathcal{X}$ is also valid in $\mathcal{X}'$.

[ILGL Morphism]
Given ILGL frames $\mathcal{X}$ and $\mathcal{X}'$, an ILGL morphism is a map $g: X \rightarrow X'$ satisfying

* $x \preccurlyeq y$ implies $g(x) \preccurlyeq' g(y)$,

* $g(x) \preccurlyeq' y'$ implies there exists $y \in X$ s.t. $x \preccurlyeq y$ and $g(y) = y'$,

* $x \in y \circ z$ implies $g(x) \in g(y) \circ' g(z)$,

* $w' \preccurlyeq' g(x)$ and $w' \in y' \circ' z'$ implies there exists $w, y, z \in X$ s.t. $w \preccurlyeq x$, $w \in y \circ z$, $y' \preccurlyeq' g(y)$ and $z' \preccurlyeq' g(z)$,

* $g(x) \preccurlyeq' w'$ and $z' \in w' \circ' y'$ implies there exists $w, y, z \in X$ s.t. $x \preccurlyeq w$, $z \in w \circ y$, $y' \preccurlyeq' g(y)$ and $g(z) \preccurlyeq' z'$, and

* $g(x) \preccurlyeq' w'$ and $z' \in y' \circ' w'$ implies there exists $w, y, z \in X$ s.t. $x \preccurlyeq w$, $z \in y \circ w$, $y' \preccurlyeq' g(y)$ and $g(z) \preccurlyeq' z'$.

For LGL, replacing $\preccurlyeq$ with $=$ collapses the above definition to a simpler and more familiar notion of morphism.

[LGL Morphism (cf. [14])] Given LGL frames $\mathcal{X}$ and $\mathcal{X}'$, a LGL morphism is a map $g: \mathcal{X} \rightarrow \mathcal{X}'$ satisfying

* $x \in y \circ z$ implies $g(x) \in g(y) \circ' g(z)$,

* $g(x) \in y' \circ' z'$ implies there exists $y, z \in X$ s.t. $x \in y \circ z, g(y) = y' \text{ and } g(z) = z'$,

* $z' \in g(x) \circ' y'$ implies there exists $y, z \in X$ s.t. $z \in x \circ y, g(y) = y' \text{ and } g(z) = z'$, and

* $z' \in y' \circ' g(x)$ implies there exists $y, z \in X$ s.t. $z \in y \circ x, g(y) = y' \text{ and } g(z) = z'$.

A variant of this definition is used in the context of BBI by Brotherston & Villard [14] to demonstrate that the logic is not sufficiently expressive to axiomatise a number of properties common to models of separation logic. Urquhart [76] defines similar maps in order to define dualities for relevant logic and Bimbó & Dunn [7] generalise Urquhart's definition further to give morphisms that respect residuals on the dual algebras of frames for gaggles; it is this definition that we modify for our morphisms — bunched logics can be seen to be variants of gaggles with extra operators and/or axioms.

§.§ Duality for (I)LGL

We now give representation and duality theorems for ILGL algebras. As a corollary we obtain the equivalence of the relational semantics to the algebraic semantics, as well as its completeness with respect to the Hilbert system of Fig. <ref>. We first define two transformations that underpin functors between the category of (I)LGL algebras and the category of (I)LGL frames.

[ILGL Complex Algebra]
Given an ILGL frame $\mathcal{X}$, the complex algebra of $\mathcal{X}$ is given by $Com^{\text{\scalebox{.7}{ILGL}}}(\mathcal{X}) = (\mathcal{P}_{\succcurlyeq}(X), \cap, \cup, \Rightarrow, X, \emptyset, \bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}, \Lres_{\mathcal{X}})$ where

\begin{align*}
\mathcal{P}_{\succcurlyeq}(X) &= \{ A \subseteq X \mid \text{ if } a \in A \text{ and } a \preccurlyeq b \text{ then } b \in A \} \\
A \Rightarrow B &= \{ x \mid \text{if } x \preccurlyeq x' \text{ and } x' \in A \text{ then } x' \in B \} \\
A \bullet_{\mathcal{X}} B &= \{ x \mid \text{there exists } w, y, z \text{ s.t } w \preccurlyeq x, w \in y \circ z, y \in A \text{ and } z \in B \} \\
A \Rres\nolimits_{\mathcal{X}} B &= \{ x \mid \text{for all } w, y, z, \text{ if } x \preccurlyeq w, z \in w \circ y \text{ and } y \in A \text{ then } z \in B \}  \\
A \Lres\nolimits_{\mathcal{X}} B &= \{ x \mid \text{for all } w, y, z, \text{ if } x \preccurlyeq w, z \in y \circ w \text{ and } y \in A \text{ then } z \in B \}. \tag*{\qed}
\end{align*}

Each operator here maps upwards-closed sets to upwards-closed sets so this is well defined. By substituting $\preccurlyeq$ for $=$, the above definition collapses to one suitable for LGL.

[LGL Complex Algebra]
Given a LGL frame $\framefont{X}$, the complex algebra of $\framefont{X}$ is given by
$Com^{\text{\scalebox{.7}{LGL}}}(\framefont{X}) = (\pow{X}, \cap, \cup, \setminus, X, \emptyset, \bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}, \Lres_{\mathcal{X}})$,
where $\bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}$, and $\Lres_{\mathcal{X}}$ are defined as follows:
\[ \begin{array}{cl}
A \Rightarrow B &= \overline{A} \cup B \\
A \bullet_{\mathcal{X}} B  &=  \{ x \mid \text{there exists } y \in A, z \in B \text{ s.t. } x \in y \circ z \} \\
A \Rres_{\mathcal{X}} B  &=  \{ x \mid \text{for all } y, z \in X, z \in x \circ y \text{ and } y \in A \text{ implies } z \in B \} \\
A \Lres_{\mathcal{X}} B  &=  \{ x \mid \text{for all } y, z \in X, z \in y \circ x \text{ and } y \in A \text{ implies }
z \in B \}.
\end{array}
\]

where $\overline{A}$ denotes set compliment.

The residuated structure in each case is then easy to verify.

Given an (I)LGL frame $\mathcal{X}$, $Com^{\text{\scalebox{.7}{(I)LGL}}}(\mathcal{X})$ is an (I)LGL algebra.

Any valuation $\Valuation$ on an (I)LGL frame $\mathcal{X}$ generates an interpretation $\Interp{-}_{\Valuation}$ on the complex algebra $Com^{\text{\scalebox{.7}{(I)LGL}}}(\mathcal{X})$. A straightforward inductive argument then shows satisfiability coincides on these two models.

For any relational (I)LGL model $(\mathcal{X}, \Valuation)$, $x \vDash_{\mathcal{V}} \varphi$ iff $x \in \Interp{\varphi}_{\Valuation}$.

Conversely we can create ILGL frames from ILGL algebras. First we will need a sequence of definitions. A filter on a bounded distributive lattice $\mathbb{A}$ is a non-empty set $F \subseteq A$ such that, for all $x, y \in A$, (i) $x \in F$ and $x \leq y$ implies $y \in F$, and (ii) $x, y \in F$ implies $x \land y \in F$. It is a proper filter if it additionally satisfies (iii) $\bot \not\in F$. It is prime if in addition it satisfies (iv) $x \lor y \in F$ implies $x \in F$ or $y \in F$. If $\mathbb{A}$ is a Boolean algebra and $F$ a proper filter, (iv) is equivalent to (v) $x \in F$ or $\neg x \in F$ and (vi) $F$ is a maximal proper filter with respect to $\subseteq$. The order-dual notion of a filter is an ideal, with proper and prime ideals defined as one would expect. Importantly, if $I$ is a prime ideal then the complement $\overline{I}$ is a prime filter.

Given a non-empty subset $X$ of an algebra $\mathbb{A}$, we define

\[
\filter{X} := \{ a \in \mathbb{A} \mid \exists b_1, \ldots, b_n \in X: a \geq b_1 \land \cdots \land b_n \}
\]

to be the filter generated by $X$. It is easily seen that this is the least filter (with respect to set theoretic inclusion) containing the set $X$. Dually, we obtain the ideal generated by X as $\ideal{X} := \{ a \in \mathbb{A} \mid \exists b_1, \ldots, b_n \in X: b_1 \lor \cdots \lor b_n \geq a \}$, and this is the least ideal containing $X$. For a singleton $\{ a\}$ we write $\filter{a}$ and $\ideal{a}$ for $\filter{\{a\}}$ and $\ideal{\{a\}}$.

We will frequently need to prove the existence of prime filters/ideals satisfying certain properties in order to prove our duality theoretic framework captures the structures associated with bunched logics. To this end we generalize a concept of Galmiche & Larchey-Wendling [44] that gives a systematic method for showing such prime filters/ideals exist. First some terminology: a $\subseteq$-chain is a sequence of sets ${(X_{\alpha})}_{\alpha < \lambda}$ such that $\alpha \leq \alpha'$ implies $X_{\alpha} \subseteq X_{\alpha'}$. A basic fact about proper filters (ideals) is that the union of a $\subseteq$-chain of proper filters (ideals) is itself a proper filter (ideal). We lift the terminology to $n$-tuples of sets by determining ${(X^1_{\alpha}, \ldots, X^n_{\alpha})}_{\alpha < \lambda}$ to be a $\subseteq$-chain if each ${(X^i_{\alpha})}_{\alpha < \lambda}$ is a $\subseteq$-chain.

[Prime Predicate]
A prime predicate is a map $P: \mathbb{F}_{\mathbb{A}}^n \times \mathbb{I}_{\mathbb{A}}^m \rightarrow \{ 0, 1\}$, where $n, m \geq 0$ and $n + m \geq 1$, such that

* Given a $\subseteq$-chain ${(F^0_{\alpha}, \ldots, F^n_{\alpha}, I^0_{\alpha}, \ldots, I^m_{\alpha})}_{\alpha < \lambda}$ of proper filters/ideals,
\[\min \{ P(F^0_{\alpha}, \ldots, I^m_{\alpha}) \mid \alpha < \lambda \} \leq P(\bigcup_\alpha F^0_\alpha, \ldots, \bigcup_{\alpha} I^m_{\alpha})\]

* $P(\ldots, H_0 \cap H_1, \ldots) \leq \max\{P(\ldots, H_0, \ldots), P(\ldots, H_1, \ldots)\}$.

A prime predicate is a property that can hold of an $(n+m)$-tuple of proper filters and ideals that is evaluated to true or false. The two simple conditions it must satisfy to be a prime predicate are that the truth of the property persists from a chain of tuples of proper filters and ideals to their component-wise union and that if an n-tuple of proper filters and ideals for which one component is an intersection $H_0 \cap H_1$ is evaluated true, at least one of the tuples of prime filters and ideals obtained by replacing that intersection with either $H_0$ or $H_1$ is also evaluated true. Our definition differs from that of Galmiche & Larchey-Wendling in a key way: our notion of prime predicate takes an argument of tuples of proper filters and ideals rather than a single filter, as we frequently need to prove the simultaneous existence of prime filters and ideals satisfying a particular condition. This will always follow from the following important lemma, which is easily proved using Zorn's lemma.

If $P$ is an $(n+m)$-ary prime predicate and $F_0, \ldots, F_n, I_0, \ldots, I_m$ an $(n+m)$-tuple of proper filters and ideals such that

\[
P(F_0, \ldots, F_n, I_0, \ldots, I_m) = 1
\]

then there exists a $(n+m)$-tuple of prime filters and ideals $F^{pr}_0, \ldots, F^{pr}_n, I^{pr}_0, \ldots I^{pr}_m$ such that

\begin{equation*}
P(F^{pr}_0, \ldots, F^{pr}_n, I^{pr}_0, \ldots I^{pr}_m)=1 \tag*{\qed}
\end{equation*}

We now return to the task at hand.

[Prime Filter (I)LGL Frame]
Given an (I)LGL algebra $\mathbb{A}$, the prime filter frame of $\mathbb{A}$ is given by $Pr^{\text{\scalebox{.7}{(I)LGL}}}(\mathbb{A}) = (Pr(A), \subseteq, \circ_{\mathbb{A}})$ where

\begin{equation*}
F \circ_{\mathbb{A}} F' = \{ F'' \in Pr(\mathbb{A}) \mid \forall a \in F, \forall b \in F': a * b \in F'' \}. \tag*{\qed} % chktex 35
\end{equation*}

Of course, because of the structure of prime filters on Boolean algebras, the order $\subseteq$ collapses to $=$ for a prime filter LGL frame, as we would expect.

Given an (I)LGL algebra $\mathbb{A}$, $Pr^\vtiny{(I)LGL}(\mathbb{A})$ is an (I)LGL frame.

In analogy with Stone's representation theorem for Boolean algebras, we can give a representation theorem for (I)LGL algebras using these constructions. In particular, for ILGL algebras this extends the representation theorem for Heyting algebras [41], whereas for LGL algebras this extends Stone's theorem. These results are closely related to various representation theorems for algebras with operators (e.g., [55], [47]). The key difference  is the use of a single operation $\circ$ for the operator $*$ and its non-operator adjoints $\wand$ and $\dnaw$. The derived structure required to take care of these adjoints was not investigated in the frameworks of Jónsson-Tarski or Goldblatt but has been in the context of gaggle theory [7, 40]. There the result for LGL algebras can be found as a particular case of that for Boolean gaggles ([7], Theorem 1.4.16).

Every (I)LGL algebra is isomorphic to a subalgebra of a complex algebra. Specifically, given an (I)LGL algebra $\mathbb{A}$, the map $\theta_{\mathbb{A}}: \mathbb{A} \rightarrow Com^\vtiny{(I)LGL}(Pr^\vtiny{(I)LGL}(\mathbb{A}))$ defined $\theta_{\mathbb{A}}(a) = \{ F \in Pr^\vtiny{(I)LGL}(\mathbb{A}) \mid a \in F \}$ is an embedding.

We prove the theorem for ILGL algebras; the case for LGL algebras can be obtained by substituting $\succcurlyeq$ for $=$ throughout. That $\theta_{\mathbb{A}}$ is an embedding and a homomorphism on the Heyting algebra operations is simply the representation theorem for Heyting algebras. It thus remains to show that $\theta_{\mathbb{A}}$ respects $*, \wand$ and $\dnaw$. We focus on the case for $\wand$; the others are similar.

We first note the corner cases: for all $a, b \in A$ we trivially have that $\theta_{\mathbb{A}}(a \wand \top) = \theta_{\mathbb{A}}(a) \Rres_{Pr(\mathbb{A})} \theta_{\mathbb{A}}(\top)$ and $\theta_{\mathbb{A}}(\bot \wand b) = \theta_{\mathbb{A}}(\bot) \Rres_{Pr(\mathbb{A})} \theta_{\mathbb{A}}(b)$ by Proposition <ref> property 6. Hence it is sufficient to consider $a \wand b$ where $a \neq \bot$ and $b \neq \top$.
For the inclusion
$\theta_{\mathbb{A}}(a\wand b) \subseteq \theta_{\mathbb{A}}(a) \Rres_{Pr(\mathbb{A})} \theta_{\mathbb{A}}(b)$, assume $a \wand b \in F$ with $F_0, F_1, F_2$ such that $F \subseteq F_0$, $F_2 \in F_0 \circ_{\mathbb{A}} F_1$ and $a \in F_1$. Then $(a \wand b) * a \in F_2$ and so $b \in F_2$ since residuation entails $(a \wand b) * a \leq b$ and $F_2$ is upwards closed. Hence $F \in \theta_{\mathbb{A}}(a) \Rres_{Pr(\mathbb{A})} \theta_{\mathbb{A}}(b)$.

For the reverse inclusion, consider $F$ such that $a \wand b \not\in F$. We show, for proper filter $G$ and proper ideal $I$, that (abusing notation for $\circ_{\mathbb{A}}$)

\[ P(G, I) =\begin{cases} 1 & \text{if } \overline{I} \in F \circ_{\mathbb{A}} G, a \in G \text{ and } b \in I \\
0 & \text{otherwise} \end{cases} \]
is a prime predicate.
We concentrate on the non-trivial verifications: suppose $P(G \cap G', I) =1$. Clearly, $a \in G, G'$ so suppose for contradiction that there exists $c, c' \in F$, $d \in G$ and $d' \in G'$ such that $c * d, c' * d' \in I$. We have that $c'' := c \land c' \in F$ and $c'' * d, c'' * d' \in I$. This entails $c'' * (d \lor d') = (c'' * d) \lor (c'' * d') \in I$. Since $d \lor d' \in G \cap G'$ we have $c'' * (d \lor d') \not\in I$ by assumption: a contradiction. Hence either $\overline{I} \in F \circ_{\mathbb{A}} G$ or $\overline{I} \in F \circ_{\mathbb{A}} G'$. If $P(G, I \cap I') = 1$ we clearly have $b \in I, I'$, so suppose for contradiction there exist $c, c' \in F$, $d, d' \in G$ such that $c * d \in I$ and $c' * d' \in I'$. $c'' = c \land c' \in F$ and $d'' = d \land d' \in G$ so we have $c'' * d'' \in \overline{I} \cup \overline{I'}$. This means $c'' * d'' \in \overline{I}$ or $c'' * d'' \in \overline{I'}$, but $c * d, c' * d' \geq c'' * d'' \in I \cap I'$, a contradiction. Thus either $\overline{I} \in F \circ_{\mathbb{A}} G$ or $\overline{I'} \in F \circ_{\mathbb{A}} G$.

Hence $P$ is a prime predicate. By our assumption on $a$ and $b$, $\filter{a}$ and $\ideal{b}$ are a proper filter and a proper ideal respectively, and $P(\filter{a}, \ideal{b}) =1$: if $x \in F$ and $y \geq a$ then $x * y \not\leq b$, otherwise by residuation and monotonicity of $*$ we would have $x \leq a \wand b \in F$, a contradiction. Hence by Lemma <ref> there exist prime $G$ and $I$ with $P(G, I) =1$. Letting $G' = \overline{I}$, we have the prime filters  we require.

That $\theta_{\mathbb{A}}$ is an embedding immediately gives us an analogous result to Prop. <ref> and thus a soundness and completeness theorem for the “relational” semantics of the logics.

For all (I)LGL algebras $\mathbb{A}$: given an interpretation $\Interp{-}$, the valuation $\Valuation_{\Interp{-}}(p) = \theta_{\mathbb{A}}(\Interp{p})$ on $Pr^\vtiny{(I)LGL}(\mathbb{A})$ is such that $\Interp{\varphi} \in F$  iff $F \vDash_{\Valuation_{\Interp{-}}} \varphi$.

For all formulas $\varphi, \psi$ of (I)LGL: $\varphi \vdash \psi$ is provable in $\mathrm{(I)LGL}_{\mathrm{H}}$ iff $\varphi \vDash \psi$ in the relational semantics.

The assignment of complex algebras and prime filter frames can be made functorial by defining $Pr^\vtiny{(I)LGL}(f) = f^{-1}$ and $Com^\vtiny{(I)LGL}(g) = g^{-1}$: that these define the appropriate morphisms is a straightforward but tedious verification.

The functors $Pr^{\vtiny{(I)LGL}}$ and $Com^{\vtiny{(I)LGL}}$ are well defined.

However we are not yet in a position to give a dual equivalence of categories: in particular, a dual adjunction does not hold between these functors: there exist frames $\mathcal{X}$ such that no morphism exists between $\mathcal{X}$ and $Pr^{\vtiny{(I)LGL}}Com^{\vtiny{(I)LGL}}(\mathcal{X})$ (cf. Venema's comments <cit.>). We can obtain this by introducing topology, however. We first define ILGL spaces. This definition (necessarily) extends that of the topological duals of Heyting algebra given by Esakia duality [42]. The coherence conditions on the composition $\circ$ are inspired by those found on the topological duals of gaggles [7].

[ILGL Space]
An ILGL space is a structure $\mathcal{X} = (X, \mathcal{O}, \preccurlyeq, \circ)$ such that:

* $(X, \mathcal{O}, \preccurlyeq)$ is an Esakia space [42];

* $(X, \preccurlyeq, \circ)$ is an ILGL frame;

* The upwards-closed clopen sets of $(X, \mathcal{O}, \preccurlyeq)$ are closed under $\bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}, \Lres_{\mathcal{X}}$;

* If $x \not\in y \circ z$ then there exist upwards-closed clopen sets $C_1, C_2$ such that $y \in C_1, z \in C_2$ and $x \not\in C_1 \bullet_{\mathcal{X}} C_2$.

A morphism of ILGL spaces is a continuous ILGL morphism, yielding a category $\mathrm{ILGLSp}$.

Once again, substituting $\preccurlyeq$ for $=$ in the definition of ILGL space obtains the topological duals for LGL algebras.

[LGL Space]
An LGL space is a structure $\mathcal{X} = (X, \mathcal{O}, \circ)$ such that

* $(X, \mathcal{O})$ is an Stone space [74];

* $(X, \circ)$ is an LGL frame;

* The clopen sets of $(X, \mathcal{O})$ are closed under $\bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}, \Lres_{\mathcal{X}}$;

* If $x \not\in y \circ z$ then there exist clopen sets $C_1, C_2$ such that $y \in C_1, z \in C_2$ and $x \not\in C_1 \bullet_{\mathcal{X}} C_2$.

A morphism of LGL spaces is a continuous LGL morphism, yielding a category $\mathrm{LGLSp}$.

We now adapt $Pr^\vtiny{(I)LGL}$ and $Com^\vtiny{(I)LGL}$ for these categories and define the natural isomorphisms obtaining the duality.  First, it is straightforward to augment the prime filter frame with the topological structure required to make it an (I)LGL space. We define a subbase by $S = \{ \theta_{\mathbb{A}}(a) \mid a \in A \} \cup \{ \overline{\theta_{\mathbb{A}}(a)} \mid a \in A \}$ where $\overline{\theta_{\mathbb{A}}(a)}$ denotes the set complement. This generates a topology $\mathcal{O}_{\mathbb{A}}$ and we can (abusing notation) define $Pr^\vtiny{ILGL}: \mathrm{ILGLAlg} \rightarrow \mathrm{ILGLSp}$ by $Pr^\vtiny{ILGL}(\mathbb{A}) = (Pr(A), \mathcal{O}_{\mathbb{A}}, \subseteq, \circ_{\mathbb{A}})$ and $Pr^\vtiny{ILGL}(f) = f^{-1}$. In the case of LGL, the sets $\overline{\theta_{\mathbb{A}}(a)}$ are redundant as for every prime filter $F$ on a Boolean algebra $\mathbb{A}$, $a \in A$ implies $a \in F$ or $\neg a \in F$. Hence $\mathcal{B} = \{ \theta_{\mathbb{A}}(a) \mid a \in A \}$ defines a base for a topology $\mathcal{O}_{\mathbb{A}}$ and we can set $Pr^\vtiny{LGL}(\mathbb{A}) = (Pr(A), \mathcal{O}_{\mathbb{A}}, \circ_{\mathbb{A}})$ and $Pr^\vtiny{LGL}(f) = f^{-1}$.

Conversely, given an ILGL space $\mathcal{X}$ we now take the set of upwards-closed clopen sets $\mathcal{CL}_{\succcurlyeq}(\mathcal{X})$ as the carrier of an ILGL algebra, together with the operations of the ILGL complex algebra; ILGL space property (3) ensures this is well defined. Hence we take $Clop^\vtiny{ILGL}: \mathrm{ILGLSp} \rightarrow \mathrm{ILGLAlg}$ to be $Clop^\vtiny{ILGL}(\mathcal{X}) = (\mathcal{CL}_{\succcurlyeq}(\mathcal{X}), \cap, \cup, \Rightarrow, X, \emptyset, \bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}, \Lres_{\mathcal{X}})$ and $Clop^\vtiny{ILGL}(g) = g^{-1}$.  For LGL we simply take the clopen sets of the underlying topological space $\mathcal{CL}(\mathcal{X})$ together with the operations of the LGL complex algebra. Hence $Clop^\vtiny{LGL}(\mathcal{X}) = (\mathcal{CL}(\mathcal{X}), \cap, \cup, \setminus, X, \emptyset, \bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}, \Lres_{\mathcal{X}})$ and $Clop^\vtiny{LGL}(g) = g^{-1}$.

The well-definedness of these functors can be seen by straightforwardly combining Stone (Esakia) duality for Boolean (Heyting) algebras with the preceding results relating to (I)LGL structures. For natural transformations, one — $\theta$ — is already defined in the representation theorem. The other is given by  $\eta_{\mathcal{X}}(x) = \{ A \in Clop^\vtiny{(I)LGL}(\mathcal{X}) \mid x \in A \}$. That these are natural isomorphisms is an easy extension of the case for Stone (Esakia) duality, with the additional verification that each $\eta_{\mathcal{X}}$ is an isomorphism on the (I)LGL frame structure following from (I)LGL space property (4). We thus obtain the duality theorem. For LGL algebras this is also obtainable as a specific case of Bimbó & Dunn's duality theorem for Boolean gaggles ([7], Theorem 9.2.22).

$\theta: Id_{\mathrm{(I)LGLAlg}} \rightarrow Clop^{\vtiny{(I)LGL}}_{\succcurlyeq}$ and $\eta: Id_{\mathrm{(I)LGLSp}} \rightarrow Pr^{\vtiny{(I)LGL}}Clop^{\vtiny{(I)LGL}}_{\succcurlyeq}$ form a dual equivalence of categories between $\mathrm{(I)LGLAlg}$ and $\mathrm{(I)LGLSp}$.

§ LOGICS OF BUNCHED IMPLICATIONS

§.§ Algebra and Frames for (B)BI

We now extend the results of the previous section to the logics BI and BBI by systematically extending the structures defined for LGL and ILGL. We begin once again with the lattice-based algebras that interpret the logics.

[(B)BI Algebra]

* A BI algebra is an algebra $\mathbb{A} = (A, \land, \lor, \rightarrow, \top, \bot, *, \wand, \mtop)$
such that $(A, \land, \lor, \rightarrow, \top, \bot, *, \wand, \wand)$ is an ILGL algebra and $(A, *, \mtop)$ a commutative monoid: that is, $*$ is commutative and associative with $\mtop$ a unit for $*$.

* A BBI algebra is a BI algebra $\mathbb{A} = (A, \land, \lor, \rightarrow, \top, \bot, *, \wand, \mtop)$ for which $(A, \land, \lor, \rightarrow, \top, \bot)$ is a Boolean algebra.

Thus BI algebras are the subclass of ILGL algebras with a commutative and associative $*$ that has unit $\mtop$, and likewise for BBI algebras with respect to LGL algebras. In particular, commutativity of $*$, together with residuation, causes $\wand = \dnaw$.  Interpretations on BI and BBI algebras are given in much the same way as ILGL and LGL algebras, with the addition of $\Interp{\mtop} = \mtop$. A soundness and completeness theorem for algebraic interpretations is proved in the same fashion as Theorem <ref>.

For (B)BI formulas $\varphi$, $\psi$, $\varphi \vdash \psi$ is provable in $\mathrm{(B)BI}_{\mathrm{H}}$ iff for all (B)BI algebras $\mathbb{A}$ and all interpretations $\Interp{-}$ on $\mathbb{A}$, $\Interp{\varphi} \leq \Interp{\psi}$.

Next we define a class of relational models appropriate for interpreting (B)BI. The outermost universal quantification in each frame condition is left implicit for readability.

[BI Frame]
A BI Frame is a tuple $\mathcal{X} = (X, \succcurlyeq, \circ, E)$ where $(X, \succcurlyeq, \circ)$ is an ILGL frame, $E \subseteq X$ and the following conditions are satisfied:

\[\begin{array}{rlrl}
\text{(Commutativity)} & z \in x \circ y \rightarrow z \in y \circ x & \text{(Closure)} & e \in E \land e' \succcurlyeq e \rightarrow e' \in E \\
\text{(Unit Existence)} & \exists e \in E(x \in x \circ e) & \text{(Coherence)} & e \in E \land x \in y \circ e \rightarrow x \succcurlyeq y \\
\multicolumn{4}{l}{\text{(Associativity) } t' \succcurlyeq t \in x \circ y \land w \in t' \circ z \rightarrow \exists s, s', w'(s' \succcurlyeq s \in y \circ z \land w \succcurlyeq w' \in x \circ s')} \qed
\end{array}\]

The notion of BI frame and its associated semantics can be defined in many ways, and indeed those given in Section <ref> can suffice for a duality theorem if one defines the natural transformations and morphisms slightly differently. These choices are driven by the requirements that the model validates the associativity axiom and that the semantic clauses for $*$ and $\wand$ satisfy persistence. This requires careful interplay between the definition of (Associativity), the conditions relating $\circ$ and $\preccurlyeq$, and the semantic clauses for $*$ and $\wand$. One such solution is that given in the original papers on BI [68], in which $\circ$ is a deterministic,  associative function that is bifunctorial with respsect to the order. This is complicated somewhat when $\circ$ is non-deterministic and partial, however. A general analysis of the choices available for such a $\circ$ when the definition of the associativity-like condition it satisfies is kept fixed can be found in the work of Cao et al. [19].

Here, we use a definition that enables a uniform extension of the structures and theorems relating to ILGL. In particular, we use a more general than usual formulation of (Associativity) that allows us to directly extend the results of Section <ref>. This solution places no coherence conditions on $\circ$ and $\preccurlyeq$ and thus requires what Cao et al. [19] call the “strong semantics” for $*$ and $\wand$ to maintain persistence: precisely the clauses given for (I)LGL frames (Fig. <ref>) together with the semantic clause for $\mtop$ given in Fig. <ref>.

$x$     $\vDash_{\mathcal{V}}$     $\mtop$     iff     l$x \in E$

Satisfaction for (B)BI.

This can be seen as a strict generalization of the UDMF models given in Section <ref>, as witnessed by the fact that the definition of non-deterministic associativity given there implies the frame condition (Associativity) when $\circ$ is additionally upwards and downwards closed.

Every upwards and downwards closed monoidal frame is a BI frame.

Further, the respective semantic clauses for $*$ and $\wand$ are equivalent when the underlying model is upwards and downwards closed [19]. The converse does not hold: not every BI frame is upwards or downwards closed. However, every BI frame generates a upwards and downwards closed monoidal frame with an equivalent satisfaction relation. Given a BI frame $\mathcal{X} = (X, \preccurlyeq, \circ, E)$, define its upwards and downwards closure by $\mathcal{X}^{\Uparrow \Downarrow} = (X, \preccurlyeq, \circ^{\Uparrow \Downarrow}, E)$ where $x \in y \circ^{\Uparrow \Downarrow} z$ iff there exist $x', y', z'$ such that $x' \preccurlyeq x$, $y \preccurlyeq y'$, $z \preccurlyeq z'$ and $x' \in y' \circ z'$. By taking care over the respective associativity properties of each frame, this can easily be seen to be an upwards and downwards closed monoidal frame. Letting $\vDash'$ denote the satisfaction relation defined for UDMFs in Fig. <ref>, we have the following result.

For all BI frames $\mathcal{X}$, persistent valuations $\mathcal{V}$ and formulas $\varphi$ of BI, $\mathcal{X}, x \vDash_{\mathcal{V}} \varphi$ iff $\mathcal{X}^{\Uparrow \Downarrow}, x \vDash'_{\mathcal{V}} \varphi$.

So, as far as the logic is concerned, these choices are academic: they all collapse to the same notion of validity. For models satisfying one or both of upwards and downwards closure this is implicit in the preservation results of Cao et al. [19]. Our analysis of the remaining class of models that lack both conditions on $\circ$ and $\preccurlyeq$ completes this picture.

A BBI frame $\framefont{X}$ is a triple $\framefont{X} = (X, \circ, E)$, such that  $(X, \circ)$ is an LGL frame, $E \subseteq X$ and the following conditions are satisfied:

\[	\begin{array}{llllr}
\text{(Commutativity)} & z \in x \circ y \rightarrow z \in y \circ x & \text{(Coherence)} &
x \in y \circ e \land e \in E \rightarrow y = x. \\ %\text{(Associativity)} & t \in x \circ y \land w \in t \circ z \rightarrow \exists s(s \in y \circ z \land w \in x \circ s) \\
\text{(Unit Existence)} & \exists e \in E(x \in x \circ e) &   \\
\multicolumn{4}{l}{\text{(Associativity) } \quad t \in x \circ y \land w \in t \circ z \rightarrow \exists s(s \in y \circ z \land w \in x \circ s)} & \qed
\end{array}  \]

We note that when $\preccurlyeq$ is substituted for $=$, all sound choices of the (Associativity) axiom that were possible for BI frames collapse to the axiom given here, while every coherence condition on $\circ$ and $\preccurlyeq$ becomes trivial. Thus, in comparison to BI, there are far fewer choices to be made about BBI models and so this definition is more familiar, appearing in the literature in precisely the same form as BBI frames [14] and non-deterministic monoids [61], and slightly modified as multi-unit separation algebras [38] and relational frames [44].

The key difference with the latter definitions is that multi-unit separation algebras are cancellative — $z \in x \circ y$ and $z \in x \circ y'$ implies $y = y'$ — and relational frames have a single unit. BBI frames do not enforce cancellativity and have multiple units. This difference is crucial for the present work as the duality theorems do not hold when we restrict to frames satisfying either of these properties. This is witnessed by the fact that BBI is not expressive enough to distinguish between cancellative/non-cancellative models and single unit/multi-unit models [14], all of which define the same notion of validity [61]. An interpretation of the duality theorem might thus be that BBI frames are the most general relational structures that soundly and completely interpret BBI.

[(B)BI Morphism]
Given (B)BI frames $\mathcal{X}$ and $\mathcal{X'}$, a (B)BI morphism is an ILGL (LGL) morphism $g: \mathcal{X} \rightarrow \mathcal{X}'$ that additionally satisfies $\text{(7) } e \in E \text{ iff } g(e) \in E'$.

BI frames together with BI morphisms form a category $\mathrm{BIFr}$, itself a subcategory of $\mathrm{ILGLFr}$; likewise, BBI frames and BBI morphisms form the category $\mathrm{BBIFr}$, a subcategory of $\mathrm{LGLFr}$. Note that commutativity of $\circ$ collapses the final conditions in the definition of (I)LGL morphism when defined on BBI (BI) frames.  As in the case for the layered graph logics, surjective (B)BI morphisms preserve validity in models.

We now relate the two categories of (B)BI semantic structures with functorial transformations and a representation theorem.

[(B)BI Complex Algebra]
Given a (B)BI frame $\mathcal{X} $, the complex algebra of $\mathcal{X}$, $Com^\vtiny{(B)BI}(\mathcal{X})$ is given by extending $Com^\vtiny{ILGL}(\mathcal{X})$ ($Com^\vtiny{LGL}(\mathcal{X})$) with the unit set of $\mathcal{X}$, $E$.

Given a (B)BI frame $\mathcal{X}$, $Com^\vtiny{(B)BI}(\mathcal{X})$ is a (B)BI algebra.

As a special case of the analogous result for (I)LGL, we obtain a correspondence between satisfiability on a frame and its complex algebra when the algebraic interpretation is generated by the valuation on the frame.

For any (B)BI frame $\mathcal{X}$ and valuation $\Valuation$, $x \vDash_{\Valuation} \varphi$ iff $x \in \Interp{\varphi}_{\mathcal{V}}$.

In the other direction we transform BI algebras into BI frames.

[Prime Filter (B)BI Frame]
Given a (B)BI algebra $\mathbb{A}$, the prime filter frame of $\mathbb{A}$, $Pr^\vtiny{(B)BI}(\mathbb{A})$, is given by extending $Pr^\vtiny{ILGL}(\mathbb{A})$ ($Pr^{\vtiny{LGL}}(\mathbb{A}))$ with $E_{\mathbb{A}} = \{ F \in Pr(A) \mid \mtop \in F \}$.

That the prime filter frame of a (B)BI algebra is a (B)BI frame follows an argument very similar to that of Galmiche & Larchey-Wendling's [44] completeness theorem for the relational semantics of BBI.

Given a (B)BI algebra $\mathbb{A}$, the prime filter frame $Pr^\vtiny{(B)BI}(\mathbb{A})$ is a (B)BI frame.

Commutativity of $\circ_{\mathbb{A}}$ can be read off the definition, given that $*$ is commutative for (B)BI. We also have that $E$ satisfies Closure trivially. We are left to verify Associativity, Unit Existence and Coherence. We note that in the case for BBI, maximality of prime filters collapses all of the inclusions to equalities in what follows, so we just give the argument for BI.

First, Associativity. Assume $F_{t'} \supseteq F_{t} \in F_x \circ F_y$ and $F_w \in F_{t'} \circ F_z$. We show that
\[ \PrimePredicate{F}{F \in F_y \circ_{\mathbb{A}} F_z \text{ and } F_w \in F_x \circ_{\mathbb{A}} F}\]

is a prime predicate. For a $\subseteq$-chain ${(F_\alpha)}_{\alpha < \lambda}$ such that $P(F_\alpha) = 1$ for all $\alpha$, we straightforwardly have $P(\bigcup_\alpha F_\alpha) = 1$. If $P(F \cap F') =1$, we have that $F, F' \in F_y \circ F_z$ immediately, so suppose for contradiction that there exists $a, a' \in F_x$, $b \in F$, $b' \in F'$ such that $a * b, a' * b' \not\in F_w$. We have that $a'' = a \land a' \in F_x$ and $b \lor b' \in F \cap F'$ so $a'' * (b \lor b') = (a'' * b) \lor (a'' * b') \in F_w$. Since $F_w$ is prime, either $a'' * b \in F_w$ or $a'' * b' \in F_w$. Thus, because $*$ is monotone, $a * b \in F_w$ or $a' * b' \in F_w$,  a contradiction.

Now consider the set $F = \{ a \in \mathbb{A} \mid \exists b \in F_y, c \in F_z: a \geq b * c\}$. We show this is a proper filter satisfying $P(F) = 1$. First, suppose for contradiction that $\bot \in F$. Then there exists $b \in F_y$ and $c \in F_z$ such that $b* c = \bot$. Letting $a \in F_x$ be arbitrary, we have that $a * b \in F_t \subseteq F_{t'}$, so $(a * b) * c = a * (b * c) = a * \bot = \bot \in F_w$, contradicting that $F_w$ is proper. $F$ is clearly upwards-closed; to see it is closed under meets, consider $a, a' \in F$. Then there exists $b, b' \in F_y$ and $c, c' \in F_z$ such that $a \geq b * c$ and $a' \geq b' * c'$. We have that $b \land b' \in F_y$ and $c \land c' \in F_z$, and by monotonicity of $*$, $(b \land b') * (c \land c') \leq a * b, a' * b'$. Hence $(b \land b') * (c \land c') \leq (a * b) \land  (a' * b') \leq c \land c'$ as required.

We now verify that $P(F) = 1$. Let $b \in F_y$ and $c \in F_z$. Clearly $b * c \in F$, so $F \in F_y \circ_{\mathbb{A}} F_z$. If $a \in F_x$ and $a' \geq b * c$ for $b \in F_y$ and $c \in F_z$, we have that $a * a' \geq a * (b * c) = (a * b) * c \in F_w$, since $a * b \in F_t \subseteq F_{t'}$ and $c \in F_z$. Thus $a * a' \in F_w$ and $F_w \in F_x \circ_{\mathbb{A}} F$ as required. We thus obtain a prime $F$ with $P(F) =1$ by the Prime Extension Lemma, which is precisely what is required to satisfy Associativity.

For Unit Existence, let $F$ be an arbitrary prime filter. We show that
\[ \PrimePredicate{G}{F \in F \circ_\mathbb{A} G\text{ and } \mtop \in G} \]
is a prime predicate. If $P(G_\alpha) =1$ for all $G_\alpha$ in a $\subseteq$-chain ${(G_\alpha)}_{\alpha < \lambda}$ then clearly $F \in F \circ_{\mathbb{A}} \bigcup_\alpha G_\alpha$. Next, let $P(G \cap G') =1$ and assume for contradiction that there exists $a, a' \in F$, $b \in G$ and $b' \in G'$ such that $a * b \not\in F$ and $a' * b' \not\in F$. $b \lor b' \in G \cap G'$ so for $a'' = a \land a' \in F$ we have $a'' * (b \lor b') = (a'' * b) \lor (a'' * b') \in F$. Since $F$ is prime, either $a'' * b \in F$ or $a'' * b' \in F$. Hence, by monotonicity of $*$, either $a * b \in F$ or $a' * b' \in F$, a contradiction. Now consider the filter $\filter{\mtop}$. We note that this can only fail to be proper when $\mtop = \bot$, but in that case it can be shown that for all $a \in \mathbb{A}$, $a = \bot$, and thus $\mathbb{A}$ is degenerate and not a BI algebra. Given any $a \in F$ and $b \geq \mtop$, we have $a * b \geq a * \mtop = a \in F$, so $a * b \in F$. Since $P(\filter{\mtop}) = 1$, there exists a prime filter $F$ with $P(F) =1$, and so Unit Existence is satisfied.

Finally, for Coherence, assume $F_x \in F_y \circ F_e$ where $\mtop \in F_e$. Then for all $a \in F_y$, $a * \mtop = a \in F_x$, so $F_y \subseteq F_x$ as required.

The representation theorem for (B)BI algebras now follows immediately from the analogous result for (I)LGL algebras and the fact that $\theta_{\mathbb{A}}(\mtop) = E_{\mathbb{A}}$.

Every (B)BI algebra is isomorphic to a subalgebra of a complex algebra. Specifically, given a (B)BI algebra $\mathbb{A}$, the map $\theta_{\mathbb{A}}: \mathbb{A} \rightarrow Com^\vtiny{(B)BI}(Pr^\vtiny{(B)BI}(\mathbb{A}))$ defined $\theta_{\mathbb{A}}(a) = \{ F \in Pr^\vtiny{(B)BI}(A) \mid a \in F \}$ is an embedding.

For all (B)BI algebras $\mathbb{A}$, given an interpretation $\Interp{-}$, the valuation $\Valuation_{\Interp{-}}(p) = \theta_{\mathbb{A}}(\Interp{p})$ on $Pr^\vtiny{(B)BI}(\mathbb{A})$ is such that $\Interp{\varphi} \in F$ iff $F \vDash_{\Valuation_{\Interp{-}}} \varphi$.

For all formulas $\varphi$, $\psi$ of $\logicfont{BI}$, $\varphi \vdash \psi$ is provable in $\mathrm{BI}_{\mathrm{H}}$ iff $\varphi \vDash \psi$ in the relational semantics.

Once again $Pr^\vtiny{(B)BI}$ and $Com^\vtiny{(B)BI}$ can be made into functors by setting $Pr^\vtiny{(B)BI}(f) = f^{-1}$ and $Com^\vtiny{(B)BI}(g) = g^{-1}$.

To obtain a dual equivalence of categories we add topological structure to BI frames. This can be achieved by straightforwardly extending (I)LGL spaces with BBI (BI) frame structure and specifying a coherence condition for the unit set $E$.

[BI Space]
A BI space is a structure $\mathcal{X} = (X, \mathcal{O}, \preccurlyeq, \circ, E)$ such that

* $(X, \mathcal{O}, \preccurlyeq, \circ)$ is an ILGL space,

* $(X, \preccurlyeq, \circ, E)$ is a BI frame, and

* $E$ is clopen in $(X, \mathcal{O})$.

A morphism of BI spaces is a continuous BI morphism, yielding a category $\mathrm{BISp}$.

[BBI Space]
A BBI space is a structure $\mathcal{X} = (X, \mathcal{O}, \circ, E)$ such that

* $(X, \mathcal{O}, \circ)$ is an LGL space,

* $(X, \circ, E)$ is a BBI frame, and

* $E$ is clopen in $(X, \mathcal{O})$.

A morphism of BBI spaces is a continuous BBI morphism, yielding a category $\mathrm{BBISp}$.

The duality theorems for BI and BBI follow essentially immediately from those for ILGL and LGL. The only additional structure that needs to be taken care of is the constant $\mtop$ and the unit set $E$. We define the functors and natural isomorphisms explicitly for their use in the Separation Logic duality. Hence for BI we have $Pr^\vtiny{BI}: \mathrm{BIAlg} \rightarrow \mathrm{BISp}$ defined by $Pr^\vtiny{BI}(\mathbb{A}) = (Pr(A), \mathcal{O}_{\mathbb{A}}, \subseteq, \circ_{\mathbb{A}}, E_{\mathbb{A}})$ (where $\mathcal{O}_{\mathbb{A}}$ is as defined for ILGL) and once again $Pr^\vtiny{BI}(f) = f^{-1}$; correspondingly, $Clop^\vtiny{BI}: \mathrm{BISp} \rightarrow \mathrm{BIAlg}$ is given by $Clop^\vtiny{BI}(\mathcal{X}) = (\mathcal{CL}_{\succcurlyeq}(\mathcal{X}), \cap, \cup, \Rightarrow, X, \emptyset, \bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}, E)$ (where $\bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}$ are the ILGL complex algebra operations) and, as in the case for ILGL, $Clop^\vtiny{BI}(g) = g^{-1}$; $\theta$ and $\eta$ are given precisely as they are in ILGL duality, relativized to $\mathrm{BIAlg}$ and $\mathrm{BISp}$.

Similarly, for BBI we have $Pr^\vtiny{BBI}(\mathbb{A}) = (Pr(A), \mathcal{O}_{\mathbb{A}}, \circ_{\mathbb{A}}, E_{\mathbb{A}})$ (where $\mathcal{O}_{\mathbb{A}}$ is as defined for LGL) and $Pr^\vtiny{BBI}(f) = f^{-1}$; $Clop^\vtiny{BBI}(\mathcal{X}) = (\mathcal{CL}(\mathcal{X}), \cap, \cup, \setminus, X, \emptyset, \bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}, E)$ (where $\bullet_{\mathcal{X}}, \Rres_{\mathcal{X}}$ are the LGL complex algebra operations) and $Clop^\vtiny{BBI}(g) = g^{-1}$; $\theta$ and $\eta$ are given precisely as they are in LGL duality, relativized to $\mathrm{BBIAlg}$ and $\mathrm{BBISp}$.

That $E_{\mathbb{A}}$ is clopen in each instance can be seen by the fact that $E = \theta_{\mathbb{A}}(\mtop)$. By Esakia duality, every set of the form $\theta_{\mathbb{A}}(a)$ for some $a \in A$ is an upwards-closed clopen set of the prime filter space of $\mathbb{A}$. Similarly, the clopen sets of the prime filter space of a Boolean algebra $\mathbb{A}$  are the sets $\theta_{\mathbb{A}}(a)$ for $a \in A$ by Stone duality, so the analogous property for BBI spaces holds too. It is also easy to see that the components of $\eta$ are additionally isomorphic with respect to $E$. The duality theorems thus obtain.  We note that the duality theorem for BI has been independently obtained by Jipsen & Litak [52].

$\theta$ and $\eta$ form a dual equivalence of categories between $\mathrm{(B)BIAlg}$ and $\mathrm{(B)BISp}$.

§ SEPARATION LOGIC

§.§ Hyperdoctrines and Indexed Frames for Separation Logic

We now extend the duality theorems for BI and BBI algebras to the algebraic and relational structures suitable for interpreting Separation Logic.
First, we must consider first-order (B)BI (FO(B)BI). Hilbert-type proof systems $\mathrm{FO(B)BI}_{\mathrm{H}}$ are obtained by extending those
given for (B)BI in Section <ref> with the usual rules for quantifiers (see, e.g., [75]).
Second, to give the semantics for the additional structure of $\logicfont{FO(B)BI}$, we expand the definitions
from the propositional case with category-theoretic structure. As these semantic structures support it,
we consider a many-sorted first-order logic. We start on the algebraic side with BI hyperdoctrines.

[(B)BI Hyperdoctrine (cf. [6])]
A (B)BI hyperdoctrine is a tuple

\[
(\algfont{P}: \catfont{C}^{op} \rightarrow \catfont{Poset}, {(=_X)}_{X \in Ob(\catfont{C})}, {(\exists X_{\Gamma}, \forall X_{\Gamma})}_{\Gamma, X \in Ob(\catfont{C})})
\]

such that:

* $\catfont{C}$ is a category with finite products;

* $\algfont{P}: \catfont{C}^{op} \rightarrow \catfont{Poset}$ is a functor such that, for each object $X$ in $\catfont{C}$, $\algfont{P}(X)$ is a (B)BI algebra, and, for each morphism $f$ in $\catfont{C}$, $\algfont{P}(f)$ is a (B)BI algebra homomorphism;

* For each object $X$ in $\catfont{C}$ and each diagonal morphism
$\Delta_X: X \rightarrow X \times X$ in $\catfont{C}$,  the element
$=_{X} \in \algfont{P}(X \times X)$ is adjoint at $\top_{\mathbb{P}(X)}$. That is, for all $a \in \algfont{P}(X \times X)$,

\[
\top_{\mathbb{P}(X)} \leq \algfont{P}(\Delta_X)(a) \text{ iff } =_{X} \leq a \,;
\]

* For each pair of objects $\Gamma, X$ in $\catfont{C}$ and each projection
$\pi_{\Gamma, X}: \Gamma \times X \rightarrow \Gamma$ in
$\catfont{C}$, $\exists X_{\Gamma}$ and $\forall X_{\Gamma}$ are left and right adjoint to $\mathbb{P}(\pi_{\Gamma, X})$. That is, they are monotone maps
$\exists X_{\Gamma}: \algfont{P}(\Gamma \times X) \rightarrow \algfont{P}(\Gamma)$ and
${\forall X_{\Gamma}: \algfont{P}(\Gamma \times X) \rightarrow \algfont{P}(\Gamma)}$
such that, for all $a, b \in \algfont{P}(\Gamma)$,

\[
\begin{array}{lll}
\exists X_{\Gamma}(a) \leq b & \text{iff} & a \leq \algfont{P}(\pi_{\Gamma, X})(b) \;\mbox{\rm and} \\
\algfont{P}(\pi_{\Gamma, X})(b) \leq a & \text{iff} & b \leq \forall X_{\Gamma}(a).
\end{array}
\]

This assignment of adjoints is additionally natural in $\Gamma$: given a morphism
$s: \Gamma \rightarrow \Gamma'$, the following diagrams commute:

\[
\begin{array}{lr}
\begin{tikzcd}
\algfont{P}(\Gamma' \times X) \arrow{r}{\algfont{P}(s \times id_X)} \arrow{d}[swap]{\exists X_{\Gamma'}} &
\algfont{P}(\Gamma \times X) \arrow{d}{\exists X_{\Gamma}} \\
\algfont{P}(\Gamma') \arrow{r}[swap]{\algfont{P}(s)} & \algfont{P}(\Gamma)
\end{tikzcd} & \begin{tikzcd}
\algfont{P}(\Gamma' \times X) \arrow{r}{\algfont{P}(s \times id_X)} \arrow{d}[swap]{\forall X_{\Gamma'}} &
\algfont{P}(\Gamma \times X) \arrow{d}{\forall X_{\Gamma}} \\
\algfont{P}(\Gamma') \arrow{r}[swap]{\algfont{P}(s)} & \algfont{P}(\Gamma)
\end{tikzcd}
\end{array} \]

(B)BI hyperdoctrines were first formulated by Biering et al. [6] to prove the existence of models of higher-order variants of Separation Logic. There it was shown that the standard model of Separation Logic could be seen as a BBI hyperdoctrine, and thus safely extended with additional structure in the domain $\mathrm{C}^{op}$ to directly define higher-order constructs like lists, trees, finite sets and relations inside the logic. The present work strengthens this result to a dual equivalence of categories. Other algebraic models of Separation Logic, like those based on Boolean quantales [31] or formal power series [39], can be seen as particular instantiations of BBI hyperdoctrines.

To specify an interpretation  $\llbracket - \rrbracket$ of FO(B)BI in a (B)BI hyperdoctrine $\algfont{P}$
we assign each type $X$ an object
$\llbracket X \rrbracket$ of $\catfont{C}$, and for each context of variables $\Gamma = \{ v_1: X_1, \ldots, v_n: X_n \}$
we have
$\llbracket \Gamma \rrbracket = \llbracket X_1 \rrbracket \times \cdots \times \llbracket X_n \rrbracket$. Each function
symbol $f: X_1 \times \cdots X_n \rightarrow X$ is assigned a morphism
$\llbracket f \rrbracket: \llbracket X_1 \rrbracket \times \cdots \llbracket X_n \rrbracket \rightarrow \llbracket X \rrbracket$.
This allows us to inductively assign to every term of type $X$ in context $\Gamma$ a morphism
$\llbracket t \rrbracket : \llbracket \Gamma \rrbracket \rightarrow \llbracket X \rrbracket$ in the standard way (see [69]).
We additionally assign, for each $m$-ary predicate symbol $P$ of type $X_1, \ldots, X_m$,
$\llbracket P \rrbracket \in \algfont{P}(\llbracket X_1 \rrbracket \times \cdots \times \llbracket X_m \rrbracket)$.
Then the structure of the hyperdoctrine allows us to extend $\llbracket - \rrbracket$ to FO(B)BI formulae $\varphi$ in context $\Gamma$ as follows:

\[
\arraycolsep=0.5pt
\def\arraystretch{1.2}
\begin{array}{llllrlll}
\Interp{Pt_1\ldots t_m} &= \mathbb{P}(\langle \llbracket t_1 \rrbracket, \ldots, \llbracket t_m \rrbracket \rangle)(\llbracket P \rrbracket) & \llbracket \varphi \land \psi \rrbracket &= \llbracket \varphi \rrbracket \land_{\algfont{P}(\llbracket \Gamma \rrbracket)} \llbracket \psi \rrbracket   &  \Interp{\top} &= \top_{\algfont{P}(\Interp{\Gamma})}  \\
\Interp{t=_X t'} &= \algfont{P}(\langle \llbracket t \rrbracket, \llbracket t' \rrbracket \rangle)(=_{\llbracket X \rrbracket}) &\llbracket \varphi \lor \psi \rrbracket &= \llbracket \varphi \rrbracket \lor_{\algfont{P}(\llbracket \Gamma \rrbracket)} \llbracket \psi \rrbracket & \Interp{\bot} &= \bot_{\algfont{P}(\Interp{\Gamma})} \\
\llbracket \varphi \rightarrow \psi \rrbracket & = \llbracket \varphi \rrbracket \rightarrow_{\algfont{P}(\llbracket \Gamma \rrbracket)} \llbracket \psi \rrbracket & \Interp{\varphi * \psi} & = \Interp{\varphi} *_{\algfont{P}(\llbracket \Gamma \rrbracket)} \Interp{\psi} & \Interp{\mtop} &= \mtop_{\algfont{P}(\Interp{\Gamma})} \\
\Interp{\varphi \wand \psi} & = \Interp{\varphi} \wand_{\algfont{P}(\llbracket \Gamma \rrbracket)} \Interp{\psi}
& \Interp{\exists v:X. \varphi} &= \exists \Interp{X}_{\Interp{\Gamma}} (\Interp{\varphi}) & \Interp{\forall v:X. \varphi} &= \forall \Interp{X}_{\Interp{\Gamma}} (\Interp{\varphi}).
\end{array}
\]

Substitution of terms is given by $\llbracket \varphi(t/x) \rrbracket = \mathbb{P}(\llbracket t \rrbracket)(\llbracket \varphi \rrbracket)$. $\varphi$ is satisfied by an interpretation $\llbracket - \rrbracket$ if $\llbracket \varphi \rrbracket = \top_{\mathbb{P}(\Interp{\Gamma})}$. $\varphi$ is valid if it is satisfied by all interpretations.
A standard Lindenbaum-Tarski style construction is sufficient to prove soundness and completeness in both cases.

For all FO(B)BI formulas $\varphi$, $\psi$ in context $\Gamma$, $\varphi \vdash^{\Gamma} \psi$ is provable in $\mathrm{FO(B)BI}_{\mathrm{H}}$  iff, for all (B)BI hyperdoctrines $\mathbb{P}$ and all interpretations $\Interp{-}$, $\Interp{\varphi} \leq_{\mathbb{P}(\Interp{\Gamma})} \Interp{\psi}$.

It is also worth stating a simple lemma that can be obtained as an immediate consequence of the adjointness properties of $\exists X_{\Gamma}$ and $\forall X_{\Gamma}$ as it will be invoked frequently in proofs.

Given a (B)BI hyperdoctrine $\mathbb{P}: \mathrm{C}^{op} \rightarrow \mathrm{Poset}$, for all $a, b \in \mathbb{P}(\Gamma)$ the following hold:

* $a \leq \mathbb{P}(\pi_{\Gamma, X})(\exists X_{\Gamma}(a))$ and $\exists X_{\Gamma}(\mathbb{P}(\pi_{\Gamma, X})(b)) \leq b$;

* $b \leq \forall X_{\Gamma}(\mathbb{P}(\pi_{\Gamma, X})(b))$ and $\mathbb{P}(\pi_{\Gamma, X})(\forall X_{\Gamma}(a)) \leq a$;

* $\exists X_{\Gamma}(\bot) = \bot$ and $\forall X_{\Gamma}(\top) = \top$.

On the `relational' side we introduce new structures: indexed (B)BI frames. This definition is adapted from the notion of indexed Stone space presented by Coumans [25] as a topological dual for Boolean hyperdoctrines. In contrast to the duality presented there, we prove the duality for the more general intuitionistic case and additionally consider (typed) equality and universal quantification. They also appear to have some relation to a more general formulation of Shirasu's metaframes [73], another type of indexed frame introduced to interpret predicate superintuitionistic and modal logics, but we defer an investigation of this connection to another occasion.

An indexed (B)BI frame is a functor
$\functorfont{R}: \catfont{C} \rightarrow \catfont{BIFr}$ such that

* $\catfont{C}$ is a category with finite products;

* For all objects $\Gamma, \Gamma'$ and $X$ in $\catfont{C}$, all morphisms
$s: \Gamma \rightarrow \Gamma'$ and all product projections
$\pi_{\Gamma, X}$,
for the following commutative square

\[
\begin{tikzcd}
\functorfont{R}(\Gamma \times X) \arrow{r}{\functorfont{R}(\pi_{\Gamma, X})} \arrow{d}{\functorfont{R}(s \times id_X)} & \functorfont{R}(\Gamma) \arrow{d}[swap]{\functorfont{R}(s)} \\
\functorfont{R}(\Gamma' \times X) \arrow{r}[swap]{\functorfont{R}(\pi_{\Gamma', X})} & \functorfont{R}(\Gamma')
\end{tikzcd} \]

(a) (for indexed BI frames) the (Pseudo Epi) property holds: $\mathcal{R}(\pi_{\Gamma', X})(y) \preccurlyeq \mathcal{R}(s)(x)$ implies there exists $z$ such that:
$\mathcal{R}(\pi_{\Gamma, X})(z) \preccurlyeq x$ and
$y \preccurlyeq \mathcal{R}(s \times id_X)(z)$;

(b) (for indexed BBI frames) the quasi-pullback property holds: the induced map

\[
\functorfont{R}(\Gamma \times X) \rightarrow \functorfont{R}(\Gamma) \times_{\functorfont{R}(\Gamma')} \functorfont{R}(\Gamma' \times X)
\]

is an epimorphism.

Given an arbitrary indexed BI frame $\functorfont{R}: \catfont{C} \rightarrow \catfont{(B)BIFr}$
and an object $X$ we denote the BI frame at $X$ by $\functorfont{R}(X) = (\functorfont{R}(X),  \preccurlyeq_{\functorfont{R}(X)}, \circ_{\functorfont{R}(X)}, E_{\functorfont{R}(X)})$. Analogously, we denote the BBI frame at $X$ by $\functorfont{R}(X) = (\functorfont{R}(X), \circ_{\functorfont{R}(X)}, E_{\functorfont{R}(X)})$ in the case of an indexed BBI frame.

Although it may not look like it yet, condition (2) ensures that an interpretation of quantifiers based on the projections coheres correctly with the appropriate changes in context. The relation between the definition for indexed BI and BBI frames may not seem entirely clear at first, but unpacking what it means for the square to be a quasi-pullback should clarify: if $\mathcal{R}(\pi_{\Gamma', X})(y) = \mathcal{R}(s)(x)$ then there exists $z$ such that:
$\mathcal{R}(\pi_{\Gamma, X})(z) = x$ and
$y = \mathcal{R}(s \times id_X)(z)$.

A Kripke-style semantics can be given for FO(B)BI on indexed (B)BI frames. For FOBI, an interpretation $\Interp{-}$ is given in precisely the same way as for BI hyperdoctrines, except for the key-difference that each $m$-ary predicate symbol $P$ of type $X_1, \ldots, X_m$ is assigned to an upwards closed subset $\Interp{P} \in \mathcal{P}_{\preccurlyeq}(\mathcal{R}(\llbracket X_1 \rrbracket \times \cdots \times \llbracket X_m \rrbracket))$. Similarly,  an interpretation $\Interp{-}$ for $\logicfont{FOBBI}$ is given in the same way as it is for BBI hyperdoctrines, except that, for every $m$-ary predicate symbol $P$ of type $X_1, \ldots, X_m$, $P$ is assigned to a subset $\Interp{P} \in \mathcal{P}(\mathcal{R}(\llbracket X_1 \rrbracket \times \cdots \times \llbracket X_m \rrbracket))$.  Then for formulas $\varphi$ of FO(B)BI in context $\Gamma$ with $x \in \functorfont{R}(\Interp{\Gamma})$ the satisfaction relation $\vDash^{\Gamma}$ is inductively defined in Fig. <ref>. There, $Ran(\mathcal{R}(\Delta_{\llbracket X \rrbracket})) =  \{ y \mid \exists z(\mathcal{R}(\Delta_{\llbracket X \rrbracket})(z) = y) \}$. We note that bound variables are renamed to be fresh throughout, in an order determined by quantifier depth.

The familiar persistence property of propositional intuitionistic logics also holds for satisfaction on indexed BI frames. For atomic predicate formulas this is by design, with the assignment of predicate symbols to upwards closed subsets akin to a persistent valuation. For formulas of the form $t =_X t'$ this follows from the fact that $\mathcal{R}(\Delta_X)$ is a BI morphism and hence order preserving. The rest of the clauses follow by an inductive argument, the most involved of which is for formulas of the form $\exists v_{n+1}:X\varphi$. Suppose $x, \Interp{-} \vDash^{\Gamma} \exists v_{n+1}:X \varphi$ and $y \succcurlyeq_{\mathcal{R}(\Interp{\Gamma})} x$. Then by definition there exists $x'$ such that $\mathcal{R}(\pi_{\llbracket \Gamma \rrbracket, \llbracket X \rrbracket})(x') = x \preccurlyeq_{\mathcal{R}(\Interp{\Gamma})} y$ and $x', \llbracket - \rrbracket  \vDash^{\Gamma \cup \{ v_{n+1}\!:\!X \}} \varphi$. Since $\mathcal{R}(\pi_{\llbracket \Gamma \rrbracket, \llbracket X \rrbracket})$ is a BI morphism, there exists $y'$ such that $y' \succcurlyeq_{\mathcal{R}(\Interp{\Gamma} \times \Interp{X})} x'$ and $\mathcal{R}(\pi_{\llbracket \Gamma \rrbracket, \llbracket X \rrbracket})(y') = y$. By the inductive hypothesis, $y', \llbracket - \rrbracket  \vDash^{\Gamma \cup \{ v_{n+1}\!:\!X \}} \varphi$ and so $y, \llbracket - \rrbracket  \vDash^{\Gamma} \exists v_{n+1}:X\varphi$.

$x, \Interp{-}$     $\vDash^{\Gamma}$     $Pt_1\ldots t_m$     iff     l$\functorfont{R}(\langle \llbracket t_1 \rrbracket, \ldots, \llbracket t_m \rrbracket \rangle)(x)
\in \llbracket P \rrbracket$
$x, \Interp{-}$     $\vDash^{\Gamma}$     $\top$

$x, \Interp{-}$     $\vDash^{\Gamma}$     $t=_X t'$     iff     l$\functorfont{R}(\langle \llbracket t \rrbracket, \llbracket t' \rrbracket \rangle)(x) \in
Ran(\functorfont{R}(\Delta_{\llbracket X \rrbracket}))$
$x, \Interp{-}$     $\not\vDash^{\Gamma}$     $\bot$

$x, \Interp{-}$     $\vDash^{\Gamma}$     $\varphi \land \psi$     iff     l$x, \Interp{-} \vDash^{\Gamma} \varphi$ and $x, \Interp{-} \vDash^{\Gamma} \psi$

$x, \Interp{-}$     $\vDash^{\Gamma}$     $\varphi \lor \psi$     iff     l$x, \Interp{-} \vDash^{\Gamma} \varphi$ or $x, \Interp{-} \vDash^{\Gamma} \psi$

$x, \Interp{-}$     $\vDash^{\Gamma}$     $\varphi \rightarrow \psi$     iff     8lfor all $x' \succcurlyeq_{\mathcal{R}(\Interp{\Gamma})} x$, $x', \Interp{-}$ $\vDash^{\Gamma}$ $\varphi$ implies $x', \Interp{-} \vDash^{\Gamma} \psi$

$x, \Interp{-}$     $\vDash^{\Gamma}$     $\mtop$     iff     l$x \in E_{\mathcal{R}(\Interp{\Gamma})}$

$x, \Interp{-}$     $\vDash^{\Gamma}$     $\varphi * \psi$     iff     8lthere exists $x' \preccurlyeq x$ s.t. $x' \in y \circ_{\mathcal{R}(\Interp{\Gamma})} z$, $y, \Interp{-} \vDash^{\Gamma} \varphi$ and  $z, \Interp{-} \vDash^{\Gamma} \psi$

$x, \Interp{-}$     $\vDash^{\Gamma}$     $\varphi \wand\psi$     iff     8lfor all $x' \succcurlyeq x$ s.t. $z \in x' \circ_{\mathcal{R}(\Interp{\Gamma})} y$,  $y, \Interp{-} \vDash^{\Gamma} \varphi$ implies $z, \Interp{-} \vDash^{\Gamma} \psi$

$x, \Interp{-}$     $\vDash^{\Gamma}$     $\exists v_{n+1}:X \varphi$     iff     8lthere exists $x' \in \functorfont{R}(\llbracket \Gamma \rrbracket \times \llbracket X \rrbracket)$
s.t. $\functorfont{R}(\pi_{\llbracket \Gamma \rrbracket, \llbracket X \rrbracket})(x') = x$

$x', \llbracket - \rrbracket  \vDash^{\Gamma \cup \{ v_{n+1}\!:\!X \}} \varphi$

$x, \Interp{-}$     $\vDash^{\Gamma}$     $\forall v_{n+1}:X \varphi$     iff     8lfor all $x' \in \functorfont{R}(\llbracket \Gamma \rrbracket \times \llbracket X \rrbracket)$,
$\functorfont{R}(\pi_{\llbracket \Gamma \rrbracket, \llbracket X \rrbracket})(x') \succcurlyeq_{\mathcal{R}(\Interp{\Gamma})} x$,

$x', \llbracket - \rrbracket  \vDash^{\Gamma \cup \{ v_{n+1}:X\}} \varphi$

Satisfaction on indexed (B)BI frames for FO(B)BI. FOBBI replaces $\preccurlyeq$ with $=$.

§.§ Pointer Logic as an Indexed Frame

Although at first sight it may not seem so, indexed frames and the semantics based
upon them are a generalization of the standard store–heap semantics of Separation Logic.

Consider the BI frame $\mathrm{Heap}^\vtiny{BI} = (H, \uplus, \sqsubseteq, H)$, where
$H$ is the set of heaps, $\sqsubseteq$ is heap extension, and $\uplus$ is defined by $h_2 \in h_0 \uplus h_1$ iff
$h_0\# h_1$ and $h_0 \cdot h_1 = h_2$. This is the BI frame corresponding to the partial monoid of heaps. We define an indexed BI frame $\mathrm{Store}^\vtiny{BI}: \catfont{Set} \rightarrow \catfont{BIFr}$ on objects
by $\mathrm{Store}^\vtiny{BI}(X) = {(X \times H, \uplus_X,\sqsubseteq_X, X \times H )}$, where $(x_2, h_2) \in (x_0, h_0) \uplus_X (x_1, h_1)$ iff $x_0=x_1=x_2$ and $h_2 \in h_0 \uplus h_1$, and $(x_0, h_0) \sqsubseteq_X (x_1, h_1)$ iff $x_0 = x_1$ and $h_0 \sqsubseteq h_1$. On morphisms, set $\mathrm{Store}^\vtiny{BI}(f: X \rightarrow Y)(x, h) = (f(x), h)$.
It is straightforward to see this defines a functor: for arbitrary $X$, $\mathrm{Store}(X)$
inherits the BI frame properties from $\mathrm{Heap}^\vtiny{BI}$ and for arbitrary $f: X \rightarrow Y$, $\mathrm{Store}(f)$
is trivially a BI morphism as it is identity on the structure that determines the back and forth conditions.
The property (Pseudo Epi) is also trivially satisfied so this defines an indexed BI frame.

For BBI pointer logic, we instead start with the BBI frame $\mathrm{Heap}^\vtiny{BBI} = (H, \uplus, \{ [] \})$ where $[]$ is the empty heap. Then $\mathrm{Store}^\vtiny{BBI}$ is defined in essentially the same way, with $\mathrm{Store}^\vtiny{BBI}(X) = (X \times H, \uplus_X, X \times \{ [] \} )$ and $\mathrm{Store}^\vtiny{BBI}(f)(x, h) = (f(x), h)$. This defines an indexed BBI frame.

We now describe the interpretations $\llbracket - \rrbracket$ on $\mathrm{Store}^\vtiny{(B)BI}$ that yield the standard models of Separation Logic.
We have one type $\mathrm{Val}$ and we set $\llbracket \mathrm{Val} \rrbracket = \mathbb{Z}$, with the arithmetic operations
$\llbracket + \rrbracket, \llbracket - \rrbracket: \llbracket \mathrm{Val} \rrbracket^2 \rightarrow \llbracket \mathrm{Val} \rrbracket$
defined as one would expect. Term morphisms $\llbracket t \rrbracket: \llbracket \mathrm{Val} \rrbracket^n \rightarrow \llbracket \mathrm{Val} \rrbracket$
in context $\Gamma = \{v_1, \ldots v_n \}$ are then defined as usual,
with each constant $n$ assigned the morphism

n : Γr     { * } rn     Val .
As one would expect, the key difference between the two interpretations is in the interpretation of the points-to predicate. For Intuitionistic Separation Logic, the points-to predicate $\mapsto$ is assigned

\[ \llbracket \mapsto \rrbracket = \{ ((a, a'), h) \mid a \in dom(h) \text{ and } h(a) = a' \}
\in \mathcal{P}_{\sqsubseteq_{\Interp{\mathrm{Val}}^2}} (\mathrm{Store}^\vtiny{BI}(\llbracket \mathrm{Val} \rrbracket^2)).\]

This set is clearly upwards closed with respect to the order $\sqsubseteq_{\Interp{\mathrm{Val}}^2}$ so this is a well-defined interpretation. For Classical Separation Logic, $\mapsto$ is instead assigned

\[ \Interp{\mapsto} = \{ ((a, a'), h) \mid \{ a \} = dom(h) \text{ and } h(a) = a' \} \in \mathcal{P}(\mathrm{Store}^\vtiny{BBI}(\Interp{\mathrm{Val}}^2)). \]

In the indexed (B)BI frame $\mathrm{Store}^\vtiny{(B)BI}: \catfont{Set} \rightarrow \catfont{(B)BIFr}$ with the interpretations just defined, a store is represented as an $n$-place vector of values over $\llbracket \mathrm{Val} \rrbracket$.
That is, the store $s = \{(v_1, a_1), \ldots, (v_n, a_n) \}$ is given by the element
$(a_1, \ldots, a_n) \in \llbracket \mathrm{Val} \rrbracket^n$. By a simple inductive argument we have the following result:

For all formulas $\varphi$ of (B)BI pointer logic, all stores $s = \{ (v_1, a_1), \dots, \!(v_n, a_n) \}$ and all
heaps $h$, $s, h \vDash \varphi \text{ iff } ((a_1, \ldots, a_n), h), \llbracket - \rrbracket \vDash^{\Gamma} \varphi$.

After verifying that terms are evaluated to the same elements as the standard model in both representations, the equivalence of the clauses for atomic formulas can be computed directly. That the clauses for the multiplicatives $*$ and $\wand$ are equivalent is a consequence of the upwards and downwards closure of heap composition with respect to heap extension, as discussed in Section <ref>. Finally, the equivalence of the quantifier clauses is down to the representation of stores as vectors and the action of the product projections under the functor $\mathrm{Store}$. The notions of indexed (B)BI frame and its associated semantics are therefore a natural generalization of the standard Separation Logic model.

§.§ Duality for (B)BI Hyperdoctrines

We now extend the results given for (B)BI algebras to (B)BI hyperdoctrines. For such results to make sense, both (B)BI hyperdoctrines and indexed (B)BI frames need to be equipped with a notion of morphism to form categories. Our definition of hyperdoctrine morphism adapts that for coherent hyperdoctrines [26].

[(B)BI Hyperdoctrine Morphism]
Given a pair of (B)BI hyperdoctrines $\mathbb{P}: \mathrm{C}^{op} \rightarrow \mathrm{Poset}$ and
$\mathbb{P}': \mathrm{D}^{op} \rightarrow \mathrm{Poset}$, a (B)BI hyperdoctrine morphism
$(\mathrm{K}, \tau): \mathbb{P} \rightarrow \mathbb{P}'$ is a pair $(\mathrm{K}, \tau)$ satisfying the following properties:

* $\mathrm{K}: \mathrm{C} \rightarrow \mathrm{D}$ is a finite product preserving functor;

* $\tau: \mathbb{P} \rightarrow \mathbb{P}' \circ K$ is a natural transformation;

* For all objects $X$ in $\mathrm{C}$: $\tau_{X \times X}(=_X) ={\ } ='_{K(X)}$;

* For all objects $\Gamma$ and $X$ in $\mathrm{C}$, the following squares commute:

\[ \begin{array}{ll}
\begin{tikzcd}
\mathbb{P}(\Gamma \times X) \arrow{r}{\tau_{\Gamma \times X}}
\arrow{d}[swap]{\exists X_{\Gamma}} & \mathbb{P'}(K(\Gamma) \times K(X))
\arrow{d}{\exists' {K(X)}_{K(\Gamma)}} \\
\mathbb{P}(\Gamma) \arrow{r}{\tau_{\Gamma}} & \mathbb{P'}(K(\Gamma))
\end{tikzcd} &
\begin{tikzcd}
\mathbb{P}(\Gamma \times X) \arrow{r}{\tau_{\Gamma \times X}}
\arrow{d}[swap]{\forall X_{\Gamma}} & \mathbb{P'}(K(\Gamma) \times K(X))
\arrow{d}{\forall' {K(X)}_{K(\Gamma)}} \\
\mathbb{P}(\Gamma) \arrow{r}{\tau_{\Gamma}} & \mathbb{P'}(K(\Gamma))
\end{tikzcd}
\end{array} \]

The composition of BI hyperdoctrine morphisms $(K, \tau): \mathbb{P} \rightarrow \mathbb{P}'$ and $(K', \tau'): \mathbb{P}' \rightarrow \mathbb{P}''$ is given by $(K' \circ K, \tau'_{K(-)} \circ \tau)$. This yields a category $\mathrm{BIHyp}$.

For indexed (B)BI frames the definition of morphism splits into two because of the weakening of equality to a preorder on the intuitionistic side. It is straightforward to show that the notion of indexed BI frame morphism collapses to that for indexed BBI frames when the preorders $\preccurlyeq$ are substituted for $=$.

[Indexed BI Frame Morphism]
Given indexed BI frames $\mathcal{R}: \mathrm{C} \rightarrow \mathrm{BIFr}$ and
$\mathcal{R}': \mathrm{D} \rightarrow \mathrm{BIFr}$, an indexed BI frame morphism
$(L, \lambda): \mathcal{R} \rightarrow \mathcal{R}'$ is a pair $(L, \lambda)$ such that:

* $L: D \rightarrow C$ is a finite product preserving functor;

* $\lambda: \mathcal{R} \circ L \rightarrow \mathcal{R}'$ is a natural transformation;

* (Lift Property) If there exists $x$ and $y$
such that $\mathcal{R}'(\Delta_X)(y) \preccurlyeq \lambda_{X \times X}(x)$ then there exists
$y'$ such that $\mathcal{R}(\Delta_{L(X)})(y')
\preccurlyeq x$;

* (Morphism Pseudo Epi)  If there exists $x$ and
$y$ with
$\mathcal{R}'(\pi_{\Gamma, X})(x) \preccurlyeq \lambda_{\Gamma}(y) $ then there exists
$z$ such that
$x \preccurlyeq\lambda_{\Gamma \times X}(z)$ and
$\mathcal{R}(\pi_{L(\Gamma), L(X)})(z) \preccurlyeq y$.

The composition of indexed BI frame morphisms $(L', \lambda'): \mathcal{R}' \rightarrow \mathcal{R}''$ and $(L, \lambda): \mathcal{R} \rightarrow \mathcal{R}'$ is given by $(L \circ L', \lambda' \circ \lambda_{L'(-)})$. This yields a category $\mathrm{IndBIFr}$.

[Indexed BBI Frame Morphism]
For indexed BBI frames $\mathcal{R}: \mathrm{C} \rightarrow \mathrm{BBIFr}$ and
$\mathcal{R}': \mathrm{D} \rightarrow \mathrm{BBIFr}$, an indexed BBI frame morphism $(L, \lambda): \mathcal{R} \rightarrow \mathcal{R}'$ is a pair $(L, \lambda)$ satisfying (1) and (2) of the previous definition as well as

($3'$) (Lift Property$'$) if there exist $x$ and
$y$ such that
$\lambda_{X \times X}(x) =  \functorfont{R'}(\Delta_X)(y)$, then there exists
$y'$ such that $\functorfont{R}((\Delta_{L(X)}))(y') = x$, and

($4'$) (Quasi-Pullback) for all objects $\Gamma$ and $X$ in $\catfont{C}$, the following square
is a quasi-pullback:

\[\begin{tikzcd}
\functorfont{R}(L(\Gamma) \times L(X)) \arrow{r}{\lambda_{\Gamma \times X}}
\arrow{d}{\functorfont{R}(\pi_{L(\Gamma), L(X)})} & \functorfont{R}(\Gamma \times X)
\arrow{d}{\functorfont{R'}(\pi_{\Gamma, X})} \\
\functorfont{R}(L(\Gamma)) \arrow{r}{\lambda_{\Gamma}} & \functorfont{R}(\Gamma)
\end{tikzcd}\]

The composition of indexed BBI frame morphisms $(L', \lambda'): \mathcal{R}' \rightarrow \mathcal{R}''$ and $(L, \lambda): \mathcal{R} \rightarrow \mathcal{R}'$ is given by $(L \circ L', \lambda' \circ \lambda_{L'(-)})$. This yields a category $\mathrm{Ind(B)BIFr}$.

We can now show that the `algebraic' and `relational' semantics of FO(B)BI correspond to each other by defining functorial transformations analogous to the complex algebras and prime filter frames of Section <ref>. We show these are related by a representation theorem which is then extended to a duality via the introduction of topology.

To obtain complex hyperdoctrines, we straightforwardly compose an indexed frame with the appropriate complex algebra functor from (B)BI.

[Complex (B)BI Hyperdoctrine]
Given an indexed BI frame $\mathcal{R}: \mathrm{C} \rightarrow \mathrm{BIFr}$, the complex hyperdoctrine of $\mathcal{R}$, $ComHyp^{\vtiny{BI}}(\mathcal{R})$, is given by
$Com^{\vtiny{BI}}(\mathcal{R}(-)): \mathrm{C}^{op} \rightarrow \mathrm{Poset}$, together with $Ran(\mathcal{R}(\Delta_X))$ as $=_X$, ${\mathcal{R}(\pi_{\Gamma, X})}^{*}$ as $\exists X_{\Gamma}$, and ${\mathcal{R}(\pi_{\Gamma, X})}_{*}$ as $\forall X_{\Gamma}$, where

\[ \begin{array}{ll}
{\mathcal{R}(\pi_{\Gamma, X})}^{*}(A) &= \{ x \mid \text{there exists } y \in A: \mathcal{R}(\pi_{\Gamma, X})(y) \preccurlyeq x \} \text{ and}\\
{\mathcal{R}(\pi_{\Gamma, X})}_{*}(A) &= \{ x \mid \text{for all } y, \text{ if } x \preccurlyeq \mathcal{R}(\pi_{\Gamma, X})(y) \text{ then } y \in A \}.
\end{array} \]

For indexed BBI frames, the definitions of ${\mathcal{R}(\pi_{\Gamma, X})}^{*}$ and ${\mathcal{R}(\pi_{\Gamma, X})}_{*}$ are as above, except with $\preccurlyeq$ replaced with $=$.

Given that the complex algebra operations thus far have matched the corresponding semantic clauses on frames, one might have expected $\exists X_{\Gamma}$ to be given by the direct image $\mathcal{R}(\pi_{\Gamma, X})$. Using the fact that $\mathcal{R}(\pi_{\Gamma, X})$ is a BI morphism it can be shown that ${\mathcal{R}(\pi_{\Gamma, X})}^{*}$ is in fact identical to $\mathcal{R}(\pi_{\Gamma, X})$ so this is indeed the case. We use its presentation as ${\mathcal{R}(\pi_{\Gamma, X})}^{*}$ as it simplifies some proofs that follow.

Given an indexed (B)BI frame $\functorfont{R}: \catfont{C} \rightarrow \catfont{(B)BIFr}$, the
complex hyperdoctrine $ComHyp^{\vtiny{(B)BI}}(\mathcal{R})$ is a (B)BI hyperdoctrine.

We concentrate on the verifications relating to ${\mathcal{R}(\pi_{\Gamma, X})}^{*}$ and ${\mathcal{R}(\pi_{\Gamma, X})}_{*}$ of a BI complex hyperdoctrine. It is straightforward to see these map upwards-closed sets to upwards-closed sets and are monotone with respect to the subset ordering $\subseteq$. The adjointness properties follow from the definitions so it just remains to prove naturality.

We give the case for $\exists X_{\Gamma}$. Given a morphism $s: \Gamma \rightarrow \Gamma'$ in $\mathrm{C}$ and an element $A \in Com^\vtiny{BI}(\mathcal{R}(\Gamma' \times X))$, we must show
${\mathcal{R}(\pi_{\Gamma, X})}^{*}({\mathcal{R}(s \times id_X)}^{-1}(A)) =
{\mathcal{R}(s)}^{-1}({\mathcal{R}(\pi_{\Gamma', X})}^{*}(A))$. Suppose
$x \in \mathcal{R}^{*}(\pi_{\Gamma, X})({\mathcal{R}(s \times id_X)}^{-1}(A))$: then there exists $y$ such that $\mathcal{R}(\pi_{\Gamma, X})(y) \preccurlyeq x$ and $\mathcal{R}(s \times id_X)(y) \in A$. We have $\mathcal{R}(\pi_{\Gamma', X})(\mathcal{R}(s \times id_X)(y)) =
\mathcal{R}(s)(\mathcal{R}(\pi_{\Gamma, X})(y)) \preccurlyeq \mathcal{R}(s)(x)$. Hence
$x \in {\mathcal{R}(s)}^{-1}({\mathcal{R}(\pi_{\Gamma', X})}^{*}(A))$, as required.

Conversely, assume $x \in {\mathcal{R}(s)}^{-1}({\mathcal{R}(\pi_{\Gamma', X})}^{*}(A))$.  Then there exists $y \in A$ such that $\mathcal{R}(\pi_{\Gamma', X})(y) \preccurlyeq \mathcal{R}(s)(x)$. Then by (Psuedo Epi), there exists $z$ such that $\mathcal{R}(\pi_{\Gamma, X})(z) \preccurlyeq x$ and $y \preccurlyeq \mathcal{R}(s \times id_X)(z)$. By upwards-closure of $A$, $\mathcal{R}(s \times id_X)(z) \in A$. Hence we have
$x \in {\mathcal{R}(\pi_{\Gamma, X})}^{*}({\mathcal{R}(s \times id_X)}^{-1}(A))$, as required.

The proof for BBI complex hyperdoctrines follows immediately by substituting every instance of $\preccurlyeq$ with $=$ in the above argument, where the quasi pullback property allows us to assume the existence of $z$ such that $\mathcal{R}(\pi_{\Gamma, X})(z) = x$ and $y = \mathcal{R}(s \times {id}_X)(z)$ from  $\mathcal{R}(\pi_{\Gamma', X})(y) = \mathcal{R}(s)(x)$.

[Indexed Prime Filter (B)BI Frame]
Given a (B)BI hyperdoctrine
the indexed prime filter frame, $IndPr^{\vtiny{(B)BI}}(\mathbb{P})$, is given by $Pr^\vtiny{(B)BI}(\algfont{P}(-))$.

Given a (B)BI hyperdoctrine
$\algfont{P}: \catfont{C}^{op} \rightarrow \catfont{Poset}$,
the indexed prime filter frame $IndPr^{\vtiny{(B)BI}}(\mathbb{P})$ is an indexed (B)BI frame.

We first show the Pseudo Epi property is satisfied in the FOBI case. Assume we have objects $\Gamma, \Gamma'$ and $X$ in $\mathrm{C}$ and a morphism
$s: \Gamma \rightarrow \Gamma'$. Let prime filters $F_x$ and $F_y$ be such that
${\mathbb{P}(\pi_{\Gamma', X})}^{-1}(F_y) \subseteq {\mathbb{P}(s)}^{-1}(F_x)$. It is easy to see that

\[\PrimePredicate{F}{{\mathbb{P}(\pi_{\Gamma, X})}^{-1}(F) \subseteq F_x \text{ and } F_y \subseteq {\mathbb{P}(s \times id_X)}^{-1}(F)}\]

is a prime predicate. The only non-trivial verification is showing $P(F \cap F') = 1$ implies $P(F) =1$ or $P(F') =1$. Suppose $P(F \cap F') =1, P(F) = 0$ and $P(F') =0$. Necessarily there exists $a$ and $b$ such that $\mathbb{P}(\pi_{\Gamma, X})(a) \in F$, $\mathbb{P}(\pi_{\Gamma, X})(b) \in F'$ and $a, b \not\in F_x$. Then $\mathbb{P}(\pi_{\Gamma, X})(a) \lor \mathbb{P}(\pi_{\Gamma, X})(b) = \mathbb{P}(\pi_{\Gamma, X})(a \lor b) \in F \cap F'$ so $a \lor b \in F_x$. However $F_x$ is prime, so $a \in F_x$ or $b \in F_x$, a contradiction.

Consider the filter $F = \filter{\mathbb{P}(s \times id_X)(F_y)}$ and suppose for contradiction it is not proper.
This entails there exists $a \in F_y$ such that $\mathbb{P}(s \times id_X)(a) = \bot$. By adjointness, $\exists X_{\Gamma}(\bot) = \bot$, so
$\mathbb{P}(s)(\exists X_{\Gamma'}(a)) = \exists X_{\Gamma}(\mathbb{P}(s \times id_X)(a)) = \bot$ by naturality.
This entails $\exists X_{\Gamma'}(a) \not\in {\mathbb{P}(s)}^{-1}(F_x)$ so
$\exists X_{\Gamma'}(a) \not\in {\mathbb{P}(\pi_{\Gamma', X})}^{-1}(F_y)$ by assumption. However, by adjointness and filterhood, $\mathbb{P}(\pi_{\Gamma', X})(\exists X_{\Gamma'}(a)) \in F_y$, a contradiction.

Clearly ${\mathbb{P}(s \times id_X)}^{-1}(F) \supseteq F_y$. To see that the other required inclusion holds, suppose
$a \in {\mathbb{P}(\pi_{\Gamma, X})}^{-1}(F)$. Then there exists $b \in F_y$ such that
$\mathbb{P}(s \times id_X)(b) \leq \mathbb{P}(\pi_{\Gamma, X})(a)$. By adjointness
$\exists X_{\Gamma}(\mathbb{P}(s \times id_X)(b)) \leq a$ and so by naturality
$\mathbb{P}(s)(\exists X_{\Gamma'}(b)) \leq a$. Since $\mathbb{P}(\pi_{\Gamma', X})(\exists X_{\Gamma'}(b)) \in F_y$, we have $\exists X_{\Gamma'}(b) \in {\mathbb{P}(\pi_{\Gamma', X})}^{-1}(F_y) \subseteq {\mathbb{P}(s)}^{-1}(F_x)$. Thus by filterhood, $a \in F_x$. Thus $P(F) =1$ and by the prime extension lemma we have a prime $F$ with $P(F) =1$, as required.

For FOBBI, we instead start with the assumption of prime filters $F_x$ and $F_y$ such that ${\mathbb{P}(\pi_{\Gamma', X})}^{-1}(F_y) = {\mathbb{P}(s)}^{-1}(F_x)$. This is sufficient to once again prove the existence of a prime filter $F$ satisfying ${\mathbb{P}(s \times id_X)}^{-1}(F) \supseteq F_y$ and ${\mathbb{P}(\pi_{\Gamma, X})}^{-1}(F) \subseteq F_x$. However, maximality of prime filters on Boolean algebras collapses the inclusions to equalities — ${\mathbb{P}(s \times id_X)}^{-1}(F) = F_y$ and ${\mathbb{P}(\pi_{\Gamma, X})}^{-1}(F) = F_x$ — so the quasi pullback property holds.

We now lift the representation theorem for (B)BI algebras to (B)BI hyperdoctrines, making essential use of the natural transformation $\theta$ used in the (B)BI duality theorems of the previous section.

Every (B)BI hyperdoctrine $\mathbb{P}: \mathrm{C}^{op} \rightarrow \mathrm{Poset}$ can be embedded in a complex (B)BI hyperdoctrine. That is, $\Theta_{\mathbb{P}}: \mathbb{P} \rightarrow Com^{\vtiny{(B)BI}}Pr^{\vtiny{(B)BI}}(\mathbb{P}(-))$, defined $(Id_{\mathrm{C}}, \theta_{\mathbb{P}(-)})$, is a monomorphism.

Clearly, by the representation theorem for (B)BI algebras, each component of $\Theta_{\mathbb{P}}$ is mono, and hence $\Theta_{\mathbb{P}}$ is mono. It remains to show that $\Theta_{\mathbb{P}}$ is a (B)BI hyperdoctrine morphism. That ${Id}_{\mathrm{C}}$ preserves finite products is immediate and that $\theta_{\mathbb{P}(-)}: \mathbb{P} \rightarrow Com^{\vtiny{(B)BI}}Pr^{\vtiny{(B)BI}}(\mathbb{P}(-))$ is a natural transformation is given by (B)BI duality.

First we show that property (3) of (B)BI hyperdoctrine morphisms holds. We must verify that $\theta_{\mathbb{P}(X \times X)}(=_{X}) = Ran({\mathbb{P}(\Delta_X)}^{-1})$ for any object $X$ of $\mathrm{C}$. First suppose $F = {\mathbb{P}(\Delta_X)}^{-1}(G)$ for some prime filter $G$. By adjointness of $=_X$ at $\top$ we have that $\mathbb{P}(\Delta_X)(=_{X}) = \top \in G$. Hence $=_{X} \in F$. Conversely, assume $=_{X} \in F$. Straightforwardly we have that

\[\PrimePredicate{G}{{\mathbb{P}(\Delta_X)}^{-1}(G) \subseteq F}\]

defines a prime predicate. By the adjointness property of $=_{X}$ we have that ${\mathbb{P}(\Delta_X)}^{-1}(\{ \top \}) \subseteq F$. Hence there exists prime $G$ with ${\mathbb{P}(\Delta_X)}^{-1}(G) \subseteq F$ by the prime extension lemma. For the case of FOBI, since ${\mathbb{P}(\Delta_X)}^{-1}$ is a BI morphism there then exists $G' \supseteq G$ with ${\mathbb{P}(\Delta_X)}^{-1}(G') = F$; for the case of FOBBI, maximality of prime filters means ${\mathbb{P}(\Delta_X)}^{-1}(G) = F$. In both cases, $F \in Ran({\mathbb{P}(\Delta_X)}^{-1})$ as required.

For property (4), we verify the naturality diagram for $\exists X_{\Gamma}$: the verification of $\forall X_{\Gamma}$ is similar. The verification reduces to showing that, given a prime filter $F$ of $\mathbb{P}(\Gamma)$ and $a \in \mathbb{P}(\Gamma \times X)$, $\exists X_{\Gamma}(a) \in F$ iff there exists $G$ such that $a \in G$ and ${\mathbb{P}(\pi_{\Gamma, X})}^{-1}(G) \subseteq F$: for $\logicfont{FOBI}$ this corresponds precisely to commutativity of the diagram, and for $\logicfont{FOBBI}$ we can conclude ${\mathbb{P}(\pi_{\Gamma, X})}^{-1}(G) = F$ by maximality of prime filters, yielding commutativity of the appropriate diagram for that case.

First assume $\exists X_{\Gamma}(a) \in F$. It is straightforward to see that

\[ \PrimePredicate{G}{{\mathbb{P}(\pi_{\Gamma, X})}^{-1}(G) \subseteq F}\]
defines a prime predicate. Consider $G = \filter{a}$. This is proper, as otherwise $a = \bot$, which would entail $\exists X_{\Gamma}(a) = \bot \in F$, contradicting that $F$ is a prime (and thus proper) filter. Let $\mathbb{P}(\pi_{\Gamma, X})(b) \geq a$. Then by adjointness, $\exists X_{\Gamma}(a) \leq b \in F$. Hence $P(G) =1$ and so there exists a prime filter $G$ with $P(G) =1$, as required. Now assume $a \in G$ and ${\mathbb{P}(\pi_{\Gamma, X})}^{-1}(G) \subseteq F$. By adjointness $a \leq \mathbb{P}(\pi_{\Gamma, X})(\exists X_{\Gamma}(a)) \in G$, so $\exists X_{\Gamma}(a) \in {\mathbb{P}(\pi_{\Gamma, X})}^{-1}(G) \subseteq F$ as required.

Just as in the propositional case, the representation theorem yields completeness for the indexed frame semantics. Given any interpretation on an indexed (B)BI frame $\Interp{-}$, we automatically have an interpretation for the complex hyperdoctrine as predicate symbols are interpreted as (upwards-closed) subsets; that is, elements of complex algebras of (B)BI frames.  A simple inductive argument shows that satisfaction coincides for these models.

Given an indexed (B)BI frame $\mathcal{R}$ and an interpretation $\Interp{-}$, for all FO(B)BI formulae $\varphi$ in context $\Gamma$ and $x \in \mathcal{R}(\Interp{\Gamma})$, $x, \Interp{-} \vDash^{\Gamma} \varphi$ iff $x \in \Interp{\varphi}$.

Similarly, given an interpretation $\Interp{-}$ on a (B)BI hyperdoctrine, we can define the interpretation $\widetilde{\Interp{-}}$ by setting $\widetilde{\Interp{P}} = \theta_{\mathbb{P}(\Interp{X_1} \times \cdots \times \Interp{X_m})}(\Interp{P})$ for each predicate symbol of type $X_1, \ldots, X_m$. As a corollary of the representation theorem we obtain the following proposition.

Given a (B)BI hyperdoctrine $\mathbb{P}$ and an interpretation $\Interp{-}$, for all FO(B)BI formulae $\varphi$ in context $\Gamma$ and prime filters $F$ of $\mathbb{P}(\Interp{\Gamma})$, $\Interp{\varphi} \in F$ iff $F, \widetilde{\Interp{-}} \vDash^{\Gamma} \varphi$.

For all FO(B)BI formulae $\varphi$ in context $\Gamma$, $\varphi \vdash^{\Gamma} \psi$ is provable iff $\varphi \vDash^{\Gamma} \psi$.

From here it is straightforward to set an assignment of morphisms to make the assignment of complex hyperdoctrines and indexed prime filter frames functorial. Given a (B)BI hyperdoctrine morphism $(K, \tau): \mathbb{P} \rightarrow \mathbb{P}'$, $IndPr^{\vtiny{(B)BI}}(K, \tau) = (K, \tau^{-1})$. Similarly, given an indexed (B)BI frame morphism $(L, \lambda): \mathcal{R} \rightarrow \mathcal{R}'$, $ComHyp^{\vtiny{(B)BI}}(L, \lambda) = (L, \lambda^{-1})$.

The functors $ComHyp^{\vtiny{(B)BI}}$ are well defined.

Let $(L, \lambda)$ be a indexed (B)BI frame morphism. First note that by definition $L$ is a finite product preserving functor. We also have that each component $\lambda_X: \mathcal{R}(LX) \rightarrow \mathcal{R}'(X)$ is a (B)BI morphism. Hence by functorality of $Com^{\vtiny(B)BI}$, each $\lambda^{-1}_X: Com^{\vtiny{(B)BI}}(\mathcal{R}'(X)) \rightarrow Com^{\vtiny{(B)BI}}(\mathcal{R}(LX))$ is a (B)BI algebra homomorphism, and naturality is inherited from $\lambda$.

Next we must verify that $\lambda^{-1}_{X \times X}(Ran(\mathcal{R}'(\Delta_X))) = Ran(\mathcal{R}(\Delta_{LX}))$. The right-to-left inclusion follows immediately from naturality of $\lambda$. For the left-to-right, suppose $\lambda_{X \times X}(x) \in Ran(\mathcal{R}'(\Delta_X))$. Then there exists $y$ such that $\lambda_{X \times X}(x) = \mathcal{R}'(\Delta_X)(y)$. In the case for FOBI, by the lift property, there exists $y'$ such that $\mathcal{R}(\Delta_{LX})(y') \preccurlyeq x$. Since $\mathcal{R}(\Delta_{LX})$ is a BI morphism, there thus exists $x'$ such that $y' \preccurlyeq x'$ and $\mathcal{R}(\Delta_{LX})(x') = x$ as required. For FOBBI we are given such an $x'$ immediately by the respective lift property.

Finally we verify the commutative diagram for $\exists X_{\Gamma}$, leaving the similar verification for $\forall X_{\Gamma}$ to the reader. We must show that ${\mathcal{R}(\pi_{L\Gamma, LX})}^{*}\lambda^{-1}_{\Gamma \times X}(A) = \lambda^{-1}_{\Gamma}{\mathcal{R}'(\pi_{\Gamma, X})}^{*}(A)$ for $A \in Com^{\vtiny{(B)BI}}(\mathcal{R}'(\Gamma \times X))$. First consider the case of FOBI. Suppose $x \in {\mathcal{R}(\pi_{L\Gamma, LX})}^{*}\lambda^{-1}_{\Gamma \times X}(A)$. Then there exists $y$ with $\lambda_{\Gamma \times X}(y) \in A$ and $\mathcal{R}(\pi_{L\Gamma, LX})(y) \preccurlyeq x$. Since $\lambda$ is a natural transformation and its components are order-preserving we have $\mathcal{R}'(\pi_{\Gamma, X})(\lambda_{\Gamma \times X}(y)) = \lambda_{\Gamma}\mathcal{R}(\pi_{L\Gamma, LX})(y) \preccurlyeq \lambda_{\Gamma}(x)$, so $x \in  \lambda^{-1}_{\Gamma}{\mathcal{R}'(\pi_{\Gamma, X})}^{*}(A)$. Now, suppose $x \in \lambda^{-1}_{\Gamma}{\mathcal{R}'(\pi_{\Gamma, X})}^{*}(A)$. Then $\mathcal{R}'(\pi_{\Gamma, X})(y) \preccurlyeq \lambda_{\Gamma}(x)$ for $y \in A$. By the Morphism Pseudo Epi property, there exists $z$ such that $y \preccurlyeq \lambda_{\Gamma \times X}(z)$ and $\mathcal{R}(\pi_{L\Gamma, LX})(z) \preccurlyeq x$. $A$ is an upwards-closed set so $\lambda_{\Gamma \times X}(z) \in A$, hence $x \in  {\mathcal{R}(\pi_{L\Gamma, LX})}^{*}\lambda^{-1}_{\Gamma \times X}(A)$ as required. For the case of FOBBI the same argument applies, where $\preccurlyeq$ is substituted for $=$ and the other Morphism Pseudo Epi property is applied to find a sufficient $z$ in the right-to-left direction.

The functors $IndPr^{\vtiny{(B)BI}}$ are well defined.

Let $(K, \tau)$ be a (B)BI hyperdoctrine morphism. As in the previous lemma, we automatically obtain properties (1) and (2) for $(K, \tau^{-1})$ from the definition and the complex algebra functor $Com^{\vtiny{(B)BI}}$. For properties (3) and (4) we verify the case for FOBI, obtaining the case for FOBBI as a special case.

First we consider the Lift Property. Suppose ${\mathbb{P}(\Delta_X)}^{-1}(G) \subseteq \tau^{-1}_{X \times X}(F)$. It is simple to see that

\[ \PrimePredicate{G'}{{\mathbb{P}'(\Delta_{KX})}^{-1}(G') \subseteq F} \]
is a prime predicate. By Theorem <ref> we have that $=_X \in {\mathbb{P}(\Delta_X)}^{-1}(G) \subseteq \tau^{-1}_{X \times X}(F)$ so $\tau_{X \times X}(=_X) ={\ } ='_{KX} \in F$. By adjointness it then follows that ${\mathbb{P}'(\Delta_{KX})}^{-1}(\{ \top \}) \subseteq F$, as $\mathbb{P}(\Delta_{KX})(a) = \top$ entails $='_{KX} \leq a$. By the prime extension lemma there thus exists prime $G$ with $P(G) =1$, as required.  For the case of FOBBI, maximality entails ${\mathbb{P}'(\Delta_{KX})}^{-1}(G') = F$.

Next, the Morphism Pseudo Epi property. Suppose ${\mathbb{P}(\pi_{\Gamma, X})}^{-1}(F) \subseteq \tau^{-1}_{\Gamma}(G)$. We can once again define a prime predicate

\[ \PrimePredicate{G'}{F \subseteq \tau^{-1}_{\Gamma \times X}(G') \text{ and } {\mathbb{P}'(\pi_{K\Gamma, KX})}^{-1}(G') \subseteq G} \]
that we can use to prove the existence of the appropriate prime filter. Consider the filter $G' = \filter{\tau_{\Gamma \times X}(F)}$. This is proper, otherwise there exists $a\in F$ such that $\tau_{\Gamma \times X}(a) = \bot$. By property (4) of BI hyperdoctrine morphism, this would entail $\tau_{\Gamma}(\exists X_{\Gamma}(a)) = \exists' KX_{K\Gamma}\tau_{\Gamma \times X}(a) = \exists' KX_{K\Gamma}(\bot) = \bot$. Since $a \in F$, by adjointness $\mathbb{P}(\pi_{\Gamma, X})(\exists X_{\Gamma}(a)) \in F$. Hence $\tau_{\Gamma}(\exists X_{\Gamma}(a)) = \bot \in G$ by assumption, contradicting that $G$ is a prime filter.

Clearly $F \subseteq \tau^{-1}_{\Gamma \times X}(G')$. Further, let $b \in {\mathbb{P}'(\pi_{K\Gamma, KX})}^{-1}(G')$. Then there exists $a \in F$ such that $\mathbb{P}'(\pi_{K\Gamma, KX})(b) \geq \tau_{\Gamma \times X}(a)$. By adjointness it follows that $\exists KX_{K\Gamma}( \tau_{\Gamma \times X}(a)) \leq b$, and by property (4) of BI hyperdoctrine morphisms we have $\tau_{\Gamma} (\exists X_{\Gamma}(a)) \leq b$. Since $a \in F$ we have that $\mathbb{P}(\pi_{\Gamma, X})(\exists X_{\Gamma}(a)) \in F$ by adjointness and upwards closure, hence $\exists X_{\Gamma}(a) \in {\mathbb{P}(\pi_{\Gamma, X})}^{-1}(F) \subseteq \tau^{-1}_{\Gamma}(G)$. It follows that $\tau_{\Gamma}(\exists X_{\Gamma}(a)) \in G$, and so $b \in G$. Thus $P(G) =1$ and so there exists a prime filter $G$ with $P(G) = 1$ by the prime extension lemma. In the case for FOBBI, by maximality of prime filters these inclusions become equalities, and this yields a witness for the Quasi-Pullback property.

At this stage topology must be introduced to yield a dual equivalence.

[Indexed (B)BI Space]
An indexed  (B)BI space is a functor $\mathcal{R}: \mathrm{C} \rightarrow \mathrm{(B)BISp}$ such that

* $U \circ \mathcal{R}: \mathrm{C} \rightarrow \mathrm{(B)BIFr}$ is an indexed (B)BI frame, where $U: \mathrm{(B)BISp} \rightarrow \mathrm{(B)BIFr}$ is the functor that forgets topological structure.

* For each object $X$ in $\mathrm{C}$, $Ran(\mathcal{R}(\Delta_X))$ is clopen;

* For each pair of objects $\Gamma$ and $X$ in $\mathrm{C}$,
${\mathcal{R}(\pi_{\Gamma, X})}^{*}$ and
${\mathcal{R}(\pi_{\Gamma, X})}_{*}$ map (upwards-closed) clopen sets to (upwards-closed) clopen sets.

In the case for FOBBI it is possible to weaken condition (3) to ${\mathcal{R}(\pi_{\Gamma, X})}^{*}$ being an open map and ${\mathcal{R}(\pi_{\Gamma, X})}_{*}$ a closed map. This is because $\mathcal{R}(\pi_{\Gamma, X})$ is a continuous map between a compact and a Hausdorff space, and so the direct image $\mathcal{R}(\pi_{\Gamma, X}) = {\mathcal{R}(\pi_{\Gamma, X})}^{*}$ is a closed map automatically. We also have that ${\mathcal{R}(\pi_{\Gamma, X})}_{*}$ is an open map by definition. In the intuitionistic case the same reasoning applies for ${\mathcal{R}(\pi_{\Gamma, X})}^{*}$ (using its equivalence with the direct image) but it is not clear how to make the analogous case for ${\mathcal{R}(\pi_{\Gamma, X})}_{*}$. Nonetheless, this definition of indexed (B)BI space gives us what we need.

Given a (B)BI hyperdoctrine $\mathbb{P}$, the indexed prime filter space $IndPr^{\vtiny{(B)BI}}(\mathbb{P})$ is an indexed (B)BI space.

Given Lemma <ref> the only verifications left are of properties (2) and (3). We immediately obtain (2) by noting once again that $Ran({\mathbb{P}(\Delta_X)}^{-1}) = \theta_{\mathbb{P}(X \times X)}(=_X)$, a clopen set by (B)BI duality. Utilising (B)BI duality once more, we have that every (upwards-closed) clopen set of $Pr^{\vtiny{(B)BI}}(\mathbb{P}(Y))$ is of the form $\theta_{\mathbb{P}(Y)}(a)$ for some $a \in \mathbb{P}(Y)$. We thus demonstrate that ${({\mathbb{P}(\pi_{\Gamma, X})}^{-1})}^{*}(\theta_{\mathbb{P}(\Gamma \times X)}(a)) = \theta_{\mathbb{P}(\Gamma)}(\exists X_{\Gamma}(a))$ and ${({\mathbb{P}(\pi_{\Gamma, X})}^{-1})}_{*}(\theta_{\mathbb{P}(\Gamma \times X)}(a)) = \theta_{\mathbb{P}(\Gamma)}(\forall X_{\Gamma}(a))$.

First assume $F \in {({\mathbb{P}(\pi_{\Gamma, X})}^{-1})}^{*}(\theta_{\mathbb{P}(\Gamma \times X)}(a))$. Then there exists $F'$ such that $a \in F'$ and ${\mathbb{P}(\pi_{\Gamma, X})}^{-1}(F') \subseteq F$. By adjointness $a \leq \mathbb{P}(\pi_{\Gamma, X})(\exists X_{\Gamma}(a))$ so $\exists X_{\Gamma}(a) \in