# Constructive S4 modal logics with the finite birelational frame property

Philippe Balbiani<EMAIL_ADDRESS>IRIT, Toulouse University.
Toulouse, France  Martín Diéguez<EMAIL_ADDRESS>LERIA, University of Angers, Angers, France  David Fernández-Duque
<EMAIL_ADDRESS>Department of Philosophy, University of Barcelona,
Barcelona, Spain  Brett McLean<EMAIL_ADDRESS>Department of
Mathematics, Ghent University. Gent, Belgium

( )

###### Abstract

The logics $\mathsf{CS4}$ and $\mathsf{IS4}$ are the two leading
intuitionistic variants of the modal logic $\mathsf{S4}$. Whether the finite
model property holds for each of these logics have been long-standing open
problems. It was recently shown that $\mathsf{IS4}$ has the finite frame
property and thus the finite model property. In this paper, we prove that
$\mathsf{CS4}$ also enjoys the finite frame property.

Additionally, we investigate the following three logics closely related to
$\mathsf{IS4}$. The logic $\mathsf{GS4}$ is obtained by adding the
Gödel–Dummett axiom to $\mathsf{IS4}$; it is both a superintuitionistic and a
fuzzy logic and has previously been given a real-valued semantics. We provide
an alternative birelational semantics and prove strong completeness with
respect to this semantics. The extension $\mathsf{GS4^{c}}$ of $\mathsf{GS4}$
corresponds to requiring a crisp accessibility relation on the real-valued
semantics. We give a birelational semantics corresponding to an extra
confluence condition on the $\mathsf{GS4}$ birelational semantics and prove
strong completeness. Neither of these two logics have the finite model
property with respect to their real-valued semantics, but we prove that they
have the finite frame property for their birelational semantics. Establishing
the finite birelational frame property immediately establishes decidability,
which was previously open for these two logics. Our proofs yield NEXPTIME
upper bounds. The logic $\mathsf{S4I}$ is obtained from $\mathsf{IS4}$ by
reversing the roles of the modal and intuitionistic relations in the
birelational semantics. We also prove the finite frame property, and thereby
decidability, for $\mathsf{S4I}$.

##  1 Introduction

Intuitionistic logic, with its roots in constructive reasoning, has found
important and profound applications in computer science, most notably through
the Curry–Howard correspondence. This correspondence, often termed the
“propositions-as-types” principle, establishes a deep connection between logic
and the type theory of programming languages.

In the context of intuitionistic _modal_ logic, this correspondence has led to
the development of expressive and powerful frameworks for reasoning about
computation and program behavior. For example, modal types can represent
computations that are guaranteed to terminate (necessity) or those that might
diverge (possibility). Moreover, modal type theory allows modalities to
capture program invariants, preconditions, and postconditions, allowing for a
more fine-grained and expressive specification of program behavior.

Davis and Pfenning [1] extended the Curry–Howard correspondence and
intuitionistic variant of $\mathsf{S4}$ in order to achieve a modal account of
_staged computation_.555A staged computation is a computation that proceeds as
a sequence of multiple stages, where each stage produces the input for the
next. These stages can be carried out on different machines by different
users—think, for example, of the (various) compilation and execution stages
that are necessary to arrive at the final output of a program. The resulting
system $\mathsf{Mini}\text{-}\mathsf{ML}^{\square}$ can be used to introduce
the notion of partially evaluated functions in functional programming.

Similarly, Choudhury and Krishnaswami [2] proposed a typed system based on an
intuitionistic variant of $\mathsf{S4}$ within the context of impure
functional programming languages that can distinguish between expressions with
and without side effects. To do so, the authors use modalities to capture
important notions such as _safety_ or _purity_ in a comonadic type discipline.

Within the context of computer security, Miyamoto and Igarashi [3] extend
intuitionistic logic with $\mathsf{S4}$ modalities to propose a typed
$\lambda$-calculus to capture typed-based information flow analysis. In their
approach, security levels are mapped to Kripke worlds and the intuitionistic
accessibility relation simulates the heritage among the levels, i.e. any
information available at a lower level is also available at higher levels.

Another important field of application related intuitionistic variants of
$\mathsf{S4}$ is the so-called Fitch-style modal $\lambda$-calculus [4, 5],
where Fitch-style calculi [6] are extended with two functions ‘later’ and
‘constant’, which can be captured in terms of the $\Box$ modality in
intuitionistic modal logic. In [7], Clouston studies a variation of the modal
$\mathsf{S4}$ Fitch-style calculus where the $\Box$ modality is idempotent
(i.e. $\Box\varphi$ and $\Box\Box\varphi$ are not only logical equivalent but
also identical).

Inspired by the previous work of Fitch [8] and Wijesekera [9], _constructive
modal logics_ provide specific semantics for the $\Diamond$ operator. Although
most of the applications we have mentioned only consider the $\Diamond$-free
fragment of intuitionistic modal logic, it is worth mentioning that although
both approaches share the same $\Diamond$-free axioms, they do not share the
same $\Diamond$-free validities, i.e. there are $\Diamond$-free theorems of
$\mathsf{IS4}$ that may only be proven using axioms involving $\Diamond$.

It is also important to mention that intuitionistic modal logic has played a
significant role in the development of formal proof assistants, providing a
foundation for expressing and reasoning about modalities, which are crucial
for capturing various aforementioned aspects of formalised computational and
mathematical reasoning.

Regarding $\mathsf{S4}$ specifically, there are (at least) three prominent
constructive/intuitionistic variants in the literature. This paper
investigates two of them, known as $\mathsf{IS4}$ [10] and $\mathsf{CS4}$
[11]. Each of these logics has a natural axiomatisation and is sound and
strongly complete for a class of Kripke structures based on two preorders: one
preorder $\preccurlyeq$ for the intuitionistic implication, and another
preorder $\sqsubseteq$ for the modalities $\Diamond$ and $\Box$. However, the
questions of whether these logics enjoy the _finite model property_ remained
open for twenty years or more: in the case of $\mathsf{CS4}$ since at least
2001 [11], and of $\mathsf{IS4}$ at least since 1994 [10]. The question for
$\mathsf{IS4}$ was recently resolved in the positive in [12]. In this paper we
do the same for $\mathsf{CS4}$, solving the other principle open problem
concerning nonclassical variants of $\mathsf{S4}$.

The third preexisting constructive/intuitionistic variant of $\mathsf{S4}$,
which we do not investigate in this paper, is the logic $\mathsf{IntS4}$
studied (along with related variants of other modal logics) by Wolter and
Zakharyaschev [13, 14]. In contrast to $\mathsf{CS4}$ and $\mathsf{IS4}$, the
logic $\mathsf{IntS4}$ was already known to have the finite model property,
although the semantics are quite different, for example employing a different
binary relation for each of $\Diamond$ and $\Box$.

In this paper as well as proving that $\mathsf{CS4}$ has the finite frame
property, we also present three slight variants of $\mathsf{IS4}$ and show
that they too all enjoy the finite frame property.

The first two $\mathsf{IS4}$ variants are tightly related both to
$\mathsf{IS4}$ and also to $\mathsf{S4}$ modal extensions of _Gödel(–Dummett)
logic_. According to Caicedo and Ramírez [15], such fuzzy versions of modal
logic may be used to model situations where modal notions may be applied to
vague predicates. One may consider propositions such as  _“The weather is
always warm in Tulum”_ or _“Alice knows that Bob is trustworthy”,_ where to be
‘warm’ or ‘trustworthy’ are treated as vague (they can be true to varying
degrees), and ‘always’ and ‘knows’ are treated as modalities.

Among many approaches for dealing with vagueness, Gödel logics [16] are
particularly appealing versions of fuzzy logic, because they can alternatively
be viewed as superintuitionistic logics [17]. Indeed, propositional Gödel
logic lies strictly between intuitionistic propositional logic and classical
propositional logic, and is characterised by a semantics that assigns to each
proposition a truth value in the interval $[0,1]$. If we further assume that
modalities are interpreted using a _crisp_ accessibility relation (that is,
expressions of the form $x\mathrel{R}y$ take values in $\\{0,1\\}$), then
Gödel modal logic may be seen as a specialisation of intuitionistic modal
logic [18, 10] where semantically the intuitionistic partial order validates
an _upward linearity_ condition.

Some modal extensions of Gödel logic have already been studied in the
literature, including combinations with the logics $\mathsf{K}$ [19, 20, 21],
$\mathsf{S4}$ [15], $\mathsf{S5}$ [15, 22, Chapter 8], and with linear
temporal logic [23, 24]. In the specific case of Gödel $\mathsf{K}$, it has
been proved that the complexity of the validity problem is pspace-complete for
the box fragment [20] (where the logics of the accessibility-crisp and
accessibility-fuzzy frames coincide) and also the diamond fragment [19] (for
both accessibility-crisp frames and accessibility-fuzzy frames). Modal logics
over accessibility-fuzzy frames have been axiomatised by Caicedo and Rodríguez
[15, 25], and over accessibility-crisp frames by Rodríguez and Vidal [26].

Our first $\mathsf{IS4}$ variant, $\mathsf{GS4}$, which we prove to be
equivalent to Gödel $\mathsf{S4}$, has semantics defined over a subclass of
the $\mathsf{IS4}$ frames: those where the intuitionistic relation is _upward
linear_ , so that the logic validates the Gödel–Dummett axiom
$(p\mathbin{\rightarrow}q)\vee(q\mathbin{\rightarrow}p)$. Its accessibility-
crisp variant, ${\mathsf{GS4}}^{\mathsf{c}}$, is defined by imposing a
forth–down confluence condition on the $\mathsf{GS4}$ frames.

Our third $\mathsf{IS4}$ variant, $\mathsf{S4I}$, is defined over the same
class of frames as $\mathsf{IS4}$, except that the roles of the intuitionistic
and the modal preorders are interchanged. These frame conditions for
$\mathsf{S4I}$ are natural from a technical point of view, as they are the
minimal conditions required so that both modalities $\Diamond$ and $\Box$ can
be evaluated ‘classically’.

The key insights involved in our proofs for the finite frame properties is
that for each logic, one of two situations occurs, depending on the strength
of the logic. Either, as is the case for the two Gödel logics $\mathsf{GS4}$
and $\mathsf{GS4^{c}}$, the associated birelational semantics is strict enough
that we can obtain finite models directly by taking an appropriate
bisimulation quotient. Or, in the case of $\mathsf{S4I}$ and $\mathsf{CS4}$,
we can first show that it is sufficient that the logic enjoys the _shallow
frame property_ , meaning that any non-valid formula may be falsified on a
frame where the length of any $\prec$-chain is bounded (as usual, $w\prec v$
means that $w\preccurlyeq v$ but $v\not\preccurlyeq w$).666The descriptor
_shallow_ has been used in a similar way in the context of classical modal
logic [27]. While shallow models may in principle be infinite, their quotients
modulo bisimulation with respect to $\preccurlyeq$ are always finite, thus
reducing the problem of proving the finite frame property to that of proving
the shallow frame property, which we then proceed to do.

#### Structure of paper

In Section 2 we present the five logics $\mathsf{CS4}$, $\mathsf{IS4}$,
$\mathsf{GS4}$, $\mathsf{GS4^{c}}$, and $\mathsf{S4I}$ studied in this paper.
We first give syntactic definitions using Hilbert-style deductive calculi, and
then give semantics in terms of classes of birelational structures. We also
present the alternative real-valued semantics for $\mathsf{GS4}$ and
$\mathsf{GS4^{c}}$.

In Section 3 we prove the soundness of the deductive systems with respect to
the associated birelational semantics. We also verify the relationships
between the five logics, in particular confirming that they are all distinct.

In Section 4 we present the corresponding strong completeness results
(Theorems 2 and 3) by constructing canonical models in the following order:
$\mathsf{IS4}$, $\mathsf{GS4}$, $\mathsf{GS4^{c}}$, $\mathsf{S4I}$,
$\mathsf{CS4}$.

Section 5 is devoted to proofs of the finite frame property for the four
logics $\mathsf{GS4}$, $\mathsf{GS4^{c}}$, $\mathsf{CS4}$, and $\mathsf{S4I}$,
that is, for all of the logics except $\mathsf{IS4}$. In Section 5.1 we
introduce notions used in all four finite frame property proofs: two notions
of bisimulation and quotients with respect to such bisimulations. In Section
5.2 we prove the finite frame property for $\mathsf{GS4}$ (Theorem 4) by
taking bisimulation quotients of falsifying birelational models from the
corresponding class, relying on the soundness and completeness results of the
previous two sections. In Section 5.3 we prove the finite frame property for
$\mathsf{GS4^{c}}$ (Theorem 6) in a similar way. In Section 5.4 we show that
in order to prove the finite frame properties for $\mathsf{CS4}$ and
$\mathsf{S4I}$, it is sufficient to prove certain _shallow_ frame properties.
Then in Section 5.5 and Section 5.6 we prove the finite frame properties for
$\mathsf{CS4}$ (Theorem 7) and $\mathsf{S4I}$ (Theorem 8), respectively, by
showing how to construct shallow falsifying models by modifying the canonical
models.

We finish the paper with Section 6, drawing conclusions and discussing
potential future lines of research.

This paper is an extended version of the two conference papers [28] and [29].
In this version, we present new, more direct proofs of the finite frame
properties for $\mathsf{GS4}$ and $\mathsf{GS4^{c}}$. These new proofs
demonstrate that $\mathsf{GS4}$ and $\mathsf{GS4^{c}}$ are in nexptime
(Corollaries 2 and 3), which did not follow previously.

##  2 Syntax and semantics

In this section we first introduce the propositional modal language shared by
all the logics we are interested in. Then we define the logics themselves.
Finally, we present the various birelational or real-valued semantics for the
logics.

Fix a _countably infinite_ set $\mathbb{P}$ of propositional variables.777The
restriction to countable $\mathbb{P}$ can be a genuine restriction for
questions about entailment (see, for example, [25, Proposition 3.1]), but not
for validity, since formulas are finite. Then the intuitionistic modal
language ${\mathcal{L}}$ is defined by the grammar (in Backus–Naur form)

$\varphi,\psi\coloneqq\ p\ |\ \bot\ |\ \left(\varphi\wedge\psi\right)\ |\
\left(\varphi\vee\psi\right)\ |\
\left(\varphi\mathbin{\rightarrow}\psi\right)\ |\ \Diamond\varphi\ |\
\Box\varphi$

where $p\in\mathbb{P}$. We also use $\neg\varphi$ as shorthand for
$\varphi\mathbin{\rightarrow}\bot$ and $\varphi\leftrightarrow\psi$ as
shorthand for
$(\varphi\mathbin{\rightarrow}\psi)\wedge(\psi\mathbin{\rightarrow}\varphi)$.
As usual, the unary modalities bind tighter than the binary connectives; we
also assume that $\wedge$ and $\vee$ bind tighter than
$\mathbin{\rightarrow}$.

In this paper a logic means a set of formulas closed under substitution (by
formulas of the underlying language, which will always be ${\mathcal{L}}$).

###  2.1 Deductive calculi

We define the logics we are interested in syntactically, via Hilbert-style
deductive calculi.

######  Definition 1.

The logic $\mathsf{CS4}$ is the smallest logic containing all intuitionistic
tautologies and closed under the following axioms and rules.

  1. $\bm{\mathrm{K}_{\Box}}$

$\Box(p\mathbin{\rightarrow}q)\mathbin{\rightarrow}(\Box
p\mathbin{\rightarrow}\Box q)$

  2. $\bm{\mathrm{K}_{\Diamond}}$

$\Box(p\mathbin{\rightarrow}q)\mathbin{\rightarrow}(\Diamond
p\mathbin{\rightarrow}\Diamond q)$

[label=, label-width=3em,label-align = right](3) [$\bm{\mathrm{MP}}$]
$\dfrac{\varphi\mathbin{\rightarrow}\psi\hskip 10.0pt\varphi}{\psi}$
[$\bm{\mathrm{T}_{\Box}}$] $\Box p\mathbin{\rightarrow}p$
[$\bm{\mathrm{4}_{\Diamond}}$] $\Diamond\Diamond
p\mathbin{\rightarrow}\Diamond p$ [$\bm{\mathrm{Nec}}$]
$\dfrac{\varphi}{\Box\varphi}$ [$\bm{\mathrm{T}_{\Diamond}}$]
$p\mathbin{\rightarrow}\Diamond p$ [$\bm{\mathrm{4}_{\Box}}$] $\Box
p\mathbin{\rightarrow}\Box\Box p$

We now define the additional axioms

[label=, label-width=3em,label-align = right](2) [$\bm{\mathrm{DP}}$]
$\,\Diamond(p\vee q)\mathbin{\rightarrow}\Diamond p\vee\Diamond q$;
[$\bm{\mathrm{FS2}}$] $\,\left(\Diamond p\mathbin{\rightarrow}\Box
q\right)\rightarrow\Box\left(p\mathbin{\rightarrow}q\right)$;
[$\bm{\mathrm{CD}}$] $\,\Box(p\vee q)\mathbin{\rightarrow}\Box p\vee\Diamond
q$; [$\bm{\mathrm{N}}$] $\,\neg\Diamond\bot$;

[$\bm{\mathrm{GD}}$]
$\,(p\mathbin{\rightarrow}q)\vee(q\mathbin{\rightarrow}p)$. Here 2.1 stands
for ‘disjunctive possibility’, 2.1 for ‘Fischer Servi 2’ [30], 2.1 for
‘constant domain’, 2.1 for ‘nullary’, and 2.1 for ‘Gödel–Dummett’.

######  Definition 2.

The logics ${\mathsf{IS4}}$, ${\mathsf{S4I}}$, ${\mathsf{GS4}}$, and
${{\mathsf{GS4}}^{\mathsf{c}}}$ are defined similarly to ${\mathsf{CS4}}$,
with additional axioms as indicated in Figure 1.

$\displaystyle{\mathsf{IS4}}$
$\displaystyle={\mathsf{CS4}}+\ref{ax:dp}+\ref{ax:null}+\ref{ax:fs}$
$\displaystyle{\mathsf{S4I}}$
$\displaystyle={\mathsf{CS4}}+\ref{ax:dp}+\ref{ax:null}+\ref{ax:cd}$
$\displaystyle{\mathsf{GS4}}$ $\displaystyle={\mathsf{IS4}}+\ref{ax:g}$
$\displaystyle{{\mathsf{GS4}}^{\mathsf{c}}}$
$\displaystyle={\mathsf{GS4}}+\ref{ax:cd}={\mathsf{S4I}}+\ref{ax:fs}+\ref{ax:g}$

$\mathsf{CS4}$$\mathsf{IS4}$$\mathsf{GS4}$$\mathsf{GS4^{c}}$$\mathsf{S4I}$

Figure 1: Definition of logics considered and Hasse diagram for these logics

Thus $\mathsf{CS4}$ will serve as the ‘minimal’ logic for the purpose of this
paper, and the remaining logics we consider are extensions. We will see in
Section 3 that only the inclusions obtained directly from the definitions (and
displayed in Figure 1) hold.

We use the standard Gentzen-style notation that defines
$\Gamma\vdash_{\Lambda}\Delta$ to mean
$\bigwedge\Gamma^{\prime}\mathbin{\rightarrow}\bigvee\Delta^{\prime}\in\Lambda$
for some finite $\Gamma^{\prime}\subseteq\Gamma$ and
$\Delta^{\prime}\subseteq\Delta$. We call $\vdash_{\Lambda}$ the syntactic
consequence relation. The logic $\Lambda$ will usually be clear from context,
in which case we will not reflect it in the notation. When working with a
turnstile, we will follow the usual proof-theoretic conventions of writing
$\Gamma,\Delta$ instead of $\Gamma\cup\Delta$ and $\varphi$ instead of
$\\{\varphi\\}$.

###  2.2 Semantics

We will consider several semantics for our intuitionistic variants of
$\mathsf{S4}$, some of which are intuitionistic semantics (that is, featuring
intuitionistic frames) and some of which are real-valued semantics. For the
various intuitionistic semantics, it will be convenient to introduce a general
class of structures that includes each of these semantics as special cases.

######  Definition 3.

An intuitionistic frame is a triple $\mathcal{F}=(W,W^{\bot},{\preccurlyeq})$,
where $W$ is a set, $\preccurlyeq$ is a preorder (that is, a reflexive and
transitive binary relation) on $W$, and $W^{\bot}\subseteq W$ is closed under
$\preccurlyeq$, that is, whenever $w\in W^{\bot}$ and $w\preccurlyeq v$, we
also have that $v\in W^{\bot}$ [31]. We say that $\mathcal{F}$ is upward
linear if $w\preccurlyeq u$ and $w\preccurlyeq v$ implies that $u\preccurlyeq
v$ or $v\preccurlyeq u$.888With respect to the topology whose opens are the
up-closed sets, upward linear is equivalent to _locally linear_ (each point
has a linear neighbourhood), but this paper is not about topological
semantics, making _upward linear_ the more transparent term.

An birelational frame is a quadruple
$\mathcal{F}=(W,W^{\bot},{\preccurlyeq},R)$, where
$(W,W^{\bot},\allowbreak{\preccurlyeq})$ is an intuitionistic frame and
$(W,W^{\bot},R)$ is a Kripke frame in which $W^{\bot}$ is closed under $R$. It
is a bi-intuitionistic frame if both $(W,W^{\bot},{\preccurlyeq})$ and
$(W,W^{\bot},R)$ are intuitionistic frames. The frame $\mathcal{F}$ is upward
linear if $(W,W^{\bot},\allowbreak{\preccurlyeq})$ is upward linear.

The set $W^{\bot}$ is called the set of fallible worlds, as in [11, 31]. Note
that in a birelational frame, $W^{\bot}$ is closed under both $\preccurlyeq$
and $R$. When $W^{\bot}=\varnothing$ we omit it, and view $\mathcal{F}$ as a
triple $(W,{\preccurlyeq},R)$. In this case, we say that $\mathcal{F}$ is
infallible.

Given an birelational frame $\mathcal{F}=(W,W^{\bot},{\preccurlyeq},R)$, a
valuation on $\mathcal{F}$ is a function $V\colon\mathbb{P}\to 2^{W}$ that is
_monotone_ in the sense that each $V(p)$ is upward closed with respect to
$\preccurlyeq$ and includes $W^{\bot}$ (to ensure the validity of
$\bot\mathbin{\rightarrow}\varphi$).

We define the satisfaction relation $\models$ recursively by

  * •

$(\mathcal{M},w)\models p\in\mathbb{P}$ if $w\in V(p)$;

  * •

$(\mathcal{M},w)\models\bot$ if $w\in W^{\bot}$;

  * •

$(\mathcal{M},w)\models\varphi\wedge\psi$ if $(\mathcal{M},w)\models\varphi$
and $(\mathcal{M},w)\models\psi$;

  * •

$(\mathcal{M},w)\models\varphi\vee\psi$ if $(\mathcal{M},w)\models\varphi$ or
$(\mathcal{M},w)\models\psi$;

  * •

$(\mathcal{M},w)\models\varphi\mathbin{\rightarrow}\psi$ if for all
$v\succcurlyeq w$, $(\mathcal{M},v)\models\varphi$ implies
$(\mathcal{M},v)\models\psi$;

  * •

$(\mathcal{M},w)\models\Diamond\varphi$ if for all $u\succcurlyeq w$ there
exists $u\mathrel{R}v$ such that $(\mathcal{M},v)\models\varphi$;

  * •

$(\mathcal{M},w)\models\Box\varphi$ if for all $u,v$ such that $w\preccurlyeq
u\mathrel{R}v$, $(\mathcal{M},v)\models\varphi$.

It can be easily proved by induction on $\varphi$ that for all $w,v\in W$, if
$w\preccurlyeq v$ and $(\mathcal{M},w)\models\varphi$ then
$(\mathcal{M},v)\models\varphi$.

An birelational model is an birelational frame equipped with a valuation; if
the frame is a bi-intuitionistic frame, then we speak of a bi-intuitionistic
model. If $\mathcal{M}=(W,W^{\bot},{\preccurlyeq},R,V)$ is any model and
$\varphi$ any formula, we write $\mathcal{M}\models\varphi$ if
$(\mathcal{M},w)\models\varphi$ for every $w\in W$.

Validity is defined as one would expect, but is worth being precise about the
surrounding terminology and notation.

######  Definition 4.

Let $\mathsf{S}$ be any class of models or class of frames. Let $\Gamma$ be a
set of formulas and $\varphi$ a formula. We write
$\Gamma\models_{\mathsf{S}}\varphi$ and say that $\varphi$ is a local semantic
consequence of $\Gamma$ if, for each model $\mathcal{M}$ from $\mathsf{S}$ and
each $w\in\mathcal{M}\setminus W^{\bot}$, we have

$\forall\psi\in\Gamma,(\mathcal{M},w)\models\psi\implies(\mathcal{M},w)\models\varphi.$

We say that $\varphi$ is valid on $\mathsf{S}$ if
$\models_{\mathsf{S}}\varphi$ (that is, if
$\varnothing\models_{\mathsf{S}}\varphi$; we may also write
$\mathsf{S}\models\varphi$), and falsifiable otherwise. We say that $\varphi$
is satisfiable on $\mathsf{S}$ if $\varphi\not\models_{\mathsf{S}}\bot$. This
terminology extends also to single models or frames.

######  Definition 5 (strongly complete).

Let $\mathsf{S}$ be a class of frames or class of models. A logic $\Lambda$ is
said to be _strongly complete_ with respect to $\mathsf{S}$ if for any set of
formulas $\Gamma$ and for any formula $\varphi$, if
$\Gamma\models_{\mathsf{S}}\varphi$ then $\Gamma\vdash_{\Lambda}\varphi$.

Since this paper is only concerned with constructive analogues of
$\mathsf{S4}$, we will only be working with birelational frames that are bi-
intuitionistic frames. Note, however, that even the class of bi-intuitionistic
frames does not validate some of the $\mathsf{S4}$ axioms, as the following
example shows.

######  Example 1.

Consider the bi-intuitionistic model
$\mathcal{M}=(W,{\preccurlyeq},{\sqsubseteq},V)$, whose corresponding frame is
displayed in Figure 2, with $V(p)=\\{x,y,z,t\\}$. Note that we omit
$W^{\bot}$: by convention, this means that $W^{\bot}=\varnothing$.

$x$$y$$z$$t$$w$ Figure 2: A bi-intuitionistic frame. Plain lines for
$\preccurlyeq$; arrows for $\sqsubseteq$. (Reflexive lines and arrows not
displayed)

Since $p$ is satisfied at $x$, $y$, and $z$, we have
$(\mathcal{M},x)\models\Box p$. But since $p$ is not satisfied at $w$, we have
$(\mathcal{M},z)\not\models\Box p$, and thus
$(\mathcal{M},x)\not\models\Box\Box p$. Hence $(\mathcal{M},x)\not\models\Box
p\mathbin{\rightarrow}\Box\Box p$, and therefore 1 is not valid on the class
of all bi-intuitionistic frames.

In order to make 1 valid, it is necessary to enforce additional constraints
governing the interaction between $\preccurlyeq$ and $\sqsubseteq$. There are
various properties that have been used to this end.

######  Definition 6.

Let $\mathcal{F}=(W,W^{\bot},{\preccurlyeq})$ be an intuitionistic frame and
$R\subseteq W\times W$. We say that $R$ is:

  1. (i)

forth–up confluent (for $\mathcal{F}$) if, whenever $w\preccurlyeq w^{\prime}$
and $w\mathrel{R}v$, there is $v^{\prime}$ such that $v\preccurlyeq
v^{\prime}$ and $w^{\prime}\mathrel{R}v^{\prime}$;

  2. (ii)

back–up confluent (for $\mathcal{F}$) if, whenever $w\mathrel{R}v\preccurlyeq
v^{\prime}$, there is $w^{\prime}$ such that $w\preccurlyeq
w^{\prime}\mathrel{R}v^{\prime}$;

  3. (iii)

forth–down confluent (for $\mathcal{F}$) if, whenever $w\preccurlyeq
v\mathrel{R}v^{\prime}$, there is $w^{\prime}$ such that
$w\mathrel{R}w^{\prime}\preccurlyeq v^{\prime}$.

Figure 3 depicts the confluence conditions. A bi-intuitionistic frame
$\mathcal{F}=(W,\allowbreak W^{\bot},\allowbreak{\preccurlyeq},{\sqsubseteq})$
is forth–up confluent (respectively, back–up confluent, forth–down confluent)
if $\sqsubseteq$ is forth–up confluent (respectively, back–up confluent,
forth–down confluent) for $(W,W^{\bot},{\preccurlyeq})$.

forth–up$\preccurlyeq$$\preccurlyeq$$R$$R$

back–up$\preccurlyeq$$\preccurlyeq$$R$$R$

forth–down$\preccurlyeq$$\preccurlyeq$$R$$R$

Figure 3: Confluence conditions

The notions of forth–up and forth–down confluence allow us to simplify the
semantic clauses for $\Diamond$ and $\Box$, respectively.

######  Lemma 1.

Let $\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$ be any bi-
intuitionistic model, $w\in W$ and $\varphi\in{\mathcal{L}}$.

  1. 1.

If $\mathcal{M}$ is forth–up confluent, then
$(\mathcal{M},w)\models\Diamond\varphi$ if and only if $\exists v\sqsupseteq
w$ such that $(\mathcal{M},v)\models\varphi$.

  2. 2.

If $\mathcal{M}$ is forth–down confluent, then
$(\mathcal{M},w)\models\Box\varphi$ if and only if $\forall v\sqsupseteq w$ we
have $(\mathcal{M},v)\models\varphi$.

###### Proof.

We prove the second claim; the first is proven similarly by dualising. It
follows immediately from the semantics of $\Box$ (and reflexivity of
$\preccurlyeq$) that if $(\mathcal{M},w)\models\Box\varphi$ and $v\sqsupseteq
w$, then $(\mathcal{M},v)\models\varphi$. Conversely, suppose that $\forall
v\sqsupseteq w$, we have $(\mathcal{M},v)\models\varphi$. Let $u\succcurlyeq
w$ and $u^{\prime}\sqsupseteq u$. By forth–down confluence, there is
$w^{\prime}\sqsupseteq w$ with $w^{\prime}\preccurlyeq u^{\prime}$. By our
assumption, $(\mathcal{M},w^{\prime})\models\varphi$. By monotonicity of the
satisfaction relation, $(\mathcal{M},u^{\prime})\models\varphi$. Since $u$ and
$u^{\prime}$ were arbitrary subject to $u\succcurlyeq w$ and
$u^{\prime}\sqsupseteq u$, we conclude that
$(\mathcal{M},w)\models\Box\varphi$. ∎

######  Definition 7.

We define the following classes of birelational frames.

  1. 1.

The class of $\mathsf{CS4}$ frames is the class of back–up confluent bi-
intuitionistic frames.

  2. 2.

The class of $\mathsf{IS4}$ frames is the class of forth–up confluent,
infallible $\mathsf{CS4}$ frames.

  3. 3.

The class of $\mathsf{S4I}$ frames is the class of forth–up and forth–down
confluent, infallible bi-intuitionistic frames.

  4. 4.

The class of $\mathsf{GS4}$ frames is the class of upward-linear
$\mathsf{IS4}$ frames.

  5. 5.

The class of ${\mathsf{GS4}}^{\mathsf{c}}$ frames is the class of forth–down
confluent $\mathsf{GS4}$ frames.

In the following sections, we will see that these names are appropriate, in
the sense that the valid formulas of each class are precisely the logics they
are named after.

For Gödel logics, alternative semantics are possible, which view the logics as
fuzzy logics.

######  Definition 8.

A real-valued (Kripke) frame is a pair $\mathcal{F}=(W,R)$, where $W$ is a set
and ${R}\colon W\times W\mapsto[0,1]$ is a function. It is reflexive if for
all $w\in W$ we have $R(w,w)=1$. It is transitive if for all $u,v,w\in W$ we
have $R(u,w)\geq\min\\{R(u,v),R(v,w)\\}$. If ${R}\colon W\times
W\mapsto\\{0,1\\}$ we will say the frame is accessibility crisp.

A (Gödel) valuation on $\mathcal{F}$ is a function $V_{\cdot}(\cdot)\colon
W\times{\mathcal{L}}\to\mathbb{R}$ such that, for all $w\in W$,

$\displaystyle V_{w}(\bot)$ $\displaystyle=0,$ $\displaystyle
V_{w}(\varphi\wedge\psi)$
$\displaystyle=\min\\{V_{w}(\varphi),V_{w}(\psi)\\},$ $\displaystyle
V_{w}(\varphi\vee\psi)$ $\displaystyle=\max\\{V_{w}(\varphi),V_{w}(\psi)\\},$
$\displaystyle V_{w}(\varphi\mathbin{\rightarrow}\psi)$
$\displaystyle=\begin{cases}1&\text{if }V_{w}(\varphi)\leq V_{w}(\psi)\\\
V_{w}(\psi)&\text{otherwise}\end{cases}$ $\displaystyle
V_{w}(\Diamond\varphi)$ $\displaystyle=\sup_{v\in
W}\\{\min\\{R(w,v),V_{v}(\varphi)\\}\\},$ $\displaystyle V_{w}(\Box\varphi)$
$\displaystyle=\inf_{v\in W}\\{1\hbox{ if }R(w,v)\leq
V_{v}(\varphi);V_{v}(\varphi)\hbox{ otherwise}\\}.$

A real-valued Kripke frame equipped with a Gödel valuation is a Gödel–Kripke
model, and an accessibility-crisp frame equipped with a valuation is a
accessibility-crisp model.

######  Definition 9.

Let $\mathsf{S}$ be any class of Gödel–Kripke models or class of real-valued
frames. Let $\Gamma$ be a set of formulas and $\varphi$ a formula. We write
$\Gamma\models_{\mathsf{S}}\varphi$ and say that $\varphi$ is a local semantic
consequence of $\Gamma$ if, for each model $\mathcal{M}$ from $\mathsf{S}$ and
each $w\in\mathcal{M}$, we have

$\forall\psi\in\Gamma,V_{w}(\psi)=1\implies V_{w}(\varphi)=1.$ (1)

We say that $\varphi$ is valid on $\mathsf{S}$ if
$\models_{\mathsf{S}}\varphi$ (that is,
$\varnothing\models_{\mathsf{S}}\varphi$), and falsifiable otherwise. This
terminology extends also to single models or frames.

The definition (1) of local semantic consequence is taken from [25]. By a
simple ‘truncate the truth values’ argument, over classes of _frames_ this
definition is equivalent to the _a priori_ stronger condition
$V_{w}(\varphi)\geq\inf\\{V_{w}(\psi)\mid\psi\in\Gamma\\}$.

The logics $\mathsf{GS4}$ and ${\mathsf{GS4}}^{\mathsf{c}}$ are known to be
strongly complete with respect to local semantic consequence on classes of
real-valued frames.

######  Theorem 1.

(Caicedo and Rodríguez). Let $\models_{\mathsf{FS4}}$ denote local semantic
consequence on the class of reflexive transitive real-valued frames, and
$\vdash_{\mathsf{GS4}}$ denote the syntactic consequence relation for the
logic $\mathsf{GS4}$. Then

$\Gamma\models_{\mathsf{FS4}}\varphi\iff\Gamma\vdash_{\mathsf{GS4}}\varphi.$
([25, Theorem 5.1(ii)])

(Rodríguez and Vidal). Let $\models_{\mathsf{cFS4}}$ denote local semantic
consequence on the class of reflexive transitive accessibility-crisp frames,
and $\vdash_{\mathsf{GS4^{c}}}$ denote the syntactic consequence relation for
the logic $\mathsf{GS4^{c}}$. Then

$\Gamma\models_{\mathsf{cFS4}}\varphi\iff\Gamma\vdash_{\mathsf{GS4^{c}}}\varphi.$
([26, Theorem 5.4])

Note that Theorem 1 would not be true if the set of propositional variables
were uncountable, even for the modality-free fragment [25, Proposition 3.1].

The logic $\mathsf{CS4}$ was introduced in [11] motivated by syntactic
considerations. In the same paper, the class of $\mathsf{CS4}$ frames was
defined in order to provide a semantics. A proof of the strong completeness of
$\mathsf{CS4}$ with respect to the $\mathsf{CS4}$ frames is sketched in [11].
We provide a full proof of this fact in Section 4. The logic $\mathsf{IS4}$
was introduced by Fischer Servi in [30], where the logic was proven complete
with respect to $\mathsf{IS4}$ frames. The logics $\mathsf{GS4}$ and
$\mathsf{GS4^{c}}$ were introduced in [25] and [26], respectively, in order to
obtain the completeness results of Theorem 1.999The axioms and rules in [25,
Theorem 5.1(ii)] are slightly different to those we use to define
$\mathsf{GS4}$, but are proven equivalent in [25, Lemma 2.1].

Regarding $\mathsf{S4I}$, it is easy to check that
$(W,{\preccurlyeq},{\sqsubseteq})$ is an $\mathsf{S4I}$ frame if and only if
$(W,{\sqsubseteq},{\preccurlyeq})$ is an $\mathsf{IS4}$ frame, so this could
be viewed as ‘commuting’ the roles of $\mathsf{S4}$ and intuitionistic logic
(which we may denote $\mathsf{I}$). In fact, in the context of expanding
products of modal logics, $\mathsf{IS4}$ frames are similar to
$\mathsf{I}\times^{e}\mathsf{S4}$ frames, where $\times^{e}$ is the ‘expanding
product’ as defined in [32], and similarly, $\mathsf{S4I}$ frames can be
regarded as $\mathsf{S4}\times^{e}\mathsf{I}$ frames. Additionally, in view of
Lemma 1, the $\mathsf{S4I}$ conditions give us the advantage of being able to
evaluate $\Diamond$ and $\Box$ classically.

##  3 Soundness

In this section we establish the soundness of the logics $\mathsf{CS4}$,
$\mathsf{IS4}$, $\mathsf{S4I}$, $\mathsf{GS4}$, and $\mathsf{GS4^{c}}$, with
respect to the corresponding classes of bi-intuitionistic frames. Using the
soundness results, we also note that these five logics are all distinct and
related exactly as shown in Figure 1.

It will be useful distinguish the following type of frame. We call a frame
$\Diamond$-regular if it is forth–up confluent and infallible. Accordingly, a
logic is $\Diamond$-regular if it extends $\mathsf{CS4}$ and contains Axioms
2.1 and 2.1. Essentially, on $\Diamond$-regular frames, $\Diamond$ works as
one would expect from classical modal logic. The only logic we consider that
is not $\Diamond$-regular is $\mathsf{CS4}$.

We first list some formulas that are valid over frame classes that need not be
$\Diamond$-regular. Of course the validities of any class of birelational
frames are closed under substitution.

######  Proposition 1.

  1. (1)

Axioms $\bm{\mathrm{K}_{\Box}}$ and $\bm{\mathrm{K}_{\Diamond}}$ are valid,
and the inference rules 1 and 1 preserve validity, over any class of
birelational frames.

  2. (2)

Axioms 1, 1, and 1 are valid over the class of bi-intuitionistic frames.

  3. (3)

Axiom 1 is valid over any bi-intuitionistic frame that is either back–up
confluent or forth–down confluent.

  4. (4)

Axiom 2.1 is valid over the class of upward-linear frames.

###### Proof.

Items (1) and (2) are standard (and see for example [10]). We check only 1.
Let $\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$ be any bi-
intuitionistic model. Suppose that $(\mathcal{M},w)\models\Diamond\Diamond p$
and let $v\succcurlyeq w$. Then there exists $u\sqsupseteq v$ such that
$(\mathcal{M},u)\models\Diamond p$. Then since $u\succcurlyeq u$, there exists
$u^{\prime}\sqsupseteq u$ such that $(\mathcal{M},u^{\prime})\models p$. By
transitivity, $u^{\prime}\sqsupseteq v$, and as $v$ was arbitrary subject to
$v\succcurlyeq w$, we conclude that $(\mathcal{M},w)\models\Diamond p$.

For item (3), the case for back–up confluence is known, as such a frame is a
$\mathsf{CS4}$ frame [11]. If instead
$\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$ is forth–down
confluent, we have by Lemma 1 that for any $w\in W$,
$(\mathcal{M},w)\models\Box p$ if and only if $\forall v\sqsupseteq w$,
$(\mathcal{M},v)\models p$. Using this characterisation, we may reason as in
the classical case to deduce $\mathcal{M}\models\Box
p\mathbin{\rightarrow}\Box\Box p$ from the transitivity of $\sqsubseteq$.

Item (4) is also well known, but we provide a proof. Assume for a
contradiction that 2.1 is not valid on the class of ${\mathsf{GS4}}$ frames.
This means that $(\mathcal{M},w)\not\models p\mathbin{\rightarrow}q$ and
$(\mathcal{M},w)\not\models p\mathbin{\rightarrow}q$ for some model
$\mathcal{M}$ based on a ${\mathsf{GS4}}$ frame and $w\in W$. From the former
assumption it follows that there is $v\succcurlyeq w$ such that
$(\mathcal{M},v)\models p$ and $(\mathcal{M},v)\not\models q$. From the latter
assumption it follows that there is $v^{\prime}\succcurlyeq w$ such that
$(\mathcal{M},v^{\prime})\models q$ and $(\mathcal{M},v^{\prime})\not\models
p$. Since ${\mathcal{M}}$ is upward linear, we need to consider two cases: if
$v\preccurlyeq v^{\prime}$ we get that $(\mathcal{M},v^{\prime})\models p$; if
$v^{\prime}\preccurlyeq v$ we conclude that $(\mathcal{M},v)\models q$. In
either case we reach a contradiction. ∎

Note that with (1), (2), and (3), we have confirmed the soundness of the logic
$\mathsf{CS4}$ with respect to the class of $\mathsf{CS4}$ frames.

Next we consider $\Diamond$-regular classes.

######  Proposition 2.

Let $\mathfrak{C}$ be any class of $\Diamond$-regular bi-intuitionistic
frames.

  1. (a)

Axiom 2.1 is valid on $\mathfrak{C}$.

  2. (b)

Axiom 2.1 is valid on $\mathfrak{C}$.

  3. (c)

If the frames of $\mathfrak{C}$ are back–up confluent, then Axiom 2.1 is valid
on $\mathfrak{C}$.

  4. (d)

If the frames of $\mathfrak{C}$ are forth–down confluent, then Axiom 2.1 is
valid on $\mathfrak{C}$.

###### Proof.

Item (a) is a straightforward consequence of infallibility. Item (b) is easily
derived from Lemma 1.1, since satisfaction of $\Diamond(p\vee q)$ requires a
single witness, which is then sufficient to witness either $\Diamond p$ or
$\Diamond q$. Item (c) is proven in [10].

For (d), assume that $\mathcal{M}$ is forth–up and forth–down confluent, and
that $(\mathcal{M},w)\models\Box\left(\varphi\vee\psi\right)$. If
$(\mathcal{M},w)\models\Box\varphi$, there is nothing to prove, so assume that
$(\mathcal{M},w)\not\models\Box\varphi$. From Lemma 1.2 it follows that there
is $v\sqsupseteq w$ such that $(\mathcal{M},v)\not\models\varphi$. But
$(\mathcal{M},v)\models\varphi\vee\psi$, so $(\mathcal{M},v)\models\psi$, and
from Lemma 1.1 we obtain $(\mathcal{M},w)\models\Diamond\psi$. ∎

Given the soundness of $\mathsf{CS4}$ (with respect to any of our frame
classes), to verify the soundness of the remaining logics with respect to
their corresponding frame classes, it suffices to check the remaining axioms
in the definition of the logics. Examining Definition 2, we see that we have
soundness of:

$\mathsf{IS4}\phantom{{}^{c}}$

by (a), (b), and (c),

$\mathsf{S4I}\phantom{{}^{c}}$

by (a), (b), and (d),

then building on the soundness of $\mathsf{IS4}$:

$\mathsf{GS4}\phantom{{}^{c}}$

by Proposition 1(4),

then

${\mathsf{GS4}}^{\mathsf{c}}$

by (d).

Thus we obtain the following.

######  Corollary 1.

Each of $\mathsf{CS4}$, $\mathsf{IS4}$, $\mathsf{S4I}$, $\mathsf{GS4}$, and
${\mathsf{GS4}}^{\mathsf{c}}$ is sound for its respective class of frames.

To end this section, we now verify that the inclusions among our logics are
exactly as depicted by the Hasse diagram in Figure 1. With the exception of
comparisons involving $\mathsf{S4I}$, these relationships are all well known.
First we show that the marked inclusions are proper. In each case, we exhibit
a formula contained in the larger logic but falsified on the frame class
corresponding to smaller logic. By soundness of the smaller logic, it does not
contain the formula.

####  $\mathsf{IS4}\not\subseteq\mathsf{CS4}$ and
$\mathsf{S4I}\not\subseteq\mathsf{CS4}$

By definition, $\ref{ax:null}\in\mathsf{IS4}$ and
$\ref{ax:null}\in\mathsf{S4I}$. Consider the bi-intuitionistic frame
$(\\{i,f\\},\\{f\\},\\{(i,i),\allowbreak(f,f)\\},\\{(i,i),(f,f),(i,f)\\})$
depicted on the top left of Figure 4. This frame is back–up confluent and thus
a $\mathsf{CS4}$ frame. The infallible world $i$ satisfies $\Diamond\bot$
(under any valuation), and so falsifies $\neg\Diamond\bot$.

####  $\mathsf{GS4}\not\subseteq\mathsf{IS4}$ and
$\mathsf{GS4^{c}}\not\subseteq\mathsf{S4I}$

By definition, $\ref{ax:g}\in\mathsf{GS4}$ and
$\ref{ax:g}\in\mathsf{GS4^{c}}$. Consider the infallible bi-intuitionistic
model depicted on the top right of Figure 4, where $p$ and $q$ are
propositional variables. As $\sqsubseteq$ is trivial, the frame validates all
confluence conditions and in particular is both an $\mathsf{IS4}$ frame and an
$\mathsf{S4I}$ frame. The world at the bottom falsifies
$(p\mathbin{\rightarrow}q)\vee(q\mathbin{\rightarrow}p)$.

#### $\mathsf{GS4^{c}}\not\subseteq\mathsf{GS4}$

By definition, $\ref{ax:cd}\in\mathsf{GS4^{c}}$. Consider the infallible bi-
intuitionistic model depicted on the bottom left of Figure 4. It is easy to
check that the frame is back–up confluent, forth–up confluent, and upward
linear, and thus is a $\mathsf{GS4}$ frame. The world at the bottom satisfies
$\Box(p\wedge q)$ but neither $\Box p$ nor $\Diamond q$, and thus falsifies
2.1.

Finally we verify the incomparability of $\mathsf{S4I}$ with either
$\mathsf{IS4}$ or $\mathsf{GS4}$.

#### $\mathsf{S4I}\not\subseteq\mathsf{GS4}$

By definition, $\ref{ax:cd}\in\mathsf{S4I}$. As we have just seen,
$\ref{ax:cd}\not\in\mathsf{GS4}$.

#### $\mathsf{IS4}\not\subseteq\mathsf{S4I}$

By definition, $\ref{ax:fs}\in\mathsf{IS4}$. Consider the infallible bi-
intuitionistic model depicted on the bottom right of Figure 4. It is easy to
check that the frame is back–up confluent and forth–up confluent, and thus is
a $\mathsf{S4I}$ frame. The bottom left world falsifies $\Diamond p$ and thus
satisfies $\Diamond p\mathbin{\rightarrow}\Box q$. But the same world does not
satisfy $\Box(p\mathbin{\rightarrow}q)$ and thus falsifies 2.1.

$i$$f$$\sqsubseteq$$W^{\bot}$

$p$$q$$\preccurlyeq$$\preccurlyeq$

$p$$p,q$$q$$\preccurlyeq$$\sqsubseteq$

$p$$\sqsubseteq$$\preccurlyeq$

Figure 4: Frames and models separating the logics. (Reflexive arrows not
displayed)

##  4 Strong completeness

In this section, we prove the strong completeness of each of the logics
$\mathsf{CS4}$, $\mathsf{IS4}$, $\mathsf{S4I}$, $\mathsf{GS4}$, and
${\mathsf{GS4}}^{\mathsf{c}}$ with respect to its corresponding birelational
semantics.

It will be convenient to observe that the following formulas are contained in
$\mathsf{CS4}$, and thus also its extensions $\mathsf{IS4}$, $\mathsf{S4I}$,
$\mathsf{GS4}$, and ${\mathsf{GS4}}^{\mathsf{c}}$. We leave the proofs to the
reader.

######  Proposition 3.

The following formulas belong to ${\mathsf{CS4}}$.

  1. (1)

$\Diamond{\left(p\rightarrow q\right)}\rightarrow\left(\Box
p\rightarrow\Diamond q\right)$,101010This is the first of Fischer Servi’s two
_connecting axioms_ [30].

  2. (2)

$\Diamond\left(p\wedge q\right)\rightarrow\Diamond p\wedge\Diamond q$,

  3. (3)

$\Box p\wedge\Box q\rightarrow\Box\left(p\wedge q\right)$,

  4. (4)

$\Box p\vee\Box q\rightarrow\Box\left(p\vee q\right)$.

###  4.1 Prime theories

We first introduce the notions common to all our completeness proofs. Fix a
logic $\Lambda$. At the moment we only need to assume that $\Lambda$ is a
logic and that it includes intuitionistic logic and the axiom 1.

A set $\Gamma$ of ${\mathcal{L}}$-formulas is called a theory if it is closed
under syntactic consequence ($\Gamma\vdash\varphi$ implies
$\varphi\in\Gamma$). Further, we say that $\Gamma$ is prime if
$\varphi\vee\psi\in\Gamma$ implies that either $\varphi\in\Gamma$ or
$\psi\in\Gamma$.

######  Definition 10.

Given sets $\Phi$ and $\Xi$ of formulas, we say that $\Phi$ is
$\Xi$-consistent if $\Phi\not\vdash\Xi$. We say that $\Phi$ is consistent if
it is $\varnothing$-consistent (with the understanding that
$\bigvee\varnothing\equiv\bot$). If $\Xi$ is a singleton $\\{\xi\\}$, we write
$\xi$-consistent instead of $\\{\xi\\}$-consistent.

Note that if $\Phi$ is $\Xi$-consistent, then necessarily $\bot\not\in\Phi$.
We say that $\Psi$ extends $\Phi$ if $\Phi\subseteq\Psi$.

######  Lemma 2.

Any $\Xi$-consistent set $\Phi$ of formulas can be extended to a
$\Xi$-consistent prime theory $\Phi_{*}$.

###### Proof.

By a standard application of Zorn’s lemma, there exists a maximal (with
respect to set inclusion) set of formulas $\Phi_{*}\supseteq\Phi$ such that
$\Phi_{*}$ is $\Xi$-consistent. Using some intuitionistic reasoning, it is
easy to see that $\Phi_{*}$ is closed under $\vdash$ and is thus a theory. To
see that $\Phi_{*}$ is prime, suppose that $\varphi\vee\psi\in\Phi_{*}$. We
cannot have that $\Phi_{*}\cup\\{\varphi\\}$ and $\Phi_{*}\cup\\{\psi\\}$ are
both $\Xi$-inconsistent, since by left disjunction introduction (formalisable
as a theorem of intuitionistic logic) we would obtain that
$\Phi_{*},\varphi\vee\psi$ is $\Xi$-inconsistent. However,
$\Phi_{*},\varphi\vee\psi$ is just $\Phi_{*}$, contrary to assumption. Thus
either $\Phi_{*},\varphi$ or $\Phi_{*},\psi$ is $\Xi$-consistent; say,
$\Phi_{*},\varphi$. But then by maximality of $\Phi_{*}$, we must already have
$\varphi\in\Phi_{*}$, as required. ∎

If $\Phi$ is a theory then we define

$\displaystyle\Phi^{\Box}$
$\displaystyle\coloneqq\\{\varphi\in{\mathcal{L}}\mid\Box\varphi\in\Phi\\},$
$\displaystyle\Phi^{\Diamond}$
$\displaystyle\coloneqq\\{\varphi\in{\mathcal{L}}\mid\Diamond\varphi\notin\Phi\\}.$

###  4.2 Completeness of $\Diamond$-regular logics

In this subsection we show that the $\Diamond$-regular logics we consider are
strongly complete, using standard canonical model arguments. In this setting,
we may uniformly define the canonical model for any $\Diamond$-regular logic
$\Lambda$.

######  Definition 11.

Let $\Lambda$ be a $\Diamond$-regular logic. We define the canonical model for
$\Lambda$ as
$\mathcal{M}_{\mathrm{c}}^{\Lambda}=(W_{\mathrm{c}},{\preccurlyeq_{\mathrm{c}}},{\sqsubseteq_{\mathrm{c}}},V_{\mathrm{c}})$,
where

  1. a)

$W_{\mathrm{c}}$ is the set of consistent prime $\Lambda$-theories,

  2. b)

${\preccurlyeq_{\mathrm{c}}}\subseteq W_{\mathrm{c}}\times W_{\mathrm{c}}$ is
defined by $\Phi\preccurlyeq_{\mathrm{c}}\Psi$ if and only if
$\Phi\subseteq\Psi$,

  3. c)

${\sqsubseteq_{\mathrm{c}}}\subseteq W_{\mathrm{c}}\times W_{\mathrm{c}}$ is
defined by $\Phi\sqsubseteq_{\mathrm{c}}\Psi$ if and only if
$\Phi^{\Box}\subseteq\Psi$ and $\Phi^{\Diamond}\cap\Psi=\varnothing$,

  4. d)

$V_{\mathrm{c}}\colon\mathbb{P}\to 2^{W_{\mathrm{c}}}$ is defined by
$V_{\mathrm{c}}(p):=\\{\Phi\in W_{\mathrm{c}}\mid p\in\Phi\\}$.

As we will see, this construction always yields $\Diamond$-regular models,
given the assumption that $\Lambda$ is $\Diamond$-regular.

######  Lemma 3.

If $\Lambda$ is any $\Diamond$-regular logic, then
$\mathcal{M}^{\Lambda}_{\mathrm{c}}$ is a $\Diamond$-regular bi-intuitionistic
model.

###### Proof.

It is immediate from the definition that $\preccurlyeq_{\mathrm{c}}$ is a
preorder. It is also straightforward to show, using Axioms 1 and 1, that
$\sqsubseteq_{\mathrm{c}}$ is a preorder, so we focus on showing that
$\mathcal{M}^{\Lambda}_{\mathrm{c}}$ is forth–up confluent.

Let $\Phi$, $\Psi$, and $\Theta$ in $W_{\mathrm{c}}$ be such that
$\Phi\preccurlyeq_{\mathrm{c}}\Psi$ and $\Phi\sqsubseteq_{\mathrm{c}}\Theta$.
We claim that $\Psi^{\Box}\cup\Theta$ is $\Diamond\Psi^{\Diamond}$-consistent.
If not, there exist $\varphi\in\Psi^{\Box}$, $\theta\in\Theta$, and
$\psi\in\Psi^{\Diamond}$ such that
$\varphi\wedge\theta\rightarrow\Diamond\psi\in\mathsf{GS4}$. (Note that we can
take single formulas since $\Theta$ is closed under conjunction; by
Proposition 3(3), $\Psi^{\Box}$ is too; and in view of 2.1 and precision of
$\Psi$, we know $\Psi^{\Diamond}$ is closed under disjunction.) Since
$\theta\in\Theta$, we then obtain $\varphi\rightarrow\Diamond\psi\in\Theta$.
Then by Axiom 1, we get
$\Diamond\left(\varphi\rightarrow\Diamond\psi\right)\in\Theta$. Therefore
$\varphi\rightarrow\Diamond\psi\not\in\Theta^{\Diamond}$, so
$\varphi\rightarrow\Diamond\psi\not\in\Phi^{\Diamond}$, and hence
$\Diamond\left(\varphi\rightarrow\Diamond\psi\right)\in\Phi$. Using
Proposition 3(1) we get $\Box\varphi\rightarrow\Diamond\Diamond\psi\in\Phi$.
Since $\Phi^{+}\subseteq\Psi^{+}$ this gives
$\Box\varphi\rightarrow\Diamond\Diamond\psi\in\Psi$. As
$\varphi\in\Psi^{\Box}$, we deduce $\Diamond\Diamond\psi\in\Psi$. By Axiom 1,
this contradicts the consistency of $\Phi$.

In view of Lemma 2, $\Psi^{\Box}\cup\Theta$ can be extended to a
$\Diamond\Psi^{\Diamond}$-consistent prime theory $\Upsilon$. It is easy to
check by our choice of $\Upsilon$ that $\Psi\sqsubseteq_{\mathrm{c}}\Upsilon$
and $\Theta\preccurlyeq_{\mathrm{c}}\Upsilon$. ∎

######  Lemma 4.

Let $\Lambda$ be any $\Diamond$-regular logic.

  1. 1.

If $\ref{ax:fs}\in\Lambda$, then $\mathcal{M}^{\Lambda}_{\mathrm{c}}$ is
back–up confluent.

  2. 2.

If $\ref{ax:cd}\in\Lambda$, then $\mathcal{M}^{\Lambda}_{\mathrm{c}}$ is
forth–down confluent.

###### Proof.

For the first item, suppose that
$\Phi\sqsubseteq_{\mathrm{c}}\Psi\preccurlyeq_{\mathrm{c}}\Theta$, and let
$\Xi\coloneqq\\{\Box\xi\in{\mathcal{L}}\mid\xi\notin\Theta\\}$ and
$\Delta=\\{\Diamond\delta\in{\mathcal{L}}\mid\Diamond\delta\in\Theta\\}$. We
claim that $\Phi\cup\Delta$ is $\Xi$-consistent. If not, there are
$\varphi\in\Phi$, $\Diamond\delta_{1},\ldots,\Diamond\delta_{n}\in\Delta$, and
$\Box\xi\in\Xi$ such that
$\varphi,\\{\Diamond\delta_{i}\\}_{i=1}^{n}\vdash\Box\xi$, which using 1
yields
$\varphi\vdash\bigwedge_{i=1}^{n}\Diamond\Diamond\delta_{i}\mathbin{\rightarrow}\Box\xi$.
Then using Proposition 3(2) we can obtain
$\varphi\vdash\Diamond\bigwedge_{i=1}^{n}\Diamond\delta_{i}\mathbin{\rightarrow}\Box\xi$.
By an application of 2.1, we obtain
$\varphi\vdash\Box\left(\bigwedge_{i=1}^{n}\Diamond\delta_{i}\mathbin{\rightarrow}\xi\right)$.
Then since $\varphi\in\Phi$, we obtain
$\Box\left(\bigwedge_{i=1}^{n}\Diamond\delta_{i}\mathbin{\rightarrow}\xi\right)\in\Phi$.
Since $\Phi\sqsubseteq_{\mathrm{c}}\Psi$, we get
$\bigwedge_{i=1}^{n}\Diamond\delta_{i}\mathbin{\rightarrow}\xi\in\Psi$, and
since $\Psi\preccurlyeq_{\mathrm{c}}\Theta$ and each
$\Diamond\delta_{i}\in\Theta$, we get $\xi\in\Theta$, contradicted by the
definition of $\Xi$. Hence $\Phi\cup\Delta$ is $\Xi$-consistent.

Let $\Upsilon$ be any $\Xi$-consistent prime extension of $\Phi\cup\Delta$.
Then $\Phi\preccurlyeq_{\mathrm{c}}\Upsilon\sqsubseteq_{\mathrm{c}}\Theta$:
that $\Phi\preccurlyeq_{\mathrm{c}}\Upsilon$ follows from
$\Phi\subseteq\Upsilon$, and we check that
$\Upsilon\sqsubseteq_{\mathrm{c}}\Theta$. We have
$\Upsilon^{\Box}\subseteq\Theta$, since if $\xi\notin\Theta$ it follows by the
definition of $\Xi$ and the fact that $\Upsilon$ is $\Xi$-consistent that
$\xi\notin\Upsilon^{\Box}$, while if $\delta\notin\Theta^{\Diamond}$ it
follows that $\Diamond\delta\in\Theta$; hence
$\Diamond\delta\in\Delta\subseteq\Upsilon$ and
$\delta\notin\Upsilon^{\Diamond}$. It follows that
$\Upsilon^{\Diamond}\subseteq\Theta^{\Diamond}$, so
$\Upsilon\sqsubseteq_{\mathrm{c}}\Theta$.

For the second item, suppose that
$\Phi\preccurlyeq_{\mathrm{c}}\Psi\sqsubseteq_{\mathrm{c}}\Theta$. Let
$\Xi={\mathcal{L}}\setminus\Theta$. We claim that $\Phi^{\Box}$ is
$\Diamond\Phi^{\Diamond}\cup\Xi$-consistent. If not, there exist
$\Box\varphi\in\Phi$, $\Diamond\psi\not\in\Phi$, and $\chi\not\in\Theta$ such
that $\varphi\rightarrow\chi\vee\Diamond\psi\in\Lambda$. By 1, Axiom
$\bm{\mathrm{K}_{\Box}}$ and 1 we get that
$\Box\varphi\mathbin{\rightarrow}\Box\left(\chi\vee\Diamond\psi\right)\in\Lambda$,
and thus $\Box\left(\chi\vee\Diamond\psi\right)\in\Lambda$. By 2.1 it follows
that $\Box\chi\vee\Diamond\Diamond\psi\in\Phi$, and then by 1, it follows that
$\Box\chi\vee\Diamond\psi\in\Phi$. Since $\chi\not\in\Theta$, we know
$\Box\chi\not\in\Phi$. Then by primality, $\Diamond\psi\in\Phi$—a
contradiction. Thanks to Lemma 2, $\Phi^{\Box}$ can be extended to a
$\Diamond\Phi^{\Diamond}\cup\Xi$-consistent prime theory $\Upsilon$. It then
readily follows that
$\Phi\sqsubseteq_{\mathrm{c}}\Upsilon\preccurlyeq_{\mathrm{c}}\Theta$, as
required. ∎

The last frame condition we need to check is that Gödel logics are indeed
upward linear.

######  Lemma 5.

If $\Lambda$ is any $\Diamond$-regular logic such that $\ref{ax:g}\in\Lambda$,
then the model $\mathcal{M}_{\mathrm{c}}^{\Lambda}$ is upward linear.

###### Proof.

Assume toward a contradiction that $\preccurlyeq_{\mathrm{c}}$ is not upward
linear. Let the theories $\Phi$, $\Psi$, and $\Omega$ be such that
$\Phi\preccurlyeq_{\mathrm{c}}\Psi$ and $\Phi\preccurlyeq_{\mathrm{c}}\Omega$,
but $\Psi\not\preccurlyeq_{\mathrm{c}}\Omega$ and
$\Omega\not\preccurlyeq_{\mathrm{c}}\Psi$. From the definition of
$\preccurlyeq_{\mathrm{c}}$ we get that $\Psi\not\subseteq\Omega$ and
$\Omega\not\subseteq\Psi$. So there exist two formulas $\varphi$ and $\psi$
such that $\varphi\in\Psi\setminus\Omega$ and $\psi\in\Omega\setminus\Psi$.
Therefore $\varphi\mathbin{\rightarrow}\psi\not\in\Psi\supseteq\Phi$ and
$\psi\mathbin{\rightarrow}\varphi\not\in\Omega\supseteq\Phi$. Consequently,
$(\varphi\mathbin{\rightarrow}\psi)\vee(\psi\mathbin{\rightarrow}\varphi)\not\in\Phi$,
contradicting Axiom 2.1. ∎

It already follows from the above that, for any of the $\Diamond$-regular
logics $\Lambda$ we consider, $\mathcal{M}^{\Lambda}_{\mathrm{c}}$ is a
$\Lambda$-model. Thus to conclude our completeness proof, it remains to
establish a standard truth lemma. Since the case for a formula of the form
$\Box\varphi$ is subtle, we establish it separately.

######  Lemma 6.

Let $\Lambda$ be a $\Diamond$-regular logic containing either 2.1 or 2.1. Then
for any $\Phi\in W_{\mathrm{c}}$ and any formula $\varphi$, we have
$\Box\varphi\in\Phi$ if and only if whenever
$\Phi\preccurlyeq_{\mathrm{c}}\Psi\sqsubseteq_{\mathrm{c}}\Theta$, it follows
that $\varphi\in\Theta$.

###### Proof.

For the left-to-right direction, suppose that $\Box\varphi\in\Phi$ and
$\Phi\preccurlyeq_{\mathrm{c}}\Psi\sqsubseteq_{\mathrm{c}}\Theta$. By the
definition of $\preccurlyeq_{\mathrm{c}}$, we have $\Box\varphi\in\Psi$, and
thus $\varphi\in\Psi^{\Box}$. Then by the definition of
$\sqsubseteq_{\mathrm{c}}$, we have $\varphi\in\Theta$, as needed.

For the other direction, we consider two cases. First assume that
$\ref{ax:fs}\in\Lambda$. If $\Box\varphi\not\in\Phi$, using Zorn’s lemma, let
$\Psi\succcurlyeq_{\mathrm{c}}\Phi$ be a $\preccurlyeq_{\mathrm{c}}$-maximal
$\Box\varphi$-consistent theory. We claim that

$\chi\in\Psi^{\Diamond}\implies\Box(\chi\mathbin{\rightarrow}\varphi)\in\Psi.$
(2)

Suppose $\chi\in\Psi^{\Diamond}$. By maximality of $\Psi$, we have
$\Psi,\Diamond\chi\vdash\Box\varphi$, so
$\Psi\vdash\Diamond\chi\mathbin{\rightarrow}\Box\varphi$. By 2.1, we obtain
$\Psi\vdash\Box(\chi\mathbin{\rightarrow}\varphi)$ and thus
$\Box(\chi\mathbin{\rightarrow}\varphi)\in\Psi$, as needed.

Note by 2.1 that $\Psi^{\Diamond}$ is closed under disjunction. (This uses the
fact that $\Psi$ is prime, which as we saw in the proof of Lemma 2, follows
from maximality.) We claim that $\Psi^{\Box}$ is
$\Diamond\Psi^{\Diamond}\cup\\{\varphi\\}$-consistent. If not, we would have
$\chi\in\Psi^{\Box}$ and $\theta\in\Psi^{\Diamond}$ such that
$\chi\vdash\varphi\vee\Diamond\theta$, and reasoning as before,
$\Box\chi\vdash\Box(\varphi\vee\Diamond\theta)$. It follows that
$\Box\chi,\Box(\Diamond\theta\mathbin{\rightarrow}\varphi)\vdash\Box(\varphi\vee\varphi)$,
that is
$\Box\chi,\Box(\Diamond\theta\mathbin{\rightarrow}\varphi)\vdash\Box\varphi$.
From 1 we see that $\Diamond\Diamond\theta\in\Psi$ implies that
$\Diamond\theta\in\Psi$, which by contraposition becomes
$\theta\in\Psi^{\Diamond}$ implies $\Diamond\theta\in\Psi^{\Diamond}$. Thus we
may use (2) to conclude that
$\Box(\Diamond\theta\mathbin{\rightarrow}\varphi)\in\Psi$, so
$\Psi\vdash\Box\varphi$, a contradiction.

Hence there exists a $\Diamond\Psi^{\Diamond}\cup\\{\varphi\\}$-consistent
prime theory $\Upsilon$ extending $\Psi^{\Box}$. It follows that
$\varphi\notin\Upsilon$ and it is readily verified that
$\Phi\preccurlyeq_{\mathrm{c}}\Psi\sqsubseteq_{\mathrm{c}}\Upsilon$, as
needed.

Next we consider the case where $\ref{ax:cd}\in\Lambda$. Suppose that
$\Box\varphi\not\in\Phi$; we claim that $\Phi^{\Box}$ is
$\Diamond\Phi^{\Diamond}\cup\\{\varphi\\}$-consistent. If not, there exist
$\Box\chi\in\Phi$ and $\Diamond\theta\not\in\Phi$ such that
$\chi\rightarrow\varphi\vee\Diamond\theta\in\Lambda$. By 1,
$\bm{\mathrm{K}_{\Box}}$ and 1 we get
$\Box(\varphi\vee\Diamond\theta)\in\Phi$. By Axiom 2.1, this gives
$\Box\varphi\vee\Diamond\Diamond\theta\in\Phi$—a contradiction since $\Phi$ is
prime, and neither $\Box\varphi\in\Phi$ nor, by 1, $\Diamond\psi\in\Phi$.
Therefore, $\Phi^{\Box}$ can be extended to a
$\Diamond\Phi^{\Diamond}\cup\varphi$-consistent prime theory $\Upsilon$.
Clearly, $\varphi\not\in\Upsilon$ and
$\Phi\preccurlyeq_{\mathrm{c}}\Phi\sqsubseteq_{\mathrm{c}}\Upsilon$. ∎

With this, we may establish the truth lemma for $\Diamond$-regular logics.

######  Lemma 7 (truth lemma).

Let $\Lambda$ be any $\Diamond$-regular logic such that $\Lambda$ contains
either 2.1 or 2.1. For any $\Phi\in W_{\mathrm{c}}$ and
$\varphi\in{\mathcal{L}}$,

$\varphi\in\Phi\iff(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Phi)\models\varphi.$

###### Proof.

By structural induction on $\varphi$. The case of propositional variables
holds by the definition of $V_{\mathrm{c}}$. The cases of $\wedge$ and $\vee$
are straightforward, and the case for $\varphi=\Box\psi$ follows from Lemma 6.

We consider the $\mathbin{\rightarrow}$ connective next. First suppose
$\psi\mathbin{\rightarrow}\chi\in\Phi$. Let
$\Psi\succcurlyeq_{\mathrm{c}}\Phi$ be such that
$(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Psi)\models\psi$. By the induction
hypothesis, $\psi\in\Psi$. Since $\Psi\succcurlyeq_{\mathrm{c}}\Phi$ and
$\psi\mathbin{\rightarrow}\chi\in\Phi$, we have
$\psi\mathbin{\rightarrow}\chi\in\Psi$. By closure under syntactic
consequence, $\chi\in\Psi$, and then by the induction hypothesis,
$(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Psi)\models\chi$. Since $\Psi$ was
arbitrary subject to $\Psi\succcurlyeq_{\mathrm{c}}\Phi$, we conclude
$(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Phi)\models\psi\mathbin{\rightarrow}\chi$.

Conversely, suppose $\psi\mathbin{\rightarrow}\chi\not\in\Phi$. We claim that
$\Phi\cup\\{\psi\\}$ is $\chi$-consistent. If not, by the definition of
$\vdash$, there exists $\xi\in\Phi$ such that
$\xi\wedge\psi\mathbin{\rightarrow}\chi\in\Lambda$. It follows that
$\xi\mathbin{\rightarrow}\left(\psi\mathbin{\rightarrow}\chi\right)\in\Lambda$.
Since $\xi\in\Phi$, we obtain $\psi\mathbin{\rightarrow}\chi\in\Phi$—a
contradiction. Hence $\Phi\cup\\{\psi\\}$ is $\chi$-consistent and so by Lemma
2 can be extended to a $\chi$-consistent prime theory $\Psi$, and hence
$\Phi\preccurlyeq_{\mathrm{c}}\Psi$. By the induction hypotheses for $\psi$
and $\chi$, we deduce $(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Psi)\models\psi$
and $(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Psi)\not\models\chi$. Therefore
$(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Phi)\not\models\psi\mathbin{\rightarrow}\chi$.

For the case that $\varphi$ is of the form $\Diamond\psi$, if
$\Diamond\psi\in\Phi$, then let us define $\Theta=\Phi^{\Box}\cup\\{\psi\\}$,
and let us assume toward a contradiction that
$\Theta\vdash\\{\chi\in{\mathcal{L}}\mid\Diamond\chi\not\in\Phi^{+}\\}$. This
means that there exist $\Box\theta\in\Phi$ and $\Diamond\chi\not\in\Phi$ such
that $\theta\rightarrow\left(\psi\rightarrow\chi\right)\in\mathsf{GS4}$. From
1 and $\bm{\mathrm{K}_{\Box}}$, we obtain
$\Box\theta\mathbin{\rightarrow}\Box(\psi\mathbin{\rightarrow}\chi)$, and thus
$\Box(\psi\mathbin{\rightarrow}\chi)\in\Phi$. Then by
$\bm{\mathrm{K}_{\Diamond}}$, we obtain
$\Diamond\psi\mathbin{\rightarrow}\Diamond\chi$, and thus
$\Diamond\chi\in\Phi$—a contradiction. Therefore $\Theta$ can be extended to a
prime theory $\Upsilon$ such that
$\Upsilon\not\vdash\\{\chi\mid\Diamond\chi\not\in\Phi\\}$. It follows that
$\Phi\sqsubseteq_{\mathrm{c}}\Upsilon$. Moreover, $\psi\in\Upsilon$. By the
induction hypothesis,
$(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Upsilon)\models\psi$, so
$(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Phi)\models\Diamond\psi$.

Conversely, assume that
$(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Phi)\models\Diamond\psi$, so
$(\mathcal{M}_{\mathrm{c}}^{{\Lambda}},\Upsilon)\models\psi$ for some
$\Phi\sqsubseteq_{\mathrm{c}}\Upsilon$. By the inductive hypothesis,
$\psi\in\Upsilon$; hence by 1, we have $\Diamond\psi\in\Upsilon$, and thus
$\psi\not\in\Upsilon^{\Diamond}$. It follows that
$\psi\not\in\Phi^{\Diamond}$, hence $\Diamond\psi\in\Phi$, as required. ∎

It follows from the above considerations that all of the $\Diamond$-regular
logics we consider are strongly complete with respect to their corresponding
class of frames, and in particular any formula that is not derivable is
falsifiable. (Completeness of $\mathsf{IS4}$ is well known and was first
proven in [30].)

######  Theorem 2.

Let
$\Lambda\in\\{{\mathsf{IS4}},{\mathsf{S4I}},{\mathsf{GS4}},{{\mathsf{GS4}}^{\mathsf{c}}}\\}$.
Let $\models_{\Lambda}$ denote semantic consequence on the class of $\Lambda$
frames as given by Definition 7, and $\vdash_{\Lambda}$ denote the syntactic
consequence relation for $\Lambda$. Then for any set of formulas
$\Gamma\cup\\{\varphi\\}$,

$\Gamma\models_{\Lambda}\varphi\iff\Gamma\vdash_{\Lambda}\varphi.$

######  Remark 1.

Theorem 2 also applies to the logics ${\mathsf{S4I}}+{\ref{ax:g}}$ and
${\mathsf{IS4}}+{\ref{ax:cd}}$, but the first logic does not seem to be the
logic of any natural class of Gödel–Kripke frames, and our techniques in
Section 5 do not settle whether the second has the finite model property,
essentially for the same reason that they do not work for $\mathsf{IS4}$.

###  4.3 Completeness of $\mathsf{CS4}$

In this subsection we prove that $\mathsf{CS4}$ is strongly complete for the
class of CS4 frames. This claim is already made in [11], where the main
elements of the proof are sketched, but there does not seem to be a detailed
proof in the literature. Moreover, our proof of the finite model property
relies on specific properties of the canonical model, and establishing these
properties will amount to the bulk of the proof of completeness. For these two
reasons, we provide a full completeness proof here.

The proof mostly follows the same pattern as for $\Diamond$-regular logics,
but some important modifications are needed to deal with the ‘irregular’
semantics for $\Diamond$. Rather than working with plain theories, we must
work with augmented theories, which are ordered pairs of sets of formulas
$\Phi=(\Phi^{+};\Phi^{\Diamond})$. We say that $\Phi$ is prime if $\Phi^{+}$
is prime. The intuition behind this definition is the following: formulas in
$\Phi^{+}$ are the ones satisfied by the theory, and the formulas in
$\Phi^{\Diamond}$ are those $\varphi$ such that $\Diamond\varphi$ is falsified
directly by $\sqsubseteq$ not having any witnesses for $\varphi$ (as opposed
to being falsified via a $\preccurlyeq$-accessible world). Any standard theory
may be regarded as an augmented theory if we identify $\Phi$ with
$(\Phi;\Phi^{\Diamond})$, where
$\Phi^{\Diamond}=\\{\varphi\in{\mathcal{L}}\mid\Diamond\varphi\notin\Phi\\}$,
as we have defined previously. However, not all augmented theories are of this
form, and in fact we often work with augmented theories of the form
$(\Phi^{+};\varnothing)$.

######  Definition 12.

Given a set of formulas $\Xi$, we say that an augmented theory $\Phi$ is
$\Xi$-consistent if for any finite set $\Delta\subseteq\Phi^{\Diamond}$,

$\Phi^{+}\not\vdash\Xi,\Diamond\bigvee\Delta.$

We adopt the convention that $\Diamond\bigvee\varnothing\coloneqq\bot$ (note
that this convention overrides $\bigvee\varnothing=\bot$). We say that $\Phi$
is consistent if it is $\varnothing$-consistent. If $\Xi$ is a singleton
$\\{\xi\\}$, we write $\xi$-consistent instead of $\\{\xi\\}$-consistent.

Note that if $\Phi$ is a $\Xi$-consistent prime augmented theory, then
necessarily $\bot\not\in\Phi^{+}$. We say that an augmented theory $\Psi$
extends $\Phi$ if $\Phi^{+}\subseteq\Psi^{+}$ and
$\Phi^{\Diamond}\subseteq\Psi^{\Diamond}$.

######  Lemma 8 (adapted from [11]).

Any $\Xi$-consistent augmented theory $(\Phi^{+};\Phi^{\Diamond})$ can be
extended to a $\Xi$-consistent prime augmented theory
$(\Phi^{+}_{*};\Phi^{\Diamond})$.

###### Proof.

Apply Lemma 2 with
$\Xi^{\prime}=\Xi\cup\\{\Diamond\bigvee\Delta\mid\Delta\subseteq_{\mathrm{fin}}\Phi^{\Diamond}\\}$,
where $\subseteq_{\mathrm{fin}}$ is the finite subset relation. ∎

If $\Phi$ is an augmented theory then we define
$\Phi^{\Box}\coloneqq\\{\varphi\in{\mathcal{L}}\mid\Box\varphi\in\Phi^{+}\\}$.

######  Definition 13 (adapted from [11]).

We define the canonical model for ${\mathsf{CS4}}$ as
$\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}}=(W_{\mathrm{c}},W^{\bot}_{\mathrm{c}},{\preccurlyeq_{\mathrm{c}}},{\sqsubseteq_{\mathrm{c}}},V_{\mathrm{c}})$,
where

  * •

$W_{\mathrm{c}}$ is the set of all prime augmented $\mathsf{CS4}$-theories,

  * •

$W^{\bot}_{\mathrm{c}}=\\{({\mathcal{L}};\varnothing)\\}$,

  * •

${\preccurlyeq_{\mathrm{c}}}\subseteq W_{\mathrm{c}}\times W_{\mathrm{c}}$ is
defined by $\Phi\preccurlyeq_{\mathrm{c}}\Psi$ if and only if
$\Phi^{+}\subseteq\Psi^{+}$,

  * •

${\sqsubseteq_{\mathrm{c}}}\subseteq W_{\mathrm{c}}\times W_{\mathrm{c}}$ is
defined by $\Phi\sqsubseteq_{\mathrm{c}}\Psi$ if and only if
$\Phi^{\Box}\subseteq\Psi^{+}$ and $\Phi^{\Diamond}\subseteq\Psi^{\Diamond}$,

  * •

$V_{\mathrm{c}}$ is defined by $V_{\mathrm{c}}(p)=\\{\Phi\in
W_{\mathrm{c}}\mid p\in\Phi^{+}\\}$.

We now show that $\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}}$ is a CS4 model.

######  Lemma 9.

$\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}}$ is a bi-intuitionistic model.

###### Proof.

It is easy to see that $\preccurlyeq_{\mathrm{c}}$ is a preorder given that
$\subseteq$ is itself a preorder, and the two monotonicity conditions for
$W^{\bot}_{\mathrm{c}}$ and the one for $V_{\mathrm{c}}$ are easily verified.

It remains to check that $\sqsubseteq_{\mathrm{c}}$ is a preorder. Let us take
$\Phi\in W_{\mathrm{c}}$ and $\Box\varphi\in\Phi^{+}$. Due to Axiom 1 and
closure of $\Phi^{+}$ under $\vdash$, we know $\varphi\in\Phi^{+}$; therefore,
$\Phi^{\Box}\subseteq\Phi^{+}$. Trivially,
$\Phi^{\Diamond}\subseteq\Phi^{\Diamond}$, so in conclusion
$\sqsubseteq_{\mathrm{c}}$ is reflexive.

To see that $\sqsubseteq_{\mathrm{c}}$ is transitive, let us consider
$\Phi,\Psi,\Omega\in W_{\mathrm{c}}$ such that
$\Phi\sqsubseteq_{\mathrm{c}}\Psi$ and $\Psi\sqsubseteq_{\mathrm{c}}\Omega$.
Let us first take $\Box\varphi\in\Phi^{+}$. From Axiom 1 and closure of
$\Phi^{+}$ under $\vdash$, we obtain $\Box\Box\varphi\in\Phi^{+}$. From
$\Phi\sqsubseteq_{\mathrm{c}}\Psi$ and $\Psi\sqsubseteq_{\mathrm{c}}\Omega$ we
get $\Box\varphi\in\Psi^{+}$ and $\varphi\in\Omega^{+}$; therefore
$\Phi^{\Box}\subseteq\Omega^{+}$. By the hypotheses
$\Phi\sqsubseteq_{\mathrm{c}}\Psi$ and $\Psi\sqsubseteq_{\mathrm{c}}\Omega$,
we also have
$\Phi^{\Diamond}\subseteq\Psi^{\Diamond}\subseteq\Omega^{\Diamond}$. We
conclude that $\Phi\sqsubseteq_{\mathrm{c}}\Omega$, so
$\sqsubseteq_{\mathrm{c}}$ is transitive. ∎

######  Lemma 10.

$\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}}$ is back–up confluent. In
particular, if
$\Phi\sqsubseteq_{\mathrm{c}}\Psi\preccurlyeq_{\mathrm{c}}\Omega$, then
$\Upsilon\coloneqq(\Phi^{+};\varnothing)$ satisfies
$\Phi\preccurlyeq_{\mathrm{c}}\Upsilon\sqsubseteq_{\mathrm{c}}\Omega$.

###### Proof.

Take $\Phi$, $\Psi$, and $\Omega$ in $W_{\mathrm{c}}$ such that
$\Phi\sqsubseteq_{\mathrm{c}}\Psi\preccurlyeq_{\mathrm{c}}\Omega$, and let us
define $\Upsilon=\left(\Phi^{+},\varnothing\right)$. Now $\Phi^{+}$ is already
prime, so $\Upsilon\in W_{\mathrm{c}}$. By definition
$\Phi^{+}\subseteq\Upsilon^{+}$; thus $\Phi\preccurlyeq_{\mathrm{c}}\Upsilon$.
Take $\Box\varphi\in\Upsilon^{+}$. By definition $\Box\varphi\in\Phi^{+}$.
Since $\Phi\sqsubseteq_{\mathrm{c}}\Psi\preccurlyeq_{\mathrm{c}}\Omega$ it
follows that $\varphi\in\Omega^{+}$. Since $\Box\varphi$ was chosen
arbitrarily, we have $\Upsilon^{\Box}\subseteq\Omega^{+}$. Clearly also
$\Upsilon^{\Diamond}=\varnothing\subseteq\Omega^{\Diamond}$, so
$\Upsilon\sqsubseteq_{\mathrm{c}}\Omega$. ∎

We have established that $\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}}$ is a CS4
model. We now proceed towards a truth lemma for
$\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}}$. Here is where we really put the
axioms and inference rules to work.

######  Lemma 11.

For all $\Gamma\in W_{\mathrm{c}}$ and for all $\varphi\in{\mathcal{L}}$, the
following hold.

  1. (a)

$\Diamond\varphi\in\Gamma^{+}$ if and only if for all
$\Psi\succcurlyeq_{\mathrm{c}}\Gamma$ there is $\Delta\in W_{\mathrm{c}}$ such
that $\Psi\sqsubseteq_{\mathrm{c}}\Delta$ and $\varphi\in\Delta^{+}$.

  2. (b)

$\Box\varphi\in\Gamma^{+}$ if and only if for all $\Psi$ and $\Delta$ such
that $\Gamma\preccurlyeq_{\mathrm{c}}\Psi\sqsubseteq_{\mathrm{c}}\Delta$, we
have $\varphi\in\Delta^{+}$.

###### Proof.

_(a)._ From left to right, assume that $\Diamond\varphi\in\Gamma^{+}$, and let
$\Psi\succcurlyeq_{\mathrm{c}}\Gamma$. Let us define the augmented theory
$\Upsilon=(\Psi^{\Box},\varphi;\Psi^{\Diamond})$. We show that $\Upsilon$ is
consistent. If not, let $\chi_{1},\ldots,\chi_{n}\in\Psi^{\Box}$ and
$\psi_{1},\ldots,\psi_{m}\subseteq\Psi^{\Diamond}$ be such that, for
$\chi\coloneqq\bigwedge_{i}\chi_{i}$ and $\psi\coloneqq\bigvee_{i}\psi_{i}$,
we have $\chi\wedge\varphi\mathbin{\rightarrow}\Diamond\psi\in{\mathsf{CS4}}$,
so that
$\chi\mathbin{\rightarrow}\left(\varphi\mathbin{\rightarrow}\Diamond\psi\right)\in{\mathsf{CS4}}$.
By 1, $\bm{\mathrm{K}_{\Box}}$, and 1, it follows that
$\Box\chi\mathbin{\rightarrow}\Box\left(\varphi\mathbin{\rightarrow}\Diamond\psi\right)\in\mathsf{CS4}$.
By Proposition 3(3) (and induction up to $n$), we also know that
$\bigwedge_{i}\Box\chi_{i}\mathbin{\rightarrow}\Box\chi\in\mathsf{CS4}$, and
hence
$\bigwedge_{i}\Box\chi_{i}\mathbin{\rightarrow}\Box\left(\varphi\mathbin{\rightarrow}\Diamond\psi\right)\in{\mathsf{CS4}}$,
or otherwise stated
$\Box\chi_{1},\dots,\Box\chi_{n}\vdash\Box\left(\varphi\mathbin{\rightarrow}\Diamond\psi\right)$.
By closure of $\Psi^{+}$ under syntactic consequence, we obtain
$\Box(\varphi\allowbreak\mathbin{\rightarrow}\allowbreak\Diamond\psi)\in\Psi^{+}$,
and then by $\bm{\mathrm{K}_{\Diamond}}$ we obtain
$\Diamond\varphi\mathbin{\rightarrow}\Diamond\Diamond\psi\in\Psi^{+}$. Since
$\Gamma\preccurlyeq_{\mathrm{c}}\Psi$ and $\Diamond\varphi\in\Gamma^{+}$, we
also have $\Diamond\varphi\in\Psi^{+}$. We know that
$\Diamond\varphi\wedge(\Diamond\varphi\mathbin{\rightarrow}\Diamond\Diamond\psi)\mathbin{\rightarrow}\Diamond\Diamond\psi\in{\mathsf{CS4}}$
by substitution on an intuitionistic theorem. Thus by closure of $\Psi^{+}$
under $\vdash$, we have $\Diamond\Diamond\psi\in\Psi^{+}$. By 1 and syntactic
closure, we reach $\Diamond\psi\in\Psi^{+}$, which contradicts the consistency
of $\Psi$. We conclude that $\Upsilon$ is consistent. By Lemma 2, $\Upsilon$
can be extended to a consistent prime augmented theory
$\Delta=(\Delta^{+};\Delta^{\Diamond})$ such that
$\Psi^{\Box}\subseteq\Delta^{+}$ and $\Psi^{\Diamond}=\Delta^{\Diamond}$
(therefore $\Psi\sqsubseteq_{\mathrm{c}}\Delta$), and moreover
$\varphi\in\Delta^{+}$, as needed.

Conversely, let us assume that $\Diamond\varphi\not\in\Gamma^{+}$ and let us
define $\Psi=(\Gamma^{+};\\{\varphi\\})$. It is easy to see that $\Psi$ is
consistent, and since $\Gamma^{+}$ is prime, $\Psi\in W_{\mathrm{c}}$.
Moreover, $\Gamma\preccurlyeq_{\mathrm{c}}\Psi$. We claim that for all
$\Delta\in W_{\mathrm{c}}$, if $\Psi\sqsubseteq_{\mathrm{c}}\Delta$ then
$\varphi\not\in\Delta^{+}$. To prove this, let us take any $\Delta\in
W_{\mathrm{c}}$ satisfying $\Psi\sqsubseteq_{\mathrm{c}}\Delta$. By
definition, $\Psi^{\Diamond}\subseteq\Delta^{\Diamond}$, so
$\varphi\in\Delta^{\Diamond}$. As $\Delta$ is a prime augmented theory,
$\Diamond\varphi\not\in\Delta^{+}$, so $\varphi\not\in\Delta^{+}$ because of
Axiom 1, as needed.

#### (b)

From left to right, let $\Box\varphi\in\Gamma^{+}$, and let $\Psi$ and
$\Delta$ be such that
$\Gamma\preccurlyeq_{\mathrm{c}}\Psi\sqsubseteq_{\mathrm{c}}\Delta$. From
$\Gamma\preccurlyeq_{\mathrm{c}}\Psi\sqsubseteq_{\mathrm{c}}\Delta$, we obtain
$\Gamma^{+}\subseteq\Psi^{+}$ and $\Psi^{\Box}\subseteq\Delta^{+}$. Since
$\Box\varphi\in\Gamma^{+}$ we have $\varphi\in\Delta^{+}$, as needed.

Conversely, let us assume that $\Box\varphi\not\in\Gamma^{+}$ and let us
define $\Psi=(\Gamma^{+};\varnothing)$. Clearly $\Psi$ is a prime theory and
it satisfies $\Gamma\preccurlyeq_{\mathrm{c}}\Psi$. Let us take
$\Upsilon=(\Psi^{\Box},\varnothing)$. $\Upsilon$ is $\varphi$-consistent,
since otherwise 1 and $\bm{\mathrm{K}_{\Box}}$ would yield
$\Box\bigwedge_{i}\psi_{i}\mathbin{\rightarrow}\Box\varphi\in\mathsf{CS4}$ for
some $\psi_{1},\dots,\psi_{n}\in\Psi^{\Box}$, from which we can obtain
$\Box\psi_{1},\dots,\Box\psi_{n}\vdash\Box\varphi$ and thus
$\Box\varphi\in\Gamma^{+}$—a contradiction. By Lemma 2, $\Upsilon$ can be
extended to a $\varphi$-consistent prime augmented theory
$\Delta=(\Delta^{+};\varnothing)$ such that $\Upsilon^{+}\subseteq\Delta^{+}$.
By the definition of $\Upsilon$, we then have
$\Psi\sqsubseteq_{\mathrm{c}}\Delta$ and $\varphi\not\in\Delta^{+}$, as
needed. ∎

######  Lemma 12 (truth lemma).

For any prime augmented theory $\Phi\in W_{\mathrm{c}}$ and
$\varphi\in{\mathcal{L}}$,

$\varphi\in\Phi^{+}\iff(\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}},\Phi)\models\varphi.$

###### Proof.

The cases for variables and $\wedge,\vee,\mathbin{\rightarrow}$ are similar to
the proof of Lemma 7. The case where $\varphi$ is of the form $\Diamond\psi$
is simple. By Lemma 11(a), $\Diamond\psi\in\Phi^{+}$ if and only if whenever
$\Phi\preccurlyeq_{\mathrm{c}}\Psi$, there exists
$\Psi\sqsubseteq_{\mathrm{c}}\Omega$ such that $\psi\in\Omega^{+}$. By the
inductive hypothesis, this happens if and only if whenever
$\Phi\preccurlyeq_{\mathrm{c}}\Psi$ there exists
$\Psi\sqsubseteq_{\mathrm{c}}\Omega$ such that
$(\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}},\Omega)\models\psi$, which is
precisely the definition of
$(\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}},\Phi)\models\Diamond\psi$.

The case where $\varphi$ is of the form $\Box\psi$ is similar. By Lemma 11(b),
$\Box\psi\in\Phi^{+}$ if and only if whenever
$\Phi\preccurlyeq_{\mathrm{c}}\Psi\sqsubseteq_{\mathrm{c}}\Omega$, we have
$\psi\in\Omega^{+}$. By the inductive hypothesis, this happens if and only if
whenever $\Phi\preccurlyeq_{\mathrm{c}}\Psi\sqsubseteq_{\mathrm{c}}\Omega$, we
have $(\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}},\Omega)\models\psi$, which is
precisely the definition of
$(\mathcal{M}_{\mathrm{c}}^{{\mathsf{CS4}}},\Phi)\models\Box\psi$. ∎

From this, we obtain strong completeness of $\mathsf{CS4}$ with respect to its
class of models.

######  Theorem 3 (Alechina, Mendler, De Paiva, and Ritter [11]).

Let $\models_{\mathsf{CS4}}$ denote local semantic consequence on the class of
$\mathsf{CS4}$ frames, and $\vdash_{\mathsf{CS4}}$ denote the syntactic
consequence relation for the logic $\mathsf{CS4}$. Then

$\Gamma\models_{\mathsf{CS4}}\varphi\iff\Gamma\vdash_{\mathsf{CS4}}\varphi.$

##  5 Finite frame properties

In this section we prove that the finite birelational frame property holds for
each of the logics $\mathsf{GS4}$, $\mathsf{GS4^{c}}$, $\mathsf{CS4}$, and
$\mathsf{S4I}$, in that order.

###  5.1 $\Sigma$-bisimulations

In this subsection we develop the theory of _$\Sigma$ -bisimulations_, a key
component common to all four of our finite frame property proofs.

######  Definition 14.

Given a set of formulas $\Sigma$ and a bi-intuitionistic model
$\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$, we define the
$\Sigma$-label of $w\in W$ to be the pair
$\ell(w)=(\ell^{+}(w),\ell^{\Diamond}(w))$, where

$\displaystyle\ell^{+}(w)$
$\displaystyle\coloneqq\\{\varphi\in\Sigma\mid(\mathcal{M},w)\models\varphi\\},$
$\displaystyle\ell^{\Diamond}(w)$
$\displaystyle\coloneqq\\{\varphi\in\Sigma\mid\forall v\sqsupseteq w\
(\mathcal{M},v)\not\models\varphi\\}.$

A $\Sigma$-bisimulation on $\mathcal{M}$ is a forth–up and back–up confluent
relation $Z\subseteq W\times W$ such that if $w\mathrel{Z}v$ then
$\ell(w)=\ell(v)$.

Notice that an arbitrary union of $\Sigma$-bisimulations is a
$\Sigma$-bisimulation (and the empty relation is a $\Sigma$-bisimulation);
thus a greatest $\Sigma$-bisimulation exists, which we denote by
$\sim_{\Sigma}$. Since the set of $\Sigma$-bisimulations clearly contains the
identity relation and is closed under compositions and under the converse
operation, $\sim_{\Sigma}$ must be an equivalence relation.

For each canonical model $\mathcal{M}^{\Lambda}_{\mathrm{c}}$, we note that
$\ell(\Phi)=(\Phi^{+}\cap\Sigma,\Phi^{\Diamond}\cap\Sigma)$.

######  Definition 15.

Given a bi-intuitionistic model
$\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$ and an equivalence
relation ${\sim}\subseteq W\times W$, we denote the equivalence class of $w\in
W$ under $\sim$ by $[w]$. We then define the quotient
$\nicefrac{{\mathcal{M}}}{{\sim}}=(\nicefrac{{W}}{{\sim}},\nicefrac{{W^{\bot}}}{{\sim}},\nicefrac{{\preccurlyeq}}{{\sim}},\nicefrac{{\sqsubseteq}}{{\sim}},\nicefrac{{V}}{{\sim}})$
by

  * •

$\nicefrac{{W}}{{\sim}}\coloneqq\\{[w]\mid w\in W\\}$,

  * •

$\nicefrac{{W^{\bot}}}{{\sim}}\coloneqq\\{[w]\mid w\in W^{\bot}\\}$,

  * •

$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[v]$ if there exist
$w^{\prime}\sim w$ and $v^{\prime}\sim v$ such that $w^{\prime}\preccurlyeq
v^{\prime}$,

  * •

$\nicefrac{{\sqsubseteq}}{{\sim}}$ is the transitive closure of
$\nicefrac{{\sqsubseteq^{0}}}{{\sim}}$ defined by
$[w]\mathrel{\nicefrac{{\sqsubseteq^{0}}}{{\sim}}}[v]$ whenever there are
$w^{\prime},v^{\prime}$ such that $w\sim w^{\prime}\sqsubseteq v^{\prime}\sim
v$,

  * •

$\nicefrac{{V}}{{\sim}}(p)\coloneqq\\{[w]\mid w\in V(p)\\}$

Of particular importance is the case where the relation $\sim$ is given by
$\Sigma$-bisimulation.

######  Lemma 13.

Let $\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$ be a bi-
intuitionistic model, and suppose that $\sim$ is an equivalence relation that
is also a $\Sigma$-bisimulation. Then

  * •

for all $w,v\in W$, we have
$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[v]$ if and only if there is
$v^{\prime}\sim v$ such that $w\preccurlyeq v^{\prime}$;

  * •

the relation $\nicefrac{{\preccurlyeq}}{{\sim}}$ is a preorder.

###### Proof.

For the first item, clearly if there is $v^{\prime}\sim v$ such that
$w\preccurlyeq v^{\prime}$, then
$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[v]$. Conversely, if
$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[v]$, then there are
$w^{\prime}\sim w$ and $v^{\prime}\sim v$ such that $w^{\prime}\preccurlyeq
v^{\prime}$. Since $\sim$ is a bisimulation, there is $v^{\prime\prime}\sim
v^{\prime}$ such that $w\preccurlyeq v^{\prime\prime}$. But then by
transitivity of $\sim$, we have $v^{\prime\prime}\sim v$, as needed.

For the second item, clearly $\nicefrac{{\preccurlyeq}}{{\sim}}$ is reflexive.
For transitivity, suppose
$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[v]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[u]$.
Then by the first item, there exists $v^{\prime}\sim v$ with $w\preccurlyeq
v^{\prime}$. Then
$[v^{\prime}]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[u]$, and so, using
the first item again, there exists $u^{\prime}\sim u$ with
$v^{\prime}\preccurlyeq u^{\prime}$. By transitivity of $\preccurlyeq$, we
have $w\preccurlyeq u^{\prime}$, and hence
$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[u^{\prime}]=[u]$. ∎

By the second item of Lemma 13, if $\mathcal{M}$ is a bi-intuitionistic model
and $\sim$ is an equivalence relation that is also a $\Sigma$-bisimulation,
then $\nicefrac{{\mathcal{M}}}{{\sim}}$ is also a bi-intuitionistic model.

We now need an auxiliary lemma confirming that confluence notions for
relations have nice closure properties. If $R,S$ are binary relations then let
$R\mathbin{;}S$ denote their composition: $x\mathrel{R\mathbin{;}S}y$ if there
is $z$ such that $x\mathrel{R}z$ and $z\mathrel{S}y$.

######  Lemma 14.

Let $\mathcal{F}=(W,W^{\bot},{\preccurlyeq})$ be an intuitionistic frame.

  1. 1.

If $R,S\subseteq W\times W$ are forth–up (respectively back–up, forth–down)
confluent, then so is $R\mathbin{;}S$.

  2. 2.

If $(R_{i})_{i\in I}\subseteq W\times W$ are forth–up (respectively back–up,
forth–down) confluent, then so is $\bigcup_{i\in I}R_{i}$.

  3. 3.

If $R$ is forth–up (respectively back–up, forth–down) confluent, then so is
its transitive closure $R^{+}$.

###### Proof.

We prove only that forth–up confluence is closed under composition and leave
other items to the reader. Suppose that $R,S\subseteq W\times W$ are forth–up
confluent and $v\succcurlyeq w\mathrel{R\mathbin{;}S}w^{\prime}$. Then there
is $w^{\prime\prime}$ such that
$w\mathrel{R}w^{\prime\prime}\mathrel{S}w^{\prime}$. By forth–up confluence of
$R$, there is $v^{\prime\prime}$ such that
$v\mathrel{R}v^{\prime\prime}\succcurlyeq w$. By forth–up confluence of $S$,
there is $v^{\prime}$ such that
$v^{\prime\prime}\mathrel{S}v^{\prime}\succcurlyeq w^{\prime}$. But then
$v\mathrel{R\mathbin{;}S}v^{\prime}\succcurlyeq w^{\prime}$, as needed. ∎

######  Lemma 15.

Let $\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$ be a bi-
intuitionistic model and $\Sigma$ be a set of formulas. Let $\sim$ be a
$\Sigma$-bisimulation that is also an equivalence relation. Then

  1. 1.

If $\mathcal{M}$ is forth–up confluent, then so is
$\nicefrac{{\mathcal{M}}}{{\sim}}$.

  2. 2.

If $\mathcal{M}$ is back–up confluent, then so is
$\nicefrac{{\mathcal{M}}}{{\sim}}$.

  3. 3.

If $\mathcal{M}$ is upward linear, then so is
$\nicefrac{{\mathcal{M}}}{{\sim}}$.

###### Proof.

For forth–up confluence, in view of Lemma 14, it suffices to show that
$\nicefrac{{\sqsubseteq^{0}}}{{\sim}}$ is forth–up confluent. Assume that
$[v]\mathrel{\nicefrac{{\succcurlyeq}}{{\sim}}}[w]\mathrel{\nicefrac{{\sqsubseteq^{0}}}{{\sim}}}[w^{\prime}]$.
By Lemma 13, there is $v^{\prime\prime}\sim v$ such that
$v^{\prime\prime}\succcurlyeq w$. Since $\mathcal{M}$ is forth–up confluent,
there is $v^{\prime}$ such that $v^{\prime\prime}\sqsupseteq
v^{\prime}\succcurlyeq w^{\prime}$. Therefore
$[v]\mathrel{\nicefrac{{\sqsupseteq^{0}}}{{\sim}}}[v^{\prime}]\mathrel{\nicefrac{{\succcurlyeq}}{{\sim}}}[w^{\prime}]$,
as needed. Back–up confluence is treated similarly, and we omit it.

For upward linearity, assume that
$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[u]$ and
$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[v]$. Using Lemma 13, let
$u^{\prime}$, $v^{\prime}$ in $W$ be such that $u\sim u^{\prime}\succcurlyeq
w\preccurlyeq v\sim v^{\prime}$. Hence $u^{\prime}\preccurlyeq v^{\prime}$ or
$v^{\prime}\preccurlyeq u^{\prime}$. Consequently
$[u]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[v]$ or
$[v]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[u]$. ∎

######  Lemma 16 (truth lemma for quotients).

If $\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$ is any bi-
intuitionistic model, $\Sigma$ is closed under subformulas, and
${\sim}\subseteq W\times W$ is a $\Sigma$-bisimulation that is also an
equivalence relation, then for all $w\in W$ and $\varphi\in\Sigma$, we have

$(\mathcal{M},w)\models\varphi\iff(\nicefrac{{\mathcal{M}}}{{\sim}},[w])\models\varphi.$

###### Proof.

Proceed by a standard structural induction on $\varphi$. We consider only the
interesting cases.

Case $\varphi=\psi\mathbin{\rightarrow}\theta$. If
$(\mathcal{M},w)\models\psi\mathbin{\rightarrow}\theta$ and
$[v]\mathrel{\nicefrac{{\succcurlyeq}}{{\sim}}}[w]$, then in view of Lemma 13
(which we henceforth use without mention), there is $v^{\prime}\sim v$ such
that $w\preccurlyeq v^{\prime}$. Since $v^{\prime}\succcurlyeq w$, either
$(\mathcal{M},v^{\prime})\not\models\psi$ or
$(\mathcal{M},v^{\prime})\models\theta$, which by the induction hypothesis and
the fact that $[v]=[v^{\prime}]$ yields
$(\nicefrac{{\mathcal{M}}}{{\sim}},[v])\not\models\psi$ or
$(\nicefrac{{\mathcal{M}}}{{\sim}},[v])\models\theta$. Since
$[v]\mathrel{\nicefrac{{\succcurlyeq}}{{\sim}}}[w]$ was arbitrary, we conclude
that $(\nicefrac{{\mathcal{M}}}{{\sim}},[w])\models\varphi$.

Conversely, if
$(\nicefrac{{\mathcal{M}}}{{\sim}},[w])\models\psi\mathbin{\rightarrow}\theta$
and $v\succcurlyeq w$, then
$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\sim}}}[v]$, which implies that
$(\nicefrac{{\mathcal{M}}}{{\sim}},[v])\not\models\psi$ or
$(\nicefrac{{\mathcal{M}}}{{\sim}},[v])\models\theta$, and then by the
induction hypothesis, that $(\mathcal{M},v)\not\models\psi$ or
$(\mathcal{M},v)\models\theta$, as needed.

Case $\varphi=\Diamond\psi$. Suppose that $(\mathcal{M},w)\models\Diamond\psi$
and let $[v]\mathrel{\nicefrac{{\succcurlyeq}}{{\sim}}}[w]$. We may assume
that $v$ is chosen so that $v\succcurlyeq w$. Then there is $v^{\prime}$ such
that $v\sqsubseteq v^{\prime}$ and $(\mathcal{M},v^{\prime})\models\psi$. But
then $[v]\mathrel{\nicefrac{{\sqsubseteq}}{{\sim}}}[v^{\prime}]$ and the
induction hypothesis yields
$(\nicefrac{{\mathcal{M}}}{{\sim}},[v^{\prime}])\models\psi$. We conclude that
$(\nicefrac{{\mathcal{M}}}{{\sim}},[w])\models\Diamond\psi$.

Conversely, suppose that $(\mathcal{M},w)\not\models\Diamond\psi$. Then there
is $v\succcurlyeq w$ such that $\psi\in\ell^{\Diamond}(v)$. Let $v^{\prime}$
be such that $[v]\mathrel{\nicefrac{{\sqsubseteq}}{{\sim}}}[v^{\prime}]$. Then
there exist sequences $(v_{i})_{i\leq n}$ and $(v^{\prime}_{i})_{i\leq n}$
such that

$v=v_{0}\sim v^{\prime}_{0}\sqsubseteq v_{1}\sim
v^{\prime}_{1}\sqsubseteq\ldots\sqsubseteq v_{n}\sim
v^{\prime}_{n}=v^{\prime}.$

By induction on $i\leq n$, one readily verifies that
$\psi\in\ell^{\Diamond}(v_{i})\cap\ell^{\Diamond}(v^{\prime}_{i})$, from which
it follows that $\psi\in\ell^{\Diamond}(v^{\prime})$, and hence
$\psi\not\in\ell^{+}(v^{\prime})$. By the induction hypothesis,
$(\nicefrac{{\mathcal{M}}}{{\sim}},[v^{\prime}])\not\models\psi$. Since
$v\succcurlyeq w$, we have
$[v]\mathrel{\nicefrac{{\succcurlyeq}}{{\sim}}}[w]$, so as $[v^{\prime}]$ was
arbitrary subject to
$[v]\mathrel{\nicefrac{{\sqsubseteq}}{{\sim}}}[v^{\prime}]$, we obtain
$(\nicefrac{{\mathcal{M}}}{{\sim}},[w])\not\models\Diamond\psi$—a
contradiction.

Case $\varphi=\Box\psi$. This case is treated very similarly to the $\Diamond$
case, but working ‘dually’. We show only that
$(\mathcal{M},w)\not\models\Box\psi$ implies that
$(\nicefrac{{\mathcal{M}}}{{\sim}},[w])\not\models\Box\psi$ to illustrate. If
$(\mathcal{M},w)\not\models\Box\psi$, there are $v^{\prime}\sqsupseteq
v\succcurlyeq w$ such that $(\mathcal{M},v^{\prime})\not\models\Box\psi$. But
then
$[v^{\prime}]\mathrel{\nicefrac{{\sqsupseteq}}{{\sim}}}[v]\mathrel{\nicefrac{{\succcurlyeq}}{{\sim}}}[w]$,
and the induction hypothesis yields
$(\nicefrac{{\mathcal{M}}}{{\sim}},[v^{\prime}])\not\models\psi$; hence
$(\nicefrac{{\mathcal{M}}}{{\sim}},[w])\not\models\Box\psi$. ∎

Recall that $\sim_{\Sigma}$ denotes the greatest $\Sigma$-bisimulation on a
model.

######  Lemma 17.

Every $\sim_{\Sigma}$-equivalence class of
$\nicefrac{{\mathcal{M}}}{{\sim_{\Sigma}}}$ is a singleton.

###### Proof.

Suppose that $[w]\sim_{\Sigma}[v]$; we must show that $w\sim_{\Sigma}v$ as
well, to conclude $[w]=[v]$ (note that $\sim_{\Sigma}$ is defined both on
$\mathcal{M}$ and $\nicefrac{{\mathcal{M}}}{{\sim}}$). Define a relation
$Z\subseteq W\times W$ given by $x\mathrel{Z}y$ if $[x]\sim_{\Sigma}[y]$.
Clearly $w\mathrel{Z}v$, so it remains to check that $Z$ is a
$\Sigma$-bisimulation to conclude that $w\sim_{\Sigma}v$. Clearly $Z$
preserves labels in $\Sigma$. We check only the ‘forth’ clause, as the ‘back’
clause is symmetric.

Suppose that $x^{\prime}\succcurlyeq x\mathrel{Z}y$. Since
$[x]\sim_{\Sigma}[y]$, there is $y^{\prime}$ such that
$[x^{\prime}]\sim_{\Sigma}[y^{\prime}]\mathrel{\nicefrac{{\succcurlyeq}}{{\sim_{\Sigma}}}}[y]$.
In view of Lemma 13, we may assume that $y^{\prime}$ is chosen so that
$y\preccurlyeq y^{\prime}$. From $[x^{\prime}]\sim_{\Sigma}[y^{\prime}]$ we
obtain $x^{\prime}\mathrel{Z}y^{\prime}$, as needed. ∎

Quotients modulo $\Sigma$-bisimulation will be instrumental in proving the
finite frame property for $\mathsf{CS4}$. However, $\Sigma$-bisimulation does
not preserve forth–down confluence, so to treat $\mathsf{S4I}$ and
$\mathsf{GS4^{c}}$ we will need a stronger notion of bisimulation. In fact, we
will also use this stronger notion to treat $\mathsf{GS4}$.

######  Definition 16.

A strong $\Sigma$-bisimulation is a $\Sigma$-bisimulation $Z$ such that both
$Z$ and $Z^{-1}$ are forth–down confluent for $\preccurlyeq$. We denote the
greatest strong $\Sigma$-bisimulation by $\approx_{\Sigma}$.

Notice that an arbitrary union of strong $\Sigma$-bisimulations is a strong
$\Sigma$-bisimulation (and the empty relation is a strong
$\Sigma$-bisimulation); hence, $\approx_{\Sigma}$ is well defined. Clearly
$\approx_{\Sigma}$ is an equivalence relation. The following is proven in
essentially the same way as the forth–up confluence preservation clause of
Lemma 15.

######  Lemma 18.

Let $\mathcal{M}$ be a bi-intuitionistic model and $\Sigma$ be a set of
formulas. Let $\approx$ be a strong $\Sigma$-bisimulation on $\mathcal{M}$
that is also an equivalence relation. Then if $\mathcal{M}$ is forth–down
confluent, so is $\nicefrac{{\mathcal{M}}}{{\approx}}$.

We remark that the quotient $\nicefrac{{\mathcal{M}}}{{\sim}}$ may be
infinite, even taking ${\sim}\in\\{{\sim_{\Sigma}},{\approx_{\Sigma}}\\}$.
However, in the following subsections we identify classes of models that do
have finite quotients.

###  5.2 The finite frame property for $\mathsf{GS4}$

In this subsection we prove our first finite frame property result, showing
that the Gödel modal logic $\mathsf{GS4}$ indeed has the finite frame
property. The upward-linear nature of $\mathsf{GS4}$ frames enables a
particularly direct proof (not via a shallow frame property).

There are two steps to the proof. First we note that we may assume frames are
not only upward but also _downward_ linear. Then, given a subformula-closed
subset $\Sigma$ of ${\mathcal{L}}$, we describe a bisimulation quotient
construction that yields finite models whenever $\Sigma$ is finite. We
describe the quotient explicitly, noting afterwards that it is in fact the
quotient by the greatest strong $\Sigma$-bisimulation $\approx_{\Sigma}$
defined in Section 5.1.

_Downward-linear $\mathsf{GS4}$ frames._ First we argue that without loss of
generality, models based on $\mathsf{GS4}$ frames are downward linear. Let
$\mathcal{M}=(W,{\preccurlyeq},{\sqsubseteq},V)$ be an arbitrary model based
on a $\mathsf{GS4}$ frame. We construct a model
$\mathcal{M}^{\prime}=(W^{\prime},{\preccurlyeq^{\prime}},{\sqsubseteq^{\prime}},V^{\prime})$
based on a downward-linear $\mathsf{GS4}$ frame and falsifying exactly the
same ${\mathcal{L}}$-formulas as $\mathcal{M}$.

The idea is to include copies of each of the (necessarily linear) principal
upsets $v^{\uparrow}$, indexed by the generating world $v$. We define

$\displaystyle W^{\prime}$ $\displaystyle=\\{(v,w)\in W\times W\mid
v\preccurlyeq w\\},$
$\displaystyle(v_{1},w_{1})\preccurlyeq^{\prime}(v_{2},w_{2})$
$\displaystyle\iff v_{1}=v_{2}\text{ and }w_{1}\preccurlyeq w_{2},$
$\displaystyle(v_{1},w_{1})\sqsubseteq^{\prime}(v_{2},w_{2})$
$\displaystyle\iff w_{1}\sqsubseteq w_{2},$ $\displaystyle V^{\prime}(v,w)$
$\displaystyle=V(w).$

As $\preccurlyeq$ is an upward-linear partial order, clearly
$\preccurlyeq^{\prime}$ is a partial order that is both upward and downward
linear. As $\sqsubseteq$ is a preorder, clearly $\sqsubseteq^{\prime}$ is a
preorder. For forth–up confluence, suppose
$(u_{1},v_{1})\sqsubseteq^{\prime}(u_{2},v_{2})$ and that
$(u_{1},v_{1})\preccurlyeq^{\prime}(u_{1},w_{1})$. Then $v_{1}\sqsubseteq
v_{2}$ and $v_{1}\preccurlyeq w_{1}$, so by forth–up confluence of
$\sqsubseteq$ there exists $w_{2}$ with $w_{1}\sqsubseteq w_{2}$ and
$v_{2}\preccurlyeq w_{2}$. By transitivity of $\preccurlyeq$, we have
$u_{2}\preccurlyeq w_{2}$, so that $(u_{2},w_{2})\in W^{\prime}$. Then
$(u_{1},w_{1})\sqsubseteq^{\prime}(u_{2},w_{2})$ and
$(u_{2},v_{2})\preccurlyeq^{\prime}(u_{2},w_{2})$, as required. Back–up
confluence is entirely analogous. Thus
$(W^{\prime},{\preccurlyeq^{\prime}},{\sqsubseteq^{\prime}})$ is a
$\mathsf{GS4}$ frame.

It is straightforward to check by structural induction on formulas that for
any ${\mathcal{L}}$-formula $\varphi$ and any $v,w\in W$, we have

$(\mathcal{M}^{\prime},(v,w))\models\varphi\iff(\mathcal{M},w)\models\varphi.$

We verify the left-to-right implication for the case that $\varphi$ is of the
form $\Box\psi$, since this will be instructive when we switch our focus to
$\mathsf{GS4^{c}}$. So suppose $(\mathcal{M}^{\prime},(v,w))\models\Box\psi$
and, let $w\preccurlyeq u$ and $u\sqsubseteq z$. Then
$(v,w)\preccurlyeq^{\prime}(v,u)$ and $(v,u)\sqsubseteq^{\prime}(z,z)$, so
$(\mathcal{M}^{\prime},(z,z))\models\psi$. Thus by the inductive hypothesis
$(\mathcal{M},z)\models\psi$. Since $u$ and $z$ were arbitrary, subject to
$w\preccurlyeq u$ and $u\sqsubseteq z$, we have
$(\mathcal{M},w)\models\Box\psi$, as required.

Thus $\mathcal{M}^{\prime}$ falsifies precisely the ${\mathcal{L}}$-formulas
falsified by $\mathcal{M}$. In other words, in proving the finite frame
property for $\mathsf{GS4}$ we may work exclusively with models based on
downward-linear $\mathsf{GS4}$ frames.

_Finite quotients._ Now let $\Sigma$ be a subformula-closed subset of
${\mathcal{L}}$. We will describe a quotient of any model based on a downward-
linear $\mathsf{GS4}$ frame that falsifies the same formulas from $\Sigma$ as
the original model and is finite whenever $\Sigma$ is finite.

Let $\mathcal{M}=(W,{\preccurlyeq},{\sqsubseteq},V)$ be a model based on a
downward-linear $\mathsf{GS4}$ frame. For $w\in W$, define
$\ell_{\mathcal{M}}(w)$ by

$\ell_{\mathcal{M}}(w)=\\{\varphi\in\Sigma\mid(\mathcal{M},w)\models\varphi\\}\text{,}$

and define

$L_{\mathcal{M}}(w)=\\{\ell(v)\mid w\preccurlyeq v\text{ or }v\preccurlyeq
w\\}.$

We define the equivalence relation $\approx$ on $W$ by

$w\approx v\iff(\ell(w),L(w))=(\ell(v),L(v)).$

If $\Sigma$ is finite, then clearly $W/{\approx}$ is finite.

It is straightforward to show that $\approx$ is a strong
$\Sigma$-bisimulation. Conversely, it is clear that if $w$ and $v$ are
strongly $\Sigma$-bisimilar, then $\ell(w)=\ell(v)$ and $L(w)=L(v)$, and hence
$w\approx v$. Thus $\approx$ is the greatest strong $\Sigma$-bisimulation
$\approx_{\Sigma}$.

By Lemma 15, the quotient $\mathcal{M}/{\approx}$ has all the properties
necessary to be a $\mathsf{GS4}$ frame. It is clear that if $\Sigma$ is finite
then $\mathcal{M}/{\approx}$ is finite.

######  Theorem 4.

$\mathsf{GS4}$ has the finite birelational frame property. That is, if a
formula $\varphi$ is falsifiable (respectively satisfiable) on a birelational
$\mathsf{GS4}$ frame, then $\varphi$ is falsifiable (respectively satisfiable)
on a finite birelational $\mathsf{GS4}$ frame.

In order to use Theorem 4 to prove decidability, we need to compute a bound on
the size of a model $\mathcal{M}/{\approx}$ in terms of the size of $\Sigma$,
when $\Sigma$ is finite. Note that $\nicefrac{{\preccurlyeq}}{{\approx}}$ is
given by the partial order

$[w]\mathrel{\nicefrac{{\preccurlyeq}}{{\approx}}}[v]\iff L(w)=L(v)\text{ and
}\ell(w)\supseteq\ell(v).$

######  Lemma 19.

Suppose $\Sigma$ is finite. Then the depth of $\mathcal{M}/{\approx}$ is
bounded by $|\Sigma|+1$, and the cardinality of the domain of
$\mathcal{M}/{\approx}$ is bounded by $(|\Sigma|+1)\cdot
2^{|\Sigma|(|\Sigma|+1)+1}$.

###### Proof.

Each element of the domain of $\mathcal{M}/{\approx}$ is a pair $(\ell,L)$
where $L$ is a (nonempty) subset of $\raisebox{2.0pt}{$\wp$}\Sigma$ and
$\ell\in L$. Since $L$ is linearly ordered by inclusion, it has depth at most
$|\Sigma|+1$. Hence $\mathcal{M}/{\approx}$ has depth at most $|\Sigma|+1$.
There are $(2^{|\Sigma|})^{i}$ subsets of $\raisebox{2.0pt}{$\wp$}\Sigma$ of
size $i$, so there are at most $\sum_{i=1}^{|\Sigma|+1}(2^{|\Sigma|})^{i}$
distinct $L$. The sum is bounded by $2^{|\Sigma|(|\Sigma|+1)+1}$. The factor
of $|\Sigma|+1$ corresponds to the choice of an $\ell\in L$, for each $L$. ∎

Thus we have an exponential bound on the size of $\mathcal{M}/{\approx}$.
Hence any falsifiable formula is falsifiable on an effectively bounded
quasimodel, and it follows that $\mathsf{GS4}$ is decidable.

######  Theorem 5.

The logic $\mathsf{GS4}$ is decidable.

###### Proof.

Since falsifiability is the complement of validity, it suffices to show that
it is decidable whether a formula $\varphi$ is falsifiable over the class of
all $\mathsf{GS4}$ frames. Let $\Sigma$ be the set of subformulas of
$\varphi$. The cardinality of $\Sigma$ is no greater than the length of
$\varphi$. If $\varphi$ is falsifiable in a $\mathsf{GS4}$ frame of size at
most $(|\Sigma|+1)\cdot 2^{|\Sigma|(|\Sigma|+1)+1}$, then in particular
$\varphi$ is falsifiable in a $\mathsf{GS4}$ frame. Conversely, if $\varphi$
is falsified in a $\mathsf{GS4}$ frame, then by Lemma 19, $\varphi$ is
falsified in a $\mathsf{GS4}$ frame of size at most $(|\Sigma|+1)\cdot
2^{|\Sigma|(|\Sigma|+1)+1}$. Hence, it suffices to check falsifiability of
$\varphi$ on the set of all $\mathsf{GS4}$ frames (with valuations only for
the variables appearing in $\varphi$) of size at most $(|\Sigma|+1)\cdot
2^{|\Sigma|(|\Sigma|+1)+1}$. It is clear that this check can be carried out
within a computable time bound; hence the problem is decidable. ∎

This argument yields a nexptime upper bound.

######  Corollary 2.

The logic $\mathsf{GS4}$ is in nexptime.

###### Proof.

Let $n$ be the length of a formula $\varphi$; thus $n$ bounds the number of
subformulas of $\varphi$. A nondeterministic algorithm runs as follows on
input $\varphi$.

  * •

Nondeterministically choose a structure
$\mathcal{M}=(W,{\preccurlyeq},{\sqsubseteq},V(p_{1}),\dots V(p_{m}))$ of
cardinality at most $(n+1)\cdot 2^{n(n+1)+1}$, where $p_{1},\dots p_{m}$ are
the variables appearing in $\varphi$. The structure $\mathcal{M}$ can be
stored with an exponential (in $n$) number of bits, and hence choosing
$\mathcal{M}$ can be done in exponential time.

  * •

Check that $\mathcal{M}$ is a $\mathsf{GS4}$ frame and reject if not. This
(deterministic) check takes exponential time.

  * •

Calculate the interpretations in $\mathcal{M}$ of each subformula of
$\varphi$. There are at most $n$ interpretations to calculate and each
calculation can be done deterministically in exponential time provided the
interpretations of subformulas of lower structural complexity are calculated
first.

  * •

Check whether there is any world not in the calculated interpretation of
$\varphi$.∎

###  5.3 The finite frame property for $\mathsf{GS4^{c}}$

We now proceed to proving the finite birelational frame property for
$\mathsf{GS4^{c}}$. The strategy is the same as for $\mathsf{GS4}$. However,
the result does not follow immediately from our $\mathsf{GS4}$ constructions,
because our construction of downward-linear $\mathsf{GS4}$ frames does not
preserve forth–down confluence and hence does not specialise to
$\mathsf{GS4^{c}}$ frames. We thus use a variant of our previous construction.
Before we define this, we need to show that without loss of generality,
$\mathsf{GS4^{c}}$ frames have an additional property.

######  Definition 17.

Let $(W,\preccurlyeq)$ be a preordered set. We say a binary relation $R$ on
$W$ is pointwise convex, if it validates the implication

$R(u,v_{1}),R(u,v_{2}),v_{1}\preccurlyeq w\preccurlyeq v_{2}\implies R(u,w).$

######  Lemma 20.

Let $(W,\preccurlyeq)$ be a preordered set and $R$ a binary relation on $W$.
Then the relation $\overline{R}$ defined by

$\overline{R}(u,w)\iff\exists v_{1}\preccurlyeq u\preccurlyeq
v_{2}:R(u,v_{1}),R(u,v_{2})$

is pointwise convex. We call this the convex closure of $R$. Forming
transitive closures preserves any confluence conditions. If $R$ is forth–up
and forth–down confluent and transitive, then $\overline{R}$ is transitive.

###### Proof.

The claims are straightforward to prove; we give the details for the last
claim. So suppose $R$ is forth–up and forth–down confluent and transitive and
that $\overline{R}(u,v)$ and $\overline{R}(v,w)$. Then there is
$v^{\prime}\preccurlyeq v$ with $R(u,v^{\prime})$ and $w^{\prime}\preccurlyeq
w$ with $R(v,w^{\prime})$. By forth–down confluence of $R$ there is
$w^{\prime\prime}\preccurlyeq w^{\prime}$ with
$R(v^{\prime},w^{\prime\prime})$. Then by transitivity of $\preccurlyeq$ and
$R$ respectively, we have $w^{\prime\prime}\preccurlyeq w$ and
$R(u,w^{\prime\prime})$. By a symmetric argument using forth–up confluence,
there also exists $z\succcurlyeq w$ with $R(u,z)$. So by definition
$\overline{R}(u,w)$. ∎

By Lemma 20, if $(W,{\preccurlyeq},{\sqsubseteq})$ is a $\mathsf{GS4^{c}}$
frame, then so is $(W,{\preccurlyeq},{\overline{\sqsubseteq}})$. Given a
valuation $V$, it is straightforward to show, by structural induction on
formulas and using monotonicity of $V$, that the satisfaction relation
$\models$ on $(W,{\preccurlyeq},{\overline{\sqsubseteq}},V)$ is identical to
that on $(W,{\preccurlyeq},{\sqsubseteq},V)$. Hence

> we may assume, without loss of generality, that $\mathsf{GS4^{c}}$ frames
> are pointwise convex.

_Downward-linear $\mathsf{GS4^{c}}$ frames._ Let
$\mathcal{M}=(W,{\preccurlyeq},{\sqsubseteq},V)$ be an arbitrary model based
on a pointwise convex $\mathsf{GS4^{c}}$ frame. We define a model
$\mathcal{M}^{\prime\prime}=(W^{\prime\prime},{\preccurlyeq^{\prime\prime}},{\sqsubseteq^{\prime\prime}},\allowbreak
V^{\prime\prime})$ based on a downward-linear $\mathsf{GS4^{c}}$ frame and
falsifying exactly the same ${\mathcal{L}}$-formulas as $\mathcal{M}$ as
follows. (The only difference with $\mathcal{M}^{\prime}$ from the previous
subsection is in the definition of $\sqsubseteq^{\prime\prime}$.)

$\displaystyle W^{\prime\prime}$ $\displaystyle=\\{(v,w)\in W\times W\mid
v\preccurlyeq w\\},$
$\displaystyle(v_{1},w_{1})\preccurlyeq^{\prime\prime}(v_{2},w_{2})$
$\displaystyle\iff v_{1}=v_{2}\text{ and }w_{1}\preccurlyeq w_{2},$
$\displaystyle(v_{1},w_{1})\sqsubseteq^{\prime\prime}(v_{2},w_{2})$
$\displaystyle\iff v_{1}\sqsubseteq v_{2}\text{ and }w_{1}\sqsubseteq w_{2},$
$\displaystyle V^{\prime\prime}(v,w)$ $\displaystyle=V(w).$

It is clear that $\mathcal{M}^{\prime\prime}$ is an upward- and downward-
linear bi-intuitionistic frame. We now check the confluence conditions. For
forth–up confluence, suppose
$(u_{1},v_{1})\sqsubseteq^{\prime\prime}(u_{2},v_{2})$ and that
$(u_{1},v_{1})\preccurlyeq^{\prime\prime}(u_{1},w_{1})$. Then
$v_{1}\sqsubseteq v_{2}$ and $v_{1}\preccurlyeq w_{1}$, so by forth–up
confluence of $\sqsubseteq$ there exists $w_{2}$ with $w_{1}\sqsubseteq w_{2}$
and $v_{2}\preccurlyeq w_{2}$. By transitivity of $\preccurlyeq$, we have
$u_{2}\preccurlyeq w_{2}$, so that $(u_{2},w_{2})\in W^{\prime\prime}$. Then
$(u_{1},w_{1})\sqsubseteq^{\prime\prime}(u_{2},w_{2})$ and
$(u_{2},v_{2})\preccurlyeq^{\prime\prime}(u_{2},w_{2})$, as required. Back–up
confluence is entirely analogous. For forth–down confluence, suppose
$(u_{1},w_{1})\sqsubseteq^{\prime\prime}(u_{2},w_{2})$ and that
$(u_{1},v_{1})\preccurlyeq^{\prime\prime}(u_{1},w_{1})$. We have
$v_{1}\succcurlyeq u_{1}\sqsubseteq u_{2}$, so by forth–up confluence, there
exists $v_{2}$ with $v_{1}\sqsubseteq v_{2}\succcurlyeq u_{2}$. By upward
linearity, either $v_{2}\preccurlyeq w_{2}$ or $w_{2}\preccurlyeq v_{2}$. In
the first case $(u_{2},v_{2})\preccurlyeq^{\prime\prime}(u_{2},w_{2})$ and we
are done. In the second case, apply forth–down confluence to
$v_{1}\preccurlyeq w_{1}\sqsubseteq w_{2}$ to obtain $z$ with
$v_{1}\sqsubseteq z\preccurlyeq w_{2}$. Then since $v_{1}\sqsubseteq z$ and
$v_{1}\sqsubseteq v_{2}$, and also $z\preccurlyeq w_{2}\preccurlyeq v_{2}$, we
have, by pointwise convexity, that $v_{1}\sqsubseteq w_{2}$. Then we have
$(u_{1},v_{1})\sqsubseteq^{\prime\prime}(u_{2},w_{2})\preccurlyeq^{\prime\prime}(u_{2},w_{2})$,
witnessing the forth–down confluence of $\sqsubseteq^{\prime\prime}$. We
conclude that
$(W^{\prime\prime},{\preccurlyeq^{\prime\prime}},{\sqsubseteq^{\prime\prime}})$
is a downward-linear $\mathsf{GS4^{c}}$ frame.

It is straightforward to check by structural induction on formulas that for
any ${\mathcal{L}}$-formula $\varphi$ and any $v,w\in W$, we have

$(\mathcal{M}^{\prime\prime},(v,w))\models\varphi\iff(\mathcal{M},w)\models\varphi.$

We verify the left-to-right implication for the case that $\varphi$ is of the
form $\Box\psi$. So suppose
$(\mathcal{M}^{\prime\prime},(v,w))\models\Box\psi$ and, let $w\preccurlyeq u$
and $u\sqsubseteq z$. Then $(v,w)\preccurlyeq^{\prime\prime}(v,u)$ and
$(v,u)\sqsubseteq^{\prime\prime}(z,z)$, so
$(\mathcal{M}^{\prime},(z,z))\models\psi$. Then $v\preccurlyeq u\sqsubseteq
z$, so by forth–down confluence there exists $y$ with $v\sqsubseteq
y\preccurlyeq z$. Then $(v,w)\preccurlyeq^{\prime\prime}(v,u)$ and
$(v,u)\sqsubseteq^{\prime\prime}(y,z)$, so
$(\mathcal{M}^{\prime\prime},(y,z))\models\psi$. Thus by the inductive
hypothesis $(\mathcal{M},z)\models\psi$. Since $u$ and $z$ were arbitrary,
subject to $w\preccurlyeq u$ and $u\sqsubseteq z$, we have
$(\mathcal{M},w)\models\Box\psi$, as required.

Thus $\mathcal{M}^{\prime\prime}$ falsifies precisely the
${\mathcal{L}}$-formulas falsified by $\mathcal{M}$. So in proving the finite
frame property for $\mathsf{GS4^{c}}$ we may work exclusively with models
based on downward-linear $\mathsf{GS4^{c}}$ frames.

Now let $\Sigma$ be a subformula-closed subset of ${\mathcal{L}}$. Given a
downward-linear $\mathsf{GS4^{c}}$ frame $\mathcal{M}$, we know from Section
5.2 that the quotient $\nicefrac{{\mathcal{M}}}{{\approx}}$ is a
$\mathsf{GS4}$ frame of size at most $(|\Sigma|+1)\cdot
2^{|\Sigma|(|\Sigma|+1)+1}$ falsifying precisely the same formulas as
$\mathcal{M}$. By Lemma 18, $\nicefrac{{\mathcal{M}}}{{\approx}}$ is also
forth–down confluent and hence a $\mathsf{GS4^{c}}$ frame. This yields the
following results.

######  Theorem 6.

The logic ${\mathsf{GS4}}^{\mathsf{c}}$ has the finite birelational frame
property, and hence is decidable.

######  Corollary 3.

The logic $\mathsf{GS4^{c}}$ is in nexptime.

###  5.4 Shallow frames

A key ingredient in our finite frame property proofs for $\mathsf{CS4}$ and
$\mathsf{S4I}$ is to work with _shallow frames_ , which are frames where the
_depths_ of worlds are bounded. Given a frame
$\mathcal{F}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq})$ and $w\in W$, the
depth of $w$ is the supremum, in $\mathbb{N}\cup\\{\infty\\}$, of all
$n\in\mathbb{N}$ such that there is a sequence

$w=w_{0}\prec w_{1}\prec\ldots\prec w_{n}.$

The depth of the frame $\mathcal{F}$ is the supremum of all depths of elements
of $W$. The depth of a model is the depth of its underlying frame. Note that
the depth of worlds or frames/models could be $\infty$. If a frame or model
has finite depth, we say that it is shallow. Shallow models will provide an
important intermediate step towards establishing the finite frame property, as
the bisimulation quotient of a shallow model is finite. Nevertheless, it can
be quite large, as it is only superexponentially bounded.

Let $2^{m}_{k}$ be the superexponential function defined recursively by
$2^{m}_{0}=m$ and $2^{m}_{k+1}=2^{2^{m}_{k}}$.

######  Lemma 21.

For all $m,n,k\geq 1$:

$2^{m}\cdot 2_{k}^{(n-1)m}\leq 2_{k}^{nm}.$

###### Proof.

Proceed by induction on $k$. If $k=1$, then

$2^{m}\cdot 2_{k}^{(n-1)m}=2^{m}\cdot 2^{(n-1)m}=2_{k}^{nm}.$

If $k>1$, then note that $1\leq 2_{k-1}^{(n-1)m}$, so that

$m+2_{k-1}^{(n-1)m}\leq(m+1)2_{k-1}^{(n-1)m}\leq 2^{m}\cdot
2_{k-1}^{(n-1)m}\stackrel{{\scriptstyle\text{{IH}}}}{{\leq}}2_{k-1}^{nm}.$

Then

$2^{m}\cdot 2_{k}^{(n-1)m}=2^{m}\cdot
2^{2_{k-1}^{(n-1)m}}=2^{m+2_{k-1}^{(n-1)m}}\leq 2^{2_{k-1}^{nm}}=2_{k}^{nm},$

as needed. ∎

######  Lemma 22.

Given a bi-intuitionistic model
$\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$ of finite depth $n$
and finite $\Sigma\subseteq{\mathcal{L}}$ with $|\Sigma|=s$:

$|\nicefrac{{W}}{{\sim_{\Sigma}}}|\leq 2^{2(n+1)s}_{n+2}.$

###### Proof sketch.

This is proven in some detail in for example [33], but we outline the main
elements of the proof. Proceed by induction on $n\in\mathbb{N}$ to show that
there are at most $2^{2(n+1)s}_{n+2}$ $\Sigma$-bisimulation classes of points
of depth $n$. Let $w\in W$. If $w$ has depth $0$, its bisimulation class is
uniquely determined by the labels $\ell(v)\in 2^{\Sigma}\times 2^{\Sigma}$ of
those $v$ in the cluster of $w$ (that is, the set of $v\in W$ such that
$v\preccurlyeq w\preccurlyeq v$), and there are at most $2^{2s}=2^{2s}_{1}$
choices for each label, so there are at most $2^{2^{2s}_{1}}=2^{2s}_{2}$
choices for the entire cluster.

For the inductive step, let $\\{[v_{i}]\mid i\in I\\}$ enumerate the
equivalence classes of the immediate successors of $w$. Note that each $v_{i}$
has depth less than that of $w$, so that by the induction hypothesis, there
are at most $2^{2ns}_{n+1}$ choices for $[v_{i}]$, and the bisimulation class
of $w$ is determined by the labels of its cluster, for which there are
$2^{2^{2s}}$ choices, and a possible choice of $\\{[v_{i}]:i\in I\\}$, of
which there are at most $2^{2^{2ns}_{n+1}}$ choices. Hence there are at most

$2^{2^{2s}}\cdot 2^{2^{2ns}_{n+1}}=2^{2^{2s}+2^{2ns}_{n+1}}\leq
2^{2^{2(n+1)s}_{n+1}}=2^{2(n+1)s}_{n+2}$

choices for the bisimulation class of $w$. ∎

The following lemma is proven analogously to Lemma 22. A bi-intuitionistic
model $\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},V)$ is forest-like
if for every $w\in W$, the set $\\{v\in W\mid v\preccurlyeq w\\}$ is totally
ordered by $\preccurlyeq$.

######  Lemma 23.

Given a forest-like bi-intuitionistic model
$\mathcal{M}=(W,W^{\bot},{\preccurlyeq},{\sqsubseteq},\allowbreak V)$ of
finite depth $n$ and finite $\Sigma\subseteq{\mathcal{L}}$ with $|\Sigma|=s$,
we have $|\nicefrac{{W}}{{\approx_{\Sigma}}}|\leq 2^{2(n+1)s}_{n+2}$.

######  Remark 2.

Note that the forest-like assumption in Lemma 23 is needed, as in general
there may be infinitely many $\approx_{\Sigma}$ equivalence classes of points
if this assumption fails. In a model consisting of an infinite sequence

$w_{0}\succ v_{0}\prec w_{1}\succ v_{1}\prec w_{2}\succ\ldots$

where $p$ is true only on $w_{0}$, no two points are strongly
$\sim_{\\{p\\}}$-bisimilar.

We conclude this section by showing that the shallow frame property implies
the finite model property for the two logics we are interested in.

######  Proposition 4.

Let $\varphi\in{\mathcal{L}}$.

  1. 1.

If $\varphi$ is falsifiable (respectively satisfiable) on a shallow
$\mathsf{CS4}$ frame, then $\varphi$ is falsifiable (respectively satisfiable)
on a finite $\mathsf{CS4}$ frame.

  2. 2.

If $\varphi$ is falsifiable (respectively satisfiable) on a shallow, forest-
like $\mathsf{S4I}$ frame, then $\varphi$ is falsifiable (respectively
satisfiable) on a finite $\mathsf{S4I}$ frame.

###### Proof.

#### 1

Let $\mathcal{M}$ be a model based on a shallow $\mathsf{CS4}$ frame that
falsifies (respectively satisfies) $\varphi$. Define $\Sigma$ to be the set of
subformulas of $\varphi$. Then $\nicefrac{{\mathcal{M}}}{{\sim_{\Sigma}}}$ is
finite by Lemma 22, is based on a $\mathsf{CS4}$ frame by Lemma 15, and
falsifies (respectively satisfies) $\varphi$ by Lemma 16.

#### 2

Let $\mathcal{M}$ be a model based on a shallow forest-like $\mathsf{S4I}$
frame that falsifies (respectively satisfies) $\varphi$. Define $\Sigma$ to be
the set of subformulas of $\varphi$. By Lemma 18 we see that
$\nicefrac{{\mathcal{M}}}{{\approx_{\Sigma}}}$ is forth–down confluent.
Reasoning as before, with Lemma 23 in place of Lemma 22, the structure
$\nicefrac{{\mathcal{M}}}{{\approx_{\Sigma}}}$ is a finite model based on an
$\mathsf{S4I}$ frame and falsifies (respectively satisfies) $\varphi$. ∎

Thus in order to prove the finite frame property for these logics, it suffices
to show that they have the shallow frame property (with respect to the
intended class of frames): that any non-valid formula is falsifiable on a
shallow frame (of the appropriate type). This is the strategy that we will
employ in the sequel.

Note that we can, in an identical manner, prove versions of Proposition 4(1)
for $\mathsf{IS4}$ and $\mathsf{GS4}$ and a version of Proposition 4(2) for
$\mathsf{GS4^{c}}$, but we do not need these results here.

###  5.5 The finite frame property for $\mathsf{CS4}$

In view of Proposition 4(1), in order to prove the finite frame property for
$\mathsf{CS4}$, it suffices to prove the shallow frame property. To this end
we define a shallow model, $\mathcal{M}_{\Sigma}^{\mathsf{CS4}}$. In this
subsection, the notation $W_{\mathrm{c}},{\preccurlyeq_{\mathrm{c}}}$, etc.
will refer to the canonical model $\mathcal{M}^{\mathsf{CS4}}_{\mathrm{c}}$
for $\mathsf{CS4}$ (see Section 4.3).

######  Definition 18.

Given $\Gamma,\Delta\in W_{\mathrm{c}}$, define
$\Gamma\preccurlyeq_{\Sigma}\Delta$ if $\Gamma\preccurlyeq_{\mathrm{c}}\Delta$
and either $\Gamma^{+}=\Delta^{+}$ or there exists $\chi\in\Sigma$ such that
$\chi\in\Delta^{+}\setminus\Gamma^{+}$. We then define
$\mathcal{M}_{\Sigma}^{\mathsf{CS4}}=(W_{\mathrm{c}},{\preccurlyeq_{\Sigma}},{\sqsubseteq_{\mathrm{c}}},V_{\mathrm{c}})$.

Thus $\mathcal{M}_{\Sigma}^{\mathsf{CS4}}$ is almost identical to
$\mathcal{M}_{\mathrm{c}}^{\mathsf{CS4}}$, but we have modified the
intuitionistic accessibility relation. It is easy to see that
$\mathcal{M}_{\Sigma}^{\mathsf{CS4}}$ is a bi-intuitionistic model.

######  Lemma 24.

For all $\Gamma\in W_{\mathrm{c}}$ and
$\varphi\mathbin{\rightarrow}\psi\in\Sigma$ we have that
$\varphi\mathbin{\rightarrow}\psi\in\Gamma^{+}$ if and only if for all
$\Delta\succcurlyeq_{\Sigma}\Gamma$, $\varphi\in\Delta^{+}$ implies
$\psi\in\Delta^{+}$.

###### Proof.

From left to right, let us take $\Gamma\in W_{\mathrm{c}}$ such that
$\varphi\rightarrow\psi\in\Gamma^{+}$. Take any $\Delta\in W_{\mathrm{c}}$
such that $\Gamma\preccurlyeq_{\Sigma}\Delta$. By definition,
$\Gamma^{+}\subseteq\Delta^{+}$ so $\varphi\rightarrow\psi\in\Delta^{+}$. If
$\varphi\in\Delta^{+}$, it follows that $\psi\in\Delta^{+}$

Conversely, assume towards a contradiction that
$\varphi\rightarrow\psi\not\in\Gamma^{+}$. Therefore, there exists
$\Delta\succcurlyeq_{\mathrm{c}}\Gamma$ such that $\varphi\in\Delta^{+}$ and
$\psi\not\in\Delta^{+}$:  1. If $\Delta^{+}\cap\Sigma=\Gamma^{+}\cap\Sigma$
then we already have $\varphi\in\Gamma^{+}$ and $\psi\not\in\Gamma^{+}$, and
$\Gamma\preccurlyeq_{\Sigma}\Gamma$, as needed.  2. If
$\Delta^{+}\cap\Sigma\neq\Gamma^{+}\cap\Sigma$, since
$\Delta\succcurlyeq_{\mathrm{c}}\Gamma$, we conclude that
$\Delta\succcurlyeq_{\Sigma}\Gamma$.  ∎

######  Lemma 25.

Any $\prec_{\Sigma}$-chain has length at most $|\Sigma|+1$.

###### Proof.

Let
$\Gamma_{0}\prec_{\Sigma}\Gamma_{1}\prec_{\Sigma}\ldots\prec_{\Sigma}\Gamma_{n}$
be any chain. For each $i<n$ there is $\varphi_{i}\in\Sigma$ such that
$\varphi_{i}\in\Gamma^{+}_{i+1}\setminus\Gamma^{+}_{i}$. Note that if $i<j<n$
then $\varphi_{i}\neq\varphi_{j}$, since by monotonicity
$\varphi_{i}\in\Gamma^{+}_{i+1}$ implies that $\varphi_{i}\in\Gamma^{+}_{j}$.
Hence $n\leq|\Sigma|$, so the length of the chain is at most $|\Sigma|+1$. ∎

######  Lemma 26.

The model $\mathcal{M}_{\Sigma}^{\mathsf{CS4}}$ is back–up confluent.

###### Proof.

If $\Phi\sqsubseteq_{\mathrm{c}}\Psi\preccurlyeq_{\Sigma}\Theta$ then also
$\Psi\preccurlyeq_{\mathrm{c}}\Theta$, so that setting
$\Upsilon\coloneqq(\Phi^{+};\varnothing)$, Proposition 10 yields
$\Phi\preccurlyeq_{\mathrm{c}}\Upsilon\sqsubseteq_{\mathrm{c}}\Theta$, and
clearly we also have $\Phi\preccurlyeq_{\Sigma}\Upsilon$, providing the
required witness. ∎

######  Lemma 27.

The following items hold.

  * •

If $\Diamond\varphi\in\Sigma$ and $\Gamma\in W_{\mathrm{c}}$ then
$\Diamond\varphi\in\Gamma^{+}$ if and only if for all
$\Psi\succcurlyeq_{\Sigma}\Gamma$ there is $\Delta$ such that
$\Psi\sqsubseteq_{\mathrm{c}}\Delta$ and $\varphi\in\Delta^{+}$.

  * •

If $\Box\varphi\in\Sigma$ and $\Gamma\in W_{\mathrm{c}}$ then
$\Box\varphi\in\Gamma^{+}$ if and only if for all $\Psi$ and $\Delta$ such
that $\Gamma\preccurlyeq_{\Sigma}\Psi\sqsubseteq_{\mathrm{c}}\Delta$,
$\varphi\in\Delta^{+}$.

###### Proof.

For the first item, suppose that $\Diamond\varphi\in\Sigma$ and $\Gamma\in
W_{\mathrm{c}}$ is such that $\Diamond\varphi\in\Gamma^{+}$. Let
$\Psi\succcurlyeq_{\Sigma}\Gamma$. It follows that
$\Psi\succcurlyeq_{\mathrm{c}}\Gamma$, so there is $\Delta$ such that
$\Psi\sqsubseteq_{\mathrm{c}}\Delta$ and $\varphi\in\Delta^{+}$, as needed.
Conversely, assume that $\Diamond\varphi\not\in\Gamma^{+}$. Consider
$\Psi\coloneqq(\Gamma^{+};\\{\varphi\\})$. Then
$\Psi\succcurlyeq_{\Sigma}\Gamma$, and if
$\Delta\sqsupseteq_{\mathrm{c}}\Psi$, it follows that
$\varphi\not\in\Delta^{+}$.

For the second item, from left to right assume that $\Box\varphi\in\Gamma^{+}$
and suppose that
$\Gamma\preccurlyeq_{\Sigma}\Psi\sqsubseteq_{\mathrm{c}}\Delta$. It follows
that $\Gamma\preccurlyeq_{\mathrm{c}}\Psi$, so $\Gamma^{+}\subseteq\Psi^{+}$,
and hence $\Box\varphi\in\Psi^{+}$. Since
$\Psi\sqsubseteq_{\mathrm{c}}\Delta$, then $\varphi\in\Delta^{+}$. Conversely,
assume that $\Box\varphi\not\in\Gamma^{+}$. As in the proof of Lemma 11, if we
define $\Psi\coloneqq(\Gamma^{+};\varnothing)$, there exists
$\Delta\sqsupseteq_{\mathrm{c}}\Psi$ such that $\varphi\not\in\Delta^{+}$.
From $\Gamma^{+}=\Psi^{+}$, it is easy to conclude that
$\Gamma\preccurlyeq_{\Sigma}\Psi$. ∎

From Lemmas 24 and 27 we immediately obtain the following.

######  Lemma 28.

For all $\Gamma\in W_{\mathrm{c}}$ and $\varphi\in\Sigma$, we have
$(\mathcal{M}_{\Sigma}^{\mathsf{CS4}},\Gamma)\models\varphi$ if and only if
$\varphi\in\Gamma^{+}$.

######  Lemma 29.

For $\varphi\in\Sigma$, we have $\varphi\in\mathsf{CS4}$ if and only if
$\mathcal{M}_{\Sigma}^{\mathsf{CS4}}\models\varphi$.

###### Proof.

We know that $\varphi\in\mathsf{CS4}$ if and only if
$\mathcal{M}^{\mathsf{CS4}}_{\mathrm{c}}\models\varphi$. So given $\Gamma\in
W_{\mathrm{c}}$, we know $\varphi\in\mathsf{CS4}$ implies
$\varphi\in\Gamma^{+}$, which then by Lemma 28 gives
$(\mathcal{M}_{\Sigma}^{\mathsf{CS4}},\Gamma)\models\varphi$. Conversely, if
$\varphi\not\in\mathsf{CS4}$ then there is $\Gamma\in W_{\mathrm{c}}$ such
that $\varphi\not\in\Gamma^{+}$, which implies that $\varphi$
$(\mathcal{M}^{\mathsf{CS4}}_{\Sigma},\Gamma)\not\models\varphi$. ∎

######  Theorem 7.

$\mathsf{CS4}$ has the finite frame property. That is, if a formula $\varphi$
is falsifiable (respectively satisfiable) on a $\mathsf{CS4}$ frame, then
$\varphi$ is falsifiable (respectively satisfiable) on a finite $\mathsf{CS4}$
frame.

###### Proof.

In view of Theorem 4(1), it suffices to show that $\mathsf{CS4}$ has the
shallow frame property. Fix a formula $\varphi$ and let $\Sigma$ be the set of
subformulas of $\varphi$. By Lemma 25 and Lemma 26,
$\mathcal{M}_{\Sigma}^{\mathsf{CS4}}$ is a model based on a shallow
$\mathsf{CS4}$ frame, and by Lemma 29,
$\mathcal{M}_{\Sigma}^{\mathsf{CS4}}\models\varphi$ if and only if
$\varphi\in\mathsf{CS4}$, as needed. ∎

###  5.6 The finite frame property for $\mathsf{S4I}$

Our aim is to prove that $\mathsf{S4I}$ has the shallow frame property, from
where the finite frame property will follow. The construction we will use has
certain elements in common with that for $\mathsf{CS4}$, with the caveat that
we need to ensure that our models are forest-like in order to apply Theorem
4(2). The following construction will ensure this. In this subsection,
$W_{\mathrm{c}},{\preccurlyeq_{\mathrm{c}}}$, etc. refer to the components of
$\mathcal{M}^{\mathsf{S4I}}_{\mathrm{c}}$ (see Section 4.2), and
$W_{\Sigma},{\preccurlyeq_{\Sigma}}$, etc. will refer to the respective
components of the model $\mathcal{M}^{\mathsf{S4I}}_{\Sigma}$ to be
constructed below.

######  Definition 19.

For a set of formulas $\Sigma$ closed under subformulas, define $W_{\Sigma}$
to be the set of all tuples $\Gamma=(\Gamma_{0},\ldots,\Gamma_{n})$, where

  1. 1.

each $\Gamma_{i}\in W_{\mathrm{c}}$,

  2. 2.

$\Gamma_{i}\preccurlyeq_{\mathrm{c}}\Gamma_{i+1}$ if $i<n$,

  3. 3.

for each $i<n$ there is a formula $\varphi\in\Sigma$ such that
$\varphi\in\Gamma_{i+1}\setminus\Gamma_{i}$.

We define $V_{\Sigma}$ by $\Gamma\in V_{\Sigma}(p)$ if and only if
$p\in\Gamma_{n}^{+}\cap\Sigma$. Define $\Gamma\preccurlyeq_{\Sigma}\Delta$ if
$\Gamma$ is an initial sequence of $\Delta$.

######  Lemma 30.

The relation $\preccurlyeq_{\Sigma}$ is a forest-like partial order on
$W_{\Sigma}$ and any strict $\preccurlyeq_{\Sigma}$-chain has length at most
$|\Sigma|+1$. Moreover, $V_{\Sigma}$ is monotone.

###### Proof.

That $\preccurlyeq_{\Sigma}$ is a forest-like partial order is easily checked
from the definitions, and the bound on chains follows from the same reasoning
as for Lemma 25, using the observation that
$\Gamma\preccurlyeq_{\Sigma}\Delta$ implies that
$\ell^{+}(\Gamma)\subsetneq\ell^{+}(\Delta)$. The monotonicity of $V_{\Sigma}$
follows from the elements of $\Gamma$ being ordered by
$\preccurlyeq_{\mathrm{c}}$. ∎

######  Lemma 31.

For all $\Gamma\in W_{\Sigma}$ and $\varphi\mathbin{\rightarrow}\psi\in\Sigma$
we have that $\varphi\mathbin{\rightarrow}\psi\in\ell^{+}(\Gamma)$ if and only
if for all $\Delta\succcurlyeq_{\Sigma}\Gamma$ with
$\varphi\in\ell^{+}(\Delta)$ we have $\psi\in\ell^{+}(\Delta)$.

###### Proof.

First assume that $\Gamma=(\Gamma_{0},\ldots,\Gamma_{n})$ is such that
$\varphi\mathbin{\rightarrow}\psi\in\ell^{+}(\Gamma)$ and let
$\Delta=(\Delta_{0},\ldots,\Delta_{m})$ be such that
$\Gamma\preccurlyeq_{\Sigma}\Delta$. Then $m\geq n$ and
$\Delta_{n}=\Gamma_{n}$, which by transitivity of $\preccurlyeq_{\mathrm{c}}$
implies that $\Gamma_{n}\preccurlyeq_{\mathrm{c}}\Delta_{m}$. It follows that
if $\varphi\in\ell^{+}(\Delta)$ then $\psi\in\ell^{+}(\Delta)$.

Conversely, suppose that
$\varphi\mathbin{\rightarrow}\psi\in\Sigma\setminus\ell^{+}(\Gamma)$. We may
further assume, without loss of generality, that if
$\varphi\in\ell^{+}(\Gamma)$ then $\psi\in\ell^{+}(\Gamma)$, for otherwise we
may take $\Delta=\Gamma$. Then there is
$\Delta_{n+1}\succcurlyeq_{\mathrm{c}}\Gamma_{n}$ such that
$\varphi\in\Delta_{n+1}$ but $\psi\not\in\Delta_{n+1}$. For $i\leq n$ set
$\Delta_{i}=\Gamma_{i}$, and define $\Delta=(\Delta_{i})_{i\leq n+1}$. It
should then be clear that $\Delta$ has the desired properties. ∎

The accessibility relation for $\mathsf{S4I}$ is a bit more involved than that
for $\mathsf{CS4}$.

######  Definition 20.

For theories $\Phi$, $\Psi$ in $W_{\mathrm{c}}$ we define
$\Phi\preccurlyeq^{0}_{\Sigma}\Psi$ if $\Phi\preccurlyeq_{\mathrm{c}}\Psi$ and
$\Phi^{+}\cap\Sigma=\Psi^{+}\cap\Sigma$. We define
$\Gamma\sqsubseteq^{0}_{\Sigma}\Delta$ if there is $\Theta$ so that
$\Gamma\sqsubseteq_{\mathrm{c}}\Theta\succcurlyeq^{0}_{\Sigma}\Delta$.

We define, for $\Gamma=(\Gamma_{0},\ldots,\Gamma_{n})$ and
$\Delta=(\Delta_{0},\ldots,\Delta_{m})\in W_{\Sigma}$,
$\Gamma\sqsubseteq^{1}_{\Sigma}\Delta$ if there is a non-decreasing sequence
$j_{1},\ldots j_{n}$ with $j_{n}=m$ such that
$\Gamma_{i}\sqsubseteq^{0}_{\Sigma}\Delta_{j_{i}}$ for $i\leq n$. We define
$\sqsubseteq_{\Sigma}$ to be the transitive closure of
$\sqsubseteq^{1}_{\Sigma}$.

With this, we define
$\mathcal{M}^{\mathsf{S4I}}_{\Sigma}=(W_{\Sigma},{\preccurlyeq_{\Sigma}},{\sqsubseteq_{\Sigma}},V_{\Sigma})$.
It is easy to check using the above lemmas that
$\mathcal{M}^{\mathsf{S4I}}_{\Sigma}$ is a bi-intuitionistic model. Next we
show that it is indeed a model based on an $\mathsf{S4I}$ frame.

######  Lemma 32.

The relation $\sqsubseteq_{\Sigma}$ is forth–up and forth–down confluent on
$S$.

###### Proof.

As before, it suffices to show that $\sqsubseteq^{1}_{\Sigma}$ is forth–up and
forth–down confluent. Suppose that $\Phi\preccurlyeq_{\Sigma}\Phi^{\prime}$
and $\Phi\sqsubseteq^{1}_{\Sigma}\Delta$ and write
$\Phi^{\prime}=(\Phi_{i})_{i\leq m^{\prime}}$, so that $\Phi=(\Phi_{i})_{i\leq
m}$ for some $m\leq m^{\prime}$, and $\Delta=(\Delta_{i})_{i\leq n}$. We
construct $\Delta^{\prime}=(\Delta_{i})_{i\leq n^{\prime}}$ for some
$n^{\prime}\geq n$ such that
$\Phi^{\prime}\sqsubseteq_{\Sigma}\Delta^{\prime}$ and
$\Delta\preccurlyeq_{\Sigma}\Delta^{\prime}$. Given $k\in[m,m^{\prime}]$, we
assume inductively that $(\Delta_{i})_{i\leq r}$ have been built so that
$(\Phi_{i})_{i\leq k}\sqsubseteq_{\Sigma}(\Delta_{i})_{i\leq r}$. The base
case with $r=m$ is already given by the assumption that
$\Phi\sqsubseteq_{\Sigma}\Delta$. For the inductive step, assume that
$(\Phi_{i})_{i\leq k}\sqsubseteq_{\Sigma}(\Delta_{i})_{i\leq r}$. Then in
particular, $\Phi_{k}\sqsubseteq^{0}_{\Sigma}\Delta_{r}$. By the definition of
$\sqsubseteq_{\Sigma}^{0}$, there is $\Theta\in W_{\mathrm{c}}$ so that
$\Phi_{k}\sqsubseteq_{\mathrm{c}}\Theta\succcurlyeq^{0}_{\Sigma}\Delta_{r}$.
By forth–up confluence of $\mathcal{M}^{\mathsf{S4I}}_{\mathrm{c}}$, there is
$\Upsilon$ such that
$\Phi_{k+1}\sqsubseteq_{\mathrm{c}}\Upsilon\succcurlyeq_{\mathrm{c}}\Theta$.
If $\Delta_{r}^{+}\cap\Sigma=\Upsilon^{+}\cap\Sigma$, we observe that
$\Delta_{r}\preccurlyeq^{0}_{\Sigma}\Upsilon$. Hence
$\Phi_{k+1}\sqsubseteq^{0}_{\Sigma}\Delta_{r}$, so that $(\Phi_{i})_{i\leq
k+1}\sqsubseteq^{1}_{\Sigma}(\Delta_{i})_{i\leq r}$. In this case, we may
simply set $r^{\prime}=r$. Otherwise, we set $r^{\prime}=r+1$ and
$\Delta_{r+1}=\Upsilon$. In this case, we also have that $(\Phi_{i})_{i\leq
k}\sqsubseteq^{1}_{\Sigma}(\Delta_{i})_{i\leq r}$. ∎

######  Lemma 33.

Let $\Gamma\in W_{\Sigma}$.

  1. 1.

If $\Diamond\varphi\in\Sigma$ then $\Diamond\varphi\in\ell^{+}(\Gamma)$ if and
only if there is $\Delta\sqsupseteq_{\Sigma}\Gamma$ such that
$\varphi\in\ell^{+}(\Delta)$.

  2. 2.

If $\Box\varphi\in\Sigma$ then $\Box\varphi\in\ell^{+}(\Gamma)$ if and only if
for every $\Delta\sqsupseteq_{\Sigma}\Gamma$, $\varphi\in\ell^{+}(\Delta)$.

###### Proof.

Let $\Gamma=(\Gamma_{i})_{i\leq n}$. For the first claim, we first prove the
easier right-to-left direction. Suppose that $\Delta=(\Delta_{i})_{i\leq
m}\sqsupseteq^{1}_{\Sigma}\Gamma$ is such that $\varphi\in\ell^{+}(\Delta)$,
meaning that $\varphi\in\Delta_{m}^{+}$. Then
$\Gamma_{n}\sqsubseteq^{0}_{\Sigma}\Delta_{m}$, which means that for some
$\Theta$,
$\Gamma_{n}\sqsubseteq_{\mathrm{c}}\Theta\succcurlyeq^{0}_{\Sigma}\Delta_{m}$.
Then $\varphi\in\Theta^{+}$; hence
$\Diamond\varphi\in\Gamma_{n}^{+}=\ell^{+}(\Gamma)$ by the truth lemma. If
instead $\Delta\sqsupseteq_{\Sigma}\Gamma$, then there is a sequence

$\Gamma=\Upsilon_{0}\sqsubseteq^{1}_{\Sigma}\Upsilon_{1}\sqsubseteq^{1}_{\Sigma}\ldots\sqsubseteq^{1}_{\Sigma}\Upsilon_{n}=\Delta,$

and back–up induction on $i$ shows that
$\Diamond\varphi\in\ell^{+}(\Upsilon_{i})$, so that in particular
$\Diamond\varphi\in\ell^{+}(\Gamma)$.

For the left-to-right direction, suppose that
$\Diamond\varphi\in\ell^{+}(\Gamma)$. By back–up induction on $k\leq n$ we
prove that there exists some sequence $(\Theta_{i})_{i=k}^{n}$ such that
$\Gamma_{i}\sqsubseteq_{\mathrm{c}}\Theta_{i}$ for each $i\in[k,n]$ and
$\Theta_{i}\preccurlyeq_{\mathrm{c}}\Theta_{i+1}$ if $i\in[k,n)$ (interval