1–LABEL:LastPageFeb. 28, 2017Oct. 30, 2018

# Intuitionistic Layered Graph Logic:
Semantics and Proof Theory

Simon Docherty  University College London, UK<EMAIL_ADDRESS>and
David Pym<EMAIL_ADDRESS>
###### Abstract.

Models of complex systems are widely used in the physical and social sciences,
and the concept of layering, typically building upon graph-theoretic
structure, is a common feature. We describe an intuitionistic substructural
logic called ILGL that gives an account of layering. The logic is a bunched
system, combining the usual intuitionistic connectives, together with a non-
commutative, non-associative conjunction (used to capture layering) and its
associated implications. We give soundness and completeness theorems for a
labelled tableaux system with respect to a Kripke semantics on graphs. We then
give an equivalent relational semantics, itself proven equivalent to an
algebraic semantics via a representation theorem. We utilise this result in
two ways. First, we prove decidability of the logic by showing the finite
embeddability property holds for the algebraic semantics. Second, we prove a
Stone-type duality theorem for the logic. By introducing the notions of ILGL
hyperdoctrine and indexed layered frame we are able to extend this result to a
predicate version of the logic and prove soundness and completeness theorems
for an extension of the layered graph semantics . We indicate the utility of
predicate ILGL with a resource-labelled bigraph model.

###### Key words and phrases:

Complex systems, modelling, graphs, layered graphs, substructural logic,
bunched logic, layered graph logic, predicate logic, tableaux, Kripke
semantics, algebraic semantics, decidability, finite model property, Stone-
type duality, soundness and completeness, bigraphs, pointer logic,
hyperdoctrine

##  1\. Introduction

Complex systems can be defined as the field of science that studies, on the
one hand, how it is that the behaviour of a system, be it natural or
synthetic, derives from the behaviours of its constituent parts and, on the
other, how the system interacts with its environment. A commonly employed and
highly effective concept that helps to manage the difficulty in
conceptualizing and reasoning about complex systems is that of _layering_ :
the system is considered to consist of a collection of interconnected layers
each of which has a distinct, identifiable role in the system’s operations.
Layers can be informational or physical and both kinds may be present in a
specific system.

Graphs provide a suitably abstract setting for a wide variety of modelling
purposes, and layered graphs already form a component of many existing systems
modelling approaches. For example, both social networks [5] and transportation
systems [34], have been modelled by a form of layered graph in which multiple
layers are given by relations over a single set of nodes. A key feature of the
TCP/IP conceptual model of communications on the Internet [8] is its
separation into layers. This form of layering is not immediately represented
in terms of graphs. However, the form of its information flows may be captured
quite naturally using layered graphs [9]. Elsewhere layered graph models have
been deployed to solve problems related to telecommunications networks [24]
and to aid the design of P2P systems for businesses [44]. A bigraph [39] is a
form of layered graph that superimposes a spatial _place graph_ of locations
and a _link graph_ designating communication structure on a single set of
nodes. Such graphs provide models of distributed systems and have been used to
generalize process models like petri nets and the $\pi$-calculus. Similar
ideas have also been used to give layered models of biological systems [38].
More generally, multi-layered networks have become ubiquitous in a range of
complex system modelling approaches (see [32] for a survey).

In this paper, we give a formal definition of layered graph and provide a
bunched logic for reasoning about layering. Bunched logics freely combine
systems of different structural strengths. For example, the logic of bunched
implications (BI) [40, 27, 41, 22] combines intuitionistic propositional logic
with multiplicative intuitionistic linear logic (MILL) [23].

This kind of combination can be most clearly understood proof-theoretically.
Consider the sequent calculus, a proof system that directly represents
consequence. In a sequent $\Gamma\vdash\varphi$ in intuitionistic logic, the
context is simply a finite sequence of formulae connected by an operation
$\,,\,$ which admits the structural properties of Exchange (E), Contraction
(C), and Weakening (W). In the bunched system BI, the context $\Gamma$ in a
sequent $\Gamma\vdash\varphi$ is constructed as a finite tree, using two
operations $\,;\,$ and $\,,\,$ with formulae at the leaves and $\,;\,$ and
$\,,\,$ at the internal vertices. In this set-up, the semi-colon $\,;\,$
admits Exchange, Contraction, and Weakening, but the comma $\,,\,$ admits only
Exchange. Both are associative. As a result, we have in BI the ‘deep’
structural rules for $;\,$

${\small\frac{\Gamma(\phi;\psi)\vdash\chi}{\Gamma(\psi;\phi)\vdash\chi}\quad
E\qquad\frac{\Gamma(\psi;\psi)\vdash\varphi}{\Gamma(\psi)\vdash\varphi}\quad
C\qquad\frac{\Gamma(\psi)\vdash\varphi}{\Gamma(\psi;\chi)\vdash\varphi}\quad
W}$

but do not have the corresponding $C$ and $W$ rules for the comma $\,,\,$.

Corresponding to the two operations are additive and multiplicative
conjunctions, $\wedge$ and $\ast$, each of which is accompanied by a
corresponding implication, $\rightarrow$ and $\mathbin{-\mkern-6.0mu*}$,
respectively. So we have rules such as

${\small\frac{\Gamma(\psi_{1},\psi_{2})\vdash\varphi}{\Gamma(\psi_{1}\ast\psi_{2})\vdash\varphi}\quad\mbox{\rm$\ast$
L}\qquad\frac{\Gamma(\psi_{1};\psi_{2})\vdash\varphi}{\Gamma(\psi_{1}\wedge\psi_{2})\vdash\varphi}\quad\mbox{\rm$\wedge$
L}}$

and

${\small\frac{\Gamma,\psi\vdash\varphi}{\Gamma\vdash\psi\mathbin{-\mkern-6.0mu*}\varphi}\quad\mbox{\rm$\mathbin{-\mkern-6.0mu*}$
R}\qquad\frac{\Gamma;\psi\vdash\varphi}{\Gamma\vdash\psi\rightarrow\varphi}\quad\mbox{\rm$\rightarrow$
R}}$

and their right and left counterparts.

The logic BI has a classical counterpart, called Boolean BI (BBI), in which
the additives are classical, That is, BBI freely combines classical
propositional logic and MILL. In [9, 10], the logic LGL, or ‘layered graph
logic’, was introduced. Like BBI, LGL employs classical additives, but, unlike
BBI, it employs a multiplicative conjunction that is neither commutative —
that is, does not admit Weakening — nor associative.

The key difference with LGL in the present work is that the additive component
of the bunched logic we employ is _intuitionistic_. Our logic is thus related
to BI in precisely the same manner that LGL is related to BBI.

There are a number of reasons to investigate such a logic. Propositional
intuitionistic logic was famously given a truth-functional semantics on
ordered sets of possible worlds by Kripke [33]. Propositions are
intuitionistically true if their classical truth value _persists_ with respect
to the introduction of new facts. This is formally captured by the notion of
_persistent valuation_. A valuation
$\mathcal{V}:\mathrm{Prop}\rightarrow\mathcal{P}(X)$ is persistent iff for all
$x,y\in X$ and all $\mathrm{p}\in\mathrm{Prop}$: $x\in\mathcal{V}(p)$ and
$x\preccurlyeq y$ implies $y\in\mathcal{V}(\mbox{\rm p})$. For persistent
$\mathcal{V}$, this property extends to the satisfaction relation of Kripke’s
semantics. Thus $\varphi$ is true at a world $x$ iff $\varphi$ is true at all
worlds $y$ such that $x\preccurlyeq y$.

Directed graphs carry a natural order: the subgraph relation. An
intuitionistic logic on graphs is therefore suitable for reasoning about
properties that persist with respect to this order. One example relevant to
systems modelling is the existence of a path satisfying desirable properties.
This principle can be generalized to a chosen order on the subgraphs of a
model.

There are also technical motivations that lie behind the introduction of an
intuitionstic variant of the logic, most prominently the question of
completeness. In [9] an algebraic completeness result was given for a class of
structures that included the layered graph models. Some of the methods in this
paper also yield a completeness result for a class of relational structures
that closely resemble the layered graph models. However a completeness result
specifically for the class of layered graph models eludes proof. This is not
unexpected: completeness proofs typically capture a general classes of models,
of which the intended class of models is a subclass. In the case of
_intuitionistic_ LGL, however, we are able to give a labelled tableaux system
that outputs intuitionistic layered graph countermodels to invalid formulae,
yielding completeness for the intended class of models. Moreover, we are able
to combine this result with those for algebraic and relational structures to
prove strong metatheoretic properties like the decidability of validity on
layered graph models.

There are precursors in the literature for such a logic. The first, a spatial
logic for querying graphs [7] also includes multiplicative connectives for
reasoning about the decomposition of graphs into disjoint subgraphs. In this
treatment directionality is not considered, with the consequence that the
spatial decomposition cannot capture a notion of layering. As a result the
multiplicative conjunction that captures decomposition is both commutative and
associative, in contrast to our logic. It also differs in that the additive
component of the logic is classical. A closer relative is the logic BiLog,
designed specifically for reasoning about bigraphs [13]. In BiLog there are
two sets of multiplicatives reflecting the two different ways bigraphs can be
composed: the side-by-side composition of place graphs and the composition of
link graphs at designated interfaces. As both compositions are order-
sensitive, the associated connectives are non-commutative, however both are
associative. Once again the additive connectives are classical. In both cases,
very little metatheoretic work has been done beyond specification of
semantics. In contrast we provide a comprehensive proof theoretic treatment of
intuitionistic LGL and give an affirmative result on decidability. This is
bolstered further by mathematically substantial results on topological duality
for the logic and a sound and complete extension to predicate logic. Although
we defer to another occasion a detailed investigation of the relationship
between bigraphs and our logic, we indicate how bigraph-like structures
provide an instance of our semantics.

The route map for this paper is as follows. In Section 2, we introduce a
formal definition of layered graph. This motivates the introduction of ordered
scaffolds, the central semantic structure for the logic. This is followed by a
specification of the syntax and semantics of Intuitionistic Layered Graph
Logic (ILGL). We give two proof systems for the logic: a simple Hilbert-type
system extending that of propositional intuitionistic logic and a labelled
tableaux system.

In Section 3, we establish the basic metatheory of the logic: namely, the
soundness and completeness of the layered graph semantics with respect to the
labelled tableaux system. This is facilitated by design choices in the
labelling algebra that allow us to extract ordered scaffold countermodels for
formulae lacking a tableaux proof.

In Section 4, we turn towards decidability of the logic. Our proof proceeds in
two stages. First, we define an algebraic semantics based on ILGL’s Hilbert
system and a relational semantics based on ILGL’s layered graph semantics.
Using the labelled tableaux system we are able to show that the relational
semantics and layered graph semantics are equivalent. Further, by a
representation theorem for the algebraic semantics, we are able to show
equivalence with the relational semantics. With this established, we prove the
finite model property holds for the algebraic semantics, and thus decidability
holds for the logic. In Section 5 we extend the representation theorem to a
Stone-type topological duality.

Finally, in Section 6 we define predicate ILGL and prove soundness and
completeness with respect to a Hilbert system for a semantics on indexed
relational structures. As an example of how this might be used, we define an
extension of the layered graph semantics for a specific signature of predicate
ILGL, and show this semantics is an instantiation of the one proven complete.
We finish the section with an extension of the duality theorem of Section 5.
In Section 7 we discuss directions for further work.

This paper is an expanded version of [16] and contains several new results. In
particular the content of Sections 4 \- 6 is new. This includes decidability
of the logic, the representation & duality theorems for ILGL’s algebraic
semantics and the extension to predicate ILGL with its associated soundness,
completeness and duality theorems. We also give full proofs of tableaux
completeness that were previously only sketched.

While layered graphs are a key component of models of complex systems, other
structure is also important. For example, in modelling the structure and
dynamics of distributed systems — in order, for example, to study security
properties — it is necessary to capture the architecture of system locations,
their associated system resources, and the processes that describe how the
system delivers its services. Tools for reasoning about the structure and
behaviour of complex systems therefore must handle location. But they must
also handle resource and process. Thus logics for layered graphs represent
just a first step in establishing a logical account of complex systems
modelling. A second step would be to reformulate the Hennessy-Milner-van
Bentham-style logics of state for location-resource-processes [12, 11, 1] to
incorporate layering.

##  2\. Intuitionistic layered graph logic

###  2.1. The Layered Graph Construction

We begin with a formal, graph-theoretic account of the notion of layering
that, we claim, captures the concept as used in complex systems. In this
definition, 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_ by
$V(\mathcal{G})$. Its edge set is given by a subset $E(\mathcal{G})\subseteq
V(\mathcal{G})\times V(\mathcal{G})$, while its set of subgraphs is denoted
$S\\!g(\mathcal{G})$. Here, H is a subgraph of $\mathcal{G}$ iff
$V(H)\subseteq V(\mathcal{G})$ and $E(H)\subseteq V(\mathcal{G})$. We thus
overload set theoretic inclusion to also refer to the subgraph relation:
$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 subgraphs of $\mathcal{G}$ is defined
$H\leadsto_{\mathcal{E}}K$ iff there exist $u\in V(H)$ and $v\in V(K)$ such
that $(u,v)\in\mathcal{E}$.

This generates a partial composition $@_{\mathcal{E}}$ on subgraphs. Let
$\downarrow$ denote definedness and $\uparrow$ denote undefinedness. For
subgraphs $H$ and $K$, $H\mathop{@_{\mathcal{E}}}\nolimits K\downarrow\text{
iff }V(H)\cap V(K)=\emptyset,H\leadsto_{\mathcal{E}}K\text{ and
}K\not\leadsto_{\mathcal{E}}H$ with output given by the graph union of the two
subgraphs and the $\mathcal{E}$-edges between them. Formally, if
$H\mathop{@_{\mathcal{E}}}\nolimits K\downarrow$, then
$H\mathop{@_{\mathcal{E}}}\nolimits K$ is defined by
$V(H\mathop{@_{\mathcal{E}}}\nolimits K)=V(H)\cup V(K)$ and
$E(H\mathop{@_{\mathcal{E}}}\nolimits K)=E(H)\cup E(K)\cup\\{(u,v)\mid u\in
V(H),v\in V(K)\text{ and }(u,v)\in\mathcal{E}\\}$.

For a graph $H$, we say it is _layered_ (with respect to $\mathcal{E}$) if
there exist $K_{0}$, $K_{1}$ such that $K_{0}\mathop{@_{\mathcal{E}}}\nolimits
K_{1}\downarrow$ and $H=K_{0}\mathop{@_{\mathcal{E}}}\nolimits K_{1}$ (see
Figure 2). Layering is evidently neither commutative nor (because of
definedness) associative: for a full exposition of these properties see [9].

Figure 1. The graph composition $H\mathop{@_{\mathcal{E}}}\nolimits K$

Figure 2. An ordered scaffold

Within a given graph, $\mathcal{G}$, we can identify a specific form of
layered structure, called an _ordered scaffold_ , on which we interpret
intuitionistic layered graph logic. To set this up, we begin with the
definition of _admissible subgraph set_ , a subset $X\subseteq
S\\!g(\mathcal{G})$ such that, for all $H,K\in S\\!g(\mathcal{G})$, if
$H\mathop{@_{\mathcal{E}}}\nolimits K\\!\\!\downarrow$, then $H,K\in X$ iff
$H\mathop{@_{\mathcal{E}}}\nolimits K\in X$.

[Ordered Scaffold] An ordered scaffold is a structure
$\mathcal{X}=(\mathcal{G},\mathcal{E},X,\preccurlyeq)$ such that $\mathcal{G}$
is a graph, $\mathcal{E}\subseteq E(\mathcal{G})$, $X$ an admissible subgraph
set and $\preccurlyeq$ a preorder on $X$. Layers are present if
$H\mathop{@_{\mathcal{E}}}\nolimits K\\!\\!\downarrow$ for at least one pair
$H,K\in X$.

Figure 2 shows a simple example of an ordered scaffold. Note that the scaffold
is preordered and we choose a subset of the subgraph set. This is a more
general definition of scaffold than that taken in [9, 10], where the structure
was less tightly defined.

There are several reasons for these choices. Properties of graphs that are
inherited by their subgraphs are naturally captured in an intuitionistic
logic. This idea is generalized by the preorder the ordered scaffold carries,
structure that allows us to extend the Kripke interpretation of propositional
intuitionistic logic to obtain our semantics for ILGL. We do not specify which
preorder the scaffold carries as there are a number of natural choices. It
also may be desirable to define more exotic orders for specific modelling
situations.

Figure 3. Place and link graphs

Figure 4. Bigraph

[Bigraphs] A bigraph [39] is comprised of a set of nodes on which a _place
graph_ and a _link graph_ are defined. The place graph has the structure of a
disjoint union of trees (a forest), whilst the link graph is a hypergraph on
which one edge can connect many nodes. Intuitively, the place graph denotes
spatial relationships, whilst the link graph denotes the communication
structure of the system.

The link graph has additional structure: finite sets of labelled vertices
$\\{x_{1},\ldots,x_{n}\\}$, $\\{y_{1},\ldots,y_{m}\\}$ denoting _inner names_
and _outer names_ respectively. These act as interfaces to enable the
composition of bigraphs: if the outer names of a bigraph match the inner names
of another, their link graphs may be connected at these vertices. This
compositional quality makes bigraphs ideal structures for modelling
distributed systems. Bigraphical Reactive Systems (BRS) provide a dynamics for
such models by defining transitions that reconfigure spatial relations and
connectivity. Such systems generalize a wealth of process calculi, including
$\pi$-calculi and the CCS.

Figure 4 shows a bigraph and Figure 4 its consituent parts. The structure of
the place graph is visually realised in the bigraph by the containment of its
nodes. We now show how a system of composed bigraphs can be encoded as an
ordered scaffold. Given we work with directed graphs, we model a form of
_directed_ bigraph [25].

We begin with a single bigraph. First, consider the link graph. We can replace
each hyperedge with a vertex attached to which we add an edge for each
connection of the hyperedge. This obtains a directed graph with the same path
information. Now note that a forest can straightforwardly be seen as a partial
order on its vertices. This generates a partial order $\preccurlyeq$ on the
set of subgraphs $\\{\\{v\\}\mid v\text{ a vertex of the place graph}\\}$. We
extend $\preccurlyeq$ to the link graph $H$ by specifying that $H\preccurlyeq
H$.

Now we consider a system of composed bigraphs. Given bigraphs
$(H,\preccurlyeq)$, $(K,\preccurlyeq^{\prime})$ where $H$ has the same outer
names as $K$’s inner names, we can connect the outer name vertices of $H$ to
the inner name vertices of $K$ with new edges. We collect all such edges as
$\mathcal{E}$. Thus the composition $H\mathop{@_{\mathcal{E}}}\nolimits K$
denotes the composition of the link graphs $(H,\preccurlyeq)$ and
$(K,\preccurlyeq^{\prime})$, and we can take the disjoint union of the partial
orders to obtain a bigraph $(H\mathop{@_{\mathcal{E}}}\nolimits
K,\preccurlyeq\sqcup\preccurlyeq^{\prime})$. In this way we obtain an ordered
scaffold with the admissible subgraph set given by the closure under
composition of the set $\\{\\{v\\}\mid v\text{ a vertex of a place graph }\\}$
together with each link graph $H$, and order generated by the union of the
partial orders defined by the place graphs of the system. ∎

We choose an admissible subgraph set in order to reason more specifically
about the layering structure of interest in the model, and to avoid degenerate
cases of layers. For example, two disjoint subgraphs $H$ and $K$ may designate
distinct, non-interacting regions in a systems model. However their disjoint
union would be interpreted as layered over another subgraph $L$ if
$H\leadsto_{\mathcal{E}}L$ but $K\not\leadsto_{\mathcal{E}}L$. The solution is
to specify $H\cup K\not\in X$ for the ordered scaffold modelling the system.

There are further technical considerations behind this choice. When we
restrict to interpreting ILGL on the full subgraph set, it is impossible to
perform any composition of models without the states proliferating wildly. A
similar issue arises during the construction of countermodels from the
tableaux system of Section 3, a procedure that breaks down when we are forced
to take the full subgraph set as the set of states.

###  2.2. The logic ILGL

Having established the layered graph construction and a semantic structure of
interest, we now set up the logic ILGL. Let $\mathrm{Prop}$ be a set of atomic
propositions, ranged over by p. The set $\mathrm{Form}$ of all propositional
formulae is generated by the following grammar:

$\varphi::=\mathrm{p}\mid\top\mid\bot\mid\varphi\wedge\varphi\mid\varphi\vee\varphi\mid\varphi\rightarrow\varphi\mid\varphi\blacktriangleright\varphi\mid\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\varphi\mid\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\varphi$

A Hilbert-type proof system for ILGL, $\mathrm{ILGL}_{\mathrm{H}}$, is given
in Figure 5. Intuitively, the judgement $\varphi\vdash\psi$ can be read as
$\varphi$ implies $\psi$; or, if $\varphi$ is provable than so too is $\psi$.
This intuition is made precise in Section 4. where it is shown that $\vdash$
can be interpreted as the order of a Heyting algebra; it is straightforward to
show that $a\leq b$ iff $a\rightarrow b=\top$ in a Heyting algebra. We say
$\varphi\vdash\psi$ is provable if it can be derived in the system; similarly,
we say the formula $\varphi$ is provable if $\top\vdash\varphi$ is provable.

The additive fragment, corresponding to intuitionistic propositional logic, is
standard (e.g., [2]). The presentation of the multiplicative fragment is
similar to that for BI’s multiplicatives [41], but for the non-commutative and
non-associative (following from the absence of a multiplicative counterpart to
$\wedge_{2}$) conjunction, $\blacktriangleright$, together with its associated
left and right implications
$\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}$ and
$\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}$ (cf. [35, 36]). The
multiplicative conjunction is key to our logic, as it captures layering.

$(\mathrm{Ax})$ $\varphi\vdash\varphi$ $\varphi\vdash\psi$ $\psi\vdash\chi$
$(\mathrm{Cut})$ $\varphi\vdash\chi$ $(\top)$ $\varphi\vdash\top$ $(\bot)$
$\bot\vdash\varphi$
---
$\varphi\vdash\psi$ $\varphi\vdash\chi$ $(\wedge_{1})$
$\varphi\vdash\psi\wedge\chi$ $(\wedge_{2})$
$\varphi_{1}\wedge\varphi_{2}\vdash\varphi_{i}$
$(\vee_{1})$ $\varphi_{i}\vdash\varphi_{1}\vee\varphi_{2}$ $\varphi\vdash\chi$
$\psi\vdash\chi$ $(\vee_{2})$ $\varphi\vee\psi\vdash\chi$
$\varphi\vdash\psi\rightarrow\chi$ $\nu\vdash\psi$ $(\rightarrow_{1})$
$\varphi\wedge\nu\vdash\chi$ $\varphi\wedge\psi\vdash\chi$ $(\rightarrow_{2})$
$\varphi\vdash\psi\rightarrow\chi$ $\varphi\vdash\psi$ $\chi\vdash\nu$
$(\blacktriangleright)$
$\varphi\blacktriangleright\chi\vdash\psi\blacktriangleright\nu$
$\varphi\vdash\psi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\chi$
$\nu\vdash\psi$ $(\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{1})$
$\varphi\blacktriangleright\nu\vdash\chi$
$\varphi\blacktriangleright\psi\vdash\chi$
$(\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{2})$
$\varphi\vdash\psi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\chi$
$\varphi\vdash\psi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\chi$
$\nu\vdash\psi$
$(\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{1})$
$\nu\blacktriangleright\varphi\vdash\chi$
$\varphi\blacktriangleright\psi\vdash\chi$
$(\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{2})$
$\psi\vdash\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\chi$
Figure 5.  Rules of the Hilbert system, $\mathrm{ILGL}_{\mathrm{H}}$

[Layered graph model] A _layered graph model_
$\mathcal{M}=(\mathcal{X},\mathcal{V})$ of $\mathrm{ILGL}$ is a pair where
$\mathcal{X}$ is an ordered scaffold and
$\mathcal{V}:\mathrm{Prop}\rightarrow\mathcal{P}(X)$ is a _persistent_
valuation; that is, $H\preccurlyeq K\text{ and
}H\in\mathcal{V}(\mathrm{p})\text{ implies }K\in\mathcal{V}(\mathrm{p})$. ∎

Given a layered graph model $\mathcal{M}=(\mathcal{X},\mathcal{V})$, we
generate the satisfaction relation $\models_{\mathcal{M}}\subseteq
X\times\mathrm{Form}$ as shown in Figure 6.

$H$ $\vDash_{\mathcal{M}}$ $\mathrm{p}$ iff $H\in\mathcal{V}(\mathrm{p})$ $H$
$\vDash_{\mathcal{M}}$ $\top$ $H\not\vDash_{\mathcal{M}}\bot$ $H$
$\vDash_{\mathcal{M}}$ $\varphi\land\psi$ iff $H\vDash_{\mathcal{M}}\varphi$
and $H\vDash_{\mathcal{M}}\psi$ $H$ $\vDash_{\mathcal{M}}$ $\varphi\lor\psi$
iff $H\vDash_{\mathcal{M}}\varphi$ or $H\vDash_{\mathcal{M}}\psi$ $H$
$\vDash_{\mathcal{M}}$ $\varphi\rightarrow\psi$ iff for all $K\succcurlyeq H$,
$K\vDash_{\mathcal{M}}\varphi$ implies $K$ $\vDash_{\mathcal{M}}$ $\psi$ $H$
$\vDash_{\mathcal{M}}$ $\varphi\blacktriangleright\psi$ iff there exists
$K_{0}\mathop{@_{\mathcal{E}}}\nolimits K_{1}\downarrow$ s.t. $H\succcurlyeq
K_{0}\mathop{@_{\mathcal{E}}}\nolimits K_{1}$,
$K_{0}\vDash_{\mathcal{M}}\varphi$ and $K_{1}\vDash_{\mathcal{M}}\psi$ $H$
$\vDash_{\mathcal{M}}$
$\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi$ iff for
all $K$ and $L\succcurlyeq H$ s.t. $L\mathop{@_{\mathcal{E}}}\nolimits
K\downarrow$: $L\vDash_{\mathcal{M}}\varphi$ implies
$L\mathop{@_{\mathcal{E}}}\nolimits K\vDash_{\mathcal{M}}\psi$ $H$
$\vDash_{\mathcal{M}}$
$\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\psi$ iff for
all $K$ and $L\succcurlyeq H$ s.t. $K\mathop{@_{\mathcal{E}}}\nolimits
L\downarrow$: $L\vDash_{\mathcal{M}}\varphi$ implies
$K\mathop{@_{\mathcal{E}}}\nolimits L\vDash_{\mathcal{M}}\psi$

Figure 6. Satisfaction for layered graph models of ILGL.

[Validity] The judgement $\varphi\vDash_{\mathcal{M}}\psi$ asserts that for
every subgraph $H$ of the layered graph model $\mathcal{M}$, whenever
$H\vDash_{\mathcal{M}}\varphi$, it follows that $H\vDash_{\mathcal{M}}\psi$.
$\varphi\vDash\psi$ asserts that $\varphi\vDash_{\mathcal{M}}\psi$ holds for
all layered graph models $\mathcal{M}$. $\varphi$ is _valid in a model
$\mathcal{M}$_ iff $\top\vDash_{\mathcal{M}}\varphi$; $\varphi$ is _valid_ iff
$\top\vDash\varphi$. ∎

A straightforward inductive argument shows that persistence extends to all
formulae for this semantics.

######  Lemma 1 (Persistence).

For all $\varphi\in\textrm{Form}$, $H\preccurlyeq K$ and
$H\models_{\mathcal{M}}\varphi$ implies $K\models_{\mathcal{M}}\varphi$. ∎

Persistence yields soundness of the Hilbert system for ILGL with respect to
the layered graph semantics; we will return to the completeness of the Hilbert
system in Section 4.

######  Theorem 2 (Soundness of (I)LGL).

$\varphi\vdash\psi$ is provable implies $\varphi\vDash\psi$. Similarly,
$\varphi$ provable implies $\varphi$ is valid.

######  Proof 2.1.

Soundness follows by showing that validity of premisses leads to validity of
the conclusion for each rule. We demonstrate with the rule
$(\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{1})$

$\quad\cfrac{\xi\vdash\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\psi\quad\eta\vdash\varphi}{\eta\blacktriangleright\xi\vdash\psi}$

on layered graph models. Suppose
$\xi\vDash\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\psi$
and $\eta\vDash\varphi$. Let $H$ be an arbitrary subgraph in a layered graph
model such that $H\vDash\eta\blacktriangleright\xi$. Then $H\succcurlyeq
K_{0}\mathop{@_{\mathcal{E}}}\nolimits K_{1}$ with $K_{0}\vDash\eta$ and
$K_{1}\vDash\xi$. By assumption $K_{0}\vDash\varphi$ and
$K_{1}\vDash\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\psi$
so $H\succcurlyeq K_{0}\mathop{@_{\mathcal{E}}}\nolimits K_{1}$ entails
$x\vDash\psi$ by persistence, as required.

Note that, unlike in BI’s resource monoid semantics, we require the
restriction ‘for all $K$, $H\preccurlyeq K\ldots$’ in the semantic clauses for
the multiplicative implications. Without this we cannot prove persistence, and
with it completeness, because we cannot apply the inductive hypothesis in
those cases. The reason for this is that we put no restriction on the
interaction between $\preccurlyeq$ and $@$ in the definition of preordered
scaffold. This is unlike the analogous case for BI, where the monoidal
composition is required to be bifunctorial with respect to the ordering. One
might resolve this issue with the following addendum to the definition of
preordered scaffold: if $H\preccurlyeq K$ and
$K\mathop{@_{\mathcal{E}}}\nolimits L\downarrow$, then
$H\mathop{@_{\mathcal{E}}}\nolimits L\downarrow$ and
$H\mathop{@_{\mathcal{E}}}\nolimits L\preccurlyeq
K\mathop{@_{\mathcal{E}}}\nolimits L$.

Two natural examples of subgraph preorderings show that this would be
undesirable. First, consider the layering preorder. Let $\preccurlyeq$ be the
reflexive, transitive closure of the relation $R(H,K)$ iff
$K\mathop{@_{\mathcal{E}}}\nolimits H\downarrow$, restricted to the admissible
subgraph set $X$. Figure 8 shows a subgraph $H$ with $L\preccurlyeq H$ and
$H\mathop{@_{\mathcal{E}}}\nolimits K\downarrow$ but
$L\mathop{@_{\mathcal{E}}}\nolimits K\uparrow$. Second, consider the subgraph
order. In Figure 8, we have $L\subseteq H$ and
$H\mathop{@_{\mathcal{E}}}\nolimits K\downarrow$ but
$L\mathop{@_{\mathcal{E}}}\nolimits K\uparrow$. It is, however, the case that,
with this ordering, if $H\subseteq K,K\mathop{@_{\mathcal{E}}}\nolimits
L\downarrow$ and $H\mathop{@_{\mathcal{E}}}\nolimits L\downarrow$, then
$H\mathop{@_{\mathcal{E}}}\nolimits L\subseteq
K\mathop{@_{\mathcal{E}}}\nolimits L$.

Figure 7. $\mathcal{E}$-reachability preorder

Figure 8. Subgraph order

###  2.3. Labelled tableaux

It’s clear that obtaining completeness for the class of layered graph models
with respect to the Hilbert system $\mathrm{ILGL}_{\mathrm{H}}$ will not be a
straightforward task. For one, there does not appear to be any sensible way to
augment equivalence classes of ILGL formulae with graph theoretic structure in
such a way that $\mathrm{ILGL}_{\mathrm{H}}$-provability is reflected. A key
reason for this is that the multiplicativity of $\blacktriangleright$ is not
directly represented in $\mathrm{ILGL}_{\mathrm{H}}$.

We take an alternative route: we define a labelled tableaux system for ILGL,
utilising a method first showcased on tableaux systems for BBI [37] and DMBI
[15], strongly influenced by previous work for BI [22]. By carefully
restricting the labelling algebra of the proof system, we are able to
uniformly transform the labels of a derivation into a layered graph model
under the right conditions. This is similar in spirit to the labelled tableaux
system for Separation Logic [21], which has a countermodel extraction
procedure that outputs heap models, the intended models of the logic. It will
be shown in Section 4 that this captures a notion of provability equivalent to
$\mathrm{ILGL}_{\mathrm{H}}$.

[Graph labels] Let $\Sigma=\\{c_{i}\mid i\in\mathbb{N}\\}$ be a countable set
of _atomic labels_. We define the set $\mathbb{L}=\\{x\in\Sigma^{\star}\mid
0<\lvert x\rvert\leq 2\\}\setminus\\{c_{i}c_{i}\mid c_{i}\in\Sigma\\}$ to be
the set of _graph labels_. A _sub-label_ $y$ of a label $x$ is a non-empty
sub-word of $x$, and we denote the set of sub-labels of $x$ by
$\mathcal{S}(x)$. ∎

The graph labels are a syntactic representation of the subgraphs of a model,
with labels of length $2$ representing a graph that can be decomposed into two
layers. We exclude the possibility $c_{i}c_{i}$ as layering is anti-reflexive.
In much the same way we give a syntactic representation of preorder.

[Constraints] A _constraint_ is an expression of the form $x\preccurlyeq y$,
where $x$ and $y$ are graph labels. ∎

Let $\mathcal{C}$ be a set of constraints. The _domain_ of $\mathcal{C}$,
$\mathcal{D}(\mathcal{C})$, is the set of all sub-labels appearing in
$\mathcal{C}$. In particular, $\mathcal{D}(\mathcal{C})=\bigcup_{x\preccurlyeq
y\in\mathcal{C}}(\mathcal{S}(x)\cup\mathcal{S}(y))$ The _alphabet_ of
$\mathcal{C}$ is the set of atomic labels appearing in $\mathcal{C}$. In
particular, we have
$\mathcal{A}(\mathcal{C})=\Sigma\cap\mathcal{D}(\mathcal{C})$.

$x\preccurlyeq y$ $\langle\mathrm{R}_{1}\rangle$ $x\preccurlyeq x$
$x\preccurlyeq y$ $\langle\mathrm{R_{2}}\rangle$ $y\preccurlyeq y$
$x\preccurlyeq yz$ $\langle\mathrm{R_{3}}\rangle$ $y\preccurlyeq y$
$x\preccurlyeq yz$ $\langle\mathrm{R_{4}}\rangle$ $z\preccurlyeq z$
---
$xy\preccurlyeq z$ $\langle\mathrm{R}_{5}\rangle$ $x\preccurlyeq x$
$xy\preccurlyeq z$ $\langle\mathrm{R}_{6}\rangle$ $y\preccurlyeq y$
$x\preccurlyeq y$ $y\preccurlyeq z$ $\langle\mathrm{Tr}\rangle$ $x\preccurlyeq
z$

Figure 9.  Rules for closure of constraints

[Closure of constraints] Let $\mathcal{C}$ be a set of constraints. The
closure of $\mathcal{C}$, denoted $\overline{\mathcal{C}}$, is the least
relation closed under the rules of Figure 9 such that
$\mathcal{C}\subseteq\overline{\mathcal{C}}$. ∎

This closure yields a preorder on $\mathcal{D}(\mathcal{C})$, with
$\langle\mathrm{R}_{1}\rangle-\langle\mathrm{R}_{6}\rangle$ generating
reflexivity and $\langle\mathrm{Tr}\rangle$ yielding transitivity. Crucially,
taking the closure of the constraint set does not cause labels to proliferate
and the generation of any particular constraint from an arbitrary constraint
set $\mathcal{C}$ is fundamentally a finite process.

######  Proposition 3.

Let $\mathcal{C}$ be a set of constraints. (1)
$x\in\mathcal{D}(\overline{\mathcal{C}})$ iff $x\preccurlyeq
x\in\overline{\mathcal{C}}$. (2)
$\mathcal{D}(\mathcal{C})=\mathcal{D}(\overline{\mathcal{C}})$ and
$\mathcal{A}(\mathcal{C})=\mathcal{A}(\overline{\mathcal{C}})$. ∎

######  Lemma 4 (Compactness).

Let $\mathcal{C}$ be a (possibly countably infinite) set of constraints. If
$x\preccurlyeq y\in\overline{\mathcal{C}}$, then there is a finite set of
constraints $\mathcal{C}_{f}\subseteq\mathcal{C}$ such that $x\preccurlyeq
y\in\overline{\mathcal{C}_{f}}$. ∎

[Labelled Formula / CSS] A _labelled formula_ is a triple
$(\mathbb{S},\varphi,x)\in\\{\mathbb{T},\mathbb{F}\\}\times\mathrm{Form}\times\mathbb{L}$,
written $\mathbb{S}\varphi:x$. A _constrained set of statements_ (CSS) is a
pair $\textsc{css}{\mathcal{F}}{\mathcal{C}}$, where $\mathcal{F}$ is a set of
labelled formulae and $\mathcal{C}$ is a set of constraints, satisfying the
following properties: for all $x\in\mathbb{L}$ and distinct
$c_{i},c_{j},c_{k}\in\Sigma$,

  1. (1)

$(\text{Ref })$ if $\mathbb{S}\varphi:x\in\mathcal{F}$, then $x\preccurlyeq
x\in\overline{\mathcal{C}}$,

  2. (2)

$(\text{Contra})$ if $c_{i}c_{j}\in\mathcal{D}(\mathcal{C})$, then
$c_{j}c_{i}\not\in\mathcal{D}(\mathcal{C})$, and

  3. (3)

$(\text{Freshness})$ if $c_{i}c_{j}\in\mathcal{D}(\mathcal{C})$, then
$c_{i}c_{k},c_{k}c_{i},c_{j}c_{k},c_{k}c_{j}\not\in\mathcal{D}(\mathcal{C})$.

A CSS $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ is _finite_ if $\mathcal{F}$
and $\mathcal{C}$ are finite. The relation $\subseteq$ is defined on CSSs by
$\textsc{css}{\mathcal{F}}{\mathcal{C}}\subseteq\textsc{css}{\mathcal{F}^{\prime}}{\mathcal{C}^{\prime}}\text{
iff }\mathcal{F}\subseteq\mathcal{F}^{\prime}\text{ and
}\mathcal{C}\subseteq\mathcal{C}^{\prime}$. We denote by
$\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}\subseteq_{f}\textsc{css}{\mathcal{F}}{\mathcal{C}}$
when
$\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}\subseteq\textsc{css}{\mathcal{F}}{\mathcal{C}}$
holds and $\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}$ is finite. ∎

The CSS properties ensure models can be built from the labels: (Ref) ensures
we have enough data for the closure rules to generate a preorder, (Contra)
ensures the contra-commutativity of graph layering is respected, and
(Freshness) ensures the layering structure of the models we construct is
exactly that specified by the labels and constraints in the CSS. As with
constraint closure, CSSs have a finite character.

######  Proposition 5.

For any CSS $\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}}$ in which
$\mathcal{F}_{f}$ is finite, there exists
$\mathcal{C}_{f}\subseteq\mathcal{C}$ such that $\mathcal{C}_{f}$ is finite
and $\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}$ is a CSS. ∎

$\langle\mathbb{T}\wedge\rangle$ | $\langle\mathbb{F}\wedge\rangle$ |  $\mathbb{\mathbb{F}}\varphi\wedge\psi:x\in\mathcal{F}$ $\textsc{css}{\\{\mathbb{\mathbb{F}}\varphi:x\\}}{\emptyset}\ \mid\ \textsc{css}{\\{\mathbb{\mathbb{F}}\psi:x\\}}{\emptyset}$
---|---|---
$\langle\mathbb{T}\vee\rangle$ | $\langle\mathbb{F}\vee\rangle$ |  $\mathbb{\mathbb{F}}\varphi\vee\psi:x\in\mathcal{F}$ $\textsc{css}{\\{\mathbb{\mathbb{F}}\varphi:x,\mathbb{\mathbb{F}}\psi:x\\}}{\emptyset}$
$\langle\mathbb{T}\rightarrow\rangle$ | $\langle\mathbb{F}\rightarrow\rangle$ |  $\mathbb{\mathbb{F}}\varphi\rightarrow\psi:x\in\mathcal{F}$ $\textsc{css}{\\{\mathbb{\mathbb{T}}\varphi:c_{i},\mathbb{\mathbb{F}}\psi:c_{i}\\}}{\\{x\preccurlyeq c_{i}\\}}$
$\langle\mathbb{T}\blacktriangleright\rangle$ | $\langle\mathbb{F}\blacktriangleright\rangle$ |  $\mathbb{\mathbb{F}}\varphi\blacktriangleright\psi:x\in\mathcal{F}\text{ and }yz\preccurlyeq x\in\overline{\mathcal{C}}$ $\textsc{css}{\\{\mathbb{\mathbb{F}}\varphi:y\\}}{\emptyset}\ \mid\ \textsc{css}{\\{\mathbb{\mathbb{F}}\psi:z\\}}{\emptyset}$
$\langle\mathbb{T}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\rangle$ | $\langle\mathbb{F}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\rangle$ |  $\mathbb{\mathbb{F}}\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi:x\in\mathcal{F}$ $\textsc{css}{\\{\mathbb{\mathbb{T}}\varphi:c_{j},\mathbb{\mathbb{F}}\psi:c_{i}c_{j}\\}}{\\{x\preccurlyeq c_{i},c_{i}c_{j}\preccurlyeq c_{i}c_{j}\\}}$
$\langle\mathbb{T}\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\rangle$ | $\langle\mathbb{F}\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\rangle$ |  $\mathbb{\mathbb{F}}\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\psi:x\in\mathcal{F}$ $\textsc{css}{\\{\mathbb{\mathbb{T}}\varphi:c_{j},\mathbb{\mathbb{F}}\psi:c_{j}c_{i}\\}}{\\{x\preccurlyeq c_{i},c_{j}c_{i}\preccurlyeq c_{j}c_{i}\\}}$
with $c_{i}$ and $c_{j}$ being fresh atomic labels.

Figure 10. Tableaux rules for ILGL

Figure 10 presents the rules of the tableaux system for ILGL. That ‘$c_{i}$
and $c_{j}$ are fresh atomic labels’ means
$c_{i}\not=c_{j}\in\Sigma\setminus\mathcal{A}(\mathcal{C})$. This means it is
impossible to introduce the word $c_{i}c_{i}\not\in\mathbb{L}$ as a label.
Note also that bunching is explicit in the labels, with concatenation of
labels occurring in the rules for the multiplicative connectives
$\blacktriangleright$,
$\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}$,
$\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}$. This is analogous
(and in fact equivalent) to the concatenation of contexts via the
multiplicative conjunction’s context former in a sequent calculus. This is in
stark contrast to the Hilbert system $\mathrm{ILGL}_{\mathrm{H}}$ which
outsources this structure to the metatheory.

[Tableaux] Let $\textsc{css}{\mathcal{F}_{0}}{\mathcal{C}_{0}}$ be a finite
CSS. A _tableau_ for this CSS is a list of CSS, called _branches_ , built
inductively according to the following rules, where $\oplus$ denotes the
concatenation of lists:

  1. (1)

The one branch list $[\textsc{css}{\mathcal{F}_{0}}{\mathcal{C}_{0}}]$ is a
tableau for $\textsc{css}{\mathcal{F}_{0}}{\mathcal{C}_{0}}$;

  2. (2)

If the list
$\mathcal{T}_{m}\oplus[\textsc{css}{\mathcal{F}}{\mathcal{C}}]\oplus\mathcal{T}_{n}$
is a tableau for $\textsc{css}{\mathcal{F}_{0}}{\mathcal{C}_{0}}$ and

cond$\textsc{css}{\mathcal{F}}{\mathcal{C}}$
$\textsc{css}{\mathcal{F}_{1}}{\mathcal{C}_{1}}$ $\mid$ …$\mid$
$\textsc{css}{\mathcal{F}_{k}}{\mathcal{C}_{k}}$

is an instance of a rule of Figure 10 for which
cond$\textsc{css}{\mathcal{F}}{\mathcal{C}}$ is fulfilled, then the list
$\mathcal{T}_{m}\oplus[\textsc{css}{\mathcal{F}\cup\mathcal{F}_{1}}{\mathcal{C}\cup\mathcal{C}_{1}};\ldots;\textsc{css}{\mathcal{F}\cup\mathcal{F}_{k}}{\mathcal{C}\cup\mathcal{C}_{k}}]\oplus\mathcal{T}_{n}$
is a tableau for $\textsc{css}{\mathcal{F}_{0}}{\mathcal{C}_{0}}$.

A _tableau_ for the formula $\varphi$ is a _tableau_ for
$\textsc{css}{\\{\mathbb{\mathbb{F}}\varphi:c_{0}\\}}{\\{c_{0}\preccurlyeq
c_{0}\\}}$. ∎

It is a simple but tedious exercise to show that the rules of Figure 10
preserve the CSS properties of Definition 4.

We now give the notion of proof for our labelled tableaux.

[Closed tableau/proof] A CSS $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ is
_closed_ if one of the following conditions holds: (1)
$\mathbb{\mathbb{T}}\varphi:x\in\mathcal{F}$,
$\mathbb{\mathbb{F}}\varphi:y\in\mathcal{F}$ and $x\preccurlyeq
y\in\overline{\mathcal{C}}$; (2) $\mathbb{\mathbb{F}}\top:x\in\mathcal{F}$;
and (3) $\mathbb{\mathbb{T}}\bot:x\in\mathcal{F}$. A CSS is _open_ iff it is
not closed. A tableau is closed iff all its branches are closed. A _proof_ for
a formula $\varphi$ is a closed tableau for $\varphi$. ∎

Figure 11 shows a tableau proof of
$q\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}(q\blacktriangleright(p\rightarrow(p\lor
q)))$ in tree form. Each branch gives the set $\mathcal{F}$ of labelled
formulae of a CSS, with the rectangular boxes giving its set of constraints
$\mathcal{C}$. $\surd_{i}$ denotes the application of a rule, with the circled
side conditions showing which condition on the closure of the constraint set
was used to allow it. Finally, the cross $\times$ marks the closure of a
branch.

The first rule application at $\surd_{1}$ is
$\langle\mathbb{F}\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\rangle$.
This introduces fresh labels $c_{1}$ and $c_{2}$ with the constraints
$c_{0}\preccurlyeq c_{1}$ and $c_{2}c_{1}\preccurlyeq c_{2}c_{1}$. Since we
have the constraint $c_{2}c_{1}\preccurlyeq c_{2}c_{1}$ we are able to apply
$\langle\mathbb{F}\blacktriangleright\rangle$ at $\surd_{2}$. The tableau then
branches. On the left hand branch we have both $\mathbb{T}q:c_{2}$ and
$\mathbb{F}q:c_{2}$, thus it is closed; on the right we apply
$\langle\mathbb{F}\rightarrow\rangle$ at $\surd_{3}$. This introduces a fresh
label $c_{3}$ with the constraint $c_{1}\preccurlyeq c_{3}$ and introduces
$\mathbb{T}p:c_{3}$ to the branch. We then apply
$\langle\mathbb{F}\lor\rangle$ at $\surd_{4}$, introducing
$\mathbb{F}p:c_{3}$, thus closing the branch. As both branches are closed, the
tableau is closed and the formula is proved.

Figure 11. A tableau proof of
$q\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}(q\blacktriangleright(p\rightarrow(p\lor
q)))$

CSSs are related back to the graph semantics via the notion of realization.

[Realization] Let $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ be a CSS. A
_realization_ of $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ is a triple
$\mathfrak{R}=(\mathcal{X},\mathcal{V},\lfloor.\rfloor)$ where
$\mathcal{M}=(\mathcal{X},\mathcal{V})$ is a layered graph model and
$\lfloor.\rfloor:\mathcal{D}(\mathcal{C})\rightarrow X$ is such that (1) for
all $x\in\mathcal{D}(\mathcal{C})$, if $x=c_{i}c_{j}$, then $\lfloor
c_{i}\rfloor\mathop{@_{\mathcal{E}}}\nolimits\lfloor c_{j}\rfloor\downarrow$
and $\lfloor x\rfloor=\lfloor
c_{i}\rfloor\mathop{@_{\mathcal{E}}}\nolimits\lfloor c_{j}\rfloor$), (2) if
$x\preccurlyeq y\in\mathcal{C}$, then $\lfloor
x\rfloor\preccurlyeq_{\mathcal{M}}\lfloor y\rfloor$, (3) if
$\mathbb{T}\varphi:x\in\mathcal{F}$, then $\lfloor
x\rfloor\models_{\mathcal{M}}\varphi$, (4) if
$\mathbb{F}\varphi:x\in\mathcal{F}$, then $\lfloor
x\rfloor\not\models_{\mathcal{M}}\varphi$. ∎

We say that a CSS is _realizable_ if there exists a realization of it. We say
that a tableau is _realizable_ if at least one of its branches is realizable.
We can also show that the relevant clauses of the definition extend to the
closure of the constraint set automatically.

######  Proposition 6.

Let $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ be a CSS and
$\mathfrak{R}=(\mathcal{X},\mathcal{V},\lfloor.\rfloor)$ a realization of it.
Then: (1) for all $x\in\mathcal{D}(\overline{\mathcal{C}})$, $\lfloor
x\rfloor$ is defined; (2) if $x\preccurlyeq y\in\overline{\mathcal{C}}$, then
$\lfloor x\rfloor\preccurlyeq\lfloor y\rfloor$. ∎

##  3\. Soundness & Completeness

In this section we establish the soundness and, via countermodel extraction,
the completeness of ILGL’s tableaux system with respect to layered graph
semantics. The proof of soundness is straightforward (cf. [15, 19, 22, 37]).
We begin with two key lemmas about realizability and closure. Their proofs
proceed by simple case analysis.

######  Lemma 7.

The tableaux rules for ILGL preserve realizability. ∎

######  Lemma 8.

Closed branches are not realizable. ∎

######  Theorem 9 (Soundness).

If there exists a closed tableau for the formula $\varphi$, then $\varphi$ is
valid in layered graph models.

######  Proof 3.1.

Suppose that there exists a proof for $\varphi$. Then there is a closed
tableau $\mathcal{T}_{\varphi}$ for the CSS
$\mathfrak{C}=\textsc{css}{\\{\mathbb{\mathbb{F}}\varphi:c_{0}\\}}{\\{c_{0}\preccurlyeq
c_{0}\\}}$. Now suppose that $\varphi$ is not valid. Then there is a
countermodel $\mathcal{M}=(\mathcal{X},\mathcal{V})$ and a subgraph $H\in X$
such that $H\not\models_{\mathcal{M}}\varphi$. Define
$\mathfrak{R}=(\mathcal{M},\mathcal{V},\lfloor.\rfloor)$ with $\lfloor
c_{0}\rfloor=H$. Note that $\mathfrak{R}$ is a realization of $\mathfrak{C}$,
hence by Lemma 7, $\mathcal{T}_{\varphi}$ is realizable. By Lemma 8,
$\mathcal{T}_{\varphi}$ cannot be closed. But, this contradicts the fact that
$\mathcal{T}_{\varphi}$ is a proof and therefore a closed tableau. It follows
that $\varphi$ is valid.

We now proceed to establish the completeness of the labelled tableaux with
respect to layered graph semantics. We begin with the notion of a Hintikka
CSS, which will facilitate the construction of countermodels.

[Hintikka CSS] A CSS $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ is a _Hintikka
CSS_ iff, for any formulae $\varphi,\psi\in\mathrm{Form}$ and any graph labels
$x,y\in\mathbb{L}$, we have the following:

${\small\begin{array}[]{rl}1.&\mbox{\rm$\mathbb{T}\varphi:x\not\in\mathcal{F}$
or $\mathbb{F}\varphi:y\not\in\mathcal{F}$ or $x\preccurlyeq
y\not\in\overline{\mathcal{C}}$ \quad 2. $\mathbb{F}\top:x\not\in\mathcal{F}$
\quad 3. $\mathbb{T}\bot:x\not\in\mathcal{F}$}\\\ 4.&\mbox{\rm if
$\mathbb{T}\varphi\wedge\psi:x\in\mathcal{F}$, then
$\mathbb{T}\varphi:x\in\mathcal{F}$ and $\mathbb{T}\psi:x\in\mathcal{F}$}\\\
5.&\mbox{\rm if $\mathbb{F}\varphi\wedge\psi:x\in\mathcal{F}$, then
$\mathbb{F}\varphi:x\in\mathcal{F}$ or $\mathbb{F}\psi:x\in\mathcal{F}$}\\\
6.&\mbox{\rm if $\mathbb{T}\varphi\vee\psi:x\in\mathcal{F}$, then
$\mathbb{T}\varphi:x\in\mathcal{F}$ or $\mathbb{T}\psi:x\in\mathcal{F}$}\\\
7.&\mbox{\rm if $\mathbb{F}\varphi\vee\psi:x\in\mathcal{F}$, then
$\mathbb{F}\varphi:x\in\mathcal{F}$ and $\mathbb{F}\psi:x\in\mathcal{F}$}\\\
8.&\mbox{\rm if $\mathbb{T}\varphi\rightarrow\psi:x\in\mathcal{F}$, then, for
all $y\in\mathbb{L}$, if $x\preccurlyeq y\in\overline{\mathcal{C}}$, then
$\mathbb{F}\varphi:y\in\mathcal{F}$ or $\mathbb{T}\psi:y\in\mathcal{F}$}\\\
9.&\mbox{\rm if $\mathbb{F}\varphi\rightarrow\psi:x\in\mathcal{F}$, then there
exists $y\in\mathbb{L}$ such that $x\preccurlyeq
y\in\overline{\mathcal{C}}$}\\\ &\mbox{\rm and
$\mathbb{T}\varphi:y\in\mathcal{F}$ and $\mathbb{F}\psi:y\in\mathcal{F}$}\\\
10.&\mbox{\rm if $\mathbb{T}\varphi\blacktriangleright\psi:x\in\mathcal{F}$,
then there are $c_{i},c_{j}\in\Sigma$ such that $c_{i}c_{j}\preccurlyeq
x\in\overline{\mathcal{C}}$ and}\\\
&\mbox{\rm$\mathbb{T}\varphi:c_{i}\in\mathcal{F}$ and
$\mathbb{T}\psi:c_{j}\in\mathcal{F}$}\\\ 11.&\mbox{\rm if
$\mathbb{F}\varphi\blacktriangleright\psi:x\in\mathcal{F}$, then, for all
$c_{i},c_{j}\in\Sigma$, if $c_{i}c_{j}\preccurlyeq
x\in\overline{\mathcal{C}}$, then}\\\
&\mbox{\rm$\mathbb{F}\varphi:c_{i}\in\mathcal{F}$ or
$\mathbb{F}\psi:c_{j}\in\mathcal{F}$}\\\ 12.&\mbox{\rm if
$\mathbb{T}\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi:x\in\mathcal{F}$,
then, for all $c_{i},c_{j}\in\Sigma$, if $x\preccurlyeq
c_{i}\in\overline{\mathcal{C}}$ and
$c_{i}c_{j}\in\mathcal{D}(\overline{\mathcal{C}})$, then}\\\
&\mbox{\rm$\mathbb{F}\varphi:c_{j}\\!\in\\!\mathcal{F}$ or
$\mathbb{T}\psi:c_{i}c_{j}\\!\in\\!\mathcal{F}$}\\\ 13.&\mbox{\rm if
$\mathbb{F}\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi:x\in\mathcal{F}$,
then there are $c_{i},c_{j}\in\Sigma$ such that $x\preccurlyeq
c_{i}\in\overline{\mathcal{C}}$ and
$c_{i}c_{j}\in\mathcal{D}(\overline{\mathcal{C}})$ and}\\\
&\mbox{\rm$\mathbb{T}\varphi:c_{j}\in\mathcal{F}$ and
$\mathbb{F}\psi:c_{i}c_{j}\in\mathcal{F}$}\\\ 14.&\mbox{\rm if
$\mathbb{T}\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\psi:x\in\mathcal{F}$,
then, for all $c_{i},c_{j}\in\Sigma$, if $x\preccurlyeq
c_{i}\in\overline{\mathcal{C}}$ and
$c_{j}c_{i}\in\mathcal{D}(\overline{\mathcal{C}})$, then}\\\
&\mbox{\rm$\mathbb{F}\varphi:c_{j}\\!\in\\!\mathcal{F}$ or \/
$\mathbb{T}\psi:c_{j}c_{i}\\!\in\\!\mathcal{F}$}\\\ 15.&\mbox{\rm if
$\mathbb{F}\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi:x\in\mathcal{F}$,
then there are $c_{i},c_{j}\in\Sigma$ such that $x\preccurlyeq
c_{i}\in\overline{\mathcal{C}}$ and
$c_{j}c_{i}\in\mathcal{D}(\overline{\mathcal{C}})$ and }\\\
&\mbox{\rm$\mathbb{T}\varphi:c_{j}\in\mathcal{F}$ and \/
$\mathbb{F}\psi:c_{j}c_{i}\in\mathcal{F}$.}\end{array}}$

∎

We now give the definition of a function $\Omega$ that extracts a countermodel
from a Hintikka CSS. A Hintikka CSS can thus be seen as the _labelled_
tableaux counterpart of Hintikka sets, which are maximally consistent sets
satisfying a subformula property.

[Function $\Omega$] Let $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ be a Hintikka
CSS. The function $\Omega$ associates to
$\textsc{css}{\mathcal{F}}{\mathcal{C}}$ a tuple
$\Omega(\textsc{css}{\mathcal{F}}{\mathcal{C}})=(\mathcal{G},\mathcal{E},X,\preccurlyeq,\mathcal{V})$,
such that

  1. (1)

$V(\mathcal{G})=\mathcal{A}(\mathcal{C}$),

  2. (2)

$E(\mathcal{G})=\\{(c_{i},c_{j})\mid
c_{i}c_{j}\in\mathcal{D}(\mathcal{C})\\}=\mathcal{E}$, $X=\\{x^{\Omega}\mid
x\in\mathcal{D}(\mathcal{C})\\}$, where $V(c^{\Omega}_{i})=\\{c_{i}\\}$,
$E(c^{\Omega}_{i})=\emptyset$, $V((c_{i}c_{j})^{\Omega})=\\{c_{i}c_{j}\\}$,
and $E((c_{i}c_{j})^{\Omega})=\\{(c_{i},c_{j})\\}$,

  3. (3)

$x^{\Omega}\preccurlyeq y^{\Omega}$ iff $x\preccurlyeq
y\in\overline{\mathcal{C}}$, and

  4. (4)

$x^{\Omega}\in\mathcal{V}(p)$ iff there exists $y\in\mathcal{D}(\mathcal{C})$
such that $y\preccurlyeq x\in\overline{\mathcal{C}}$ and
$\mathbb{T}p:y\in\mathcal{F}$. ∎

The next lemma shows that there is a precise correspondence between the
structure that the Hintikka CSS properties impose on the labels and the
layered structure specified by the construction of the model.

######  Lemma 10.

Let $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ be a Hintikka CSS and
$\Omega(\textsc{css}{\mathcal{F}}{\mathcal{C}})=(\mathcal{G},\mathcal{E},X,\preccurlyeq,\mathcal{V})$.

  1. (1)

If $c_{i},c_{j}\in\mathcal{A}(\mathcal{C})$, then
$c_{i}c_{j}\in\mathcal{D}(\mathcal{C})$ iff
$c^{\Omega}_{i}\mathop{@_{\mathcal{E}}}\nolimits c^{\Omega}_{j}\downarrow$.

  2. (2)

If $c_{i}c_{j}\in\mathcal{D}(\mathcal{C})$, then
$(c_{i}c_{j})^{\Omega}=c^{\Omega}_{i}\mathop{@_{\mathcal{E}}}\nolimits
c^{\Omega}_{j}$.

  3. (3)

$x^{\Omega}\mathop{@_{\mathcal{E}}}\nolimits y^{\Omega}\downarrow$ iff there
exist $c_{i},c_{j}\in\mathcal{A}(\mathcal{C})$ s.t. $x=c_{i}$, $y=c_{j}$ and
$c_{i}c_{j}\in\mathcal{D}(\mathcal{C})$.

######  Proof 3.2.

  1. (1)

Immediate from CSS property (Contra).

  2. (2)

Immediate from 1. and the definition of $\Omega$.

  3. (3)

The right-to-left direction is trivial, so assume
$x^{\Omega}\mathop{@_{\mathcal{E}}}\nolimits y^{\Omega}\downarrow$. There are
three possible cases for $x$ and $y$ other than $x=c_{i}$ and $y=c_{j}$: we
attend to one as the others are similar. Suppose $x=c_{i}c_{j}$ and $y=c_{k}$.
Then $x^{\Omega}\mathop{@_{\mathcal{E}}}\nolimits y^{\Omega}\downarrow$ must
hold because of either $(c_{i},c_{k})\in\mathcal{E}$ or
$(c_{j},c_{k})\in\mathcal{E}$. That is,
$c_{i}c_{k}\in\mathcal{D}(\mathcal{C})$ or
$c_{j}c_{k}\in\mathcal{D}(\mathcal{C})$. In both cases the $CSS$ property
(Freshness) is contradicted so neither can hold. It follows that only the case
$x=c_{i}$ and $y=c_{j}$ is non-contradictory, and so by 1.
$c_{i}c_{j}\in\mathcal{D}(\mathcal{C})$.

######  Lemma 11.

Let $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ be a Hintikka CSS.
$\Omega(\textsc{css}{\mathcal{F}}{\mathcal{C}})$ is a layered graph model.

######  Proof 3.3.

$\mathcal{G}$ is clearly a graph and $\preccurlyeq$ being a preorder on $X$
can be read off of the rules for the closure of constraint sets. Thus the only
non-trivial aspects of the proof are that $X$ is admissible and that
$\mathcal{V}$ is persistent.

First we show that $X$ is an admissible subgraph set. Let $H,K\in
S\\!g(\mathcal{G})$ with $H\mathop{@_{\mathcal{E}}}\nolimits K\downarrow$.
First we assume $H,K\in X$. Then $H=x^{\Omega}$ and $K=y^{\Omega}$ for labels
$x,y$. By the previous lemma it follows that $x=c_{i}$ and $y=c_{j}$ and
$c_{i}c_{j}\in\mathcal{D}(\mathcal{C})$. Thus
$H\mathop{@_{\mathcal{E}}}\nolimits
K=c_{i}^{\Omega}\mathop{@_{\mathcal{E}}}\nolimits
c_{j}^{\Omega}=(c_{i}c_{j})^{\Omega}\in X$. Now suppose
$H\mathop{@_{\mathcal{E}}}\nolimits K\in X$. Then
$H\mathop{@_{\mathcal{E}}}\nolimits K=x^{\Omega}$ for some
$x\in\mathcal{D}(\mathcal{C})$. The case $x=c_{i}$ is clearly impossible as
$E(c_{i}^{\Omega})=\emptyset$ so necessarily $x=c_{i}c_{j}$. Then we have
$c_{i},c_{j}\in\mathcal{D}(\mathcal{C})$ as sub-labels of $c_{i}c_{j}$ and
$c^{\Omega}_{i}\mathop{@_{\mathcal{E}}}\nolimits c^{\Omega}_{j}\downarrow$
with $c^{\Omega}_{i}\mathop{@_{\mathcal{E}}}\nolimits c^{\Omega}_{j}$ the only
possible composition equal to $(c_{i}c_{j})^{\Omega}$. It follows that
$H=c_{i}^{\Omega}\in X$ and $K=c_{j}^{\Omega}\in X$ as required.

Finally we must show $\mathcal{V}$ is a persistent valuation. Let
$H\in\mathcal{V}(\mbox{\rm p})$ with $H\preccurlyeq K$. Then $H=x^{\Omega}$
and $K=y^{\Omega}$ for some $x,y\in\mathcal{D}(\mathcal{C})$ with
$x\preccurlyeq y\in\overline{\mathcal{C}}$. By definition of $\mathcal{V}$
there exists $z\in\mathcal{D}(\mathcal{C})$ with $z\preccurlyeq
x\in\overline{\mathcal{C}}$ and $\mathbb{\mathbb{T}}p:z\in\mathcal{F}$. By the
closure rule $\langle Tr\rangle$ we have $z\preccurlyeq
y\in\overline{\mathcal{C}}$ so $K=y^{\Omega}\in\mathcal{V}(p)$.

######  Lemma 12.

Let $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ be a Hintikka CSS and
$\mathcal{M}=\Omega(\textsc{css}{\mathcal{F}}{\mathcal{C}})=(\mathcal{G},\mathcal{E},X,\preccurlyeq,\mathcal{V})$.
For all formulae $\varphi\in\mathrm{Form}$, and all
$x\in\mathcal{D}(\mathcal{C})$. we have (1) if
$\mathbb{F}\varphi:x\in\mathcal{F}$, then
$x^{\Omega}\not\models_{\mathcal{M}}\varphi$, and (2) if
$\mathbb{T}\varphi:x\in\mathcal{F}$, then
$x^{\Omega}\models_{\mathcal{M}}\varphi$. Hence, if
$\mathbb{F}\varphi:x\in\mathcal{F}$, then $\varphi$ is not valid and
$\Omega(\textsc{css}{\mathcal{F}}{\mathcal{C}})$ is a countermodel of
$\varphi$.

######  Proof 3.4.

We proceed by a simultaneous structural induction on $\varphi$, concentrating
on cases of interest.

  * -

Base cases.

    * –

Case $\mathbb{F}\mbox{\rm p}:x\in\mathcal{F}$. We suppose that
$x^{\Omega}\models_{\mathcal{M}}\mbox{\rm p}$. Then
$x^{\Omega}\in\mathcal{V}(\mbox{\rm p})$. By the definition of $\mathcal{V}$,
there is a label $y$ such that $y\preccurlyeq x\in\overline{\mathcal{C}}$ and
$\mathbb{T}\mbox{\rm p}:y\in\mathcal{F}$. Then by condition (1) of Definition
3.1, $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ is not a Hintikka CSS, a
contradiction. It follows that $x^{\Omega}\not\models_{\mathcal{M}}\mbox{\rm
p}$.

    * –

Case $\mathbb{T}\mbox{\rm p}:x\in\mathcal{F}$. By property $(Ref)$,
$x\preccurlyeq x\in\overline{\mathcal{C}}$. Thus, by definition of
$\mathcal{V}$ we have $x^{\Omega}\in\mathcal{V}(\mbox{\rm p})$. Thus
$x^{\Omega}\models_{\mathcal{M}}\mbox{\rm p}$.

  * -

Inductive step. We now suppose that (1) and (2) hold for formulae $\varphi$
and $\psi$ (IH).

    * –

Case $\mathbb{T}\varphi\rightarrow\psi:x\in\mathcal{F}$. Suppose
$x^{\Omega}\preccurlyeq y^{\Omega}$. Then $x\preccurlyeq y\in\overline{C}$ and
by Definition 3.1 property (8) it follows that
$\mathbb{F}\varphi:y\in\mathcal{F}$ or $\mathbb{T}\psi:y\in\mathcal{F}$. By
(IH) it follows that if $y^{\Omega}\models_{\mathcal{M}}\varphi$ then
$y^{\Omega}\models_{\mathcal{M}}\psi$ as required.

    * –

Case $\mathbb{T}\varphi\blacktriangleright\psi:x\in\mathcal{F}$. By Definition
3.1 property (10) there exist labels $c_{i},c_{j}\in\mathcal{D}(\mathcal{C})$
such that $c_{i}c_{j}\preccurlyeq x\in\overline{\mathcal{C}}$ and
$\mathbb{T}\varphi:c_{i}\in\mathcal{F}$ and
$\mathbb{T}\psi:c_{j}\in\mathcal{F}$. By (IH) we have
$c_{i}^{\Omega}\models_{\mathcal{M}}\varphi$ and
$c_{j}^{\Omega}\models_{\mathcal{M}}\psi$. Further, by definition of $\Omega$
we have that
$(c_{i}c_{j})^{\Omega}=c_{i}^{\Omega}\mathop{@_{\mathcal{E}}}\nolimits
c_{j}^{\Omega}\preccurlyeq x^{\Omega}$, so
$x^{\Omega}\models_{\mathcal{M}}\varphi\blacktriangleright\psi$.

This construction of a countermodel would fail in the analogous labelled
tableaux system for LGL (i.e., the layered graph logic with classical
additives [9]). We would require a systematic way to construct the internal
structure of each subgraph in the model, as the classical semantics for
$\blacktriangleright$ demands strict equality between the graph under
interpretation and the decomposition into layers. This issue is sidestepped
for ILGL since each time the tableaux rules require a decomposition of a
subgraph into layers we can move to a ‘fresh’ layered subgraph further down
the ordering. Thus we can safely turn each graph label into the simplest
instantiation of the kind of graph it represents: either a single vertex
(indecomposable) or two vertices and an edge (layered). A well-foundedness
condition on CSSs may make this method adaptable to LGL but we defer this
investigation to another occasion.

We now show how to construct a Hintikka CSS. We first require a listing of all
labelled formulae that may need to be added to the CSS in order to satisfy
properties $4$–$15$. We require a particularly strong condition on the listing
to make this procedure work: that every labelled formula appears infinitely
often to be tested.

[Fair strategy] A _fair strategy_ for a language $\mathcal{L}$ is a labelled
sequence of formulæ $(\mathbb{S}_{i}\varphi_{i}:x_{i})_{i\in\mathbb{N}}$ in
$\\{\mathbb{T},\mathbb{F}\\}\times\mathrm{Form}\times\mathbb{L}$ such that
$\\{i\in\mathbb{N}\mid\mathbb{S}_{i}\varphi_{i}:x_{i}\equiv\mathbb{S}\varphi:x\\}$
is infinite for any
$\mathbb{S}\varphi:x\in\\{\mathbb{T},\mathbb{F}\\}\times\mathrm{Form}\times\mathbb{L}$.
∎

######  Proposition 13 (cf. [15]).

There exists a fair strategy for the language of ILGL. ∎

Next we need the concept of an oracle. Here an oracle allows Hintikka sets to
be constructed inductively, testing the required consistency properties at
each stage.

[Oracle] Let $\mathcal{P}$ be a set of CSSs. (1) $\mathcal{P}$ is _$\subseteq$
-closed_ if $\textsc{css}{\mathcal{F}}{\mathcal{C}}\in\mathcal{P}$ holds
whenever
$\textsc{css}{\mathcal{F}}{\mathcal{C}}\subseteq\textsc{css}{\mathcal{F}^{\prime}}{\mathcal{C}^{\prime}}$
and $\textsc{css}{\mathcal{F}^{\prime}}{\mathcal{C}^{\prime}}\in\mathcal{P}$
holds. (2) $\mathcal{P}$ is of _finite character_ if
$\textsc{css}{\mathcal{F}}{\mathcal{C}}\in\mathcal{P}$ holds whenever
$\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}\in\mathcal{P}$ holds for every
$\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}\subseteq_{f}\textsc{css}{\mathcal{F}}{\mathcal{C}}$.
(3) $\mathcal{P}$ is _saturated_ if, for any
$\textsc{css}{\mathcal{F}}{\mathcal{C}}\in\mathcal{P}$ and any instance

$cond(\mathcal{F},\mathcal{C})$
$\textsc{css}{\mathcal{F}_{1}}{\mathcal{C}_{1}}\ \mid\ \ldots\ \mid\
\textsc{css}{\mathcal{F}_{k}}{\mathcal{C}_{k}}$

of a rule of Figure 10, if $cond(\mathcal{F},\mathcal{C})$ is fulfilled, then
$\textsc{css}{\mathcal{F}\cup\mathcal{F}_{i}}{\mathcal{C}\cup\mathcal{C}_{i}}\in\mathcal{P}$,
for at least one $i\in\\{1,\ldots,k\\}$. An _oracle_ is a set of open CSSs
which is $\subseteq$-closed, of finite character, and saturated. ∎

[Consistency] Let $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ be a CSS. We say
$\textsc{css}{\mathcal{F}}{\mathcal{C}}$ is _consistent_ if it is finite and
has no closed tableau. We say $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ is
_finitely consistent_ if every finite sub-CSS
$\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}$ is consistent. ∎

######  Proposition 14 (cf. [15]).

(1) Consistency is $\subseteq$-closed. (2) A finite CSS is consistent iff it
is finitely consistent. ∎

We denote the set of finitely consistent CSS by
$\mathcal{P}_{\mathrm{fincon}}$.

######  Lemma 15.

$\mathcal{P}_{\mathrm{fincon}}$ is an oracle.

######  Proof 3.5.

For $\subseteq$-closure and finite character see [15]. For saturation we show
the case
$\langle\mathbb{T}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\rangle$:
the rest are similar.

Let $\textsc{css}{\mathcal{F}}{\mathcal{C}}\in\mathcal{P}_{\mathrm{fincon}}$,
$\mathbb{T}\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi:x\in\mathcal{F}$
and $x\preccurlyeq y,yz\preccurlyeq yz\in\overline{\mathcal{C}}$. Suppose
neither
$\textsc{css}{\mathcal{F}\cup\\{\mathbb{F}\varphi:z\\}}{\mathcal{C}}\in\mathcal{P}_{\mathrm{fincon}}$
nor
$\textsc{css}{\mathcal{F}\cup\\{\mathbb{T}\psi:yz\\}}{\mathcal{C}}\in\mathcal{P}_{\mathrm{fincon}}$.
Then there exist
$\textsc{css}{\mathcal{F}^{A}_{f}}{\mathcal{C}^{A}_{f}}\subseteq_{f}\textsc{css}{\mathcal{F}\cup\\{\mathbb{F}\varphi:z\\}}{\mathcal{C}}$
and
$\textsc{css}{\mathcal{F}^{B}_{f}}{\mathcal{C}^{B}_{f}}\subseteq_{f}\textsc{css}{\mathcal{F}\cup\\{\mathbb{T}\psi:yz\\}}{\mathcal{C}}$
that are inconsistent. By compactness (Lemma 4), there exist finite
$\mathcal{C}_{0},\mathcal{C}_{1}\subseteq\mathcal{C}$ such that $z\preccurlyeq
z\in\mathcal{C}_{0}$ and $yz\preccurlyeq yz\in\mathcal{C}_{1}$. Thus we define
$\mathcal{F}^{\prime}_{f}=(\mathcal{F}^{A}_{f}\setminus\\{\mathbb{F}\varphi:z\\})\cup(\mathcal{F}^{B}_{f}\setminus\\{\mathbb{T}\psi:yz\\})\cup\\{\mathbb{T}\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi:x\\}$
and
$\mathcal{C}^{\prime}_{f}=\mathcal{C}^{A}_{f}\cup\mathcal{C}^{B}_{f}\cup\mathcal{C}_{0}\cup\mathcal{C}_{1}$.
Then $\textsc{css}{\mathcal{F}^{\prime}_{f}}{\mathcal{C}^{\prime}_{f}}$ is a
finite CSS and
$[\textsc{css}{\mathcal{F}^{\prime}_{f}\cup\\{\mathbb{F}\varphi:z\\}}{\mathcal{C}^{\prime}_{f}};\textsc{css}{\mathcal{F}^{\prime}_{f}\cup\\{\mathbb{T}\psi:yz\\}}{\mathcal{C}^{\prime}_{f}}]$
is a tableau for it. We have
$\textsc{css}{\mathcal{F}^{A}_{f}}{\mathcal{C}^{A}_{f}}\subseteq_{f}\textsc{css}{\mathcal{F}^{\prime}_{f}\cup\\{\mathbb{F}\varphi:z\\}}{\mathcal{C}^{\prime}_{f}}$
and
$\textsc{css}{\mathcal{F}^{B}_{f}}{\mathcal{C}^{B}_{f}}\subseteq_{f}\textsc{css}{\mathcal{F}^{\prime}_{f}\cup\\{\mathbb{T}\psi:yz\\}}{\mathcal{C}^{\prime}_{f}}$
so by $\subseteq$-closure of consistency
$\textsc{css}{\mathcal{F}^{A}_{f}}{\mathcal{C}^{A}_{f}}$ and
$\textsc{css}{\mathcal{F}^{B}_{f}}{\mathcal{C}^{B}_{f}}$ are inconsistent:
respectively let $\mathcal{T}_{A}$ and $\mathcal{T}_{B}$ be closed tableaux
for them. Then $\mathcal{T}_{A}\oplus\mathcal{T}_{B}$ is a closed tableau for
$\textsc{css}{\mathcal{F}^{\prime}_{f}}{\mathcal{C}^{\prime}_{f}}$ and the CSS
is inconsistent: contradicting
$\textsc{css}{\mathcal{F}^{\prime}_{f}}{\mathcal{C}^{\prime}_{f}}\subseteq_{f}\textsc{css}{\mathcal{F}}{\mathcal{C}}\in\mathcal{P}_{\mathrm{fincon}}$.

We can now show completeness of our tableaux system. Consider a formula
$\varphi$ for which there exists no closed tableau. We show there is a
countermodel to $\varphi$. We start with the initial tableau $\mathcal{T}_{0}$
for $\varphi$. Then, we have (1)
$\mathcal{T}_{0}=[\textsc{css}{\\{\mathbb{F}\varphi:c_{0}\\}}{\\{c_{0}\preccurlyeq
c_{0})\\}}]$ and (2) $\mathcal{T}_{0}$ cannot be closed. By Proposition 13,
there exists a fair strategy, which we denote by $\mathcal{S}$, with
$\mathbb{S}_{i}\varphi_{i}:x_{i}$ the $i^{\text{th}}$ formula of
$\mathcal{S}$. As $\mathcal{T}_{0}$ cannot be closed,
$\textsc{css}{\\{\mathbb{F}\varphi:c_{0}\\}}{\\{c_{0}\preccurlyeq
c_{0}\\}}\in\mathcal{P}_{\mathrm{fincon}}$. We build a sequence
$\textsc{css}{\mathcal{F}_{i}}{\mathcal{C}_{i}}_{i\geqslant 0}$ as follows:

  * -

$\textsc{css}{\mathcal{F}_{0}}{\mathcal{C}_{0}}=\textsc{css}{\\{\mathbb{F}\varphi:c_{0}\\}}{\\{c_{0}\preccurlyeq
c_{0}\\}}$;

  * -

if
$\textsc{css}{\mathcal{F}_{i}\cup\\{\mathbb{S}_{i}\varphi_{i}:x_{i}\\}}{\mathcal{C}_{i}}\not\in\mathcal{P}_{\mathrm{fincon}}$,
then we have
$\textsc{css}{\mathcal{F}_{i+1}}{\mathcal{C}_{i+1}}=\textsc{css}{\mathcal{F}_{i}}{\mathcal{C}_{i}}$;
and

  * -

if
$\textsc{css}{\mathcal{F}_{i}\cup\\{\mathbb{S}_{i}\varphi_{i}:x_{i}\\}}{\mathcal{C}_{i}}\in\mathcal{P}_{\mathrm{fincon}}$,
then we have
$\textsc{css}{\mathcal{F}_{i+1}}{\mathcal{C}_{i+1}}=\textsc{css}{\mathcal{F}_{i}\cup\\{\mathbb{S}_{i}\varphi_{i}:x_{i}\\}\cup
F_{e}}{\mathcal{C}_{i}\cup\mathcal{C}_{e}}$ where $F_{e}$ and
$\mathcal{C}_{e}$ are determined by

$\mathbb{S}_{i}$ | $\varphi_{i}$ | $F_{e}$ | $\mathcal{C}_{e}$
---|---|---|---
$\mathbb{F}$ | $\varphi\rightarrow\psi$ | $\\{\mathbb{T}\varphi:c_{\mathfrak{I}+1},\mathbb{F}\psi:c_{\mathfrak{I}+1}\\}$ | $\\{x_{i}\preccurlyeq c_{\mathfrak{I}+1}\\}$
$\mathbb{T}$ | $\varphi\blacktriangleright\psi$ | $\\{\mathbb{T}\varphi:c_{\mathfrak{I}+1},\mathbb{T}\psi:c_{\mathfrak{I}+2}\\}$ | $\\{c_{\mathfrak{I}+1}c_{\mathfrak{I}+2}\preccurlyeq x_{i}\\}$
$\mathbb{F}$ | $\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi$ | $\\{\mathbb{T}\varphi:c_{\mathfrak{I}+2},\mathbb{F}\psi:c_{\mathfrak{I}+1}c_{\mathfrak{I}+2}\\}$ | $\\{x_{i}\preccurlyeq c_{\mathfrak{I}+1},c_{\mathfrak{I}+1}c_{\mathfrak{I}+2}\preccurlyeq c_{\mathfrak{I}+1}c_{\mathfrak{I}+2}\\}$
$\mathbb{F}$ | $\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\psi$ | $\\{\mathbb{T}\varphi:c_{\mathfrak{I}+2},\mathbb{F}\psi:c_{\mathfrak{I}+2}c_{\mathfrak{I}+1}\\}$ | $\\{x_{i}\preccurlyeq c_{\mathfrak{I}+1},c_{\mathfrak{I}+2}c_{\mathfrak{I}+1}\preccurlyeq c_{\mathfrak{I}+2}c_{\mathfrak{I}+1}\\}$
Otherwise | $\emptyset$ | $\emptyset$

with $\mathfrak{I}=\text{max}\\{j\mid
c_{j}\in\mathcal{A}(\mathcal{C}_{i})\cup\mathcal{S}(x_{i})\\}$.

######  Proposition 16.

For any $i\in\mathbb{N}$, the following properties hold: (1)
$\mathcal{F}_{i}\subseteq\mathcal{F}_{i+1}$ and
$\mathcal{C}_{i}\subseteq\mathcal{C}_{i+1}$; (2)
$\textsc{css}{\mathcal{F}_{i}}{\mathcal{C}_{i}}\in\mathcal{P}_{\mathrm{fincon}}$.

######  Proof 3.6.

Only 2 is non-trivial. and we prove it by induction on $i$. The base case
$i=0$ is given by our initial assumption. Now for the inductive hypothesis
(IH) we have that
$\textsc{css}{\mathcal{F}_{i}}{\mathcal{C}_{i}}\in\mathcal{P}_{\mathrm{fincon}}$.
Then the inductive step is an immediate consequence of Lemma 15 for the non-
trivial cases.

We now define the limit
$\textsc{css}{\mathcal{F}_{\infty}}{\mathcal{C}_{\infty}}=\textsc{css}{\bigcup_{i\geqslant
0}\mathcal{F}_{i}}{\bigcup_{i\geqslant 0}\mathcal{C}_{i}}$ of the sequence
$\textsc{css}{\mathcal{F}_{i}}{\mathcal{C}_{i}}_{i\geqslant 0}$.

######  Proposition 17.

The following properties hold: (1)
$\textsc{css}{\mathcal{F}_{\infty}}{\mathcal{C}_{\infty}}\in\mathcal{P}_{\mathrm{fincon}}$;
(2) For all labelled formulae $\mathbb{S}\varphi:x$, if
$\textsc{css}{\mathcal{F}_{\infty}\cup\\{\mathbb{S}\varphi:x\\}}{\mathcal{C}_{\infty}}\in\mathcal{P}_{\mathrm{fincon}}$,
then $\mathbb{S}\varphi:x\in\mathcal{F}_{\infty}$.

######  Proof 3.7.

  1. (1)

First note that $\textsc{css}{\mathcal{F}_{\infty}}{\mathcal{C}_{\infty}}$ is
a CSS since each stage of construction satisfies (Ref) and by our choice of
constants throughout the construction (Contra) and (Freshness) are satisfied.
Further, it is open since otherwise there would be some stage
$\textsc{css}{\mathcal{F}_{k}}{\mathcal{C}_{k}}$ at which the offending
closure condition is satisfied, which would contradict that each
$\textsc{css}{\mathcal{F}_{i}}{\mathcal{C}_{i}}$ is consistent. Now let
$\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}\subseteq_{f}\textsc{css}{\mathcal{F}_{\infty}}{\mathcal{C}_{\infty}}$.
Then there exists $k\in\mathbb{N}$ such that
$\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}\subseteq_{f}\textsc{css}{\mathcal{F}_{k}}{\mathcal{C}_{k}}$.
By Proposition 16
$\textsc{css}{\mathcal{F}_{k}}{\mathcal{C}_{k}}\in\mathcal{P}_{\mathrm{fincon}}$
so it follows
$\textsc{css}{\mathcal{F}_{f}}{\mathcal{C}_{f}}\in\mathcal{P}_{\mathrm{fincon}}$.
As $\mathcal{P}_{\mathrm{fincon}}$ is of finite character, we thus have
$\textsc{css}{\mathcal{F}_{\infty}}{\mathcal{C}_{\infty}}\in\mathcal{P}_{\mathrm{fincon}}$.

  2. (2)

First note that
$\textsc{css}{\mathcal{F}_{\infty}\cup\\{\mathbb{S}\varphi:x\\}}{\mathcal{C}_{\infty}}$
is a CSS so (Contra) and (Freshness) are satisfied when the label $x$ is
introduced. By compactness, there exists finite
$\mathcal{C}_{0}\subseteq\mathcal{C}_{\infty}$ such that $x\preccurlyeq
x\in\overline{\mathcal{C}_{0}}$. As it is finite, there exists
$k\in\mathbb{N}$ such that $\mathcal{C}_{0}\subseteq\mathcal{C}_{k}$ and by
fairness there exists $l\geq k$ such that
$\mathbb{S}_{l}\varphi_{l}:x_{l}\equiv\mathbb{S}\varphi:x$. Since (Freshness)
and (Contra) are fufilled with respect to $\mathcal{F}_{\infty}$ they are also
fulfilled with respect to $\mathcal{F}_{l}\cup\\{\mathbb{S}\varphi:x\\}$ so
$\textsc{css}{\mathcal{F}_{l+1}}{\mathcal{C}_{l+1}}=\textsc{css}{\mathcal{F}_{l}\cup\\{\mathbb{S}\varphi:x\\}}{\mathcal{C}_{l}}\in\mathcal{P}_{\mathrm{fincon}}$
and
$\textsc{css}{\mathcal{F}_{l+1}}{\mathcal{C}_{l+1}}=\textsc{css}{\mathcal{F}_{l}\cup\\{\mathbb{S}\varphi:x\\}\cup\mathcal{F}_{e}}{\mathcal{C}_{l}\cup\mathcal{C}_{e}}$.
Hence $\mathbb{S}\varphi:x\in\mathcal{F}_{\infty}$.

######  Lemma 18.

The limit CSS is a Hintikka CSS.

######  Proof 3.8.

For properties $(1)-(3)$ we have that
$\textsc{css}{\mathcal{F}_{\infty}}{\mathcal{C}_{\infty}}$ is open. For the
other conditions, the saturation property of the oracle
$\mathcal{P}_{\mathrm{fincon}}$ and Proposition 17 item 2. suffice.

We immediately obtain completeness.

######  Theorem 19 (Completeness).

If $\varphi$ is valid, then there exists a closed tableau for $\varphi$. ∎

##  4\. Decidability

In this section, we prove the decidability of ILGL. Given the infinite
behaviour of the countermodel extraction procedure, we do not do so by means
of a tableaux termination argument. Instead, we define a semantics on a class
of algebras that we prove equivalent to the layered graph semantics by means
of a representation theorem. By proving the finite embeddability property
holds for this class of algebras, we obtain the finite model property and thus
decidability of validity for the layered graph semantics. We are able to
extend the representation theorem to a full topological duality, and do so in
Section 5.

###  4.1. Algebraic and Relational Semantics

We begin by defining algebraic structures appropriate for interpreting ILGL.
As one might be expected, these are obtained by replacing the Boolean algebra
base of the _layered algebras_ that act as LGL’s algebraic semantics with a
Heyting algebra in order to soundly interpret the propositional intuitionistic
logic fragment of ILGL.

[Layered Heyting algebra] A _layered Heyting algebra_ is a structure
$\mathbb{A}=(A,\wedge,\vee,\rightarrow,\bot,\top,\blacktriangleright,\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright},\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-})$
such that $(A,\wedge,\vee,\rightarrow,\bot,\top)$ is a Heyting algebra and
$\blacktriangleright$,
$\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}$, and
$\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}$ are binary
operations on $A$ satisfying $a\blacktriangleright b\leq c\text{ iff }a\leq
b\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}c\text{ iff }b\leq
a\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}c.$ ∎

We can derive some simple but useful properties about the residuated groupoid
structure of a layered Heyting algebra.

######  Proposition 20 (cf. [30]).

Let $\mathbb{A}$ be a layered Heyting algebra. Then, for all
$a,b,a^{\prime},b^{\prime}\in A$ and $X,Y\subseteq A$, we have

  1. (1)

If $a\leq a^{\prime}$ and $b\leq b^{\prime}$ then $a\blacktriangleright b\leq
a^{\prime}\blacktriangleright b^{\prime}$;

  2. (2)

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

  3. (3)

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

  4. (4)

If $\bigvee X$ exists then for any $z\in A$: $\bigwedge_{x\in
X}x\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}z$ and
$\bigwedge_{x\in
X}x\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}z$ exist with
$\bigwedge_{x\in
X}x\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}z=\bigvee
X\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}z$ and $\bigwedge_{x\in
X}x\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}z=\bigvee
X\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}z$

  5. (5)

If $\bigwedge X$ exists then for any $z\in A$ $\bigwedge_{x\in
X}z\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}x$ and
$\bigwedge_{x\in
X}z\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}x$ exist with
$\bigwedge_{x\in
X}z\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}x=z\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\bigwedge
X$ and $\bigwedge_{x\in
X}z\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}x=z\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\bigwedge
X$;

  6. (6)

$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\top=a\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\top=\bot\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}a=\bot\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}a=\top$.
∎

We interpret ILGL on layered Heyting algebras as follows. A valuation
$\mathcal{V}:\mathrm{Prop}\rightarrow\mathbb{A}$ on a layered Heyting algebra
$\mathbb{A}$, is uniquely extended to an interpretation
$\llbracket-\rrbracket$ as follows:
$\llbracket\mathrm{p}\rrbracket=\mathcal{V}(\mathrm{p})$,
$\llbracket\top\rrbracket=\top$, $\llbracket\bot\rrbracket=\bot$,
$\llbracket\varphi\circ\psi\rrbracket=\llbracket\varphi\rrbracket\circ\llbracket\psi\rrbracket$
for
$\circ\in\\{\land,\lor,\rightarrow,\blacktriangleright,\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright},\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\\}$.
An algebra $\mathbb{A}$ and an interpretation $\llbracket-\rrbracket$
_satisfies_ $\varphi$ if $\llbracket\varphi\rrbracket=\top$. Correspondingly,
$\varphi$ is _valid_ if it is satisfied by every algebra $\mathbb{A}$ and
interpretation $\llbracket-\rrbracket$.

We obtain soundness and completeness for this semantics with respect to the
Hilbert-type system $\mathrm{ILGL}_{\mathrm{H}}$ of Fig 5 by forming a
Lindenbaum-Tarski algebra from it, utilising precisely the same argument as
that given for LGL.

######  Theorem 21 (Algebraic Soundness & Completeness (cf. [9])).

For all formulae $\varphi$ and $\psi$ of ILGL, $\varphi\vdash\psi$ is provable
in $\mathrm{ILGL}_{\mathrm{H}}$ iff, for all algebraic interpretations
$\llbracket-\rrbracket$,
$\llbracket\varphi\rrbracket\leq\llbracket\psi\rrbracket$.∎

We now define relational structures appropriate to interpret ILGL. These are
simple extensions of the frames that interpret propositional intuitionistic
logic.

[Intuitionistic Layered Frame] An _intuitionistic layered frame_ is a triple
$\mathcal{F}=(X,\preccurlyeq,R)$ where $(X,\preccurlyeq)$ is a preorder and
$R$ a ternary relation over $X$. ∎

This is an obvious generalization of ordered scaffold. By defining $R(G,H,K)$
iff $G\mathop{@_{\mathcal{E}}}\nolimits H\downarrow$ and
$G\mathop{@_{\mathcal{E}}}\nolimits H=K$ we obtain an intuitionistic layered
frame from an ordered scaffold. An alternative frame semantics can be derived
from recent independent work by Galatos & Jipsen [20]. There, algebras called
_generalized bunched implication algebras_ are investigated. These algebras
can be seen as layered Heyting algebras for which $\blacktriangleright$ is
associative and has an associated unit. Such algebras, together with sequent
calculus presentations of substructural logics, motivate the definition of
_distributive residuated frames_ which provide an alternative semantics to BI-
like logics. Similar structures can be defined for ILGL, though we do not
pursue that here.

As with the semantics on scaffolds, we require a valuation on an
intuitionistic layered frame to be persistent with respect to the preorder
$\preccurlyeq$. An intuitionistic layered frame $\mathcal{F}$ together with a
persistent valuation $\mathcal{V}$ is a _relational model_ $\mathcal{M}$ of
ILGL, with a satisfaction relation $\vDash_{\mathcal{M}}$ defined analogously
to that of layered graph models in Figure 12.

$x$ $\vDash_{\mathcal{M}}$ $\mathrm{p}$ iff $x\in\mathcal{V}(\mathrm{p})$ $x$
$\vDash_{\mathcal{M}}$ $\top$ $x\not\vDash_{\mathcal{M}}\bot$ $x$
$\vDash_{\mathcal{M}}$ $\varphi\land\psi$ iff $x\vDash_{\mathcal{M}}\varphi$
and $x\vDash_{\mathcal{M}}\psi$ $x$ $\vDash_{\mathcal{M}}$ $\varphi\lor\psi$
iff $x\vDash_{\mathcal{M}}\varphi$ or $x\vDash_{\mathcal{M}}\psi$ $x$
$\vDash_{\mathcal{M}}$ $\varphi\rightarrow\psi$ iff for all $y\succcurlyeq x$,
$y\vDash_{\mathcal{M}}\varphi$ implies $y$ $\vDash_{\mathcal{M}}$ $\psi$ $x$
$\vDash_{\mathcal{M}}$ $\varphi\blacktriangleright\psi$ iff there exists
$x^{\prime},y,z$ s.t. $x\succcurlyeq x^{\prime}$, $Ryzx^{\prime}$,
$y\vDash_{\mathcal{M}}\varphi$ and $z\vDash_{\mathcal{M}}\psi$ $x$
$\vDash_{\mathcal{M}}$
$\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi$ iff for
all $x^{\prime},y,z$: $x^{\prime}\succcurlyeq x,Rx^{\prime}yz$ and
$y\vDash_{\mathcal{M}}\varphi$ implies $z\vDash_{\mathcal{M}}\psi$ $x$
$\vDash_{\mathcal{M}}$
$\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\psi$ iff for
all $x^{\prime},y,z$: $x^{\prime}\succcurlyeq x,Ryx^{\prime}z$ and
$y\vDash_{\mathcal{M}}\varphi$ implies $z\vDash_{\mathcal{M}}\psi$

Figure 12. Satisfaction for relational models of ILGL.

We can define a new notion of realization for our labelled tableaux system to
give soundness and completeness for the relational semantics.

[Relational Realization] Let $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ be a
CSS. A _relational realization_ of $\textsc{css}{\mathcal{F}}{\mathcal{C}}$ is
a triple $\mathfrak{R}=(\mathcal{F},\mathcal{V},\lfloor.\rfloor)$ where
$\mathcal{M}=(\mathcal{F},\mathcal{V})$ is a relational model and
$\lfloor.\rfloor:\mathcal{D}(\mathcal{C})\rightarrow X$ is such that (1) For
all $x\in\mathcal{D}(\mathcal{C})$, if $x=c_{i}c_{j}$, then $R\lfloor
c_{i}\rfloor\lfloor c_{j}\rfloor\lfloor c_{i}c_{j}\rfloor$; (2) If
$x\preccurlyeq y\in\mathcal{C}$, then $\lfloor
x\rfloor\preccurlyeq_{\mathcal{M}}\lfloor y\rfloor$; (3) If
$\mathbb{T}\varphi:x\in\mathcal{F}$, then $\lfloor
x\rfloor\models_{\mathcal{M}}\varphi$; and (4) If
$\mathbb{F}\varphi:x\in\mathcal{F}$, then $\lfloor
x\rfloor\not\models_{\mathcal{M}}\varphi$. ∎

Precisely the same argument as that given in Section 3 gives that the labelled
tableaux system is sound for the relational semantics. Noting that we can
transform a layered graph model into an intuitionistic layered frame with an
equivalent satisfaction relation, we also have completeness by transforming
the layered graph countermodels. As the labelled tableaux is sound and
complete for both the layered graph semantics and the relational semantics, we
obtain their equivalence.

######  Theorem 22 (Relational Soundness & Completeness).

  1. (1)

For all formulae $\varphi$ of ILGL, $\varphi$ is valid in the relational
semantics iff there exists a closed tableau for $\varphi$.

  2. (2)

For all formulae $\varphi$ of ILGL, $\varphi$ is valid in the relational
semantics iff $\varphi$ is valid in the layered graph semantics. ∎

We also define a notion of morphism for intuitionistic layered frames,
yielding a category $\mathrm{IntLayFr}$. This will be important for Section
5’s duality theorem and the extension to predicate ILGL in Section 6.

[Intuitionistic Layered P-Morphism] An _intuitionistic layered p-morphism_ is
a map $f:X\rightarrow X^{\prime}$ between intuitionistic layered frames
$\mathcal{F}=(X,\preccurlyeq,R)$ and
$\mathcal{F}^{\prime}=(X^{\prime},\preccurlyeq^{\prime},R^{\prime})$
satisfying the following conditions:

  1. (1)

$f$ is order preserving;

  2. (2)

If $f(x)\preccurlyeq y^{\prime}$ then there exists $y$ such that
$x\preccurlyeq y$ and $f(y)=y^{\prime}$;

  3. (3)

If $Rxyz$ then $R^{\prime}f(x)f(y)f(z)$;

  4. (4)

If $w^{\prime}\preccurlyeq^{\prime}f(x)$ and
$R^{\prime}y^{\prime}z^{\prime}w^{\prime}$ then there exists $w,y,z$ such that
$w\preccurlyeq x$ and $Ryzw$ with $y^{\prime}\preccurlyeq^{\prime}f(y)$ and
$z^{\prime}\preccurlyeq^{\prime}f(z)$;

  5. (5)

If $f(x)\preccurlyeq^{\prime}w^{\prime}$ and
$R^{\prime}w^{\prime}y^{\prime}z^{\prime}$ then there exists $w,y,z$ such that
$x\preccurlyeq w$ and $Rwyz$ with $y^{\prime}\preccurlyeq^{\prime}f(y)$ and
$f(z)\preccurlyeq^{\prime}z^{\prime}$;

  6. (6)

If $f(x)\preccurlyeq^{\prime}w^{\prime}$ and
$R^{\prime}y^{\prime}w^{\prime}z^{\prime}$ then there exists $w,y,z$ such that
$x\preccurlyeq w$ and $Rywz$ with $y^{\prime}\preccurlyeq f(y)$ and
$f(z)\preccurlyeq z^{\prime}$. ∎

###  4.2. Equivalence of Semantics

We now show that the algebraic and relational semantics are equivalent. This
means we can prove properties of the layered graph semantics algebraically and
yields the equivalence of the Hilbert and labelled tableaux systems. We begin
by lifting the semantic clauses of the relational semantics to operations on
the upward-closed subsets of the frame.

[Complex Algebra] Given an intuitionistic layered frame $\mathcal{X}$, the
_complex algebra_ of $\mathcal{X}$ is given by
$Com(\mathcal{X})=(\mathcal{P}_{\preccurlyeq}(X),\cap,\cup,\Rightarrow,X,\emptyset,\blacktriangleright_{R},\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R},\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{R})$,
where

$\displaystyle\begin{array}[b]{cl}\mathcal{P}_{\preccurlyeq}(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^{\prime}\text{ and
}x^{\prime}\in A\text{ then }x^{\prime}\in B\\}\\\
A\blacktriangleright_{R}B&=\\{x\mid\text{there exists }w,y,z\text{ s.t
}w\preccurlyeq x,Ryzw,y\in A\text{ and }z\in B\\}\\\
A\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R}B&=\\{x\mid\text{for
all }w,y,z,\text{ if }x\preccurlyeq w,Rwyz\text{ and }y\in A\text{ then }z\in
B\\}\\\
A\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{R}B&=\\{x\mid\text{for
all }w,y,z,\text{ if }x\preccurlyeq w,Rywz\text{ and }y\in A\text{ then }z\in
B\\}.\end{array}$ ∎

It is standard that the
$(\mathcal{P}_{\preccurlyeq}(X),\cap,\cup,\Rightarrow,X,\emptyset)$-fragment
of this structure is a Heyting algebra. That $\blacktriangleright_{R}$,
$\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R}$ and
$\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{R}$ satisfy the
residuation property can also easily be verified. We therefore have that
complex algebras are layered Heyting algebras.

######  Lemma 23.

Given an intuitionistic layered frame $\mathcal{X}$ the complex algebra
$Com(\mathcal{X})$ is a layered Heyting algebra. ∎

A persistent valuation $\mathcal{V}:\mathrm{Prop}\rightarrow\mathcal{P}(X)$ on
an intuitionistic layered frame $\mathcal{X}$ automatically generates an
interpretation $\llbracket-\rrbracket_{\mathcal{V}}$ on its complex algebra
$Com(\mathcal{X})$. An inductive argument shows that satisfaction coincides in
both structures.

######  Lemma 24.

Given a relational model $\mathcal{M}=(\mathcal{X},\mathcal{V})$, for all
$x\in X$ and all formulae $\varphi$ of ILGL,
$x\in\llbracket\varphi\rrbracket_{\mathcal{V}}$ iff
$x\vDash_{\mathcal{M}}\varphi$. ∎

Conversely, we can generate a frame from any layered Heyting algebra. We first
recall some definitions.

For a bounded distributive lattice $\mathbb{A}$, a _filter_ is a subset
$F\subseteq\mathbb{A}$ satisfying, for all $a,b\in\mathbb{A}$: i) if $a\in F$
and $a\leq b$ then $b\in F$; and ii) if $a,b\in F$ then $a\land b\in F$. It is
_proper_ if $F\neq\mathbb{A}$. By upwards-closure this condition is equivalent
to $\bot\not\in F$. A _prime filter_ is a proper filter additionally
satisfying, for all $a,b\in\mathbb{A}$, if $a\lor b\in F$ then $a\in F$ or
$b\in F$. For a set $X\subseteq\mathbb{A}$ we define $[X)=\\{a\mid\text{there
exists }b_{1},\ldots,b_{n}\in X\text{ such that }b_{1}\land\cdots\land
b_{n}\leq a\\}$. It can be shown that this defines the least filter containing
$X$. For $X=\\{a\\}$ we simply write $[a)$, and for $X=Y\cup\\{a\\}$ we write
$[Y,a)$.

An _ideal_ is the dual notion of a filter. Analogous definitions for proper
and prime ideals can be obtained by switching $\land$ and $\lor$ and reversing
the order in the above definitions. We also obtain the dual notation $(X]$ for
least ideal containing $X$.

Importantly, given a prime ideal $P$, the complement
$\overline{P}=\\{a\in\mathbb{A}\mid a\not\in P\\}$ is a prime filter (and vice
versa). A (prime) filter/ideal of a layered Heyting algebra is simply a
(prime) filter/ideal of the underlying bounded distributive lattice.

[Prime Filter Frame] Given a layered Heyting algebra $\mathbb{A}$, the _prime
filter frame_ $Pr(\mathbb{A})$ is defined
$Pr(\mathbb{A})=(Pr(A),\subseteq,R_{Pr(\mathbb{A})})$ where $Pr(A)$ is the set
of prime filters of $\mathbb{A}$ and $R_{Pr(\mathbb{A})}$ is given by
$R_{Pr(\mathbb{A})}F_{0}F_{1}F_{2}\text{ iff for all }a\in F_{0}\text{ and all
}b\in F_{1},a\blacktriangleright b\in F_{2}.$ ∎

We can prove the satisfaction on a layered Heyting algebra and its prime
filter frame coincides. To show this we first prove a representation theorem
for layered Heyting algebras. This is an analogue of the Stone representation
theorem for Boolean algebras [43] that shows that every Boolean algebra is
isomorphic to a field of sets. Specifically, it extends the representation
theorem for Heyting algebras [17].

######  Theorem 25 (Representation Theorem for Layered Heyting Algebras).

Every layered Heyting algebra is isomorphic to a subalgebra of a complex
algebra. Specifically, the map $h_{\mathbb{A}}(a):\mathbb{A}\rightarrow
Com(Pr(\mathbb{A}))$ defined $h_{\mathbb{A}}(a)=\\{F\in Pr(A)\mid a\in F\\}$
is an embedding.

######  Proof 4.1.

That $h_{\mathbb{A}}$ is injective and respects the Heyting algebra operations
is simply the representation theorem for Heyting algebras. We must therefore
verify $h_{\mathbb{A}}$ also respects the residuated structure. We attend to
$\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}$, leaving the similar
$\blacktriangleright$ and
$\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}$ cases to the
reader.

First suppose $a=\bot$. Then by Proposition 20,
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b=\top$. We have that
$h_{\mathbb{A}}(a)\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R_{Pr(\mathbb{A})}}h_{\mathbb{A}}(b)=Pr(A)$
since the defining condition of
$\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R_{Pr(\mathbb{A})}}$
is vacuously true ($h_{\mathbb{A}}(a)=\emptyset$), so every prime filter is
trivially a member of
$h_{\mathbb{A}}(a)\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R_{Pr(\mathbb{A})}}h(b)$.
Thus
$h_{\mathbb{A}}(a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b)=h_{\mathbb{A}}(a)\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R_{Pr(\mathbb{A})}}h_{\mathbb{A}}(b)$
as required. The case $b=\top$ is similar.

We divide the case where both $a\neq\bot$ and $b\neq\top$ into two subcases:
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\neq\bot$ and
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b=\bot$. First
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\neq\bot$. The left-
to-right direction is easy: suppose
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\in F$. Then for any
$F_{0}\supseteq F$ we have
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\in F_{0}$. Suppose
for such a $F_{0}$ we have $R_{pr}F_{0}F_{1}F_{2}$ and $F_{1}\in
h_{\mathbb{A}}(a)$. Then
$(a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b)\blacktriangleright
a\in F_{2}$. We have
$(a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b)\blacktriangleright
a\leq b$, so by filterhood $b\in F_{2}$. Thus $F\in
h_{\mathbb{A}}(a)\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R_{Pr(\mathbb{A})}}h_{\mathbb{A}}(b)$.

The other direction is more involved. Suppose we have $F_{0}\in
h_{\mathbb{A}}(a)\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R_{Pr(\mathbb{A})}}h_{\mathbb{A}}(b)$
and for contradiction
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\not\in F_{0}$. We
claim this entails the existence of $F_{1},F_{2}$ such that
$R_{pr}F_{0}F_{1}F_{2}$ and $F_{1}\in h_{\mathbb{A}}(a)$ but $F_{2}\not\in
h_{\mathbb{A}}(b)$. Since $a\neq\bot$ and $b\neq\top$ we have a proper filter
$[a)$ and a proper ideal $(b]$ such that, for all $x\in F_{0}$ and all
$y\in[a)$ we have $x\blacktriangleright y\not\in(b]$: if there existed $x$ and
$y$ contradicting this statement then $x\blacktriangleright a\leq
x\blacktriangleright y\leq b$, so by residuation $x\leq
a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b$ and
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\in F_{0}$,
contradicting our assumption. Hence we define $E=\\{\langle F,I\rangle\mid
F\text{ is a proper filter},I\text{ is a proper ideal},a\in F,b\in I\text{ and
for all }x\in F_{0},y\in F:x\blacktriangleright y\not\in I\\}$. $E$ is non-
empty. Further, when ordered by component-wise inclusion, every chain in $E$
has a maximum given by taking the union of each component of the chain. Hence,
by Zorn’s lemma, $E$ has a maximum $\langle F^{max},I^{max}\rangle$. We claim
$F^{max}$ is a prime filter and $I^{max}$ is a prime ideal.

We prove that $I^{max}$ is a prime ideal; the case for $F^{max}$ is similar.
Suppose $x\land y\in I^{max}$ but $x,y\not\in I^{max}$. Then we have proper
ideals $(I^{max},x],(I^{max},y]\supset I^{max}$. $\langle
F^{max},(I^{max},x]\rangle$ and $\langle F^{max},(I^{max},y]\rangle$ can only
fail to be maximal in $E$ if there exist $a_{0},a^{\prime}_{0}\in F_{0}$ and
$a_{1},a^{\prime}_{1}\in F^{max}$ such that $a_{0}\blacktriangleright
a_{1}\in(I^{max},x]$ and $a^{\prime}_{0}\blacktriangleright
a^{\prime}_{1}\in(I^{max},y]$. There then exist $c,c^{\prime}\in I^{max}$ such
that $a_{0}\blacktriangleright a_{1}\leq x\lor c$ and
$a^{\prime}_{0}\blacktriangleright a^{\prime}_{1}\leq y\lor c^{\prime}$. Set
$a^{\prime\prime}=a_{1}\land a^{\prime}_{1}$ and $c^{\prime\prime}=c\lor
c^{\prime}$. Then $a^{\prime\prime}\in F^{max}$ and $c^{\prime\prime}\in
I^{max}$. By monotonicity of $\blacktriangleright$ we have
$a_{0}\blacktriangleright a^{\prime\prime}\leq c^{\prime\prime}\lor x$ and
$a^{\prime}_{0}\blacktriangleright a^{\prime\prime}\leq c^{\prime\prime}\lor
y$. Hence, by residuation and filterhood of $F_{0}$, we have
$(a^{\prime\prime}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}(c^{\prime\prime}\lor
x))\land(a^{\prime\prime}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}(c^{\prime\prime}\lor
y))\in F_{0}$. Now $\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}$
distributes over $\land$ in its right argument so we have
$a^{\prime\prime}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}(c^{\prime\prime}\lor(x\land
y))\in F_{0}$. Hence
$(a^{\prime\prime}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}(c^{\prime\prime}\lor(x\land
y)))\blacktriangleright a^{\prime\prime}\not\in I^{max}$. Since $I^{max}$ is
downwards-closed and
$(a^{\prime\prime}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}(c^{\prime\prime}\lor(x\land
y)))\blacktriangleright a^{\prime\prime}\leq(c^{\prime\prime}\lor(x\land y))$
we have that $c^{\prime\prime}\lor(x\land y)\not\in I^{max}$. However, by
assumption, $c^{\prime\prime},x\land y\in I^{max}$, hence
$c^{\prime\prime}\lor(x\land y)\in I^{max}$ : contradiction. It follows that
$x\in I^{max}$ or $y\in I^{max}$ and $I^{max}$ is prime.

Take $F_{1}=F^{max}$ and $F_{2}=\overline{I^{max}}$. Then $F_{0}\subseteq
F_{0}$, $R_{pr}F_{0}F_{1}F_{2}$, $F_{1}\in h_{\mathbb{A}}(a)$ and
$F_{2}\not\in h_{\mathbb{A}}(b)$, contradicting that $F_{0}\in
h_{\mathbb{A}}(a)\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R_{Pr(\mathbb{A})}}h_{\mathbb{A}}(b)$.
Hence $a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\in F$ as
required.

Finally, suppose
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b=\bot$. Then
$h_{\mathbb{A}}(a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b)=\emptyset$.
Let $F$ be arbitrary. We have, for all $x\in F$ and all $y\in[a)$, that
$x\blacktriangleright y\not\in(b]$ since otherwise $x\blacktriangleright a\leq
b$ and then $x\leq
a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b=\bot$: hence
$x=\bot\not\in F$, a contradiction. Hence we can run the argument of the
previous subcase to obtain $F_{1}$ and $F_{2}$ such that $F_{1}\in h(a)$,
$R_{pr}FF_{1}F_{2}$, but $F_{2}\not\in h_{\mathbb{A}}(b)$.

Now given an interpretation $\llbracket-\rrbracket$ on a layered Heyting
algebra $\mathbb{A}$ we immediately obtain a persistent valuation on the prime
filter frame by setting
$\mathcal{V}(\mathrm{p})=h_{\mathbb{A}}(\llbracket\mathrm{p}\rrbracket)$. This
makes $\mathrm{Pr}=(Pr(\mathbb{A}),\mathcal{V})$ a relational model of ILGL.
The fact that $h_{\mathbb{A}}$ is a homomorphism, together with Lemma 24,
immediately yields the following lemma.

######  Lemma 26.

Given a layered Heyting algebra $\mathbb{A}$ and an interpretation
$\llbracket-\rrbracket$, for all $F\in Pr(A)$ and all formulae $\varphi$ of
ILGL, $\llbracket\varphi\rrbracket\in F$ iff $F\vDash_{\mathrm{Pr}}\varphi$. ∎

Taking Lemmas 24 and 26 together yields the equivalence of the algebraic and
relational semantics.

######  Theorem 27 (Equivalence of algebraic and relational semantics).

For all formulae $\varphi\in\mathrm{Form}$: $\varphi$ is satisfiable (valid)
on layered Heyting algebras iff $\varphi$ is satisfiable (valid) on layered
frames. ∎

We also obtain the equivalence of the Hilbert and labelled tableaux systems,
and with it soundness and completeness with respect to
$\mathrm{ILGL}_{\mathrm{H}}$ for the layered graph semantics. With these
equivalences proven, we may refer to ILGL without specifying the particular
semantics and proof system of those stated thus far.

######  Corollary 28 (Equivalence of the Hilbert and tableaux systems).

  1. (1)

For all formulae $\varphi$ and $\psi$ of ILGL, $\varphi\vdash\psi$ is provable
in $\mathrm{ILGL}_{\mathrm{H}}$ iff there is a closed tableau for
$\varphi\rightarrow\psi$.

  2. (2)

For all formulae $\varphi$ and $\psi$ of ILGL, $\varphi\vdash\psi$ is provable
in $\mathrm{ILGL}_{\mathrm{H}}$ iff $\varphi\rightarrow\psi$ is valid on
preordered scaffolds. ∎

A sequent calculus, a natural deduction system, and a display calculus
(satisfying cut elimination) can be given for LGL. They define equivalent
notions of provability to its Hilbert system [9]. It is straightforward to
weaken the classical propositional logic component of each to obtain such
systems for ILGL. Each of these systems is also proven equivalent to our
labelled tableaux system by this corollary.

###  4.3. Finite Model Property & Decidability

We now prove the finite embeddability property (FEP) for the class of layered
Heyting algebras, and with it, decidability of ILGL. We first recall the
definition of the FEP for classes of ordered algebras.

[Finite Embeddability Property] A class of algebras $\mathcal{K}$ has the
_finite embeddability property_ (FEP) if, for any algebra
$\mathbb{A}\in\mathcal{K}$ and any finite subset $B\subseteq A$ there exists a
finite algebra $\mathbb{C}\in\mathcal{K}$ and an injective map $g:B\rightarrow
C$ such that for all algebraic operations $f$, if $b_{1},\ldots,b_{n}\in B$
and $f_{\mathbb{A}}(b_{1},\ldots,b_{n})\in B$ then
$g(f_{\mathbb{A}}(b_{1},\ldots,b_{n}))=f_{\mathbb{C}}(g(b_{1}),\ldots,g(b_{n}))$.
∎

Intuitively, the FEP states that every finite partial subalgebra can be
completed as a finite algebra. If the class of layered Heyting algebras has
the FEP then ILGL has a finite model property and is thus decidable by the
following argument. Suppose the algebra $\mathbb{A}$ with interpretation
$\llbracket-\rrbracket$ witnesses that $\varphi\vdash\psi$ does not hold: that
is,
$\llbracket\varphi\rrbracket\not\leq_{\mathbb{A}}\llbracket\psi\rrbracket$.
Set $B=\\{\llbracket\chi\rrbracket\mid\chi\text{ a subformula of
}\varphi\rightarrow\psi\\}\cup\\{\top_{\mathbb{A}},\bot_{\mathbb{A}}\\}$. By
the FEP we obtain a finite algebra $\mathbb{C}$ and injective map
$g:B\rightarrow\mathbb{C}$, yielding an interpretation
$\widetilde{\llbracket-\rrbracket}$ generated by setting
$\widetilde{\llbracket\mathrm{p}\rrbracket}=g(\llbracket\mathrm{p}\rrbracket)$
for all propositional atoms $\mathrm{p}$ occurring in
$\varphi\rightarrow\psi$. As $g$ is injective and preserves existing algebraic
operations in $B$ this gives that
$\widetilde{\llbracket\varphi\rightarrow\psi\rrbracket}<_{\mathbb{C}}\top_{\mathbb{C}}$.
Since in layered Heyting algebras $a\leq b$ iff $a\rightarrow b=\top$, we have
a finite algebra $\mathbb{C}$ and interpretation
$\widetilde{\llbracket-\rrbracket}$ such that
$\widetilde{\llbracket\varphi\rrbracket}\not\leq\widetilde{\llbracket\psi\rrbracket}$,
witnessing that $\varphi\vdash\psi$ does not hold. As layered Heyting algebras
are finitely axiomatised this yields decidability of the logic.

We adapt an argument given by Haniková & Horc̆ík [26] to prove the class of
bounded residuated distributive-lattice ordered groupoids has the FEP. If such
an algebra supports Heyting implication it is a layered Heyting algebra. Thus
we simply have to additionally account for Heyting implication to make the
desired proof go through.

######  Theorem 29 (cf. [26]).

The class of layered Heyting algebras has the FEP.

######  Proof 4.2.

Let $\mathbb{A}$ be a layered Heyting algebra and $B\subseteq\mathbb{A}$ a
finite subset that, _wlog_ , contains $\top_{\mathbb{A}}$ and
$\bot_{\mathbb{A}}$. Denote by
$(C,\land_{\mathbb{C}},\lor_{\mathbb{C}},\top_{\mathbb{C}},\bot_{\mathbb{C}})$
the distributive sublattice of the distributive lattice reduct of $\mathbb{A}$
generated by $B$. As $B$ was finite, so too is $C$. Define
$a\rightarrow_{\mathbb{C}}b=\bigvee_{\mathbb{C}}\\{c\in C\mid
a\land_{\mathbb{C}}c\leq_{\mathbb{C}}b\\}$. Since each join is finite this is
well defined, and this makes
$(C,\land_{\mathbb{C}},\lor_{\mathbb{C}},\rightarrow_{\mathbb{C}},\top_{\mathbb{C}},\bot_{\mathbb{C}})$
a Heyting algebra. It can be shown that if
$b,b^{\prime},b\rightarrow_{\mathbb{A}}b^{\prime}\in B$ then
$b\rightarrow_{\mathbb{A}}b^{\prime}=b\rightarrow_{\mathbb{C}}b^{\prime}$.

The rest of the proof now proceeds as in [26]. Define operations
$\lambda,\sigma:A\rightarrow A$ by $\lambda(a)=\bigwedge_{\mathbb{C}}\\{c\in
C\mid a\leq_{\mathbb{A}}c\\}$ and $\sigma(a)=\bigvee_{\mathbb{C}}\\{c\in C\mid
c\leq_{\mathbb{A}}a\\}$. These are both well-defined because $C$ is finite. It
follows that for $c\in C$, $\lambda(c)=c=\sigma(c)$. We then define
$\blacktriangleright_{\mathbb{C}},\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{\mathbb{C}},\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{\mathbb{C}}$
on $C$ by
$c\blacktriangleright_{\mathbb{C}}c^{\prime}=\lambda(c\blacktriangleright_{\mathbb{A}}c^{\prime})$,
$c\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{\mathbb{C}}c^{\prime}=\sigma(c\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{\mathbb{A}}c^{\prime})$
and
$c\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{\mathbb{C}}c^{\prime}=\sigma(c\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{\mathbb{A}}c^{\prime})$.
The fact that $\lambda$ is a closure operator and $\sigma$ an interior
operator can be used to show that the required residuation properties hold for
these operations. We thus have a finite layered Heyting algebra
$\mathbb{C}=(C,\land_{\mathbb{C}},\lor_{\mathbb{C}},\rightarrow_{\mathbb{C}},\top_{\mathbb{C}},\bot_{\mathbb{C}},\blacktriangleright_{\mathbb{C}},\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{\mathbb{C}},\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{\mathbb{C}})$,
with the inclusion map of $B$ into $C$ satisfying the defining property of the
FEP.

######  Corollary 30 (Decidability of ILGL).

The consequence relation $\vdash$ for ILGL is decidable. ∎

The finite countermodel for an invalid formula is bounded in size: for a
formula $\varphi$ with $n$ subformulae, the cardinality of the finite algebra
is bounded by $2^{2^{n}}$. In [26] this is improved upon by showing such an
algebra can be represented by a poset of join-irreducibles of cardinality
$m\leq 2^{n}-2$ and a ternary relation $R$ of cardinality $m^{3}$, where join-
irreducibles are those elements that are not equal to $\bot$ and cannot be
represented as the join of two distinct, non-$\bot$ elements. We defer to
another occasion an in-depth investigation of the computational complexity of
the decision procedure.

##  5\. Duality

We now extend Theorem 25 to give a Stone-type [31] duality result for ILGL.
Such duality theorems elegantly abstract the relationship between syntax and
semantics in logic, and support systematic approaches to soundness and
completeness theorems. As previously noted, ILGL is the weakest bunched logic
with intuitionistic additives. Not only can the other intuitionistic bunched
logics be constructed by adding structure to ILGL, but also duality theorems
for each intuitionistic bunched logic, including BI and Separation Logic. We
defer the presentation of these results to another occasion, although we
demonstrate the extension to predicate logic in Section 6. We also note that a
duality theorem for BI that can be relativized to ILGL has been independently
given by Jipsen & Litak [29].

Our duality theorem extends Esakia’s duality for Heyting algebras [18], which
we now recall. A _Priestley Space_ $\mathcal{X}$ is a structure
$\mathcal{X}=(X,\mathcal{O},\preccurlyeq)$ such that $(X,\mathcal{O})$ is a
compact topological space, $\preccurlyeq$ is a preorder and the _Priestley
separation axiom_ holds: if $x\not\preccurlyeq y$ then there exists a clopen,
upward-closed set $C$ such that $x\in C$ and $y\not\in C$. The upward-closed
clopen sets $\mathcal{C}_{\preccurlyeq}(\mathcal{X})=\\{C\in\mathcal{O}\mid
C\text{ clopen and for all }x\in C,\text{ if }x\preccurlyeq y\text{ then }y\in
C\\}$ of a Priestley space carry the structure of a bounded distributive
lattice. An _Esakia space_ is a Priestley space satisfying the additional
property that for each clopen set $C$, the downwards closure $\\{x\in
X\mid\exists y\in C:x\preccurlyeq y\\}$ is clopen. This extra property is
sufficient for the upward-closed clopen sets to additionally support Heyting
implication.

For a Heyting algebra $\mathbb{A}$ define $\neg h_{\mathbb{A}}(a)=\\{F\in
Pr(A)\mid a\not\in F\\}$. Then $S=\\{h_{\mathbb{A}}(a)\mid a\in
A\\}\cup\\{\neg h_{\mathbb{A}}(a)\mid a\in A\\}$ (where $h_{\mathbb{A}}$ is
defined as in Theorem 25) forms a subbase that generates a topology
$\mathcal{O}_{Pr(A)}$ on the set of prime filters of $\mathbb{A}$, $Pr(A)$.
This topology makes $(Pr(A),\mathcal{O}_{Pr(A)},\subseteq)$ an Esakia space.
Conversely, given an Esakia space $\mathcal{X}$ the set of upward-closed
clopen sets carries the structure of a Heyting algebra. Now define maps
$f_{\mathcal{X}}:\mathcal{X}\rightarrow
Pr(\mathcal{C}_{\preccurlyeq}(\mathcal{X}))$ by
$f_{\mathcal{X}}(x)=\\{C\in\mathcal{C}_{\preccurlyeq}(\mathcal{X})\mid x\in
C\\}$. Then $f_{(-)}$ and $h_{(-)}$ define natural isomorphisms underpinning a
dual equivalence of the category of Heyting algebras with the category of
Esakia spaces.

We now define the topological dual of layered Heyting algebras,
_intuitionistic layered spaces_ , which combine the structure of an
intuitionistic layered frame with that of an Esakia space, with compatibility
conditions on $R$ providing the glue. Intuitonistic layered spaces are closely
related to gaggle spaces, the topological dual of distributive gaggles [4].

[Intuitionistic Layered Space] An _intutionistic layered space_ is a structure
$\mathcal{X}=(X,\mathcal{O},\preccurlyeq,R)$ such that

  1. (1)

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

  2. (2)

$R$ is a ternary relation over $X$;

  3. (3)

$\mathcal{C}_{\preccurlyeq}(\mathcal{X})$ is closed under
$\blacktriangleright_{R},\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R}$
and $\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{R}$;

  4. (4)

If $Rxyz$ does not hold then there exists $C_{1}$,
$C_{2}\in\mathcal{C}_{\preccurlyeq}(\mathcal{X})$ such that $x\in C_{1}$,
$y\in C_{2}$ and $z\not\in C_{1}\blacktriangleright_{R}C_{2}$. ∎

A morphism of intuitonistic layered spaces is simply a _continuous_
intuitionistic layered p-morphism (see Definition 22). This yields a category
$\mathrm{IntLaySp}$. Note that continuity, together with conditions (1) and
(2) of Definition 22 define morphisms of Esakia spaces. $\mathrm{IntLaySp}$ is
thus a subcategory of the category of Esakia spaces.

We define contravariant functors
$\mathrm{F}:\mathrm{LayHeyAlg}^{op}\rightarrow\mathrm{IntLaySp}$ and
$\mathrm{G}:\mathrm{IntLaySp}^{op}\rightarrow\mathrm{LayHeyAlg}$ as follows:

$\begin{cases}\mathrm{F}(\mathbb{A})=(Pr(A),\mathcal{O}_{Pr(\mathbb{A})},\subseteq,R_{Pr(\mathbb{A})})\\\
\mathrm{F}f:\mathrm{F}(\mathbb{A}^{\prime})\rightarrow\mathrm{F}(\mathbb{A}),X^{\prime}\mapsto
f^{-1}[X^{\prime}]\end{cases}\begin{cases}\mathrm{G}(\mathcal{X})=(\mathcal{C}_{\preccurlyeq}(\mathcal{X}),\cap,\cup,\Rightarrow,X,\emptyset,\blacktriangleright_{R},\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R},\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{R})\\\
\mathrm{G}g:\mathrm{G}(\mathcal{X}^{\prime})\rightarrow\mathrm{G}(\mathcal{X}),C^{\prime}\mapsto
g^{-1}[C^{\prime}]\end{cases}$

where $\mathcal{O}_{Pr(\mathbb{A})}$ and
$\mathcal{C}_{\preccurlyeq}(\mathcal{X})$ are as given in the preceeding
discussion on Esakia duality and
$\blacktriangleright_{R},\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R},\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{R}$
are as defined in Definition 4.2. We show the output of these functors gives
structures and morphisms of the correct type.

######  Lemma 31.

The functor $\mathrm{F}:\mathrm{LayHeyAlg}^{op}\rightarrow\mathrm{IntLaySp}$
is well-defined.

######  Proof 5.1.

We first verify objects. Let $\mathbb{A}$ be a layered Heyting algebra. By
Esakia duality, $(Pr(A),\mathcal{O}_{\mathbb{A}},\subseteq)$ is an Esakia
space. Closure under
$\blacktriangleright_{R_{Pr(\mathbb{A})}},\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R_{Pr(\mathbb{A})}}$
and
$\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{R_{Pr(\mathbb{A})}}$
is given by Theorem 25 and the fact that, by Esakia duality, every upward-
closed clopen set is of the form $h_{\mathbb{A}}(a)$ for $a\in A$. Finally,
suppose $R_{Pr(\mathbb{A})}F_{0}F_{1}F_{2}$ does not hold. Then there exist
$a\in F_{0}$ and $b\in F_{1}$ such that $a\blacktriangleright b\not\in F_{2}$.
The upward-closed clopen sets $h_{\mathbb{A}}(a)$ and $h_{\mathbb{A}}(b)$ then
satisfy condition 4.

Next morphisms. Let $f:\mathbb{A}\rightarrow\mathbb{A}^{\prime}$ be a
homomorphism. That $\mathrm{F}(f)=f^{-1}$ maps prime filters to prime filters,
is continuous and satisfies properties (1) and (2) of Definition 22 is
precisely Esakia duality. It remains to verify properties 3–6. We show 3 and
the characteristic example of 5, leaving the other similar cases as an
exercise to the reader. First, suppose
$R^{\prime}_{Pr(\mathbb{A})}F^{\prime}_{0}F^{\prime}_{1}F^{\prime}_{2}$ and
let $a\in\mathrm{F}(f)(F^{\prime}_{0})$ and
$b\in\mathrm{F}(f)(F^{\prime}_{1})$. Then $f(a)\in F^{\prime}_{0}$ and
$f(b)\in F^{\prime}_{1}$ so $f(a)\blacktriangleright
f(b)=f(a\blacktriangleright b)\in F^{\prime}_{2}$. It thus follows that
$a\blacktriangleright b\in\mathrm{F}(f)(F^{\prime}_{2})$ so
$R_{Pr(\mathbb{A})}\mathrm{F}(f)(F^{\prime}_{0})\mathrm{F}(f)(F^{\prime}_{1})\mathrm{F}(f)(F^{\prime}_{2})$
as required.

For 5, suppose $R_{Pr(\mathbb{A})}F_{3}F_{1}F_{2}$ and
$\mathrm{F}(f)(F^{\prime}_{0})\subseteq F_{3}$. Consider
$\gamma=(f(\overline{F_{3}})]$, $\alpha=[f(F_{1}))$ and
$\beta=(f(\overline{F_{2}})]$. We will use these ideals and filter to prove
the existence of the requisite prime filters by showing that the partial order
of tuples of proper filters and ideals defined by the satisfaction of the
properties required for 5 is non-empty. We can then apply Zorn’s lemma and
obtain the required prime filters as in Theorem 25. First we note an important
alternative characterization of $R_{Pr(\mathbb{A})}$:

$R_{Pr(\mathbb{A})}F_{3}F_{1}F_{2}\text{ iff for all }a,b:a\in F_{1}\text{ and
}b\not\in F_{2}\text{ implies
}a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\not\in F_{3}.$

We leave it to the reader to verify this holds. With this we show that each of
$\gamma$, $\alpha$, $\beta$ is proper. Suppose $\top\in\gamma$. Then there
exists $c\not\in F_{2}$ such that $f(c)=\top$. Hence
$c\not\in\mathrm{F}(f)(F^{\prime}_{0})$ so $\top=f(c)\not\in F^{\prime}_{0}$,
contradicting filterhood of $F^{\prime}_{0}$. Suppose $\bot\in\alpha$. Then
there exists $a\in F_{1}$ such that $f(a)=\bot$. Let $b\not\in F_{2}$ be
arbitrary (this is possible because $F_{2}$ is proper). Then we have
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\not\in F_{3}$, so it
follows that
$a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b\not\in\mathrm{F}(f)(F^{\prime}_{0})$.
But this entails that
$f(a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b)=f(a)\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}f(b)=\top\not\in
F^{\prime}_{0}$, contradicting filterhood of $F^{\prime}_{0}$. Finally,
suppose $\top\in\beta$. There thus exists $b\not\in F_{2}$ such that
$f(b)=\top$. Let $a\in F_{1}$ be arbitrary. Then, similarly to the previous
case,
$f(a\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}b)=f(a)\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}f(b)=\top\not\in
F^{\prime}_{0}$, contradicting filterhood.

Next we show the defining condition of $R^{\prime}_{Pr(\mathbb{A})}$ is
satisfied by $\overline{\gamma}$, $\alpha$ and $\overline{\beta}$. Let
$a\in\overline{\gamma}$ and $b\in\alpha$. It follows that if $a\leq f(d)$ then
$d\in F_{3}$ and that there exists $b^{\prime}\in F_{1}$ such that
$f(b^{\prime})\leq b$. We now show $a\blacktriangleright
b\in\overline{\beta}$. Suppose instead that $a\blacktriangleright b\in\beta$.
Then there exists $c\not\in F_{2}$ such that $a\blacktriangleright b\leq
f(c)$. We have $a\blacktriangleright f(b^{\prime})\leq a\blacktriangleright
b\leq f(c)$ so $a\leq
f(b^{\prime}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}c)$. Thus
$b^{\prime}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}c\in F_{3}$
and so necessarily $c\in F_{2}$, but this is a contradiction. Hence
$a\blacktriangleright b\in\overline{\beta}$, as required.

Finally, we show that the required inclusions hold. That
$F_{1}\subseteq\mathrm{F}(f)(\alpha)$ and
$\mathrm{F}(f)(\overline{\beta})\subseteq F_{2}$ is obvious. For
$F^{\prime}_{0}\subseteq\overline{\gamma}$, suppose $a\in F^{\prime}_{0}$ and
assume for contradiction that $a\in\gamma$. There thus exists $c\not\in F_{3}$
such that $a\leq f(c)$. By assumption,
$c\not\in\mathcal{F}(f)(F^{\prime}_{0})\subseteq F_{3}$ but $a\leq f(c)$
entails $c\in\mathrm{F}(f)(F^{\prime}_{0})$, a contradiction. Hence
$a\in\overline{\gamma}$.

By a similar argument to that of Theorem 25, there thus exist prime ideals
$I^{max}_{2}$, $I^{max}_{3}$ and a prime filter $F^{\prime}_{1}$ such that
$F^{\prime}_{3}=\overline{I^{max}_{3}}$,
$F^{\prime}_{2}=\overline{I^{max}_{2}}$ and $F^{\prime}_{1}$ are prime filters
with the property that
$R^{\prime}_{Pr(\mathbb{A^{\prime}})}F^{\prime}_{3}F^{\prime}_{1}F^{\prime}_{2}$
with $F^{\prime}_{0}\subseteq F^{\prime}_{3}$,
$F_{1}\subseteq\mathrm{F}(f)(F^{\prime}_{1})$ and
$\mathrm{F}(f)(F^{\prime}_{2})\subseteq F_{2}$, as required.

######  Lemma 32.

The functor $\mathrm{G}:\mathrm{IntLaySp}\rightarrow\mathrm{LayHeyAlg}$ is
well-defined.

######  Proof 5.2.

Verifying objects: the fact that, for an intuitionistic layered space
$\mathcal{X}$, $\mathrm{G}(\mathcal{X})$ is a layered Heyting algebra
essentially follows from Lemma 23 and the fact the upward-closed clopen sets
are closed under
$\blacktriangleright_{R},\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R},\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}_{R}$.

Verifying morphisms: let $g:\mathcal{X}\rightarrow\mathcal{X}^{\prime}$ be an
intuitionistic layered morphism. That $\mathrm{G}(g)$ maps upward-closed
clopen sets to upward-closed clopen sets and respects the Heyting algebra
operations is simply Esakia duality. We show that it also respects the
operation $\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}$, leaving
the similar $\blacktriangleright$ and
$\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}$ cases to the
reader.

First, assume
$x\in\mathrm{G}(g)(C_{1}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R^{\prime}}C_{2})$
and suppose $x\preccurlyeq w$ with $Rwyz$ and $y\in\mathrm{G}(g)(C_{1})$. Then
$g(x)\preccurlyeq g(w)$ with $R^{\prime}g(w)g(y)g(z)$ and $g(y)\in C_{1}$. By
assumption, this entails $g(z)\in C_{2}$ so $z\in\mathrm{G}(g)(C_{2})$, as
required.

Conversely, assume
$x\in\mathrm{G}(g)(C_{1})\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R}\mathrm{G}(g)(C_{2})$
and let $g(x)\preccurlyeq^{\prime}w^{\prime}$ with
$R^{\prime}w^{\prime}y^{\prime}z^{\prime}$ and $y^{\prime}\in C_{1}$. Since
$g$ is an intuitionistic layered p-morphism, there exist $w,y,z$ such that
$Rwyz$, $x\preccurlyeq w$, $y^{\prime}\preccurlyeq^{\prime}g(y)$ and
$g(z)\preccurlyeq^{\prime}z^{\prime}$. By upwards-closure, $g(y)\in C_{1}$, so
$y\in\mathrm{G}(g)(C_{1})$ and by assumption this entails
$z\in\mathrm{G}(g)(C_{2})$. By upwards-closure again, $z^{\prime}\in C_{2}$.
Hence $g(x)\in
C_{1}\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}_{R^{\prime}}C_{2}$,
as required.

######  Theorem 33 (Duality Theorem for Layered Heyting Algebras).

The categories $\mathrm{LayHeyAlg}$ and $\mathrm{IntLaySp}$ are dually
equivalent.

######  Proof 5.3.

The natural isomorphisms $h_{(-)}$ and $f_{(-)}$ defined in the discussion on
Esakia duality together with the functors $\mathrm{F}$ and $\mathrm{G}$
suffice to give the dual equivalence of categories. By Theorem 25 each
$h_{\mathbb{A}}$ is a homomorphism (in fact an isomorphism). To see each
$f_{\mathcal{X}}$ is an isomorphism it suffices to show: $Rxyz$ iff
$R_{Pr(\mathrm{G}(\mathcal{X}))}f_{\mathcal{X}}(x)f_{\mathcal{X}}(y)f_{\mathcal{X}}(z)$.
The left-to-right direction is a simple unpacking of the definitions, whilst
the right-to-left definition is proved by contraposition, using property 4 in
the definition of intuitionistic layered space. Naturality is then immediate
from Esakia duality.

##  6\. Extension To Predicate ILGL

In this final section we extend ILGL to predicate ILGL and prove soundness and
completeness with respect to a truth-functional semantics. Our motivation is
to provide metatheory for an expressive extension in which real systems
modelling can be done.

As an example, consider the following two predicates: an unary predicate
$Contains(-)$ and a binary predicate $-\mapsto-$. Informally, $Contains(r)$
designates that a subgraph contains a resource $r$ and $r\mapsto r^{\prime}$
designates that a subgraph contains a path from a resource $r$ to a resource
$r^{\prime}$. This signature is styled after Pointer Logic [28] (the
formulation of Separation Logic [42] as a model of BI) and as such is joined
by the standard intuitionistic quantifiers. Note that we do not consider
_multiplicative_ quantification (see, for example, [12]): our extension is
instead akin to the definition of predicate BI given by Biering et al [3].

We specify a model of this extended language as follows. Let $\mathcal{X}$ be
a bigraph scaffold of the sort defined in Example 4. Denote by $G$ the union
of the place graphs of the system. A _resource assignment_ $s$ is a finite
partial function $s:Res\rightarrow\mathcal{P}_{\preccurlyeq}(\mathcal{V}(G))$.
As the order is determined by the spatial containment encoded by the place
graphs, that a resource assignment maps resources to upwards closed sets just
means that if a location $x$ contains a resource $r$, and $x$ is contained in
$y$ then $y$ also contains $r$.

Given a resource assignment $s$, together with $r\in Res$, we define
$s[r\mapsto A]$ to be the resource assignment that is equal to $s$ everywhere
except $r$, where it assigns $r$ to the upward-closed set of vertices $A$. We
define a semantics on pairs $(s,H)$ for this extended language in Figure 13.

$s,H$ $\vDash$ $\top$ always $s,H$ $\vDash$ $\bot$ never $s,H$ $\vDash$
$\mathrm{Contains}(r)$ iff $H$ contains a $s(r)$-vertex $s,H$ $\vDash$
$r\mapsto r^{\prime}$ iff exists a non-empty path from a $s(r)$-vertex to a
$s(r^{\prime})$-vertex in H $s,H$ $\vDash$ $\varphi\land\psi$ iff
$s,H\vDash\varphi$ and $s,H\vDash\psi$ $s,H$ $\vDash$ $\varphi\lor\psi$ iff
$s,H\vDash\varphi$ or $s,H\vDash\psi$ $s,H$ $\vDash$ $\varphi\rightarrow\psi$
iff for all $K\succcurlyeq H$, $s,K\vDash\varphi$ implies $s,K$ $\vDash$
$\psi$ $s,H$ $\vDash$ $\varphi\blacktriangleright\psi$ iff there exists
$K_{0}\mathop{@_{\mathcal{E}}}\nolimits K_{1}\downarrow$ s.t. $H\succcurlyeq
K_{0}\mathop{@_{\mathcal{E}}}\nolimits K_{1}$, $s,K_{0}\vDash\varphi$ and
$s,K_{1}\vDash\psi$ $s,H$ $\vDash$
$\varphi\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\psi$ iff for
all $K$ and $L\succcurlyeq H$ s.t. $L\mathop{@_{\mathcal{E}}}\nolimits
K\downarrow$: $s,L\vDash\varphi$ implies $s,L\mathop{@_{\mathcal{E}}}\nolimits
K\vDash\psi$ $s,H$ $\vDash$
$\varphi\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\psi$ iff for
all $K$ and $L\succcurlyeq H$ s.t. $K\mathop{@_{\mathcal{E}}}\nolimits
L\downarrow$: $s,L\vDash\varphi$ implies $s,K\mathop{@_{\mathcal{E}}}\nolimits
L\vDash\psi$ $s,H$ $\vDash$ $\exists r\varphi$ iff there exists $A$ s.t.
$s[r\mapsto A],H\vDash\varphi$ $s,H$ $\vDash$ $\forall r\varphi$ iff for all
$A$, $H\preccurlyeq K$ implies $s[r\mapsto A],K\vDash\varphi$

Figure 13. Satisfaction for bigraph models of predicate ILGL.

There are many design choices possible here. For example, we could
additionally assign weights or permissions to edges, with satisfaction of the
$\mapsto$ predicate mediated by conditions on the path. Coupled with a notion
of dynamics that evolves assignments and the underlying graph theoretic
structure we would have a rich environment within which to model a variety of
distributed systems. We defer to another occasion an in-depth investigation of
such a framework.

###  6.1. Soundness & completeness for predicate ILGL

We now prove soundness and completeness of many-sorted predicate ILGL
(henceforth predicate ILGL) with respect to a truth-functional semantics and a
Hilbert system. The model described in the preceeding discussion is a
particular instantiation of this semantics. We consider a many-sorted language
to enable the construction of models where different types of entity are
assigned to the graph and because the category theoretic structures we employ
easily support it.

A _signature_ for predicate ILGL is comprised of $n$-ary function symbols $f$
of type $X_{1}\times\cdots\times X_{n}\rightarrow X$ and $m$-ary predicate
symbols $P$ of type $Y_{1},\ldots,Y_{m}$. Terms of predicate ILGL are given in
much the same way as classical predicate logic: each variable $v:X$ is a term
of type $X$, and for terms $t_{1},\ldots,t_{n}$ of type $X_{1},\ldots,X_{n}$
respectively and an n-ary function symbol $f$ of type $X_{1}\times\cdots\times
X_{n}\rightarrow X$, $f(t_{1},\ldots,t_{n})$ is a term of type $X$. The syntax
of predicate ILGL is then given as follows, where $t_{i}$, $t$, $t^{\prime}$
range over the terms of the right type for the predicate symbols:

$\varphi\\!::=\\!Pt_{1}\ldots t_{m}\mid
t\\!=_{X}\\!t^{\prime}\mid\top\mid\bot\mid\varphi\wedge\varphi\mid\varphi\vee\varphi\mid\varphi\\!\rightarrow\\!\varphi\mid\varphi\\!\blacktriangleright\\!\varphi\mid\varphi\\!\mathop{-\\!\\!\\!\\!\\!-\\!\\!\\!\blacktriangleright}\\!\varphi\mid\varphi\\!\mathop{\blacktriangleright\\!\\!\\!\\!-\\!\\!\\!\\!\\!-}\\!\varphi\mid\exists
v\\!\\!:\\!\\!X\varphi\mid\forall v\\!\\!:\\!\\!X\varphi$

Figure 14 gives rules for intuitionistic quantifiers that extend the Hilbert
system $\mathrm{ILGL}_{\mathrm{H}}$ of Figure 5 to predicate ILGL. These rules
have auxillary conditions: in rules $\exists_{1}$ and $\forall_{1}$, $v$ must
not be free in $\varphi$; in rules $\exists_{2}$ and $\forall_{2}$, $t$ must
be a term of type $X$ and it must be that no occurence of a variable in $t$
becomes bound when substituted into $\varphi$ .

$\varphi\vdash\psi$ $(\exists_{1})$ $\exists v:X\varphi\vdash\psi$
$\varphi\vdash\psi$ $(\forall_{1})$ $\varphi\vdash\forall v:X\psi$
---
$(\exists_{2})$ $\varphi(t)\vdash\exists v:X\varphi(v)$ $(\forall_{2})$
$\forall v:X\varphi(v)\vdash\varphi(t)$
Figure 14. Extension of $\mathrm{ILGL}_{\mathrm{H}}$ to predicate ILGL

Our proof mirrors the structure of the results given in Section 4. First, we
define algebraic structures on which a completeness argument for the Hilbert
system can easily be constructed. We then introduce relational structures, of
which our intended semantics is a particular instance, and show we can
generate an algebraic structure from a relational structure and vice versa,
with satisfiability coinciding in each case.

[ILGL Hyperdoctrine] An _ILGL hyperdoctrine_ is a tuple
$(\mathbb{P}:\mathrm{C}^{op}\rightarrow\mathrm{Poset},(=_{X})_{X\in
Ob(\mathrm{C})},(\exists X_{\Gamma},\forall X_{\Gamma})_{\Gamma,X\in
Ob(\mathrm{C})})$ such that:

  1. (1)

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

  2. (2)

$\mathbb{P}:\mathrm{C}^{op}\rightarrow\mathrm{Poset}$ is a contravariant
functor;

  3. (3)

For each object $X$ and each morphism $f$ in $\mathrm{C}$, $\mathbb{P}(X)$ is
additionally a layered Heyting algebra and $\mathbb{P}(f)$ a layered Heyting
algebra homomorphism

  4. (4)

For each object $X$ in $\mathrm{C}$ and each diagonal morphism
$\Delta_{X}:X\rightarrow X\times X$ in $\mathrm{C}$,
$=_{X}\in\mathbb{P}(X\times X)$ is such that, for all $a\in\mathbb{P}(X\times
X)$, $\top\leq\mathbb{P}(\Delta_{X})(a)\text{ iff }=_{X}\leq a$;

  5. (5)

For each pair of objects $\Gamma,X$ in $\mathrm{C}$ and each projection
$\pi_{\Gamma,X}:\Gamma\times X\rightarrow\Gamma$ in $\mathrm{C}$, $\exists
X_{\Gamma}$ and $\forall X_{\Gamma}$ are left and right adjoints to
$\mathbb{P}(\pi_{\Gamma,X})$ respectively: that is, monotone maps $\exists
X_{\Gamma}:\mathbb{P}(\Gamma\times X)\rightarrow\mathbb{P}(\Gamma)$ and
$\forall X_{\Gamma}:\mathbb{P}(\Gamma\times X)\rightarrow\mathbb{P}(\Gamma)$
such that, for all $a,b\in\mathbb{P}(\Gamma)$, $\exists X_{\Gamma}(a)\leq
b\text{ iff }a\leq\mathbb{P}(\pi_{\Gamma,X})(b)$ and
$\mathbb{P}(\pi_{\Gamma,X})(b)\leq a\text{ iff }b\leq\forall X_{\Gamma}(a)$.
This assignment of maps is additionally natural in $\Gamma$: given a morphism
$s:\Gamma\rightarrow\Gamma^{\prime}$, the following diagrams commute:

${\mathbb{P}(\Gamma^{\prime}\times X)}$${\mathbb{P}(\Gamma\times
X)}$${\mathbb{P}(\Gamma^{\prime})}$${\mathbb{P}(\Gamma)}$$\scriptstyle{\mathbb{P}(s\times
id_{X})}$$\scriptstyle{\exists X_{\Gamma^{\prime}}}$$\scriptstyle{\exists
X_{\Gamma}}$$\scriptstyle{\mathbb{P}(s)}$${\mathbb{P}(\Gamma^{\prime}\times
X)}$${\mathbb{P}(\Gamma\times
X)}$${\mathbb{P}(\Gamma^{\prime})}$${\mathbb{P}(\Gamma)}$$\scriptstyle{\mathbb{P}(s\times
id_{X})}$$\scriptstyle{\forall X_{\Gamma^{\prime}}}$$\scriptstyle{\forall
X_{\Gamma}}$$\scriptstyle{\mathbb{P}(s)}$

∎

For a given signature of predicate ILGL, an interpretation
$\llbracket-\rrbracket$ on an ILGL hyperdoctrine
$\mathbb{P}:\mathrm{C}^{op}\rightarrow\mathrm{Poset}$ is defined as follows
below. For each type $X$, we assign an object $\llbracket X\rrbracket$ in
$\mathrm{C}$ and for each n-ary function symbol $f$ of type
$X_{1}\times\cdots\times X_{n}\rightarrow X$ in the signature, we assign a
morphism $\llbracket f\rrbracket:\llbracket
X_{1}\rrbracket\times\cdots\times\llbracket
X_{n}\rrbracket\rightarrow\llbracket X\rrbracket$. A context
$\Gamma=\\{v_{1}:X_{1},\ldots,v_{n}:X_{n}\\}$ is then assigned
$\llbracket\Gamma\rrbracket=\llbracket
X_{1}\rrbracket\times\cdots\times\llbracket X_{n}\rrbracket$ and each term $t$
of type $X$ in context $\Gamma$ is inductively assigned a morphism $\llbracket
t\rrbracket:\llbracket\Gamma\rrbracket\rightarrow\llbracket X\rrbracket$: for
variables $v_{i}$, $\llbracket v_{i}\rrbracket=\pi_{i}$, the i-th projection
from $\llbracket\Gamma\rrbracket$; for terms $t_{1},\ldots,t_{n}$ and n-ary
function symbol $f$, $\llbracket f(t_{1},\ldots,t_{n})\rrbracket=\llbracket
f\rrbracket\circ\langle\llbracket t_{1}\rrbracket,\ldots,\llbracket
t_{n}\rrbracket\rangle.$