smullyan tableaux/.style=for tree=math content,where n children=1!1.before
computing xy=l=,!1.no edge,closed/.style=label=below:$\times$,,

# Crisp bi-Gödel modal logic and its paraconsistent expansion††thanks: The
research of Marta Bílková was supported by the grant 22-01137S of the Czech
Science Foundation. The research of Sabine Frittella and Daniil Kozhemiachenko
was funded by the grant ANR JCJC 2019, project PRELAP (ANR-19-CE48-0006).

Marta Bílková  The Czech Academy of Sciences, Institute of Computer Science,
Czech Republic  Sabine Frittella  INSA Centre Val de Loire, Univ. Orléans,
LIFO EA 4022, France  Daniil Kozhemiachenko  INSA Centre Val de Loire, Univ.
Orléans, LIFO EA 4022, France

###### Abstract

In this paper, we provide a Hilbert-style axiomatisation for the crisp bi-
Gödel modal logic $\mathbf{K}\mathsf{biG}$. We prove its completeness w.r.t.
crisp Kripke models where formulas at each state are evaluated over the
standard bi-Gödel algebra on $[0,1]$. We also consider a paraconsistent
expansion of $\mathbf{K}\mathsf{biG}$ with a De Morgan negation $\neg$ which
we dub $\mathbf{K}\mathsf{G}^{2}$. We devise a Hilbert-style calculus for this
logic and, as a consequence of a conservative translation from
$\mathbf{K}\mathsf{biG}$ to $\mathbf{K}\mathsf{G}^{2}$, prove its completeness
w.r.t. crisp Kripke models with two valuations over $[0,1]$ connected via
$\neg$.

For these two logics, we establish that their decidability and validity are
$\mathsf{PSPACE}$-complete.

We also study the semantical properties of $\mathbf{K}\mathsf{biG}$ and
$\mathbf{K}\mathsf{G}^{2}$. In particular, we show that Glivenko theorem holds
only in finitely branching frames. We also explore the classes of formulas
that define the same classes of frames both in $\mathbf{K}$ (the classical
modal logic) and the crisp Gödel modal logic $\mathfrak{GK}^{c}$. We show
that, among others, all Sahlqvist formulas and all formulas
$\phi\rightarrow\chi$ where $\phi$ and $\chi$ are monotone, define the same
classes of frames in $\mathbf{K}$ and $\mathfrak{GK}^{c}$.

Keywords:  paraconsistent logics; Gödel modal logic; correspondence theory;
axiomatic systems; complexity

##  1 Introduction

The present paper is conceived as a natural continuation of the project
commenced in [8] and continued in [5] and then in [6]. In the project, we aim
at devising logics that formalise reasoning with inconsistent, incomplete and
(or) uncertain information.

In the last paper, we provided two logics — the bi-Gödel modal logic
$\mathbf{K}\mathsf{biG}$ (and its fuzzy version
$\mathbf{K}\mathsf{biG}^{\mathsf{f}}$) and $\mathbf{K}\mathsf{G}^{2}$ — its
paraconsistent expansion with a De Morgan negation $\neg$. We also studied
finitely branching both logics whose validity was restricted to finitely
branching frames and argued for their utility in the representation of agents’
beliefs. In this paper, we aim at the study of the logics not restricted to
the finitely branching frames.

#### Gödel modal logics

Conceptually, this paper has two sources of inspiration. First of all, we
expand on the existing research on Gödel modal logics as provided in multiple
papers [16, 14, 17, 15, 29]. Gödel modal logics are well-researched: their
complete axiomatisations (both over fuzzy and crisp Kripke frames) are
established; their mono- and bi-modal fragments are shown to be decidable and,
in fact, $\mathsf{PSPACE}$-complete; it is also known that they are strictly
more expressive than the classical modal logic $\mathbf{K}$.

On the other hand, the modal logics expanding the Gödel logic with
coimplication $\Yleft$ or the Baaz Delta $\triangle$111Note that $\Yleft$ and
$\triangle$ are interdefinable: $\triangle
p\coloneqq\mathbf{1}\Yleft(\mathbf{1}\Yleft p)$ and $p\Yleft q\coloneqq
p\wedge{\sim}\triangle(p\rightarrow q)$. (also known as bi-Gödel logic or
symmetric Gödel logic, $\mathsf{biG}$) have remained relatively unstudied. To
the best of our knowledge, there are only two papers studying modal expansions
of $\mathsf{biG}$. First is [20] where an algebraic semantics for the
provability bi-Gödel (symmetric Gödel, in the authors’ terminology) logic is
studied. The other text is [1] where a linear temporal logic expanding
$\mathsf{biG}$ is explored.

Furthermore, while it is well established that every class of frames
classically definable by some formula $\phi(\overrightarrow{p_{i}})$ is also
$\mathfrak{GK}$-definable with
$\phi(\overrightarrow{p_{i}}/\overrightarrow{{\sim\sim}p_{i}})$, there are
examples of formulas that define the same class of frames both in $\mathbf{K}$
and the crisp Gödel modal logic $\mathfrak{GK}^{c}$: $\Box p\rightarrow p$ and
$p\rightarrow\lozenge p$ define reflexive frames; $\lozenge\mathbf{1}$ defines
serial frames, etc. However, there has been no systematic study which formulas
can be ‘transferred’ in this manner from $\mathbf{K}$ to $\mathfrak{GK}^{c}$.

#### Paraconsistent expansions of the bi-intuitionistic logic

The second source of inspiration is the study of the expansions of
(super-)intuitionistic logics with the strong or constructive De Morgan
negation as proposed in [31]. In that paper, several constructive De Morgan
negations for the bi-intuitionistic logic were studied: in particular, the
Nelson negation that was initially proposed in [25] and defined for the
implication as $\neg(p\rightarrow q)\coloneqq p\wedge\neg q$, and the negation
of the logic dubbed $\mathsf{I}_{4}\mathsf{C}_{4}$ by Wansing where
$\neg(p\rightarrow q)$ is defined as $\neg q\Yleft\neg p$ and $\neg(p\Yleft
q)\coloneqq\neg q\rightarrow\neg p$. The latter logic, in fact, was introduced
several times222We are grateful to Heinrich Wansing for pointing this out to
us.: first by Moisil [24] as symmetric propositional calculus, then by Wansing
[31] as $\mathsf{I}_{4}\mathsf{C}_{4}$, and then by Leitgeb [22] as HYPE. Cf.
[26] for a recent and more detailed discussion. In [31], Nelson’s logic with
coimplication and $\mathsf{I}_{4}\mathsf{C}_{4}$ are equipped with frame
semantics on bi-intuitionistic frames with two _independent_ valuations
$v^{+}$ and $v^{-}$ that are interpreted as support of truth and support of
falsity. The valuations are connected via the strong De Morgan negation in the
following sense: support of falsity of $\phi$ is defined as support of truth
of $\neg\phi$ and vice versa.

In [5], we discussed two paraconsistent logics collectively dubbed
$\mathsf{G}^{2}$ expanding Gödel logic with a De Morgan negation which were,
in fact, pre-linear extensions of Nelson’s logic $\mathsf{N4}$ and
$\mathsf{I}_{4}\mathsf{C}_{4}$. We also provided them with algebraic semantics
over the algebra $[0,1]^{\Join}$ — defined on the twist product of the lattice
$[0,1]$ with itself — thus linking them to other paraconsistent fuzzy logics
such as the ones in [18]. In [7], we applied
$\mathsf{G}^{2}(\rightarrow,\Yleft)$ (the linear expansion of Moisil’s logic)
and $\mathsf{G}^{2}(\rightarrowtriangle,\multimap)$ (the linear expansion of
$\mathsf{N4}$) presented via Hilbert-style axiomatisations to study
qualitative reasoning under uncertainty.

#### Logics

In this paper, we will be discussing several logics obtained from the
propositional Gödel logic $\mathsf{G}$. Our main interest lies in the logics
we denote $\mathbf{K}\mathsf{biG}$ and $\mathbf{K}\mathsf{G}^{2}$. They can be
produced from $\mathsf{G}$ in several ways: (1) adding De Morgan negation
$\neg$ to obtain $\mathsf{G}^{2}$ (in which case $\phi\Yleft\phi^{\prime}$ can
be defined as $\neg(\neg\phi^{\prime}\rightarrow\neg\phi)$) and then further
expanding the language with $\Box$ or $\lozenge$; (2) adding $\Yleft$ or
$\triangle$ to $\mathsf{G}$, then both $\Box$ and $\lozenge$ thus acquiring
$\mathbf{K}\mathsf{biG}$ (modal bi-Gödel logic) which is further enriched with
$\neg$. The reader may see these relations in fig. 1.

---
$\textstyle{{\mathbf{K}\mathsf{biG}}^{\mathsf{f}}}$$\textstyle{\mathbf{K}\mathsf{G}^{2}}$$\textstyle{\mathbf{K}\mathsf{biG}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\neg}$$\scriptstyle{\mathsf{ff}}$$\textstyle{\mathfrak{GK}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Yleft/\Delta}$$\textstyle{\mathsf{biG}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Box,\lozenge}$$\textstyle{\mathfrak{GK}^{c}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\neg}$$\scriptstyle{\mathsf{ff}}$$\scriptstyle{\Yleft/\Delta}$$\textstyle{\mathsf{G}^{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Box/\lozenge}$$\textstyle{\mathsf{G}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\Yleft/\Delta}$$\scriptstyle{\Box,\lozenge}$$\scriptstyle{\neg}$
Figure 1: Logics in the article. $\mathsf{ff}$ stands for ‘permitting fuzzy
frames’. Subscripts on arrows denote language expansions. $/$ stands for ‘or’
and comma for ‘and’.

#### Plan of the paper

In this paper, we bring together the two sources of inspiration and try to
close the gaps outlined above. Namely, we axiomatise the modal bi-Gödel logic
over crisp frames $\mathbf{K}\mathsf{biG}$ in the language with $\triangle$
and its paraconsistent expansion $\mathbf{K}\mathsf{G}^{2}$. We study their
semantical properties, establish their decidability, and provide complexity
evaluations.

The remainder of the paper is structured as follows. In section 2, we provide
the required logical preliminaries for this paper. We define semantics for
fuzzy and crisp $\mathbf{K}\mathsf{biG}$ and for crisp
$\mathbf{K}\mathsf{G}^{2}$ and establish some of their useful properties. We
also discuss the contribution of $\triangle$ and $\Yleft$ to the expressivity
of the $\mathbf{K}\mathsf{biG}$ language in comparison to $\mathfrak{GK}$.

In section 3, we define a Hilbert-style calculus for crisp
$\mathbf{K}\mathsf{biG}$ and establish its weak and strong completeness. Then,
we show how to expand our system so as to obtain the complete axiomatisation
of crisp $\mathbf{K}\mathsf{G}^{2}$. We also prove that in the presence of
$\neg$, some axioms of $\mathbf{K}\mathsf{biG}$ become redundant in
$\mathbf{K}\mathsf{G}^{2}$.

In section 4, we investigate the semantical properties of $\mathfrak{GK}^{c}$,
$\mathbf{K}\mathsf{biG}$, and $\mathbf{K}\mathsf{G}^{2}$. In particular, we
study transferrable formulas, i.e., formulas classically and Gödel valid on
the same classes of frames. We also characterise the class of frames the
logics of which allow Glivenko’s theorem and its paraconsistent version.

In section 5, we tackle the decidability and complexity of
$\mathbf{K}\mathsf{biG}$ and $\mathbf{K}\mathsf{G}^{2}$. Using the method of
[15], we provide a tableaux-based decision algorithm for
$\mathbf{K}\mathsf{biG}$ and prove $\mathsf{PSPACE}$ completeness of
satisfiability and validity of $\mathbf{K}\mathsf{biG}$. As a corollary, we
obtain $\mathsf{PSPACE}$ completeness of $\mathbf{K}\mathsf{G}^{2}$.

Finally, in section 6, we recapitulate the results obtained in the paper and
set the goals for future research.

##  2 Preliminaries

In this section, we provide the semantics of $\mathbf{K}\mathsf{biG}$ and
$\mathbf{K}\mathsf{G}^{2}$ in terms of $[0,1]$-valued Kripke models. We also
establish several properties that will help us in the next sections.

###  2.1 Semantics of the propositional fragments

We begin with the semantics of the propositional fragment of
$\mathbf{K}\mathsf{biG}$, namely, with $\mathsf{biG}$. The language is
generated from the countable set $\mathtt{Prop}$ via the following grammar.

$\displaystyle\phi$ $\displaystyle\coloneqq
p\in\mathtt{Prop}\mid{\sim}\phi\mid\triangle\phi\mid(\phi\wedge\phi)\mid(\phi\vee\phi)\mid(\phi\rightarrow\phi)$
($\mathcal{L}_{\triangle}$)

We also introduce two defined constants

$\displaystyle\mathbf{1}$ $\displaystyle\coloneqq p\rightarrow p$
$\displaystyle\mathbf{0}$ $\displaystyle\coloneqq{\sim}\mathbf{1}$

In our presentation, we choose $\triangle$ over $\Yleft$ as a primitive symbol
because the former allows for a shorter and more elegant axiomatisation of the
propositional fragment. Furthermore, the use of $\triangle$ simplifies the
completeness proof of $\mathbf{K}\mathsf{biG}$. Recall once again the
definitions of $\triangle$ and $\Yleft$ via one another.

$\displaystyle\triangle p$
$\displaystyle\coloneqq\mathbf{1}\Yleft(\mathbf{1}\Yleft p)$ $\displaystyle
p\Yleft q$ $\displaystyle\coloneqq p\wedge{\sim}\triangle(p\rightarrow q)$

The semantics of $\mathcal{L}_{\triangle}$ is given in the following
definition. For the sake of simplicity, we also include $\Yleft$ in the
definition of bi-Gödel algebras. We remind our readers that we consider
$\Yleft$ a defined connective. It will, however, simplify the presentation of
the $\mathsf{G}^{2}$ semantics.

######  Definition 2.1.

The bi-Gödel algebra
$[0,1]_{\mathsf{G}}=\langle[0,1],0,1,\wedge_{\mathsf{G}},\vee_{\mathsf{G}},\rightarrow_{\mathsf{G}},\Yleft,\sim_{\mathsf{G}},\triangle_{\mathsf{G}}\rangle$
is defined as follows: for all $a,b\in[0,1]$, the standard operations are
given by $a\wedge_{\mathsf{G}}b\coloneqq\min(a,b)$,
$a\vee_{\mathsf{G}}b\coloneqq\max(a,b)$,

$\displaystyle a\rightarrow_{G}b$ $\displaystyle=\begin{cases}1,\text{ if
}a\leq b\\\ b\text{ else}\end{cases}$ $\displaystyle a\Yleft_{G}b$
$\displaystyle=\begin{cases}0,\text{ if }a\leq b\\\ a\text{ else}\end{cases}$
$\displaystyle{\sim}a$ $\displaystyle=\begin{cases}0,\text{ if }a>0\\\ 1\text{
else}\end{cases}$ $\displaystyle\triangle a$
$\displaystyle=\begin{cases}0,\text{ if }a<1\\\ 1\text{ else}\end{cases}$

A _$\mathsf{biG}$ valuation_ is a homomorphism
$v:\mathcal{L}_{\triangle}\rightarrow[0,1]$ that is defined for the complex
formulas as
$v(\phi\circ\phi^{\prime})=v(\phi)\circ_{\mathsf{G}}v(\phi^{\prime})$ for
every connective $\circ$. We say that $\phi$ is _valid_ iff $v(\phi)=1$ under
every valuation. Moreover, $\Gamma\subseteq\mathcal{L}_{\triangle}$ _entails_
$\chi\in\mathcal{L}_{\triangle}$ ($\Gamma\models_{\mathsf{biG}}\chi$) iff for
every valuation $v$, it holds that

$\inf\\{v(\phi):\phi\in\Gamma\\}\leq v(\chi).$

In order to obtain the paraconsistent expansion of $\mathsf{biG}$, we add
$\neg$ to $\mathcal{L}_{\triangle}$. We dub the resulting language
$\mathcal{L}^{\neg}_{\triangle}$. The semantics of $\mathsf{G}^{2}$ is as
follows.

######  Definition 2.2.

A $\mathsf{G}^{2}$ model is a tuple $\langle[0,1],v_{1},v_{2}\rangle$ with
$v_{1},v_{2}:\mathtt{Prop}\rightarrow[0,1]$ being extended on the complex
formulas as follows.

$v_{1}(\neg\phi)$ | $=$ | $v_{2}(\phi)$ | $v_{2}(\neg\phi)$ | $=$ | $v_{1}(\phi)$
---|---|---|---|---|---
$v_{1}(\phi\wedge\phi^{\prime})$ | $=$ | $v_{1}(\phi)\wedge_{\mathsf{G}}v_{1}(\phi^{\prime})$ | $v_{2}(\phi\wedge\phi^{\prime})$ | $=$ | $v_{2}(\phi)\vee_{\mathsf{G}}v_{2}(\phi^{\prime})$
$v_{1}(\phi\vee\phi^{\prime})$ | $=$ | $v_{1}(\phi)\vee_{\mathsf{G}}v_{1}(\phi^{\prime})$ | $v_{2}(\phi\vee\phi^{\prime})$ | $=$ | $v_{2}(\phi)\wedge_{\mathsf{G}}v_{2}(\phi^{\prime})$
$v_{1}(\phi\rightarrow\phi^{\prime})$ | $=$ | $v_{1}(\phi)\\!\rightarrow_{\mathsf{G}}\\!v_{1}(\phi^{\prime})$ | $v_{2}(\phi\rightarrow\phi^{\prime})$ | $=$ | $v_{2}(\phi^{\prime})\Yleft_{\mathsf{G}}v_{2}(\phi)$
$v_{1}({\sim}\phi)$ | $=$ | ${\sim_{\mathsf{G}}}v_{1}(\phi)$ | $v_{2}({\sim}\phi)$ | $=$ | $1\Yleft_{\mathsf{G}}v_{2}(\phi^{\prime})$
$v_{1}(\triangle\phi)$ | $=$ | $\triangle_{\mathsf{G}}v_{1}(\phi)$ | $v_{2}(\triangle\phi)$ | $=$ | ${\sim_{\mathsf{G}}\sim_{\mathsf{G}}}v_{2}(\phi^{\prime})$

$\phi\in\mathcal{L}^{\neg}_{\triangle}$ is _valid_ iff for every
$\mathsf{G}^{2}$ model, $v_{1}(\phi)=1$ and $v_{2}(\phi)=0$.
$\Gamma\subseteq\mathcal{L}^{\neg}_{\triangle}$ _entails_
$\chi\in\mathcal{L}^{\neg}_{\triangle}$ ($\Gamma\models_{\mathsf{G}^{2}}\phi$)
iff

$\inf\\{v_{1}(\phi):\phi\in\Gamma\\}\leq v_{1}(\chi)\text{ and
}\sup\\{v_{2}(\phi):\phi\in\Gamma\\}\geq v_{2}(\chi).$

When there is no risk of confusion, we will write $v(\phi)=(x,y)$ as a
shorthand for $v_{1}(\phi)=x$ and $v_{2}(\phi)=y$.

Observe that $v_{1}$ and $v_{2}$ in the previous definition can be construed
as support of truth and support of falsity of the given formula. Under this
condition, we can intuitively say that in order for the entailment to be
valid, the conclusion should be _at least as true_ and _at most as false_ as
the premises.

######  Convention 2.1.

To facilitate the presentation, we will introduce the following shorthands.
Let $\phi,\phi^{\prime}\in\mathcal{L}^{\neg}_{\triangle}$, we set

$\displaystyle v(\phi)\leq^{\pm}v(\phi^{\prime})$ $\displaystyle\text{ iff
}v_{1}(\phi)\leq v_{1}(\phi^{\prime})\text{ and }v_{2}(\phi)\geq
v_{2}(\phi^{\prime})$ $\displaystyle v(\phi)<^{\pm}v(\phi^{\prime})$
$\displaystyle\text{ iff }v(\phi)\leq^{\pm}v(\phi^{\prime})\text{ and
}v(\phi)\neq v(\phi^{\prime})$

The next statements are straightforward generalisations of the results in
[31]. First, we note that $\mathsf{G}^{2}$ has the $\neg$ negation normal form
property.

######  Proposition 2.1.

For every formula $\phi\in\mathcal{L}^{\neg}_{\triangle}$ there is a formula
$\mathsf{NNF}(\phi)$ s.t. all its $\neg$’s are applied to variables only, and
for every $\mathsf{G}^{2}$ model, it holds that

$v_{1}(\phi)=v_{1}(\mathsf{NNF}(\phi))\text{ and
}v_{2}(\phi)=v_{2}(\mathsf{NNF}(\phi)).$

###### Proof.

We introduce a shorthand
$\phi\leftrightarrow\chi\coloneqq(\phi\rightarrow\chi)\wedge(\chi\rightarrow\phi)$.
Observe that $v(\phi\leftrightarrow\chi)=(1,0)$ iff $v(\phi)=v(\chi)$. It is
now easy to check that the following formulas are valid.

$\displaystyle\neg\neg\phi\leftrightarrow\phi$
$\displaystyle\neg(\phi\vee\chi)\leftrightarrow(\neg\phi\wedge\neg\chi)$
$\displaystyle\neg(\phi\wedge\chi)\leftrightarrow(\neg\phi\vee\neg\chi)$
$\displaystyle\neg\triangle\phi\leftrightarrow{\sim\sim}\neg\phi$
$\displaystyle\neg{\sim}\phi\leftrightarrow{\sim}\triangle\neg\phi$
$\displaystyle\neg(\phi\rightarrow\chi)\leftrightarrow(\neg\chi\wedge{\sim}\triangle(\neg\chi\rightarrow\neg\phi))$

As this shows that $\neg$ can be pushed inside every other connective, the
result follows. ∎

######  Proposition 2.2 ([5, Corollary 1]).

$\phi$ is valid iff $v_{1}(\phi)=1$ for any $\mathsf{G}^{2}$ model.

The following statement is an immediate consequence of proposition 2.2.

######  Proposition 2.3.

Let $\phi$ be in $\mathsf{NNF}$ and denote with $\phi^{+}$ the result of the
replacement of every negated variable $\neg p$ with a fresh variable $p^{*}$.
Then $\phi$ is $\mathsf{G}^{2}$ valid iff $\phi^{+}$ is $\mathsf{biG}$ valid.

###  2.2 Axiomatisation of the propositional fragment

Let us now define the Hilbert-style calculi for $\mathsf{biG}$ and
$\mathsf{G}^{2}$. First, we recall from [3] the $\mathcal{L}_{\triangle}$
axiomatisation of $\mathsf{biG}$ which we call
$\mathcal{H}\mathsf{G}\triangle$.

######  Definition 2.3 ($\mathcal{H}\mathsf{G}\triangle$ — Hilbert-style
calculus for $\mathsf{biG}$).

The calculus has the following axiom schemas and rules (for any $\phi$,
$\chi$, $\psi$):

  1. 1.

$(\phi\rightarrow\chi)\rightarrow((\chi\rightarrow\psi)\rightarrow(\phi\rightarrow\psi))$

  2. 2.

$\phi\rightarrow(\phi\vee\chi)$; $\chi\rightarrow(\phi\vee\chi)$

  3. 3.

$(\phi\rightarrow\psi)\rightarrow((\chi\rightarrow\psi)\rightarrow((\phi\vee\chi)\rightarrow\psi))$

  4. 4.

$(\phi\wedge\chi)\rightarrow\phi$; $(\phi\wedge\chi)\rightarrow\chi$

  5. 5.

$(\phi\rightarrow\chi)\rightarrow((\phi\rightarrow\psi)\rightarrow(\phi\rightarrow(\chi\wedge\psi)))$

  6. 6.

$(\phi\rightarrow(\chi\rightarrow\psi))\rightarrow((\phi\wedge\chi)\rightarrow\psi)$;
$((\phi\wedge\chi)\rightarrow\psi)\rightarrow(\phi\rightarrow(\chi\rightarrow\psi))$

  7. 7.

$(\phi\rightarrow\chi)\rightarrow({\sim}\chi\rightarrow{\sim}\phi)$

  8. 8.

$(\phi\rightarrow\chi)\vee(\chi\rightarrow\phi)$

  9. 9.

$\triangle\phi\vee{\sim}\triangle\phi$

  10. 10.

$\triangle(\phi\rightarrow\chi)\rightarrow(\triangle\phi\rightarrow\triangle\chi)$;
$\triangle(\phi\vee\chi)\rightarrow(\triangle\phi\vee\triangle\chi)$

  11. 11.

$\triangle\phi\rightarrow\phi$;
$\triangle\phi\rightarrow\triangle\triangle\phi$

  12. MP

$\dfrac{\phi\quad\phi\rightarrow\chi}{\chi}$

  13. $\triangle$nec

$\dfrac{\vdash\phi}{\vdash\triangle\phi}$

Next, we state several important properties of
$\mathcal{H}\mathsf{G}\triangle$ that we will utilise in the following parts
of the paper.

######  Proposition 2.4.

$\mathcal{H}\mathsf{G}\triangle$ is strongly complete: for any
$\Gamma\cup\\{\phi\\}\subseteq\mathcal{L}_{\triangle}$, it holds that

$\Gamma\vdash_{\mathcal{H}\mathsf{G}\triangle}\phi\text{ iff
}\Gamma\models_{\mathsf{biG}}\phi.$

######  Proposition 2.5 ($\triangle$ deduction theorem).

For any $\Gamma$, $\phi$, and $\chi$ it holds that

$\displaystyle\Gamma,\phi\vdash_{\mathcal{H}\mathsf{G}\triangle}\chi$
$\displaystyle\text{ iff
}\Gamma\vdash_{\mathcal{H}\mathsf{G}\triangle}\triangle\phi\rightarrow\chi.$

The calculus for $\mathsf{G}^{2}$ can be easily obtained from
$\mathcal{H}\mathsf{G}\triangle$: we only need to add De Morgan postulates for
the propositional connectives.

######  Definition 2.4 ($\mathcal{H}\mathsf{G}^{2}$ — Hilbert-style calculus
for $\mathsf{G}^{2}$).

The calculus consists of the following axioms and rules.

A0:

All instances of $\mathcal{H}\mathsf{G}\triangle$ rules and axioms in
$\mathcal{L}^{\neg}_{\triangle}$ language.

$\mathsf{neg}$:

$\neg\neg\phi\leftrightarrow\phi$

$\mathsf{DeM}\wedge$:

$\neg(\phi\wedge\chi)\leftrightarrow(\neg\phi\vee\neg\chi)$

$\mathsf{DeM}\vee$:

$\neg(\phi\vee\chi)\leftrightarrow(\neg\phi\wedge\neg\chi)$

$\mathsf{DeM}\\!\rightarrow$:

$\neg(\phi\rightarrow\chi)\leftrightarrow(\neg\chi\wedge{\sim}\triangle(\neg\chi\rightarrow\neg\phi))$

$\mathsf{DeM}\triangle$:

$\neg\triangle\phi\leftrightarrow{\sim\sim}\neg\phi$

$\mathsf{DeM}{\sim}$:

$\neg{\sim}\phi\leftrightarrow{\sim}\triangle\neg\phi$

The completeness result for $\mathcal{H}\mathsf{G}^{2}$ formulated with
$\Yleft$ instead of $\triangle$ was provided in [7]. The proof followed the
technique from [31] that relied on the existence of $\mathsf{NNF}$’s in
$\mathsf{G}^{2}$, proposition 2.3, and the completeness of the Hilbert-style
calculus for $\mathsf{biG}$. But the axioms of $\mathcal{H}\mathsf{G}^{2}$ in
$\mathcal{L}^{\neg}_{\triangle}$ contain the $\mathsf{NNF}$ transformations as
well. Likewise, $\mathcal{H}\mathsf{G}\triangle$ is strongly complete. Thus,
we can state the strong completeness of $\mathcal{H}\mathsf{G}^{2}$.

######  Proposition 2.6.

$\mathcal{H}\mathsf{G}^{2}$ is strongly complete: for any
$\Gamma\cup\\{\phi\\}\subseteq\mathcal{L}^{\neg}_{\triangle}$, it holds that

$\Gamma\vdash_{\mathcal{H}\mathsf{G}^{2}}\phi\text{ iff
}\Gamma\models_{\mathsf{G}^{2}}\phi.$

We end this section by establishing the following fact.

######  Proposition 2.7.

The following rule is admissible in $\mathsf{G}^{2}$:

$\displaystyle\dfrac{\mathcal{H}\mathsf{G}^{2}\vdash\phi\rightarrow\chi}{\mathcal{H}\mathsf{G}^{2}\vdash\neg\chi\rightarrow\neg\phi}$

###  2.3 Semantics of the modal expansions

Let us now provide semantics of $\mathbf{K}\mathsf{biG}$ (both fuzzy and
crisp) and crisp $\mathbf{K}\mathsf{G}^{2}$. The language
$\mathcal{L}^{\neg}_{\triangle,\Box,\lozenge}$ is defined via the following
grammar.

$\displaystyle\phi$ $\displaystyle\coloneqq
p\in\mathtt{Prop}\mid\neg\phi\mid{\sim}\phi\mid\triangle\phi\mid(\phi\wedge\phi)\mid(\phi\vee\phi)\mid(\phi\rightarrow\phi)\mid\Box\phi\mid\lozenge\phi$

Two constants, $\mathbf{0}$ and $\mathbf{1}$, can be introduced as in section
2.1. The $\neg$-less fragment of $\mathcal{L}^{\neg}_{\Yleft,\Box,\lozenge}$
is denoted with $\mathcal{L}_{\triangle,\Box,\lozenge}$.

######  Definition 2.5 (Frames).

  *   * •

A _fuzzy frame_ is a tuple $\mathfrak{F}=\langle W,R\rangle$ with
$W\neq\varnothing$ and $R:W\times W\rightarrow[0,1]$.

  * •

A _crisp frame_ is a tuple $\mathfrak{F}=\langle W,R\rangle$ with
$W\neq\varnothing$ and $R\subseteq W\times W$.

######  Definition 2.6 ($\mathbf{K}\mathsf{biG}$ models).

A _$\mathbf{K}\mathsf{biG}$ model_ is a tuple $\mathfrak{M}=\langle
W,R,v\rangle$ with $\langle W,R\rangle$ being a (crisp or fuzzy) frame, and
$v:\mathsf{Var}\times W\rightarrow[0,1]$. $v$ (a valuation) is extended on
complex $\mathcal{L}_{\triangle,\Box,\lozenge}$ formulas as follows:

$\displaystyle v(\phi\circ\phi^{\prime},w)$
$\displaystyle=v(\phi,w)\circ_{\mathsf{G}}v(\phi^{\prime},w).$
($\circ\in\\{{\sim},\triangle,\wedge,\vee,\rightarrow\\}$)

The interpretation of modal formulas on _fuzzy_ frames is as follows:

$\displaystyle v(\Box\phi,w)$ $\displaystyle=\inf\limits_{w^{\prime}\in
W}\\{wRw^{\prime}\rightarrow_{\mathsf{G}}v(\phi,w^{\prime})\\},$
$\displaystyle v(\lozenge\phi,w)$ $\displaystyle=\sup\limits_{w^{\prime}\in
W}\\{wRw^{\prime}\wedge_{\mathsf{G}}v(\phi,w^{\prime})\\}.$

On _crisp_ frames, the interpretation is simpler (here,
$\inf(\varnothing)\\!=\\!1$ and $\sup(\varnothing)\\!=\\!0$):

$\displaystyle v(\Box\phi,w)$
$\displaystyle=\inf\\{v(\phi,w^{\prime}):wRw^{\prime}\\},$ $\displaystyle
v(\lozenge\phi,w)$ $\displaystyle=\sup\\{v(\phi,w^{\prime}):wRw^{\prime}\\}.$

We say that $\phi\in\mathcal{L}_{\Yleft,\Box,\lozenge}$ is
_$\mathbf{K}\mathsf{biG}$ valid on frame $\mathfrak{F}$_ (denote,
$\mathfrak{F}\models_{\mathbf{K}\mathsf{biG}}\phi$) iff for any
$w\in\mathfrak{F}$, it holds that $v(\phi,w)=1$ for any model $\mathfrak{M}$
on $\mathfrak{F}$. $\Gamma$ _entails_ $\chi$ (on $\mathfrak{F}$), denoted
$\Gamma\models_{\mathbf{K}\mathsf{biG}}\phi$
($\Gamma\models^{\mathfrak{F}}_{\mathbf{K}\mathsf{biG}}\chi$), iff for every
model $\mathfrak{M}$ (on $\mathfrak{F}$) and every $w\in\mathfrak{M}$, it
holds that

$\inf\\{v(\phi):\phi\in\Gamma\\}\leq v(\chi).$

In what follows, we use $\mathbf{K}\mathsf{biG}$ to stand for the set of all
$\mathcal{L}_{\triangle,\Box,\lozenge}$ formulas valid on all _crisp_ frames
and $\mathbf{K}\mathsf{biG}^{\mathsf{f}}$ to stand for the set of all
$\mathcal{L}_{\triangle,\Box,\lozenge}$ formulas valid on all _fuzzy_ frames.

In [6], we argued that one can think of _crisp_ $R$ as availability of trusted
sources represented by states in the model. _Fuzzy_ accessibility relation can
be interpreted as the degree of trust an agent has in a source.

Since sources can refer to one another and can consider one another more or
less reliable, we can understand modalities as follows. $\lozenge\phi$ is the
search for evidence that supports $\phi$ from trusted sources:
$v(\lozenge\phi,t)>0$ iff there is a source $t^{\prime}$ to which $t$ has
positive degree of trust and that has at least some certainty in $\phi$. If,
however $t$ trusts nobody (i.e., $tRu=0$ for all $u$), then
$v(\lozenge\phi,t)=0$. Similarly, $\Box\chi$ represents the search of evidence
given by trusted sources that does not support $\chi$: $v(\Box\chi,t)<1$ iff
there is a source $t^{\prime}$ that gives to $\chi$ less certainty than $t$
gives trust to $t^{\prime}$. This means that if $t$ trusts no sources, or if
all sources have at least as high confidence in $\chi$ as $t$ has in them,
then $t$ fails to find a trustworthy enough counterexample.

######  Definition 2.7 ($\mathbf{K}\mathsf{G}^{2}$ models).

A _$\mathbf{K}\mathsf{G}^{2}$ model_ is a tuple $\mathfrak{M}=\langle
W,R,v_{1},v_{2}\rangle$ with $\langle W,R\rangle$ being a _crisp_ frame, and
$v_{1},v_{2}:\mathsf{Var}\times W\rightarrow[0,1]$. The valuations which we
interpret as support of truth and support of falsity, respectively, are
extended on complex formulas as expected.

Namely, the propositional connectives are defined state-wise according to
definition 2.2. The modalities are defined as follows.

$\displaystyle v_{1}(\Box\phi,w)$
$\displaystyle=\inf\\{v_{1}(\phi,w^{\prime}):wRw^{\prime}\\}$ $\displaystyle
v_{2}(\Box\phi,w)$
$\displaystyle=\sup\\{v_{2}(\phi,w^{\prime}):wRw^{\prime}\\}$ $\displaystyle
v_{1}(\lozenge\phi,w)$
$\displaystyle=\sup\\{v_{1}(\phi,w^{\prime}):wRw^{\prime}\\}$ $\displaystyle
v_{2}(\lozenge\phi,w)$
$\displaystyle=\inf\\{v_{2}(\phi,w^{\prime}):wRw^{\prime}\\}$

We say that $\phi\in\mathcal{L}^{\neg}_{\Yleft,\Box,\lozenge}$ is
_$\mathbf{K}\mathsf{G}^{2}$ valid on frame $\mathfrak{F}$_
($\mathfrak{F}\models_{\mathbf{K}\mathsf{G}^{2}}\phi$) iff for any
$w\in\mathfrak{F}$, it holds that $v_{1}(\phi,w)=1$ and $v_{2}(\phi,w)=0$ for
any model $\mathfrak{M}$ on $\mathfrak{F}$. $\Gamma$ _entails_ $\chi$ (on
$\mathfrak{F}$), denoted $\Gamma\models_{\mathbf{K}\mathsf{G}^{2}}\phi$
($\Gamma\models^{\mathfrak{F}}_{\mathbf{K}\mathsf{G}^{2}}\chi$), iff for every
model $\mathfrak{M}$ (on $\mathfrak{F}$) and every $w\in\mathfrak{M}$, it
holds that

$\inf\\{v_{1}(\phi):\phi\in\Gamma\\}\leq v_{1}(\chi)\text{ and
}\sup\\{v_{2}(\phi):\phi\in\Gamma\\}\geq v_{2}(\chi).$

######  Remark 2.1.

Note that $\mathbf{K}\mathsf{G}^{2}$ entailment is paraconsistent in the
following sense: if $\phi$ is not valid, then there is some $\chi$ s.t.
$\phi,\neg\phi\not\models_{\mathbf{K}\mathsf{G}^{2}}\chi$ (i.e., the
entailment is not explosive w.r.t. $\neg$). This accounts for the possibility
of the sources giving contradictory information.

Furthermore, in contrast to $\mathbf{K}$, the agent can believe in
contradictions _in a non-trivial manner_ as we have that $\Box(p\wedge\neg
p)\not\models_{\mathbf{K}\mathsf{G}^{2}}\Box q$ and $\lozenge(p\wedge\neg
p)\not\models_{\mathbf{K}\mathsf{G}^{2}}\lozenge q$.

######  Convention 2.2.

For each frame $\mathfrak{F}$ and each $w\in\mathfrak{F}$, we denote

$\displaystyle R(w)$ $\displaystyle=\\{w^{\prime}:wRw^{\prime}=1\\}$ (for
fuzzy frames) $\displaystyle R^{+}(w)$
$\displaystyle=\\{w^{\prime}:wRw^{\prime}>0\\}$ (for fuzzy frames)
$\displaystyle R(w)$ $\displaystyle=\\{w^{\prime}:wRw^{\prime}\\}$ (for crisp
frames)

Observe that $v(\Box\phi,w)=v(\neg\lozenge\neg\phi,w)$. Thus, we can treat
$\lozenge$ as a defined connective. Furthermore, this means that
$\mathbf{K}\mathsf{G}^{2}$ has the $\neg$ $\mathsf{NNF}$ property as well, and
that the following statement holds.

######  Proposition 2.8 ([6, Proposition 1]).

$\mathfrak{F}\models_{\mathbf{K}\mathsf{G}^{2}}\\!\phi$ iff for any model
$\mathfrak{M}$ on $\mathfrak{F}$ and any $w\\!\in\\!\mathfrak{F}$,
$v_{1}(\phi,w)\\!=\\!1$.

In fact, we can reduce $\mathbf{K}\mathsf{G}^{2}$ validity to
$\mathbf{K}\mathsf{biG}$ validity in the same manner as we did for their
propositional fragments.

######  Proposition 2.9.

Let $\mathfrak{F}$ be a crisp frame and $\phi$ be in $\mathsf{NNF}$. Then
$\mathfrak{F}\models_{\mathbf{K}\mathsf{G}^{2}}\phi$ iff
$\mathfrak{F}\models_{\mathbf{K}\mathsf{biG}}\phi^{+}$ for any
$\phi\in\mathcal{L}^{\neg}_{\triangle,\Box,\lozenge}$.

###### Proof.

By proposition 2.8, we have that
$\mathfrak{F}\models_{\mathbf{K}\mathsf{G}^{2}}\phi$ iff in every
$\mathbf{K}\mathsf{G}^{2}$ model $\mathfrak{M}$ on $\mathfrak{F}$ and every
$w\in\mathfrak{M}$ it holds that $v_{1}(\phi,w)=1$. It remains to construct a
$\mathbf{K}\mathsf{biG}$ model $\mathfrak{M}^{+}$ on the same frame where
$v_{1}(\phi,u)=v^{+}(\phi^{+},u)$ for every $\phi$ and $u$.

For any $u\in W$, define the valuation as follows:

$\displaystyle v^{+}(p,u)$ $\displaystyle=v_{1}(p,u)$ $\displaystyle
v^{+}(p^{*},u)$ $\displaystyle=v_{2}(p,u)$

It now suffices to show that $v^{+}(\phi^{+},u)=v_{1}(\phi,u)$ for any $\phi$
and $w$. We proceed by induction on $\phi$. The basis cases of literals are
straightforward as well as those of the propositional connectives. Thus, we
consider the case of $\phi=\Box\phi^{\prime}$.

$\displaystyle v_{1}(\Box\phi^{\prime},u)$
$\displaystyle=\inf\\{v_{1}(\phi^{\prime},u^{\prime}):uRu^{\prime}\\}$
$\displaystyle=\inf\\{v^{+}(\phi^{\prime+},u^{\prime}):uRu^{\prime}\\}$ (by
IH) $\displaystyle=v^{+}(\Box\phi^{\prime+},u)$

The case of $\phi=\lozenge\phi^{\prime}$ can be considered in the same manner.
∎

We end the section by recalling the conservativity results.

######  Proposition 2.10 ([6, Proposition 2]).

  1.   2. 1.

Let $\phi$ be a formula over
$\\{\mathbf{0},\wedge,\vee,\rightarrow,\Box,\lozenge\\}$. Then,
$\mathfrak{F}\models_{\mathfrak{GK}}\phi$ iff
$\mathfrak{F}\models_{\mathbf{K}\mathsf{biG}^{\mathsf{f}}}\phi$ and
$\mathfrak{F}\models_{\mathfrak{GK}^{c}}\phi$ iff
$\mathfrak{F}\models_{\mathbf{K}\mathsf{biG}}\phi$, for any $\mathfrak{F}$.

  3. 2.

Let $\phi\in\mathcal{L}_{\triangle,\Box,\lozenge}$. Then,
$\mathfrak{F}\models_{\mathbf{K}\mathsf{biG}}\phi$ iff
$\mathfrak{F}\models_{\mathbf{K}\mathsf{G}^{2}}\phi$, for any crisp
$\mathfrak{F}$.

###  2.4 Expressivity of $\triangle$

We have added $\triangle$ to the language of Gödel modal logic. It is thus
instructive to investigate whether it gives us the expressive capacity one
does not have without it.

First of all, it is easy to see that $\triangle$ allows us to express the
statements of _comparative belief_. For example333More examples and a more
detailed discussion of such statements can be found in [6]., consider the
following statement

> weather: _Paula considers a rain happening today strictly more likely than a
> hailstorm_.

Thus, to formalise this statement, one needs a formula that is true iff the
value of $\Box r$ (Paula believes it is going to rain today) is strictly
greater than that of $\Box s$ (Paula believes that a hailstorm is going to
happen today). Paula also does not state that she _believes completely_ in the
rain, nor does she exclude the possibility of a hailstorm. Hence, $\Box
r\wedge\Box{\sim}s$ does not suit the purpose. In fact, there is no Gödel
formula $\phi(p,q)$ s.t.

$v(\phi)=1\text{ iff }v(p)>v(q)$

On the other hand, it is easy to see that

$v({\sim}\triangle(\Box r\rightarrow\Box s),w)=1\text{ iff }v(\Box r,w)>v(\Box
s,w)$

and thus is a suitable formalisation of weather.

It is also possible to formalise comparative statements in the
$\mathsf{G}^{2}$ (and hence, $\mathbf{K}\mathsf{G}^{2}$) setting. Notice,
first, that when we consider support of truth and support of falsity
_independently_ , it is no longer the case that every two beliefs are
comparable. This, actually, aligns with our intuition: indeed, if the contents
of two statements have no connection to each other, an agent might not be
ready to choose one that they find more believable.

Formally, we can represent this as follows. Define

$\displaystyle\triangle^{\neg}\phi\coloneqq\triangle\phi\wedge\neg{\sim}\triangle\phi$

One can see that

$\displaystyle v(\triangle^{\neg}\phi,w)$
$\displaystyle=\begin{cases}(1,0)&\text{if }v(\phi,w)=(1,0)\\\
(0,1)&\text{otherwise}\end{cases}$

and that $\triangle^{\neg}(p\rightarrow q)\vee\triangle^{\neg}(q\rightarrow
p)$ is not $\mathsf{G}^{2}$ valid while $\triangle(p\rightarrow
q)\vee\triangle(q\rightarrow p)$ _is $\mathsf{biG}$ valid_. Now, to formalise
weather in a $\mathbf{K}\mathsf{G}^{2}$ setting, we use the following formula.

$\psi\coloneqq\triangle^{\neg}(\Box s\rightarrow\Box
r)\wedge{\sim}\triangle^{\neg}(\Box r\rightarrow\Box s)$

One can check, that, indeed

$\displaystyle v(\psi,w)$ $\displaystyle=\begin{cases}(1,0)&\text{ iff }v(\Box
s,w)<^{\pm}v(\Box r,w)\\\ (0,1)&\text{ otherwise}\end{cases}$

As we have just seen, the addition of $\triangle$ allows us to formalise the
statements we were not able to treat without it. On a more formal side,
however, $\triangle$ makes both $\Box$ and $\lozenge$ fragments444Note that
$\Box$ and $\lozenge$ are not interdefinable in $\mathfrak{GK}^{c}$ [29,
Corollary 6.2], nor in $\mathbf{K}\mathsf{biG}$ [6, Corollary 2]. of
$\mathbf{K}\mathsf{biG}$ more expressive. Namely, $\lozenge$ fragment of
$\mathfrak{GK}$ has finite model property while crisp and fuzzy $\Box$
fragments coincide [16]. We show that neither of these is the case in
$\mathbf{K}\mathsf{biG}$.

######  Proposition 2.11.

  1.   2. 1.

$\mathfrak{F}\models_{\mathbf{K}\mathsf{biG}}\triangle\Box
p\rightarrow\Box\triangle p$ iff $\mathfrak{F}$ is crisp.

  3. 2.

There are only infinite countermodels of $\triangle\lozenge
p\rightarrow\lozenge\triangle p$.

###### Proof.

We begin with $1$. Assume that $\mathfrak{F}$ is crisp, and let $v$ be a
valuation thereon s.t. $v(\triangle\Box p,w)=1$. Then, $v(\Box p,w)=1$. But
$\mathfrak{F}$ is crisp, whence, $v(p,w^{\prime})=1$ and thus, $v(\triangle
p,w^{\prime})=1$ for every accessible $w^{\prime}$. Thus, $v(\Box\triangle
p,w)=1$, as required. For the converse, assume that $\mathfrak{F}$ is _fuzzy_
and that w.l.o.g. $wRw^{\prime}=\frac{1}{2}$. We refute $\triangle\Box
p\rightarrow\Box\triangle p$ at $w$ as follows. Set
$v(p,w^{\prime})=\frac{2}{3}$ and $v(p,w^{\prime\prime})=1$ in all other
states. It is clear that $v(\triangle\Box p,w)=1$ but $v(\Box\triangle p,w)=0$
for we have $v(\triangle p,w^{\prime})=0$.

For $2$, we proceed as follows. Let $\mathfrak{M}$ be a finite model and let
$v(\triangle\lozenge p,w)=1$. Then, there is $w^{\prime}\in R(w)$ s.t.
$v(p,w^{\prime})=1$, whence $v(\lozenge\triangle p,w)=1$. For the converse,
assume that $v(\triangle\lozenge p,w)=1$ and $v(\triangle\lozenge p,w)<1$. We
define an infinite fuzzy555Recall from [16] that the crisp $\lozenge$ fragment
of $\mathfrak{GK}$ lacks FMP. countermodel as follows.

  * •

$W=\\{w\\}\cup\\{w_{i}:i\in\mathbb{N}\text{ and }i\geq 1\\}$.

  * •

$wRw_{i}=\frac{i}{i+1}$; $uRu^{\prime}=0$ for every $u\neq w$ and $u\neq
w_{i}$.

  * •

$v(p,w_{i})=\frac{i}{i+1}$.

It is clear that this model is infinite and that $v(\triangle\lozenge
p\rightarrow\lozenge\triangle p,w)=0$. ∎

######  Remark 2.2.

Note that it is also easy to show that $\lozenge\triangle
p\rightarrow\triangle\lozenge p$ defines crisp frames but, of course, one can
define crisp frames without $\triangle$: ${\sim\sim}\lozenge
p\rightarrow\lozenge{\sim\sim}p$ [16].

##  3 Axiomatisation of $\mathbf{K}\mathsf{biG}$ and
$\mathbf{K}\mathsf{G}^{2}$

We are now finally ready to formulate Hilbert-style calculi for crisp
$\mathbf{K}\mathsf{biG}$ and $\mathbf{K}\mathsf{G}^{2}$ and prove their
completeness. Our completeness proof follows the approach of [17] and [29].
Note, however, that we cannot completely copy the original proof from [29]
because it employs that

  1. 1.

Gödel modal logic has deduction theorem;

  2. 2.

the entailment in Gödel logic can be _equivalently_ defined either as
preservation of the order on $[0,1]$ or as preservation of $1$ as the
designated value.

Neither of these is true of modal expansions of $\mathsf{biG}$. First of all,
$\mathcal{H}\mathsf{G}\triangle$ has only $\triangle$ deduction theorem.
Second, note that $p$ entails $\triangle p$ if $1$ is the designated value
but, of course, $p\not\models_{\mathsf{biG}}\triangle p$.

We begin with the calculus for $\mathbf{K}\mathsf{biG}$ which we dub
$\mathcal{H}\mathbf{K}\mathsf{biG}$.

######  Definition 3.1 ($\mathcal{H}\mathbf{K}\mathsf{biG}$ — Hilbert-style
calculus for $\mathbf{K}\mathsf{biG}$).

The calculus has the following axiom schemas and rules.

$\mathsf{biG}$:

All substitution instances of $\mathcal{H}\mathsf{G}\triangle$ theorems and
rules.

$\mathbf{0}$:

${\sim}\lozenge\mathbf{0}$

K:

$\Box(\phi\rightarrow\chi)\rightarrow(\Box\phi\rightarrow\Box\chi)$;
$\lozenge(\phi\vee\chi)\rightarrow(\lozenge\phi\vee\lozenge\chi)$

FS:

$\lozenge(\phi\rightarrow\chi)\rightarrow(\Box\phi\rightarrow\lozenge\chi)$;
$(\lozenge\phi\rightarrow\Box\chi)\rightarrow\Box(\phi\rightarrow\chi)$

${\sim}\triangle\lozenge$:

${\sim}\triangle(\lozenge\phi\rightarrow\lozenge\chi)\rightarrow\lozenge{\sim}\triangle(\phi\rightarrow\chi)$

Cr:

$\Box(\phi\vee\chi)\rightarrow(\Box\phi\vee\lozenge\chi)$;
$\triangle\Box\phi\rightarrow\Box\triangle\phi$

nec:

$\dfrac{\vdash\phi}{\vdash\Box\phi}$;
$\dfrac{\vdash\phi\rightarrow\chi}{\vdash\lozenge\phi\rightarrow\lozenge\chi}$

As one sees from the definition above, we have added two modal axioms to the
Hilbert-style calculus $\mathcal{H}\mathfrak{GK}^{c}$ ($\mathcal{GK}^{c}$, in
the notation of [29]) that axiomatises $\mathfrak{GK}^{c}$.
${\sim}\triangle\lozenge$ says that if the supremum of $\phi$ is strictly
greater than supremum of $\chi$, then there must be a state where the value of
$\phi$ is greater than that of $\chi$. The second axiom is the definition of
crisp frames without $\lozenge$ but with $\triangle$.

In what follows, we denote the set of $\mathcal{H}\mathbf{K}\mathsf{biG}$
theorems (i.e., formulas provable without assumptions) with
$\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG})$. Observe that
$\mathsf{Th}(\mathcal{H}\mathfrak{GK}^{c})\\!\subseteq\\!\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG})$.
In particular,
$\mathsf{P}\\!\coloneqq\\!\Box(\phi\\!\rightarrow\\!\chi)\\!\rightarrow\\!(\lozenge\phi\\!\rightarrow\\!\lozenge\chi)$
is provable and

$\mathsf{M}_{\Box}:\dfrac{\Gamma\vdash\phi}{\Box\Gamma\vdash\Box\phi}$

is admissible. Using this, we obtain the following statement.

######  Proposition 3.1.

  1.   2. 1.

The Barcan’s formula $\Box\triangle\phi\rightarrow\triangle\Box\phi$ is
provable in $\mathcal{H}\mathbf{K}\mathsf{biG}$ _without_ using $\mathbf{Cr}$.

  3. 2.

The $\lozenge\triangle$ definition of crispness
$\lozenge\triangle\phi\rightarrow\triangle\lozenge\phi$ is provable in
$\mathcal{H}\mathbf{K}\mathsf{biG}$.

###### Proof.

We begin with 1. First, observe that the following rule is admissible in
$\mathcal{H}\mathfrak{GK}$.

$\dfrac{\mathcal{H}\mathfrak{GK}\vdash{\sim}\phi\vee\phi}{\mathcal{H}\mathfrak{GK}\vdash{\sim}\Box\phi\vee\Box\phi}$

Furthermore, the following rule is admissible in
$\mathcal{H}\mathsf{G}\triangle$:

$\dfrac{\mathcal{H}\mathsf{G}\triangle\vdash{\sim}\phi\vee\phi\quad\mathcal{H}\mathsf{G}\triangle\vdash\phi\rightarrow\chi}{\mathcal{H}\mathsf{G}\triangle\vdash\phi\rightarrow\triangle\chi}$

Thus, we can prove the Barcan’s formula as follows.

  1. 1.

${\sim}\triangle\phi\vee\triangle\phi$ — a theorem of
$\mathcal{H}\mathsf{G}\triangle$

  2. 2.

${\sim}\Box\triangle\phi\vee\Box\triangle\phi$ — from $1$

  3. 3.

$\triangle\phi\rightarrow\phi$ — a theorem of $\mathcal{H}\mathsf{G}\triangle$

  4. 4.

$\Box\triangle\phi\rightarrow\Box\phi$ — from 3, $\mathbf{nec}$, and
$\mathbf{K}$

  5. 5.

$\Box\triangle\phi\rightarrow\triangle\Box\phi$ — from 2 and 4

To prove the $\lozenge\triangle$ definition of the crispness, we proceed as
follows.

  1. 1.

${\sim}\triangle\phi\vee\triangle\phi$ — a theorem of
$\mathcal{H}\mathsf{G}\triangle$

  2. 2.

$\Box({\sim}\triangle\phi\vee\triangle\phi)$ — from 1 using $\mathbf{nec}$

  3. 3.

$\Box{\sim}\triangle\phi\vee\lozenge\triangle\phi$ — from 2 using
$\mathbf{Cr}$

  4. 4.

${\sim}\lozenge\triangle\phi\vee\lozenge\triangle\phi$ — from 3 since
$\mathcal{H}\mathfrak{GK}\vdash\Box{\sim}\chi\rightarrow{\sim}\lozenge\phi$

  5. 5.

$\triangle\phi\rightarrow\phi$ — a theorem of $\mathcal{H}\mathsf{G}\triangle$

  6. 6.

$\lozenge\triangle\phi\rightarrow\lozenge\phi$ — from 5 using $\mathbf{K}$

  7. 7.

$\lozenge\triangle\phi\rightarrow\triangle\lozenge\phi$ — from 4 and 6

∎

Furthermore, just as in the case of $\mathfrak{GK}$, the modal rules of
$\mathcal{H}\mathbf{K}\mathsf{biG}$ are restricted to theorems. Thus, we can
reduce the proofs in $\mathcal{H}\mathbf{K}\mathsf{biG}$ to the
$\mathcal{H}\mathsf{G}\triangle$ derivations from
$\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG})$. This also entails that the
$\triangle$ deduction theorem holds in $\mathcal{H}\mathbf{K}\mathsf{biG}$.

######  Proposition 3.2.

For any
$\Gamma\cup\\{\phi,\chi\\}\subseteq\mathcal{L}_{\triangle,\Box,\lozenge}$, it
holds that

  1. 1.

$\Gamma\vdash_{\mathcal{H}\mathbf{K}\mathsf{biG}}\phi$ iff
$\Gamma,\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG})\vdash_{\mathcal{H}\mathsf{G}\triangle}\phi$;

  2. 2.

$\Gamma,\phi\vdash_{\mathcal{H}\mathbf{K}\mathsf{biG}}\chi$ iff
$\Gamma\vdash_{\mathcal{H}\mathbf{K}\mathsf{biG}}\triangle\phi\rightarrow\chi$.

We are now ready to prove the completeness theorem. Our proof is a
modification of the completeness theorem for crisp Gödel modal logic in [29].

######  Convention 3.1.

For any $\phi\in\mathcal{L}_{\triangle,\Box,\lozenge}$, we denote with
$\mathsf{Sf}^{\mathbf{0},\mathbf{1}}(\phi)$ the set containing all its
subformulas and the constants $\mathbf{1}$ and $\mathbf{0}$.

For every $\tau\in\mathcal{L}_{\triangle,\Box,\lozenge}$ s.t.
$\mathcal{H}\mathbf{K}\mathsf{biG}\not\vdash\tau$, we are building a canonical
model $\mathfrak{M}^{\tau}$ that refutes it.

######  Definition 3.2 (Canonical model for $\tau$).

We define $\mathfrak{M}^{\tau}=\langle W^{\tau},R^{\tau},v^{\tau}\rangle$ as
follows.

  * •

$W^{\tau}$ is the set of all $\mathsf{G}\triangle$ homomorphisms
$u:\mathcal{L}_{\triangle,\Box,\lozenge}\rightarrow[0,1]_{\mathsf{biG}}$ s.t.
all theorems of $\mathcal{H}\mathbf{K}\mathsf{biG}$ are evaluated at $1$.

  * •

$uR^{\tau}u^{\prime}$ iff $u(\Box\psi)\leq u^{\prime}(\psi)$ and $u(\psi)\leq
u^{\prime}(\lozenge\psi)$ for all
$\psi\in\mathsf{Sf}^{\mathbf{0},\mathbf{1}}(\tau)$.

  * •

$v^{\tau}(p,u)=u(p)$.

Following [29], we introduce the following notation.

######  Convention 3.2.

Let $u\in W^{\tau}$, $\alpha\in[0,1]$, $\heartsuit\in\\{\Box,\lozenge\\}$, and
$\curlyvee\in\\{\leq,\geq,=\\}$. We set

$\displaystyle\heartsuit^{\curlyvee\alpha}_{u}$
$\displaystyle\coloneqq\\{\chi\in\mathsf{Sf}^{\mathbf{0},\mathbf{1}}(\tau):u(\heartsuit\chi)\curlyvee\alpha\\}$
$\displaystyle{}^{*}\Box^{=1}_{u}$
$\displaystyle\coloneqq\\{\psi:u(\Box\psi)=1\\}$

Observe that $\heartsuit^{\curlyvee\alpha}_{u}$ is always finite, whence
$\bigwedge\heartsuit^{\curlyvee\alpha}_{u},\bigvee\heartsuit^{\curlyvee\alpha}_{u}\in\mathcal{L}_{\triangle,\Box,\lozenge}$.
Furthermore, if $\heartsuit^{\curlyvee\alpha}_{u}=\varnothing$, we set
$\bigwedge\varnothing=\mathbf{1}$ and $\bigvee\varnothing=\mathbf{0}$.

The following two statements are the analogues of lemma 4.1 and remark 4.2
from [29] and can be proven in exactly the same manner.

######  Proposition 3.3.

Let $\phi\in\Box^{=\alpha}_{u}$ with $\alpha<1$ and set

$\delta\coloneqq\left(\bigwedge\Box^{>\alpha}_{u}\rightarrow\phi\right)\rightarrow\phi$

Then $u(\Box\delta)>\alpha$.

######  Proposition 3.4.

For any $\mathsf{biG}$ homomorphism $v$ s.t. $v(\delta)=1$ and $v(\phi)<1$, it
holds that $v(\phi)<v(\chi)$ for any $\chi\in\Box^{>\alpha}_{u}$.

We are now ready to prove the analogue of [29, Proposition 4.3]. Note,
however, that we cannot exactly follow the original proof step by step as it
uses the fact that the propositional entailment in Gödel logic can be
_equivalently_ defined either via preservation of the order on $[0,1]$ or via
preservation of $1$. This, of course, is not the case in $\mathsf{G}\triangle$
as we have noted above.

######  Proposition 3.5.

For any $\alpha\\!<\\!1$ and $\phi\\!\in\\!\Box^{=\alpha}_{u}$, there exists a
homomorphism
$h\\!:\\!\mathcal{L}_{\triangle,\Box,\lozenge}\\!\rightarrow\\![0,1]_{\mathsf{biG}}$,
s.t.:

C1:

$h(\chi)=1$ for any $\chi\in\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG})$;

C2:

$h(\psi)=1$ for every $\psi\in{}^{*}\Box^{=1}_{u}$;

C3:

$h(\rho)<1$ for every $\rho\in\lozenge^{<1}_{u}$;

C4:

$h(\phi)<h(\sigma)$ for every $\sigma\in\Box^{>\alpha}_{u}$.

###### Proof.

Recall that for any $\phi_{1}$, $\phi_{2}$, and $\phi_{3}$, it holds that

$\mathcal{H}\mathsf{G}\triangle\vdash(((\phi_{1}\rightarrow\phi_{2})\rightarrow\phi_{2})\wedge(\phi_{2}\rightarrow\phi_{3}))\vee(((\phi_{1}\rightarrow\phi_{2})\rightarrow\phi_{2})\rightarrow(\phi_{3}\rightarrow\phi_{2}))$

We replace $\phi_{1}$ with $\bigwedge\Box^{>\alpha}_{u}$, $\phi_{2}$ with
$\phi$, and use $\delta$ from proposition 3.3 which gives us that

$\mathcal{H}\mathbf{K}\mathsf{biG}\vdash\left(\delta\wedge\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\right)\vee\left(\delta\rightarrow\left(\bigvee\lozenge^{<1}_{u}\rightarrow\phi\right)\right)$

Since

$\dfrac{\mathcal{H}\mathsf{G}\triangle\vdash(\varphi\wedge\varphi^{\prime})\vee\eta}{\mathcal{H}\mathsf{G}\triangle\vdash(\triangle\varphi\wedge\varphi^{\prime})\vee\eta}$

is admissible in $\mathcal{H}\mathsf{G}\triangle$, we have

$\mathcal{H}\mathbf{K}\mathsf{biG}\vdash\left(\triangle\delta\wedge\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\right)\vee\left(\delta\rightarrow\left(\bigvee\lozenge^{<1}_{u}\rightarrow\phi\right)\right)$

Now, we use the commutativity of $\vee$, apply $\mathbf{nec}$, and then
$\mathbf{Cr}$ to obtain that

$\mathcal{H}\mathbf{K}\mathsf{biG}\vdash\lozenge\left(\triangle\delta\wedge\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\right)\vee\Box\left(\delta\rightarrow\left(\bigvee\lozenge^{<1}_{u}\rightarrow\phi\right)\right)$

Since $u\in W^{\tau}$, we have that one of the following holds:

  1. (A)

$u\left(\lozenge\left(\triangle\delta\wedge\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\right)\right)=1$
or

  2. (B)

$u\left(\Box\left(\delta\rightarrow\left(\bigvee\lozenge^{<1}_{u}\rightarrow\phi\right)\right)\right)=1$.

We prove the statement in both cases.

Assume that (A) holds. We show that

$\displaystyle\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}),\triangle({}^{*}\Box^{=1}_{u}),\triangle\delta\not\models_{\mathsf{biG}}\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\rightarrow\bigvee\lozenge^{<1}_{u}$
(1)

We reason for the contradiction. Note that $\mathcal{H}\mathsf{G}\triangle$ is
strongly complete w.r.t. $\mathsf{biG}$, and that
$\mathcal{H}\mathsf{G}\triangle\vdash\triangle\delta\rightarrow\triangle\triangle\delta$.
Thus, applying proposition 3.2, we obtain

$\triangle({}^{*}\Box^{=1}_{u})\vdash_{\mathcal{H}\mathbf{K}\mathsf{biG}}\left(\triangle\delta\wedge\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\right)\rightarrow\bigvee\lozenge^{<1}_{u}$

We apply $\mathsf{M}_{\Box}$, $\mathsf{P}$, and $\mathbf{K}$ and get

$\Box\triangle({}^{*}\Box^{=1}_{u})\vdash_{\mathcal{H}\mathbf{K}\mathsf{biG}}\lozenge\left(\triangle\delta\wedge\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\right)\rightarrow\bigvee\lozenge\lozenge^{<1}_{u}$

Now, since $\triangle\Box\phi\rightarrow\Box\triangle\phi$ is an axiom scheme
$\mathbf{Cr}$, we have that

$\triangle\Box({}^{*}\Box^{=1}_{u})\vdash_{\mathcal{H}\mathbf{K}\mathsf{biG}}\lozenge\left(\triangle\delta\wedge\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\right)\rightarrow\bigvee\lozenge\lozenge^{<1}_{u}$

We apply proposition 3.2 again which gives us that

$\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}),\triangle\Box({}^{*}\Box^{=1}_{u})\models_{\mathsf{biG}}\lozenge\left(\triangle\delta\wedge\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\right)\rightarrow\bigvee\lozenge\lozenge^{<1}_{u}$

However, we can show that $u$ refutes this entailment. Indeed, observe that
$u(\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}))=\\{1\\}$ since $u\in
W^{\tau}$. Moreover, since $u(\Box{}^{*}\Box^{=1}_{u})=\\{1\\}$ by definition,
we have that $u(\triangle\Box{}^{*}\Box^{=1}_{u})=1$ as well. Finally, (A)
gives us that
$u\left(\lozenge\left(\triangle\delta\wedge\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)\right)\right)=1$
but $u\left(\bigvee\lozenge\lozenge^{<1}_{u}\right)<1$ by definition.

Thus, since the premises of (1) are either theorems of
$\mathcal{H}\mathbf{K}\mathsf{biG}$ or formulas whose main connective is
$\triangle$, there is a homomorphism $h$ that sends the premises of (1) to $1$
and the conclusion to a lesser value. We show that $h$ satisfies the
conditions of the statement. Indeed, $\mathbf{C1}$ is obtained immediately
since $\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG})$ is closed under
$\triangle$. To see that $\mathbf{C2}$ holds, we note that
$h(\triangle({}^{*}\Box^{=1}_{u}))=\\{1\\}$, whence
$h({}^{*}\Box^{=1}_{u})=\\{1\\}$ are evaluated at $1$ too.

Since $h$ refutes the conclusion of (1), we have that
$h\left(\bigvee\lozenge^{<1}_{u}\right)<h\left(\phi\rightarrow\bigvee\lozenge^{<1}_{u}\right)$.
Hence, $h$ satisfies $\mathbf{C3}$. Finally, $h(\triangle\delta)=1$ entails
that $h(\delta)=1$. But one can see that $h(\phi)\leq
h\left(\bigvee\lozenge^{<1}_{u}\right)$, whence $\mathbf{C4}$ also holds
w.r.t. $h$ by proposition 3.4.

We consider (B). We assume that

$\displaystyle\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}),\triangle({}^{*}\Box^{=1}_{u}),\delta,\delta\rightarrow\left(\bigvee\lozenge^{<1}_{u}\rightarrow\phi\right)\models_{\mathsf{biG}}\phi$
(2)

and reason for contradiction. For this, we apply proposition 3.2, strong
completeness of $\mathcal{H}\mathsf{G}\triangle$ w.r.t. $\mathsf{biG}$, and
$\mathsf{M}_{\Box}$ to obtain

$\displaystyle\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}),\Box\triangle({}^{*}\Box^{=1}_{u}),\Box\delta,\Box\left(\delta\rightarrow\left(\bigvee\lozenge^{<1}_{u}\rightarrow\phi\right)\right)\models_{\mathsf{biG}}\Box\phi$

Now, we apply $\mathbf{Cr}$ which gives us

$\displaystyle\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}),\triangle\Box({}^{*}\Box^{=1}_{u}),\Box\delta,\Box\left(\delta\rightarrow\left(\bigvee\lozenge^{<1}_{u}\rightarrow\phi\right)\right)\models_{\mathsf{biG}}\Box\phi$

Again, we can refute this entailment with $u$. Since $u\in W^{\tau}$,
$u(\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}))=\\{1\\}$. Furthermore,
$u(\triangle\Box({}^{*}\Box^{=1}_{u}))=1$ since
$u(\Box({}^{*}\Box^{=1}_{u}))=1$ by definition of $u$, and $u(\Box\delta)=1$
by proposition 3.3, and
$u\left(\Box\left(\delta\rightarrow\left(\bigvee\lozenge^{<1}_{u}\rightarrow\phi\right)\right)\right)=1$
by assumption (B). On the contrary, $u(\Box\phi)<\alpha$.

Thus, there exists a homomorphism $h$ that evaluates the premises of (2) at
$1$666Note that theorems are closed under $\triangle$, that
$h\left(\delta\rightarrow\left(\bigvee\lozenge^{<1}_{u}\rightarrow\phi\right)\right),h(\delta)\in\\{1,h(\phi)\\}$.
and $\phi$ at a lesser value.

It remains to show that $h$ satisfies $\mathbf{C1}$–$\mathbf{C4}$. Indeed,
$\mathbf{C1}$ and $\mathbf{C2}$ hold because the premises of (2) are sent to
$1$. Furthermore, by the same reason, we have that
$h\left(\bigvee\lozenge^{<1}_{u}\right)<1$ ($\mathbf{C3}$). Finally, since
$h(\phi)<h(\delta)=1$, we obtain $\mathbf{C4}$ via an application of
proposition 3.4. ∎

Next, we prove the counterpart of proposition 4.7 in [29]. Again, we will not
be able to mimic it step-by-step since $\mathsf{biG}$ does not have the
deduction theorem, only the $\triangle$ deduction theorem. Thus, we need a
stronger version of [29, Lemma 4.6]. Our next proposition serves exactly this
goal.

######  Proposition 3.6.

Let $\phi\in\lozenge^{=\alpha}_{u}$ for some $\alpha>0$ and set

$\displaystyle\delta^{\prime}$
$\displaystyle\coloneqq\left(\phi\rightarrow\bigvee\lozenge^{<\alpha}_{u}\right)\rightarrow\bigvee\lozenge^{<\alpha}_{u}$

Then $u(\lozenge\triangle\delta^{\prime})=1$.

###### Proof.

Note that
$u(\lozenge\phi)\\!>\\!u\left(\bigvee\lozenge\lozenge^{<\alpha}_{u}\right)$ by
definition. Thus we have
$u\left(\lozenge\phi\\!\rightarrow\\!\lozenge\bigvee\lozenge^{<\alpha}_{u}\right)\\!<\\!1$
by $\mathbf{K}$, whence
$u\left({\sim}\triangle\left(\lozenge\phi\\!\rightarrow\\!\lozenge\bigvee\lozenge^{<\alpha}_{u}\right)\right)\\!=\\!1$.
Now, we use ${\sim}\triangle\lozenge$ axiom to obtain that
$u(\lozenge{\sim}\triangle(\phi\rightarrow\bigvee\lozenge^{<1}_{u}))=1$. From
here, since
$\mathcal{H}\mathsf{G}\triangle\vdash{\sim}\triangle(\phi\rightarrow\bigvee\lozenge^{<1}_{u})\rightarrow\triangle((\phi\rightarrow\bigvee\lozenge^{<1}_{u})\rightarrow\bigvee\lozenge^{<1}_{u})$,
we obtain $u(\lozenge\triangle\delta^{\prime})\\!=\\!1$ by an application of
$\mathbf{nec}$ and $\mathbf{K}$, as required. ∎

We are now ready to prove the $\lozenge$ counterpart of proposition 3.5.

######  Proposition 3.7.

For any $\alpha>0$ and $\phi\in\lozenge^{=\alpha}_{u}$, there exists a
homomorphism
$h:\mathcal{L}_{\triangle,\Box,\lozenge}\rightarrow[0,1]_{\mathsf{biG}}$,
s.t.:

C1:

$h(\chi)=1$ for any $\chi\in\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG})$;

C2:

$h(\psi)=1$ for every $\psi\in{}^{*}\Box^{=1}_{u}$;

C3:

$h(\rho)<1$ for every $\rho\in\lozenge^{<1}_{u}$;

$\mathbf{C4}^{\prime}$:

$h(\phi)>h(\sigma)$ for every $\sigma\in\lozenge^{<\alpha}_{u}$.

###### Proof.

We assume

$\displaystyle\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}),\triangle({}^{*}\Box^{=1}_{u}),\triangle\delta^{\prime}\models_{\mathsf{biG}}\bigvee\lozenge^{<1}_{u}$
(3)

and reason for contradiction. Again, we use the completeness of
$\mathcal{H}\mathsf{G}\triangle$, proposition 3.2, $\mathbf{K}$,
$\mathsf{M}_{\Box}$, $\mathsf{P}$, and $\mathbf{Cr}$ to arrive at

$\displaystyle\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}),\triangle\Box({}^{*}\Box^{=1}_{u})\models_{\mathsf{biG}}\lozenge\triangle\delta^{\prime}\rightarrow\bigvee\lozenge\lozenge^{<1}_{u}$

It is easy to see that $u$ refutes this entailment:
$u(\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG}))=1$ since $u\in W^{\tau}$,
$u(\Box^{*}\Box^{=1}_{u})=1$ by definition, whence
$u(\triangle\Box^{*}\Box^{=1}_{u})=1$, and
$u(\lozenge\triangle\delta^{\prime})=1$ by proposition 3.6 but
$u\left(\bigvee\lozenge\lozenge^{<1}_{u}\right)<1$ by definition.

Thus, there exists a homomorphism $h$ that sends the premises of (3) to
$1$777Again, observe that $\mathsf{Th}(\mathcal{H}\mathbf{K}\mathsf{biG})$ is
closed under $\triangle$ and all other premises have $\triangle$ as their main
connective. and its conclusion to a lesser value. Hence, $h$ satisfies
$\mathbf{C1}$ and $\mathbf{C2}$. Furthermore,
$h\left(\bigvee\lozenge^{<1}_{u}\right)<1$, and thus, $\mathbf{C3}$ is
satisfied. Finally, since $h(\triangle\delta^{\prime})=1$, we have that
$h(\delta^{\prime})=1$, whence $\mathbf{C4}^{\prime}$ is satisfied as well. ∎

######  Remark 3.1.

It is clear that since $h(\Box\mathbf{1})=1$, every homomorphism $h$
satisfying the conditions of proposition 3.5 satisfies

C4.1:

$h(\phi)<1$.

Furthermore, from $h(\lozenge\mathbf{0})=0$, it follows that for every $h$
that satisfies the conditions of proposition 3.7, it holds that

$\mathbf{C4^{\prime}.1}$:

$h(\phi)>0.$

Finally, if $\mathbf{C1}$–$\mathbf{C3}$ are true for $h$, then the following
properties hold for all
$\theta,\theta^{\prime}\in\mathcal{L}_{\triangle,\Box,\lozenge}$.

$\mathbf{C2.a}$:

If $u(\lozenge\theta)\leq u(\Box\theta^{\prime})$, then $h(\theta)\leq
h(\theta^{\prime})$ since
$\theta\rightarrow\theta^{\prime}\in{}^{*}\Box^{=1}_{u}$ using $\mathbf{FS}$.

$\mathbf{C2.b}$:

If $\theta\in\mathsf{Sf}^{\mathbf{0},\mathbf{1}}(\tau)$ and
$u(\lozenge\theta)<u(\Box\theta^{\prime})$, then
$h(\theta)<h(\theta^{\prime})$. For

$\mathcal{H}\mathbf{K}\mathsf{biG}\vdash((\Box\theta^{\prime}\rightarrow\lozenge\theta)\rightarrow\lozenge\theta)\rightarrow(\Box((\theta^{\prime}\rightarrow\theta)\rightarrow\theta)\vee\lozenge\theta)$

$u(\lozenge\theta)<1$, and
$u(\Box\theta^{\prime}\rightarrow\lozenge\theta)\rightarrow\lozenge\theta)=1$
imply that
$(\theta^{\prime}\rightarrow\theta)\rightarrow\theta\in{}^{*}\Box^{=1}_{u}$
and $\mathbf{C3}$ implies $h(\theta)<1$.

$\mathbf{C2.c}$:

If $u(\Box\theta)>0$, then $h(\theta)>0$.

$\mathbf{C2.d}$:

If $u(\lozenge\theta)=0$, then $h(\theta)=0$.

We can now establish the next statement which is analogous to propositions 4.5
and 4.8 in [29] using propositions 3.5 and 3.7 as well as remark 3.1. The
proof is exactly the same as in the original version.

######  Proposition 3.8.

  1.   2. 1.

For any $\phi\in\Box^{=\alpha}_{u}$, $\alpha<1$, and $\varepsilon>0$ there is
$u^{\prime}\in W^{\tau}$ s.t. $uR^{\tau}u^{\prime}$ and
$u^{\prime}(\phi)\in[\alpha,\alpha+\varepsilon]$.

  3. 2.

For any $\phi\in\lozenge^{=\alpha}_{u}$, $\alpha>0$, and $\varepsilon>0$ there
is $u^{\prime}\in W^{\tau}$ s.t. $uR^{\tau}u^{\prime}$ and
$u^{\prime}(\phi)\in[\alpha-\varepsilon,\alpha]$.

The truth lemma can be established using proposition 3.8 that guarantees that
for every value $\alpha$ of $\Box\phi$ or $\lozenge\phi$, one can find an
accessible state where the value of $\phi$ is arbitrarily close to $\alpha$.
Thus, $\Box\phi$ will be indeed evaluated as the infimum and $\lozenge\phi$ as
the supremum of $\phi$’s values in the accessible states. Again, the proof can
be conducted in the same manner as in [29].

######  Proposition 3.9 (Truth lemma).

For any $\phi\in\mathsf{Sf}^{\mathbf{0},\mathbf{1}}(\tau)$, it holds that
$v^{\tau}(\phi,u)=u(\phi)$.

Now, weak completeness will follow from the truth lemma and the validity of
axioms and rules.

######  Theorem 3.1.

$\mathcal{H}\mathbf{K}\mathsf{biG}$ is weakly complete: for any
$\phi\in\mathcal{L}_{\triangle,\Box,\lozenge}$, it holds that
$\models_{\mathbf{K}\mathsf{biG}}\phi$ iff
$\mathcal{H}\mathbf{K}\mathsf{biG}\vdash\phi$.

The strong completeness is a bit more complicated.

######  Theorem 3.2.

$\mathcal{H}\mathbf{K}\mathsf{biG}$ is strongly complete: for any
$\Gamma\cup\\{\phi\\}\subseteq\mathcal{L}_{\triangle,\Box,\lozenge}$, it holds
that $\Gamma\models_{\mathbf{K}\mathsf{biG}}\phi$ iff
$\Gamma\vdash_{\mathcal{H}\mathbf{K}\mathsf{biG}}\phi$.

###### Proof.

The proof follows [29, Corollary 4.12]. The only two differences are that we
need to account for $\triangle$ and that the $\mathbf{K}\mathsf{biG}$
entailment $\Gamma\models_{\mathbf{K}\mathsf{biG}}\chi$ is defined via the
order on $[0,1]$. That is, if the entailment is refuted by $v$, then
$\inf\\{v(\phi,w):\phi\in\Gamma\\}>v(\chi,w)$ for some $w\in\mathfrak{F}$.
This, in turn, is equivalent to

$\exists d\\!\in\\!(0,1]~{}\forall\phi\in\Gamma:v(\phi,w)\geq d\text{ but
}v(\chi,w)<d$

Now let $\Gamma\cup\\{\phi\\}\subseteq\mathcal{L}_{\triangle,\Box,\lozenge}$
and $\Gamma\nvdash_{\mathcal{H}\mathbf{K}\mathsf{biG}}\phi$. We consider the
classical first order theory $\Gamma^{*}$ whose signature contains two unary
predicates $W$ and $P$, one binary predicate $<$, binary functions $\circ$ and
$\mathsf{s}$, unary function $\blacktriangle$, constants $0$, $1$, $c$, $d$,
and a function symbol $f_{\theta}$ for each
$\theta\in\mathcal{L}_{\triangle,\Box,\lozenge}$. The axioms are as follows.

  * •

$\forall x{\sim}(W(x)\wedge P(x))$

  * •

$\forall x(W(x)\vee{\sim}W(x))$

  * •

‘$P(d)$ and $\langle P,<\rangle$ is a strict linear order with $0$ and $1$
being its minimum and maximum and $0<d\leq 1$’.

  * •

$\forall x\forall y((W(x)\wedge
W(y))\rightarrow(\mathsf{s}(x,y)=1\vee\mathsf{s}(x,y)=0))$

  * •

$\forall x\forall y(P(x)\wedge P(y))\rightarrow((x\leq y\wedge x\circ
y=1)\vee(x>y\wedge x\circ y=y))$

  * •

$\forall
x(P(x)\rightarrow(x=1\wedge\blacktriangle(x)=1)\vee(x<1\wedge\blacktriangle(x)=0))$

  * •

For each $\theta,\theta^{\prime}\in\mathcal{L}_{\triangle,\Box,\lozenge}$, we
add the following formulas.

    * –

$\forall x(W(x)\rightarrow P(f_{\theta}(x)))$

    * –

$\forall x(W(x)\rightarrow f_{{\sim}\theta}(x)=(f_{\theta}(x)\circ 0))$

    * –

$\forall x(W(x)\rightarrow
f_{\triangle\theta}(x)=\blacktriangle(f_{\theta}(x)))$

    * –

$\forall x(W(x)\rightarrow
f_{\theta\wedge\theta^{\prime}}(x)=\min\\{f_{\theta}(x),f_{\theta^{\prime}}(x)\\})$

    * –

$\forall x(W(x)\rightarrow
f_{\theta\vee\theta^{\prime}}(x)=\max\\{f_{\theta}(x),f_{\theta^{\prime}}(x)\\})$

    * –

$\forall x(W(x)\rightarrow
f_{\theta\rightarrow\theta^{\prime}}(x)=f_{\theta}(x)\circ
f_{\theta^{\prime}}(x))$

    * –

$\forall x(W(x)\rightarrow
f_{\Box\theta}(x)=\inf\limits_{y}\\{\mathsf{s}(x,y)\circ f_{\theta}(y)\\})$

    * –

$\forall x(W(x)\rightarrow
f_{\lozenge\theta}(x)=\sup\limits_{y}\\{\min\\{\mathsf{s}(x,y),f_{\theta}(y)\\}\\})$

  * •

For each $\gamma\in\Gamma$, we add $f_{\gamma}(c)\geq d$.

  * •

We also add $P(d)\wedge W(c)\wedge(f_{\phi}(c)<d)$.

The rest of the proof is identical to that in [29]. For each finite subset
$\Gamma^{-}$ of $\Gamma^{*}$, we let
$\mathcal{L}_{\triangle,\Box,\lozenge}^{-}=\\{\theta:f_{\theta}\text{ occurs
in }\Gamma^{-}\\}$. Since
$\mathcal{L}_{\triangle,\Box,\lozenge}^{-}\cap\Gamma\nvdash_{\mathcal{H}\mathbf{K}\mathsf{biG}}\phi$
by assumption, theorem 3.1 entails that there is a crisp pointed model
$\langle\mathfrak{M},c\rangle$ with $\mathfrak{M}=\langle
W,\mathsf{s}^{\Gamma^{-}},e^{\Gamma^{-}}\rangle$ being such that
$e^{\Gamma^{-}}(\phi,c)<d$ and $e^{\Gamma^{-}}(\theta,c)\geq d$ for every
$\theta\in\Gamma\cap\Gamma^{-}$. Thus, the following structure

$\langle
W\sqcup[0,1],W,[0,1],<,0,1,c,d,\circ,\blacktriangle,\mathsf{s}^{\Gamma^{-}},\\{f_{\theta}\\}_{\theta\in\mathcal{L}_{\triangle,\Box,\lozenge}}\rangle$

is a model of $\Gamma^{-}$. Now, by compactness and the downward
Löwenheim–Skolem theorem, $\Gamma^{*}$ has a countable model

$\mathfrak{M}^{*}=\langle
B,W,P,<,0,1,c,d,\circ,\blacktriangle,\mathsf{s}\\{f_{\theta}\\}_{\theta\in\mathcal{L}_{\triangle,\Box,\lozenge}}\rangle$

Now, we can embed $\langle P,<\rangle$ into
$\langle\mathbb{Q}\cap[0,1],<\rangle$ preserving $0$, $1$ as well as all
infima and suprema. Hence, we may w.l.o.g. assume that $\mathsf{s}$ is crisp
and the ranges of $f_{\theta}$’s are contained in $[0,1]$. Then, it is
straightforward to verify that $\mathfrak{M}=\langle W,S,e\rangle$, where
$e(\theta,w)=f_{\theta}(w)$ for all $w\in W$ and
$\theta\in\mathcal{L}_{\triangle,\Box,\lozenge}$, is a crisp
$\mathbf{K}\mathsf{biG}$ model with a distinguished world $c$ such that
$v[\Gamma,c]\geq d$ and $v(\phi,c)<d$ for some $0<d\leq 1$. Hence,
$\inf\\{v(\gamma,c):\gamma\in\Gamma\\}>v(\phi,c)$, and thus,
$\Gamma\not\models_{\mathbf{K}\mathsf{biG}}\phi$. ∎

We end the section by providing a complete calculus for
$\mathbf{K}\mathsf{G}^{2}$ in $\mathcal{L}^{\neg}_{\triangle,\Box,\lozenge}$.

######  Definition 3.3 ($\mathcal{H}\mathbf{K}\mathsf{G}^{2}$ — Hilbert-style
calculus for $\mathbf{K}\mathsf{G}^{2}$).

$\mathcal{H}\mathbf{K}\mathsf{G}^{2}$ contains the following axioms and rules.

A0:

All instances of $\mathcal{H}\mathbf{K}\mathsf{biG}$ rules and axioms in
$\mathcal{L}^{\neg}_{\triangle,\Box,\lozenge}$ language.

$\mathsf{neg}$:

$\neg\neg\phi\leftrightarrow\phi$

$\mathsf{DeM}\wedge$:

$\neg(\phi\wedge\chi)\leftrightarrow(\neg\phi\vee\neg\chi)$

$\mathsf{DeM}\vee$:

$\neg(\phi\vee\chi)\leftrightarrow(\neg\phi\wedge\neg\chi)$

$\mathsf{DeM}\\!\rightarrow$:

$\neg(\phi\rightarrow\chi)\leftrightarrow(\neg\chi\wedge{\sim}\triangle(\neg\chi\rightarrow\neg\phi))$

$\mathsf{DeM}\triangle$:

$\neg\triangle\phi\leftrightarrow{\sim\sim}\neg\phi$

$\mathsf{DeM}{\sim}$:

$\neg{\sim}\phi\leftrightarrow{\sim}\triangle\neg\phi$

$\mathsf{DeM}\Box\lozenge$:

$\Box\phi\leftrightarrow\neg\lozenge\neg\phi$

It is instructive to observe that several axioms of
$\mathcal{H}\mathbf{K}\mathsf{biG}$ become redundant in
$\mathcal{H}\mathbf{K}\mathsf{G}^{2}$.

######  Proposition 3.10.

The following $\mathcal{H}\mathbf{K}\mathsf{biG}$ axioms are redundant in
$\mathcal{H}\mathbf{K}\mathsf{G}^{2}$:

  * •

${\sim}\lozenge\mathbf{0}$;

  * •

$\lozenge(\phi\vee\chi)\rightarrow(\lozenge\phi\vee\lozenge\chi)$;

  * •

${\sim}\triangle(\lozenge\phi\rightarrow\lozenge\chi)\rightarrow\lozenge{\sim}\triangle(\phi\rightarrow\chi)$;

  * •

$\triangle\Box\phi\rightarrow\Box\triangle\phi$.

###### Proof.

Recall that $\neg$ contraposition

$\dfrac{\mathcal{H}\mathsf{G}^{2}\vdash\phi\rightarrow\chi}{\mathcal{H}\mathsf{G}^{2}\vdash\neg\chi\rightarrow\neg\phi}$

is admissible in $\mathcal{H}\mathsf{G}^{2}$.

We begin with ${\sim}\lozenge\mathbf{0}$. Since ${\sim}$ can be defined via
$\rightarrow$, we need to prove $\lozenge\mathbf{0}\rightarrow\mathbf{0}$. By
contraposition, we can prove
$\neg\mathbf{0}\rightarrow\neg\lozenge\mathbf{0}$. By De Morgan laws, we
transform this into $\neg\mathbf{0}\rightarrow\Box\neg\mathbf{0}$. Now recall
that $\mathcal{H}\mathsf{G}^{2}\vdash\neg\mathbf{0}$, whence
$\mathcal{H}\mathbf{K}\mathsf{G}^{2}\vdash\neg\mathbf{0}\rightarrow\Box\neg\mathbf{0}$.

For $\lozenge(\phi\vee\chi)\rightarrow(\lozenge\phi\vee\lozenge\chi)$, note
again that we can prove
$\neg(\lozenge\phi\vee\lozenge\chi)\rightarrow\neg\lozenge(\phi\vee\chi)$
instead. But this is equivalent to
$\Box(\neg\phi\wedge\neg\chi)\rightarrow(\Box\neg\phi\wedge\Box\neg\chi)$
which is provable in $\mathfrak{GK}$.

For ${\sim}\triangle\lozenge$, we proceed as follows. First, note that

$\Box({\sim}\neg\chi\vee\triangle(\neg\chi\rightarrow\neg\phi))\rightarrow(\lozenge{\sim}\neg\chi\vee\triangle(\Box\neg\chi\rightarrow\Box\neg\phi))$

can be proven via an application of $\vee$-commutativity to $\mathbf{Cr}$, the
Barcan’s formula, and $\mathbf{K}$.

From here, since,
$\mathcal{H}\mathfrak{GK}^{c}\vdash\lozenge{\sim}\neg\chi\rightarrow{\sim}\Box\neg\chi$,
we obtain

$\Box({\sim}\neg\chi\vee\triangle(\neg\chi\rightarrow\neg\phi))\rightarrow({\sim}\Box\neg\chi\vee\triangle(\Box\neg\chi\rightarrow\Box\neg\phi))$

Now, applying ${\sim\sim}\triangle\psi\leftrightarrow\triangle\psi$, we obtain

$\Box({\sim}\neg\chi\vee{\sim\sim}\triangle(\neg\chi\rightarrow\neg\phi))\rightarrow({\sim}\Box\neg\chi\vee{\sim\sim}\triangle(\Box\neg\chi\rightarrow\Box\neg\phi))$

We use the De Morgan law for $\sim$ —
${\sim}(\psi\wedge\psi^{\prime})\leftrightarrow({\sim}\psi\vee{\sim}\psi^{\prime})$
to get

$\Box{\sim}(\neg\chi\wedge{\sim}\triangle(\neg\chi\rightarrow\neg\phi))\rightarrow{\sim}(\Box\neg\chi\wedge{\sim}\triangle(\Box\neg\chi\rightarrow\Box\neg\phi))$

At this point, we apply the De Morgan laws for $\rightarrow$ and $\triangle$
and $\lozenge$ and $\Box$ which give us

$\Box{\sim}\neg(\phi\rightarrow\chi)\rightarrow{\sim}\neg(\lozenge\phi\rightarrow\lozenge\chi)$

Recall now that
$\mathcal{H}\mathsf{G}\triangle\vdash{\sim}\psi\leftrightarrow{\sim\sim\sim}\psi$
and
$\mathcal{H}\mathsf{G}\triangle\vdash\triangle{\sim}\psi\leftrightarrow{\sim}\psi$.
Thus, we have

$\Box{\sim}\triangle{\sim\sim}\neg(\phi\rightarrow\chi)\rightarrow{\sim}\triangle{\sim\sim}\neg(\lozenge\phi\rightarrow\lozenge\chi)$

The application of $\mathsf{DeM}\triangle$ gives us

$\Box{\sim}\triangle\neg\triangle(\phi\rightarrow\chi)\rightarrow{\sim}\triangle\neg\triangle(\lozenge\phi\rightarrow\lozenge\chi)$

We can now apply $\mathsf{DeM}{\sim}$ to obtain

$\Box\neg{\sim}\triangle(\phi\rightarrow\chi)\neg\rightarrow\neg{\sim}\triangle(\lozenge\phi\rightarrow\lozenge\chi)$

Finally, we use the $\neg$ contraposition $\mathsf{neg.}$, and
$\mathsf{DeM}\Box\lozenge$ to get

${\sim}\triangle(\lozenge\phi\rightarrow\lozenge\chi)\rightarrow\lozenge{\sim}\triangle(\phi\rightarrow\chi)$

At last, we can see that $\triangle\Box\phi\rightarrow\Box\triangle\phi$ can
be transformed via contraposition and De Morgan laws into
$\lozenge{\sim\sim}\neg\phi\rightarrow{\sim\sim}\lozenge\neg\phi$ which is
provable in $\mathcal{H}\mathfrak{GK}^{c}$. ∎

The following completeness theorem is a straightforward corollary of theorem
3.1 and proposition 2.9 since every
$\phi\in\mathcal{L}^{\neg}_{\triangle,\Box,\lozenge}$ can be transformed into
its NNF using the axioms of $\mathcal{H}\mathbf{K}\mathsf{G}^{2}$.

######  Theorem 3.3.

$\mathcal{H}\mathbf{K}\mathsf{G}^{2}$ is strongly complete: for any
$\Gamma\cup\\{\phi\\}\subseteq\mathcal{L}^{\neg}_{\triangle,\Box,\lozenge}$,
it holds that $\Gamma\models_{\mathbf{K}\mathsf{G}^{2}}\phi$ iff
$\Gamma\vdash_{\mathcal{H}\mathbf{K}\mathsf{G}^{2}}\phi$.

##  4 Model-theoretic properties of $\mathbf{K}\mathsf{biG}$ and
$\mathbf{K}\mathsf{G}^{2}$

In this section, we further investigate semantical properties of
$\mathbf{K}\mathsf{G}^{2}$. However, to simplify the presentation, we will
formulate most results in the language of $\mathfrak{GK}$ (i.e., without
$\triangle$ and $\neg$). Still, they are applicable to
$\mathbf{K}\mathsf{biG}$ and $\mathbf{K}\mathsf{G}^{2}$ by virtue of
proposition 2.10.

###  4.1 Transferrable formulas

As we have already discussed in the introduction, it is known (cf. e.g. [14])
that $\mathfrak{GK}^{c}$ can be embedded into $\mathbf{K}$ if we replace each
variable $p$ with ${\sim\sim}p$ in the formulas. Furthermore, some formulas
defining useful classes of frames do not require any translation at all. For
example [29], the following formulas define the same classes of frames both in
$\mathbf{K}$ and $\mathfrak{GK}^{c}$.

$\displaystyle\Box p\rightarrow p$ $\displaystyle p\rightarrow\lozenge p$
(reflexivity) $\displaystyle\Box p\rightarrow\Box\Box p$
$\displaystyle\lozenge\lozenge p\rightarrow\lozenge p$ (transitivity)
$\displaystyle p\rightarrow\Box\lozenge p$ $\displaystyle\lozenge\Box
p\rightarrow p$ (symmetry) $\displaystyle\lozenge p\rightarrow\Box\lozenge p$
$\displaystyle\lozenge\Box p\rightarrow\Box p$ (Euclideanness)
$\displaystyle\lozenge\mathbf{1}$ (seriality)

One should observe, however, that since $\Box$ and $\lozenge$ are not
interdefinable in $\mathfrak{GK}^{c}$ [29, Lemma 6.1], nor in
$\mathbf{K}\mathsf{biG}$ [6, Corollary 2], one needs _both_ formulas to define
a class of frames in the bi-modal languages. On the other hand, the
interdefinability of $\Box$ and $\lozenge$ in $\mathbf{K}\mathsf{G}^{2}$
allows for the use of only one of these formulas.

A natural question now is whether _every_ classical definition of a class of
frames $\mathbb{F}$ defines $\mathbb{F}$ in $\mathfrak{GK}^{c}$. Evidently,
the answer is negative. For consider $\lozenge(p\vee{\sim}p)$. Even though, it
defines serial frames in classical modal logic, it does not do so in the Gödel
modal logic. In fact, $\lozenge(p\vee{\sim}p)$ can be refuted _on every
frame_.

One could also think that every $\phi$ that classically defines $\mathbb{F}$,
defines it in $\mathfrak{GK}^{c}$ as long as $\phi^{-}$ ($\phi$ with all
modalities removed) is a $\mathsf{G}$-tautology. It turns out to be false too.
For consider $\lozenge(\Box{\sim\sim}p\rightarrow{\sim\sim}\Box p)$. Clearly,
$\phi^{-}$ is a $\mathsf{G}$-tautology. Classically, $\phi$ defines serial
frames. However, it is not valid on the following frame:

$\textstyle{w_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ldots}$$\textstyle{w_{n}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\ldots}$$\textstyle{w_{0}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{u\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$

Indeed, it suffices to put $v(p,w_{i})=\frac{1}{i}$. Then, $v(\Box
p,w_{0})=0$, while $v(\Box{\sim\sim}p,w_{0})=1$. Hence,
$v(\Box{\sim\sim}p\rightarrow{\sim\sim}\Box p,w_{0})=0$ and $v(\phi,u)=0$,
although the frame is serial.

A question thus arises: which classes of formulas are _transferrable_ , i.e.,
define the same frames in $\mathbf{K}$ and $\mathfrak{GK}^{c}$. In this
section, we establish several such classes.

######  Definition 4.1 (Transferrable formulas).

$\phi\in\\{\mathbf{0},\mathbf{1},{\sim},\wedge,\vee,\rightarrow,\Box,\lozenge\\}$
is called _locally transferrable_ iff for any crisp frame $\mathfrak{F}$ and
$w\in\mathfrak{F}$, it holds that $\mathfrak{F},w\models_{\mathbf{K}}\phi$ iff
$\mathfrak{F},w\models_{\mathbf{K}\mathsf{biG}}\phi$.

######  Proposition 4.1.

Every closed formula (i.e., built only from constants $\mathbf{0}$ and
$\mathbf{1}$) $\phi$ is transferrable.

######  Theorem 4.1.

Let $\phi$, $\phi^{\prime}$, and $\psi$ be locally transferrable. Let further,
$\mathsf{Var}(\phi)\cap\mathsf{Var}(\psi)=\varnothing$. Then,
$\phi\wedge\phi^{\prime}$, $\phi\vee\psi$, and $\Box\phi$ are locally
transferrable.

###### Proof.

The case of $\phi\wedge\phi^{\prime}$ is straightforward, so we will only
consider $\phi\vee\psi$ and $\Box\phi$.

$\phi\vee\psi$

$\displaystyle\mathfrak{F},w\not\models_{\mathbf{K}\mathsf{biG}}\phi\vee\phi^{\prime}$
$\displaystyle\text{ iff
}\mathfrak{F},w\not\models_{\mathbf{K}\mathsf{biG}}\phi\text{ and
}\mathfrak{F},w\not\models_{\mathbf{K}\mathsf{biG}}\psi$ $\displaystyle\text{
iff }\mathfrak{F},w\not\models_{\mathbf{K}}\phi\text{ and
}\mathfrak{F},w\not\models_{\mathbf{K}}\psi$ (by assumption)
$\displaystyle\text{ iff }\mathfrak{F}.w\not\models_{\mathbf{K}}\phi\vee\psi$

$\Box\phi$

$\displaystyle\mathfrak{F},w\not\models_{\mathbf{K}\mathsf{biG}}\Box\phi$
$\displaystyle\text{ iff }\exists w^{\prime}:wRw^{\prime}\text{ and
}\mathfrak{F},w^{\prime}\not\models_{\mathbf{K}\mathsf{biG}}\phi$
$\displaystyle\text{ iff }\exists w^{\prime}:wRw^{\prime}\text{ and
}\mathfrak{F},w^{\prime}\not\models_{\mathbf{K}}\phi$ (by assumption)
$\displaystyle\text{ iff }\mathfrak{F},w\not\models_{\mathbf{K}}\Box\phi$

∎

To establish further transfer results, we will need the notions of _positive_
and _monotone_ formulas.

######  Definition 4.2.

  *   * •

$\phi\in\mathcal{L}^{\neg}_{\triangle,\Box,\lozenge}$ is called _monotone_ iff
it does not contain $\rightarrow$, $\sim$, $\triangle$, and $\neg$.

  * •

A _monotone_ formula is called _positive_ iff it does not contain $\mathbf{1}$
and $\mathbf{0}$.

######  Lemma 4.1.

Let $\phi$ and $\phi^{\prime}$ be monotone. Let further,
$v(\phi,w)>v(\phi^{\prime},w^{\prime})=x^{\prime}$. Define

$\displaystyle v^{\mathsf{cl}}(p,u)$ $\displaystyle=\begin{cases}1&\text{ iff
}v(p,u)>x^{\prime}\\\ 0&\text{ iff }otherwise\end{cases}$ (vCL)

Then $v^{\mathsf{cl}}(\phi,w)=1$ and
$v^{\mathsf{cl}}(\phi^{\prime},w^{\prime})=0$.

###### Proof.

We proceed by induction on the total number of connectives in $\phi$ and
$\phi^{\prime}$. The basis case of $\phi$ and $\phi^{\prime}$ being variables
or constants is straightforward. The cases of propositional connectives are
easy as well.

For $v(\lozenge\phi,w)>v(\phi^{\prime},w^{\prime})$, we proceed as follows.

$\displaystyle v(\lozenge\phi,w)>v(\phi^{\prime},w^{\prime})$
$\displaystyle\text{ iff }\sup\\{v(\phi,u):wRu\\}>v(\phi^{\prime},w^{\prime})$
$\displaystyle\text{ iff }\exists u:wRu\text{ and
}v(\phi,u)>v(\phi^{\prime},w^{\prime})$ $\displaystyle\text{ iff }\exists
u:wRu\text{ and }v^{\mathsf{cl}}(\phi,u)=1\text{ and
}v^{\mathsf{cl}}(\phi^{\prime},w^{\prime})=0$ (by IH) $\displaystyle\text{ iff
}v^{\mathsf{cl}}(\lozenge\phi,w)=1\text{ and
}v^{\mathsf{cl}}(\phi^{\prime},w^{\prime})=0$

Other cases of modalities can be tackled in a similar manner. ∎

######  Theorem 4.2.

Let $\phi$ and $\phi^{\prime}$ be monotone. Then
$\phi\rightarrow\phi^{\prime}$ is locally transferrable.

###### Proof.

Immediately from lemma 4.1. ∎

The final transfer result we are going to discuss in this section is that
Sahlqvist formulas are transferrable. We recall the definition from [9].

######  Definition 4.3.

A _Sahlqvist implication_ ($\mathsf{SI}$) is a formula $\phi\rightarrow\chi$
with

$\mathsf{SI}\ni\phi\coloneqq
l\in\mathtt{Prop}\cup\\{{\sim}p:p\in\mathtt{Prop}\\}\cup\\{\underbrace{\Box\ldots\Box}_{k\text{
times}}p:p\in\mathtt{Prop},k\in\mathbb{N}\\}\mid\phi\wedge\phi\mid\phi\vee\phi\mid\lozenge\phi$

and $\chi$ being _positive_. _Sahlqvist formulas_ ($\mathsf{SF}$) are obtained
using the following grammar:

$\mathsf{SF}\ni\psi,\psi^{\prime}\coloneqq\tau\in\mathsf{SI}\mid\psi\wedge\psi\mid\psi\vee\psi^{\prime}~{}(\mathsf{Var}(\psi)\cap\mathsf{Var}(\psi^{\prime})=\varnothing)\mid\Box\psi$

######  Theorem 4.3.

Sahlqvist formulas are locally transferrable.

###### Proof.

By theorem 4.1, it suffices to prove the statement only for Sahlqvist
implications.

Let $\phi\rightarrow\chi\in\mathsf{SI}$. Assume that $v(\phi,w)>x^{\prime}$
and $v(\chi,w^{\prime})=x^{\prime}\neq 1$.

We show by induction on the total number of connectives that

$\displaystyle v(\phi,u)>x^{\prime}$ $\displaystyle\Rightarrow
v^{\mathsf{cl}}(\phi,u)=1$ ($\phi$ as in definition 4.3) $\displaystyle
v(\chi,u^{\prime})\leqslant x^{\prime}$ $\displaystyle\Rightarrow
v^{\mathsf{cl}}(\chi,u^{\prime})=0$ ($\chi$ is positive)

The basis case of variables and constants is straightforward.

$v({\sim}p,w)=1$, $v(\chi,w^{\prime})<1$

$\displaystyle v({\sim}p,w)=1\text{ and }v(\chi,w^{\prime})<1$
$\displaystyle\Rightarrow v(p,w)=0\text{ and }v(\chi,w^{\prime})=x^{\prime}<1$
$\displaystyle\Rightarrow v^{\mathsf{cl}}(p,w)=0\text{ and
}v^{\mathsf{cl}}(\chi,w^{\prime})=0$ (by IH since $p$ is positive)
$\displaystyle\Rightarrow v^{\mathsf{cl}}({\sim}p,w)=1\text{ and
}v^{\mathsf{cl}}(\chi,w^{\prime})=0$

The cases of propositional connectives as well as
$\phi=\underbrace{\Box\ldots\Box}_{k\text{ times}}p$ are easy as well.

$v(\lozenge\phi^{\prime},w)>x^{\prime}$, $v(\chi,w^{\prime})=x^{\prime}<1$

$\displaystyle v(\lozenge\phi^{\prime},w)>x^{\prime}\text{ and
}v(\chi,w^{\prime})=x^{\prime}<1$
$\displaystyle\Rightarrow\sup\\{v(\phi^{\prime},u):wRu\\}>x^{\prime}\text{ and
}v(\chi,w^{\prime})=x^{\prime}$ $\displaystyle\Rightarrow\exists u:wRu\text{
and }v(\phi^{\prime},u)>x^{\prime}\text{ and }v(\chi,w^{\prime})=x^{\prime}$
$\displaystyle\Rightarrow\exists u:wRu\text{ and
}v^{\mathsf{cl}}(\phi^{\prime},u)=1\text{ and
}v^{\mathsf{cl}}(\chi,w^{\prime})=0$ (by IH) $\displaystyle\Rightarrow
v^{\mathsf{cl}}(\lozenge\phi^{\prime},w)=1\text{ and
}v^{\mathsf{cl}}(\chi,w^{\prime})=0$

∎

Note that the two classes of transferrable formulas in theorems 4.2 and 4.3 do
not coincide as there are Sahlqvist implications that are not monotone and
there are implications of monotone formulas that are not Sahlqvist. Note,
furthermore, that the above theorems _do not_ characterise the class of
transferrable formulas completely: for example, we can show that the Gödel-Löb
formula $\Box(\Box p\rightarrow p)\rightarrow\Box p$ is locally transferrable,
even though, it is neither monotone, nor Sahlqvist, nor obtained from
transferrable formulas via theorem 4.1.

######  Proposition 4.2.

Let $\mathfrak{F}=\langle W,R\rangle$ be a crisp frame. Then,
$\mathfrak{F},w\models_{\mathbf{K}\mathsf{biG}}\Box(\Box p\rightarrow
p)\rightarrow\Box p$ iff $R$ is transitive and does not contain an infinite
chain $wRw_{0}Rw_{1}Rw_{2}R\ldots$ originating from $w$ (i.e., conversely
well-founded).

###### Proof.

Since $\mathbf{K}\mathsf{biG}$ valuations preserve classical values, we only
prove the ‘only if’ direction. Let $\mathfrak{F}=\langle W,R\rangle$ be a
crisp frame s.t. $R$ is transitive and conversely well founded. We let

$v(\Box(\Box p\rightarrow p),w)=x>0$

for some $w\in\mathfrak{F}$ and $v$ on $\mathfrak{F}$. Then, for every
$w^{\prime}\in R(w)$, it holds either $v(p,w)\geq x$ or $v(\Box
p,w^{\prime})\leq v(p,w^{\prime})$.

Recall that $R$ does not have infinite chains beginning from $w$. Thus,
$v(p,w^{\prime\prime})\geq x$ for every $w^{\prime\prime}\in R(w)$ s.t.
$R(w^{\prime\prime})=\varnothing$ because $v(\Box p,w^{\prime\prime})=1$ for
every such $w^{\prime\prime}$. Denote the set of these states with $W_{0}$.

In general, for every $n\in\mathbb{N}$, we define $W_{-n}$ to be the set of
all $t\in R(w)$ s.t. the longest $R$-sequence originating from $t$ has $n$
members.

It is clear that $w\in W_{-(k+1)}$ for some $k\in\mathbb{N}$ and that
$R(w)=\bigcup\limits^{k}_{i=0}W_{-i}$. We show by induction on $k$ that
$v(p,u)\geq x$ for every $u\in\bigcup\limits^{k}_{i=0}W_{i-1}$. The basis case
is already shown. Assume that the statement holds for some $l$. We show it for
$l+1$ and reason for a contradiction. Let $u^{\prime}\in W_{-(l+1)}$ and
$v(p,u^{\prime})<x$. But then, since $R$ is transitive and irreflexive, we
have $v(\Box p,u^{\prime})\geq x$ by the induction hypothesis. Hence, $v(\Box
p\rightarrow p,u^{\prime})<x$ and further, $v(\Box(\Box p\rightarrow p),w)<x$,
contrary to the assumption.

Thus, $v(p,u)\geq x$ for every $u\in R(w)$. But then, $v(\Box p,w)\geq x$, as
required. ∎

###  4.2 Glivenko’s theorem and its relatives

In this section, we study the fragments of $\mathbf{K}\mathsf{biG}$ and
$\mathbf{K}\mathsf{G}^{2}$ that admit Glivenko’s theorem [19] that we present
in its semantical form.

######  Theorem 4.4.

$\phi$ is a classical propositional tautology iff ${\sim\sim}\phi$ is a
(super-)intuitionistically valid propositional formula.

Glivenko’s theorem in non-intermediate propositional logics is well studied
(cf., e.g. [28] and the literature referred to therein). It is also known [21]
that the theorem holds for the $\exists$ fragment of the first-order
intuitionistic logic. Furthermore, versions of Glivenko’s theorem for modal
intuitionistic logics are studied in [4].

Considering $\mathbf{K}\mathsf{biG}$ and
$\mathbf{K}\mathsf{biG}^{\mathsf{f}}$, we, first, notice that the unrestricted
version of Glivenko’s theorem (unsurprisingly) fails:
${\sim\sim}\Box(p\vee{\sim}p)$ is not $\mathbf{K}\mathsf{biG}$ valid. In fact,
it is easy to see that it defines finitely branching888A _crisp_ frame
$\langle W,R\rangle$ is finitely branching iff $R(w)$ is finite for every
$w\in W$. A _fuzzy_ frame is finitely branching iff $R^{+}(w)$ is finite for
every $w$. frames.

######  Proposition 4.3.

A (crisp or fuzzy) frame $\mathfrak{F}$ is finitely branching iff
$\mathfrak{F}\models_{\mathbf{K}\mathsf{biG}}{\sim}{\sim}\Box(p\vee{\sim}p)$.

###### Proof.

We show only the fuzzy case as the crisp one can be proven in a similar
manner.

Assume that $\mathfrak{F}$ is finitely branching. Then, clearly,
$v(\Box(p\vee{\sim}p),w)=\max\\{R(w,w^{\prime})\rightarrow_{\mathsf{G}}v(p\vee{\sim}p,w^{\prime}):w^{\prime}\in
W\\}>0$. Hence, $v({\sim}{\sim}\Box(p\vee{\sim}p),w)=1$.

Now let $\mathfrak{F}$ be infinitely branching, let $X\subseteq R(w)$ be
countable and w.l.o.g. $R(w,w_{i})\geqslant R(w,w_{j})$ iff $i<j$ for every
$w_{i},w_{j}\in X$. We define $v(p,w_{1})=\frac{R(w,w_{1})}{2}$ and

$\displaystyle v(p,w_{i+1})$
$\displaystyle=\begin{cases}\dfrac{v(p,w_{i})}{2}&\text{ iff
}v(p,w_{i})\leqslant R(w,w_{i+1})\\\ \dfrac{R(w,w_{i+1})}{2}&\text{
otherwise}\end{cases}$

It is clear that $v({\sim}p,w_{i})=0$ and that
$v(p\vee{\sim}p,w_{i})=v(p,w_{i})$ for every $w_{i}\in R(w)$.

Observe that
$\inf\\{R(w,w^{\prime})\rightarrow_{\mathsf{G}}v(p,w^{\prime}):w\in W\\}=0$.
Thus, $v(\Box(p\vee{\sim}p),w)=0$, and thus
$v({\sim}{\sim}\Box(p\vee{\sim}p),w)=0$, as required. ∎

In what follows, we will show, that Glivenko’s theorem holds in all finitely
branching frames, and that, conversely, if Glivenko’s theorem holds for a
logic of a class of frames $\mathbb{F}$, then $\mathbb{F}$ does not contain
infinitely branching frames. For this, we require some preliminary definitions
and statements.

######  Definition 4.4 (Logic of $\mathbb{F}$).

Let $\mathbb{F}$ be a class of frames. A _$\mathbf{K}\mathsf{biG}$
($\mathbf{K}\mathsf{G}^{2}$) logic of $\mathbb{F}$_ is a set
$\mathsf{L}\subseteq\mathcal{L}_{\triangle,\Box,\lozenge}$
($\mathsf{L}\subseteq\mathcal{L}^{\neg}_{\triangle,\Box,\lozenge}$) s.t.
$\mathfrak{F}\models_{\mathbf{K}\mathsf{biG}}\mathsf{L}$
($\mathfrak{F}\models_{\mathbf{K}\mathsf{G}^{2}}\mathsf{L}$) for every
$\mathfrak{F}\in\mathbb{F}$.

######  Definition 4.5.

For any model $\mathfrak{M}=\langle W,R,v\rangle$, define a model
$\mathfrak{M}^{\mathsf{cl}}=\langle W,R^{\mathsf{cl}},v^{\mathsf{cl}}\rangle$
s.t.

$\displaystyle wR^{\mathsf{cl}}w^{\prime}$
$\displaystyle=\begin{cases}1&\text{ iff }wRw^{\prime}\neq 0\\\ 0&\text{ iff
}wRw^{\prime}=0\end{cases}$ $\displaystyle v^{\mathsf{cl}}(p,w)$
$\displaystyle=\begin{cases}1&\text{ iff }v(p,w)\neq 0\\\ 0&\text{ iff
}v(p,w)=0\end{cases}$

For any frame $\mathfrak{F}=\langle W,R\rangle$, we set
$\mathfrak{F}^{\mathsf{cl}}=\langle W,R^{\mathsf{cl}}\rangle$.

######  Lemma 4.2.

Let $\phi$ be a formula over
$\\{\mathbf{0},\wedge,\vee,\rightarrow,\Box,\lozenge\\}$. Then for any
finitely branching frame $\mathfrak{F}$ and for any $v$ on $\mathfrak{F}$, it
holds that

$\displaystyle v^{\mathsf{cl}}(\phi,w)$ $\displaystyle=\begin{cases}1&\text{
iff }v(\phi,w)\neq 0\\\ 0&\text{ iff }v(\phi,w)=0\end{cases}$ (4)

###### Proof.

We prove by induction. The cases when $\phi=p$ or $\phi=\mathbf{0}$ are
trivial.

$\phi=\psi\wedge\psi^{\prime}$

$\displaystyle v(\psi\wedge\psi^{\prime},w)=0$ $\displaystyle\text{ iff
}v(\psi,w)=0\text{ or }v(\psi^{\prime},w)=0$ $\displaystyle\text{ iff
}v^{\mathsf{cl}}(\psi,w)=0\text{ or }v^{\mathsf{cl}}(\psi^{\prime},w)=0$ (by
IH) $\displaystyle\text{ iff }v^{\mathsf{cl}}(\psi\wedge\psi^{\prime},w)=0$

$\phi=\psi\vee\psi^{\prime}$ is dual.

$\phi=\psi\rightarrow\psi^{\prime}$

$\displaystyle v(\psi\rightarrow\psi^{\prime},w)=0$ $\displaystyle\text{ iff
}v(\psi,w)\neq 0\text{ and }v(\psi^{\prime},w)=0$ $\displaystyle\text{ iff
}v^{\mathsf{cl}}(\psi,w)=1\text{ or }v^{\mathsf{cl}}(\psi^{\prime},w)=0$ (by
IH) $\displaystyle\text{ iff
}v^{\mathsf{cl}}(\psi\rightarrow\psi^{\prime},w)=0$ $\displaystyle
v(\psi\wedge\psi^{\prime},w)\neq 0$ $\displaystyle\text{ iff
}v(\psi^{\prime},w)\neq 0$ $\displaystyle\text{ iff
}v^{\mathsf{cl}}(\psi^{\prime},w)=1$ (by IH) $\displaystyle\text{ iff
}v^{\mathsf{cl}}(\psi\wedge\psi^{\prime},w)=1$

$\phi=\Box\psi$

$\displaystyle v(\Box\psi,w)=0$ $\displaystyle\text{ iff }\exists
w^{\prime}:wRw^{\prime}>0\text{ and }v(\psi,w^{\prime})=0$
$\displaystyle\text{ iff }\exists w^{\prime}:wRw^{\prime}=1\text{ and
}v^{\mathsf{cl}}(\psi,w^{\prime})=0$ (by IH) $\displaystyle\text{ iff
}v^{\mathsf{cl}}(\Box\psi,w)=0$ (by finite branching)

$\phi=\lozenge\psi$

$\displaystyle v(\lozenge\psi,w)\neq 0$ $\displaystyle\text{ iff }\exists
w^{\prime}:wRw^{\prime}>0\wedge v(\psi,w^{\prime})\neq 0$ $\displaystyle\text{
iff }\exists w^{\prime}:wRw^{\prime}=1\Rightarrow
v^{\mathsf{cl}}(\psi,w^{\prime})=1$ (by IH) $\displaystyle\text{ iff
}v^{\mathsf{cl}}(\lozenge\psi,w)=1$

∎

The following unsurprising statement is immediate.

######  Proposition 4.4.

Let $\phi\in\\{\mathbf{0},\wedge,\vee,\rightarrow,\lozenge\\}$. Then

  1. 1.

$\phi$ is $\mathbf{K}$ valid iff ${\sim\sim}\phi$ is $\mathbf{K}\mathsf{biG}$
valid iff ${\sim\sim}\phi$ is $\mathbf{K}\mathsf{biG}^{\mathsf{f}}$ valid;

  2. 2.

$\mathfrak{F}\models_{\mathbf{K}}\phi$ iff
$\mathfrak{F}\models_{\mathbf{K}\mathsf{biG}}\phi$ for every crisp
$\mathfrak{F}$.

###### Proof.

Note that in the proof of lemma 4.2, we use the finite branching only in the
$\Box$ case but $\phi$ is $\Box$-free. ∎

######  Theorem 4.5.

  1.   2. 1.

Let $\phi$ be a formula over
$\\{\mathbf{0},\wedge,\vee,\rightarrow,\Box,\lozenge\\}$. Then it is
$\mathbf{K}$-valid iff ${\sim\sim}\phi$ is $\mathbf{K}\mathsf{biG}$-valid
($\mathbf{K}\mathsf{biG}^{\mathsf{f}}$) on all finitely branching frames.

  3. 2.

Let $\mathbb{F}$ be a class of (fuzzy or crisp) frames and let $\mathsf{L}$ be
the $\mathbf{K}\mathsf{biG}$ logic of $\mathbb{F}$. Then,
$\\{{\sim\sim}\phi:\phi\text{ is
}\mathbb{F}\models_{\mathbf{K}}\phi\\}\subseteq\mathsf{L}$ implies that every
$\mathfrak{F}\in\mathbb{F}$ is finitely branching.

###### Proof.

We begin with 1. Clearly, if $\phi$ is not valid in $\mathbf{K}$, there is a
finite branching frame where it is invalidated by a classical valuation. But
classical valuations are preserved in $\mathbf{K}\mathsf{biG}$.

For the converse, let ${\sim\sim}\phi$ be not $\mathbf{K}\mathsf{biG}$-valid
on some finitely branching frame $\mathfrak{F}$. Then, there exist
$w\in\mathfrak{F}$ and $v$ on $\mathfrak{F}$ s.t. $v({\sim\sim}\phi,w)\neq 1$.
But then, $v(\phi,w)=0$. Hence, by lemma 4.2, we have a classical valuation
$v^{\mathsf{cl}}$ on $\mathfrak{F}^{\mathsf{cl}}$ s.t.
$v^{\mathsf{cl}}(\phi,w)=0$. The result follows.

Consider 2. We reason by contraposition. Assume that $\mathbb{F}$ contains
some infinitely branching frame $\mathfrak{F}$. But then
$\mathfrak{F}\not\models_{\mathbf{K}\mathsf{biG}}{\sim\sim}\Box(p\vee{\sim}p)$.
Thus, $\\{{\sim\sim}\phi:\phi\text{ is }\mathbf{K}\text{ valid on
}\mathbb{F}\\}\not\subseteq\mathsf{L}$ as required. ∎

By conservativity (proposition 2.10), the above result extends to
$\mathbf{K}\mathsf{G}^{2}$. Moreover, we can obtain a result similar to
theorem 4.5 but with adding $\neg{\sim}$ on top of formulas instead of
${\sim\sim}$. This can be considered as a counterpart of Glivenko’s theorem
for $\mathsf{I}_{4}\mathsf{C}_{4}$ and its extensions999Recall that
$\mathsf{G}^{2}$ is a linear extension of $\mathsf{I}_{4}\mathsf{C}_{4}$. for
it holds for every $\phi$ over $\\{\mathbf{0},\wedge,\vee,\rightarrow\\}$ that
$\phi$ is classically valid iff $\neg{\sim}\phi$ is valid in
$\mathsf{I}_{4}\mathsf{C}_{4}$.

######  Theorem 4.6.

  1.   2. 1.

Let $\phi$ be a formula over
$\\{\mathbf{0},\wedge,\vee,\rightarrow,\Box,\lozenge\\}$. Then it is
$\mathbf{K}$-valid iff $\neg{\sim}\phi$ is $\mathbf{K}\mathsf{G}^{2}$-valid on
all finitely branching crisp frames.

  3. 2.

Let $\mathbb{F}$ be a class of crisp frames, and let $\mathsf{L}$ be the
$\mathbf{K}\mathsf{G}^{2}$ logic of $\mathbb{F}$. Then,
$\\{\neg{\sim}\phi:\mathbb{F}\models_{\mathbf{K}}\phi\\}\subseteq\mathsf{L}$
implies that every $\mathfrak{F}\in\mathbb{F}$ is finitely branching.

###### Proof.

Consider 1. It is clear that no classically valid $\phi$ can have
$v_{1}(\phi,w)=0$, nor $v_{2}(\phi,w)=1$. Otherwise, by lemma 4.2 and
proposition 2.8, there is a classical valuation $v^{\mathsf{cl}}$ s.t.
$v^{\mathsf{cl}}(\phi,w)=(0,1)$. Thus, $v(\neg{\sim}\phi,w)=(1,0)$, as
required.

For 2, assume that $\mathbb{F}$ contains an infinitely branching frame
$\mathfrak{F}$. Let now $R(w)$ be infinite for some $w\in\mathfrak{F}$ and
$\\{w_{i}:i\\!\geq\\!1,i\\!\in\\!\mathbb{N}\\}\subseteq R(w)$. We set
$v(p,w_{i})\\!=\\!\left(\frac{1}{i+1},1-\frac{1}{i}\right)$. It is easy to see
that $v(\Box(p\\!\vee\\!{\sim}p),w)\\!=\\!(0,1)$, whence
$v(\neg{\sim}\Box(p\\!\vee\\!{\sim}p),w)\\!=\\!(0,1)$, and thus,
$\\{\neg{\sim}\phi\\!:\\!\mathbb{F}\models_{\mathbf{K}}\phi\\}\not\subseteq\mathsf{L}$.
∎

##  5 Decidability and complexity

In this section, we establish that, as expected, the satisfiability and
validity101010Satisfiability and falsifiability (non-validity) are reducible
to each other using $\triangle$: $\phi$ is satisfiable (falsifiable) iff
${\sim}\triangle\phi$ is falsifiable (satisfiable). of
$\mathbf{K}\mathsf{biG}$ and $\mathbf{K}\mathsf{G}^{2}$ are $\mathsf{PSPACE}$
complete. We apply the approach proposed in [14, 15].

The next definition is a straightforward adaptation of [14] to
$\mathbf{K}\mathsf{biG}$.

######  Definition 5.1 ($\mathsf{F}$-models of $\mathbf{K}\mathsf{biG}$).

An $\mathsf{F}$-model is a tuple $\mathfrak{M}=\langle W,R,T,v\rangle$ with
$\langle W,R,v\rangle$ being a $\mathbf{K}\mathsf{biG}$ model and
$T:W\rightarrow\mathcal{P}_{<\omega}([0,1])$ be s.t. $\\{0,1\\}\subseteq T(w)$
for all $w\in W$. $v$ is extended to the complex formulas as in
$\mathbf{K}\mathsf{biG}$ in the cases of propositional connectives, and in the
modal cases, as follows.

$\displaystyle v(\Box\phi,w)$ $\displaystyle=\max\\{x\in
T(w):x\leq\inf\\{v(\phi,w^{\prime}):wRw^{\prime}\\}\\}$ $\displaystyle
v(\lozenge\phi,w)$ $\displaystyle=\min\\{x\in
T(w):x\geq\sup\\{v(\phi,w^{\prime}):wRw^{\prime}\\}\\}$

######  Example 5.1 (A finite $\mathsf{F}$-model).

Recall that there are no finite $\mathbf{K}\mathsf{biG}$ countermodels for
$\phi=\triangle\lozenge p\rightarrow\lozenge\triangle p$. It is, however, easy
to provide a finite $\mathsf{F}$-model of $\phi$ (cf. fig. 2). Indeed, it is
clear that $v(\phi,w)=0$.

$\textstyle{w:\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{w^{\prime}:p=\frac{1}{2}}$
Figure 2: $T(w)=\\{0,1\\}$, $T(w^{\prime})$ can be arbitrary.

One sees that $v(p,w^{\prime})=\frac{1}{2}$, whence
$\inf\\{v(p,w^{\prime}):wRw^{\prime}\\}=\frac{1}{2}$ as well. But then the
minimal $T(w)$ that is at least as great as $\frac{1}{2}$ is $1$. Thus,
$v(\triangle\lozenge p,w)=1$. On the other hand, $v(\triangle
p,w^{\prime})=0$, whence, $v(\lozenge\triangle p,w)=0$.

The next lemma is a straightforward extension of [14, Theorem 1] to
$\mathbf{K}\mathsf{biG}$. The proof is essentially the same since we add only
$\triangle$ to the language.

######  Lemma 5.1.

$\phi$ is $\mathbf{K}\mathsf{biG}$ valid iff $\phi$ is true in all
$\mathsf{F}$-models iff $\phi$ is true in all $\mathsf{F}$-models whose depth
is $O(|\phi|)$ s.t. $|W|\leq(|\phi|+2)^{|\phi|}$ and $|T(w)|\leq|\phi|+2$ for
all $w\in W$.

It is now clear that $\mathbf{K}\mathsf{biG}$ (and hence
$\mathbf{K}\mathsf{G}^{2}$) are decidable. It remains to establish its
complexity. Let us now provide an algorithm that checks the satisfiability.

First of all, we observe from lemma 5.1 that for every
$\phi(p_{1},\ldots,p_{n})\in\mathcal{L}_{\Yleft,\Box,\lozenge}$, the number of
possible values of the subformulas is bounded from above with

$r+1=(|\phi|+2)\cdot(|\phi|+2)^{|\phi|}+n\cdot(|\phi|+2)^{|\phi|}$

since the values of the subformulas of $\phi$ are contained in the following
set

$U=\bigcup\limits_{w\in W}\left(\\{v(p_{i},w):1\leq i\leq n\\}\cup
T(w)\right)$

In the following, we w.l.o.g. assume that the set of values is given as
follows:

$\mathsf{V}=\left\\{0,\dfrac{1}{r},\ldots,\dfrac{r-1}{r},1\right\\}$

We adapt the approach from [6]. Namely, we provide rule schemas for a tableaux
calculus111111Alternatively, we could utilise the algorithm described in [15].
The algorithm would work for $\mathbf{K}\mathsf{biG}$ since its only
difference from $\mathfrak{GK}^{c}$ is $\triangle$ which is a propositional
connective. that can be applied to particular formulas.

######  Definition 5.2 (Tableaux calculus
$\mathcal{T}\left(\mathbf{K}\mathsf{biG}\right)$).

We fix a countable set of state labels $\mathsf{W}$ and define a labelled
formula to be $w:\phi=\mathsf{v}$ with $w\in\mathsf{W}$ and
$\mathsf{v}\in\mathsf{V}$. A tableau is a downward branching tree each node of
which is either a labelled formula or a relational term
$w\mathsf{R}w^{\prime}$ with $w,w^{\prime}\in\mathsf{W}$.

Now let $\heartsuit_{w}=\\{w:\heartsuit\phi_{i}=\mathsf{v}_{i}:1\leq i\leq
m\\}$ be the set of all modal formulas in $\mathcal{B}$ labelled with $w$. We
define the _value successor_ and the _value predecessor_ of $\mathsf{v}_{i}$
($\mathsf{s}_{w}(\mathsf{v}_{i})$ and $\mathsf{pr}_{w}(\mathsf{v}_{i})$,
respectively) as follows.

$\displaystyle\mathsf{s}_{w}(\mathsf{v}_{i})$
$\displaystyle=\max\\{\mathsf{v}\in\mathsf{V}:\mathsf{v}\neq\mathsf{v}_{i+1}\\}$
$\displaystyle\mathsf{pr}_{w}(\mathsf{v}_{i})$
$\displaystyle=\min\\{\mathsf{v}\in\mathsf{V}:\mathsf{v}\neq\mathsf{v}_{i+1}\\}$
(5)

Every branch $\mathcal{B}$ can be extended by an application of a
propositional (cf. fig. 3 for propositional rules) or a modal rule

$\displaystyle{\sim}1:\dfrac{w:{\sim}\phi=1}{w:\phi=0}$
$\displaystyle{\sim}0:\dfrac{w:{\sim}\phi=0}{w:\phi=1\mid\ldots\mid
w:\phi=\frac{1}{r}}$ $\displaystyle\triangle
1:\dfrac{w:\triangle\phi=1}{w:\phi=1}$ $\displaystyle\triangle
0:\dfrac{w:\triangle\phi=0}{w:\phi=0\mid\ldots\mid w:\phi=\frac{r-1}{r}}$

$\displaystyle\rightarrow
1:\dfrac{w\\!:\\!\phi\rightarrow\phi^{\prime}\\!=\\!1}{w\\!:\\!\phi=0\left|\begin{matrix}w\\!:\\!\phi\\!=\\!\frac{1}{r}\\\
w\\!:\\!\phi^{\prime}\\!=\\!\frac{1}{r}\end{matrix}\right.\left|\begin{matrix}w\\!:\\!\phi\\!=\\!\frac{1}{r}\\\
w\\!:\\!\phi^{\prime}\\!=\\!\frac{2}{r}\end{matrix}\right|\ldots\left|\begin{matrix}w\\!:\\!\phi\\!=\\!\frac{r-2}{r}\\\
w\\!:\\!\phi^{\prime}\\!=\\!\frac{r-1}{r}\end{matrix}\right|w\\!:\\!\phi^{\prime}\\!=\\!1}$
$\displaystyle\rightarrow<\\!1:\dfrac{\dfrac{w:\phi\rightarrow\phi^{\prime}=\frac{k}{r}}{w:\phi^{\prime}=\frac{k}{r}}}{w:\phi=1\mid\ldots\mid\phi^{\prime}=\frac{k+1}{r}}$

Figure 3: Propositional rules for ${\sim}$, $\rightarrow$, and $\triangle$.
Vertical bars denote branching. $\rightarrow<1$ works in two steps: it first
adds $w:\phi^{\prime}=\frac{k}{r}$ and then splits the branch. Rules
corresponding to other propositional connectives are defined similarly.

(cf. fig. 4 for the modal rules) if no propositional rule is applicable.
$\mathcal{B}$ is _closed_ if
$\\{w:\phi=\mathsf{v},w:\phi=\mathsf{v}^{\prime}\\}\subseteq\mathcal{B}$ for
some $\mathsf{v}\neq\mathsf{v}^{\prime}$, or if
$w:\triangle\phi=\mathsf{v}\in\mathcal{B}$ for some $0<\mathsf{v}<1$, or if
$w:{\sim}\phi=\mathsf{v}\in\mathcal{B}$ for some $0<\mathsf{v}<1$. A tableau
is closed iff all branches are closed. A branch is _open and complete_ if it
is not closed but for every possible application of a rule, one of its
conclusions already appears on the branch.

$\displaystyle\Box^{+}\\!:\dfrac{\dfrac{w\\!:\\!\Box\phi\\!=\\!\frac{k}{r}}{w\mathsf{R}w^{\prime}}}{\left.\begin{matrix}w^{\prime}\\!:\\!\phi\\!=\\!\frac{k}{r}\end{matrix}\right|\left.\begin{matrix}w^{\prime}\\!:\\!\phi\\!=\\!\frac{k+1}{r}\end{matrix}\right|\ldots\left|\begin{matrix}w^{\prime}\\!:\\!\phi\\!=\\!\mathsf{s}_{w}\left(\frac{k}{r}\right)\end{matrix}\right.}$
$\displaystyle\Box^{\mathsf{R}}\\!:\dfrac{w\\!:\\!\Box\phi\\!=\\!\frac{k}{r};w\mathsf{R}w^{\prime\prime}}{w^{\prime\prime}\\!:\\!\phi\\!=\\!1\mid\ldots\mid
w^{\prime\prime}\\!:\\!\phi\\!=\\!\frac{k}{r}}$ $\displaystyle\Box
1\\!:\dfrac{w\\!:\\!\Box\phi\\!=\\!1,w\mathsf{R}w^{\prime\prime}}{w^{\prime\prime}\\!:\\!\phi\\!=\\!1}$
$\displaystyle\lozenge^{+}\\!:\dfrac{\dfrac{w:\lozenge\phi\\!=\\!\frac{k}{r}}{w\mathsf{R}w^{\prime}}}{\left.\begin{matrix}w^{\prime}\\!:\\!\phi\\!=\\!\frac{k}{r}\end{matrix}\right|\left.\begin{matrix}w^{\prime}\\!:\\!\phi\\!=\\!\frac{k-1}{r}\end{matrix}\right|\ldots\left|\begin{matrix}w^{\prime}\\!:\\!\phi\\!=\\!\mathsf{pr}_{w}\left(\frac{k}{r}\right)\end{matrix}\right.}$
$\displaystyle\lozenge^{\mathsf{R}}\\!:\dfrac{w\\!:\\!\lozenge\phi\\!=\\!\frac{k}{r};w\mathsf{R}w^{\prime\prime}}{w^{\prime\prime}\\!:\\!\phi\\!=\\!0\mid\ldots\mid
w^{\prime\prime}\\!:\\!\phi\\!=\\!\frac{k}{r}}$ $\displaystyle\lozenge
0\\!:\dfrac{w\\!:\\!\lozenge\phi\\!=\\!0,w\mathsf{R}w^{\prime\prime}}{w^{\prime\prime}\\!:\\!\phi\\!=\\!0}$
Figure 4: Vertical bars denote branching. $w^{\prime}$ is fresh on the branch.
$\Box^{+}$ and $\lozenge^{+}$ work in two steps: first, a new accessible state
is added, then the branching occurs.

Before designing the decision algorithm, we show that
$\mathcal{T}\left(\mathbf{K}\mathsf{biG}\right)$ is sound and complete w.r.t.
$\mathsf{F}$-models. Namely, if $\phi$ is valid, then any tableau whose root
is $w:\phi=\mathsf{v}$ ($\mathsf{v}<1$) is closed. And if a tableaux for
$w:\phi=\mathsf{v}$ contains a complete open branch, then there are an
$\mathsf{F}$-model $\mathfrak{M}$ and $w\in\mathfrak{M}$ s.t.
$v(\phi,w)=\mathsf{v}$.

######  Definition 5.3 (Branch realisation).

We say that $\mathfrak{M}=\langle W,R,T,v\rangle$ _realises_ $\mathcal{B}$ iff
the following conditions apply.

  * •

$W=\\{w\mid w\text{ occurs on }\mathcal{B}\\}$.

  * •

$R=\\{\langle w,w^{\prime}\rangle\mid w\mathsf{R}w^{\prime}\text{ occurs on
}\mathcal{B}\\}$.

  * •

$T(w)=\\{0,1\\}\cup\\{\mathsf{v}\mid w:\heartsuit\phi=\mathsf{v}\text{ occurs
on }\mathcal{B}\\}$.

  * •

$v(\phi,w)=\mathsf{v}$ for every $w:\phi=\mathsf{v}\in\mathcal{B}$.

######  Theorem 5.1 (Completeness).

$\mathcal{T}\left(\mathbf{K}\mathsf{biG}\right)$ is sound and complete w.r.t.
$\mathsf{F}$-models.

###### Proof.

We begin with the soundness part. Since no closed branch is realisable, it
suffices to check that if the premise of a rule is realised, then so is at
least one of its conclusion. The cases of propositional rules are
straightforward as well as that of $\Box 1$.

The case of $\Box^{\mathsf{R}}$ is also easy. Indeed, assume that
$v(\Box\phi,w)=\mathsf{v}<1$ and that also $w\mathsf{R}w^{\prime\prime}$. It
is clear that $v(\phi,w^{\prime\prime})\geqslant v(\Box\phi,w)$. Thus, at
least one of the conclusions is satisfied.

Consider now the case of $\Box^{+}$. Assume that $w:\Box\phi=\frac{k}{r}<1$ is
realised. Thus, $\frac{k}{r}\in T(w)$ and $\frac{k}{r}=\max\\{x\in T(w)\mid
x\leq\inf\\{v(\phi,w^{\prime})\mid wRw^{\prime}\\}\\}$. Furthermore, since the
model is finite, there must exist an accessible state $w^{\prime}$ s.t.
$\frac{k}{r}\leq v(\phi,w^{\prime})\leq\mathsf{s}_{w}\left(\frac{k}{r}\right)$
and $v(\phi,w^{\prime\prime})\geq v(\phi,w^{\prime})$ for every
$w^{\prime\prime}\in R(w)$. But then, at least one of the conclusions of
$\Box^{+}$ is satisfied.

The cases of $\lozenge^{\mathsf{R}}$ and $\lozenge^{+}$ can be tackled in a
dual manner.

Let us now show that every complete open branch is realisable. We proceed by
induction on formulas. All labelled variables are realisable by the
construction of the model. The induction steps of propositional connectives
are straightforward. Let us now consider the case of $w:\Box\phi=\mathsf{v}$.
We have two options: (1) $\mathsf{v}=1$ or (2) $\mathsf{v}<1$.

If (1), then applying $\Box 1$ $w^{\prime\prime}:\phi=1\in\mathcal{B}$ for
every $w^{\prime\prime}$ occurring in $\mathcal{B}$ s.t.
$w\mathsf{R}w^{\prime\prime}\in\mathcal{B}$. By the induction hypothesis,
every $w^{\prime\prime}:\phi=1$ is realised, i.e.,
$v(\phi,w^{\prime\prime})=1$. But then, $v(\Box\phi,w)=1$ as well, as
required.

If (2), we have that $w:\Box\phi=\frac{k}{r}\in\mathcal{B}$. Since
$\mathcal{B}$ is open and complete, then by $\Box^{+}$, there is a fresh
$w^{\prime}$ s.t. $w\mathsf{R}w^{\prime}\in\mathcal{B}$ and
$w^{\prime}:\phi=\mathsf{v}^{\prime}\in\mathcal{B}$ for some
$\frac{k}{r}\leq\mathsf{v}^{\prime}\leq\mathsf{s}_{w}\left(\frac{k}{r}\right)$
and, by $\Box^{\mathsf{R}}$, for every $w^{\prime\prime}$ s.t.
$w\mathsf{R}w^{\prime\prime}$ is already on the branch,
$w^{\prime\prime}:\phi=\mathsf{v}^{\prime\prime}\in\mathcal{B}$ for some
$\mathsf{v}^{\prime\prime}\geq\frac{k}{r}$. By the induction hypothesis, all
these formulas are realised. Furthermore, since modal rules can be applied
only after no propositional rule is applicable, $\frac{k}{r}$ is indeed the
maximal value in $T(w)$ that does not exceed
$\inf\\{v(\phi,x):w\mathsf{R}x\\}$. Thus, $w:\Box\phi=\frac{k}{r}$ is
realised, as required.

The cases of $\lozenge$ rules can be considered dually. ∎

Note that now the complete open branch contains the entire model satisfying
the root of the tableau. In the remainder of the section, we are presenting a
more efficient algorithm that does not require the storage of the whole model.
The algorithm is a straightforward adaptation of the one for
$\mathbf{K}\mathsf{biG}_{\mathsf{fb}}$ [6] and is inspired by the decision
algorithm for $\mathbf{K}$ [9, §6.7].

######  Theorem 5.2.

The satisfiability of $\mathbf{K}\mathsf{biG}$ (and hence,
$\mathbf{K}\mathsf{G}^{2}$) is $\mathsf{PSPACE}$-complete.

###### Proof.

We will only prove the membership part. The hardness follows from the
embedding of $\mathbf{K}$ into $\mathbf{K}\mathsf{biG}$.

We show how to use the tableaux for checking the satisfiability of a formula
using polynomial space. We start building a tableau for $w_{0}:\phi=1$. We
begin with the application of propositional rules that do not require
branching. Once no such rule is applicable anymore, we apply propositional
rules with branching. When we have branching in the tableau, we guess one
branch and work with it until no rules are applicable (in which case, the
model is constructed) or until it is closed (after which we guess another
one). At this stage, we need to store only the subformulas of $\phi$ and their
value labels at $w_{0}$.

Once no propositional rule is applicable to the branch, we guess a modal
formula whose decomposition requires the introduction of a new state. Note
that at this stage, all labelled formulas are either variables or have the
form $w_{0}:\heartsuit\chi=\mathsf{v}$ ($\heartsuit\in\\{\Box,\lozenge\\}$).
Thus, $T(w_{0})$ is already formed and $\mathsf{s}_{w_{0}}$ is defined for the
value of every modal formula.

Say, we picked $w_{0}:\Box\chi=\frac{k}{r}$. We apply $\Box^{+}$, create a new
state ($w_{1}$), add $w_{0}\mathsf{R}w_{1}$, and guess the branch. Now, we
apply all modal rules that use $w_{0}\mathsf{R}w_{1}$ as a premise guessing
the branch if needed. From here, we start from beginning with the
propositional rules (first the non-branching and then the branching ones). If
we reach a contradiction, we close the branch. Once again, we need only to
store the subformulas of $\phi$ (now with fewer modalities) and their values
at $w_{1}$. Recall that the depth of the model is $O(|\phi|)$ and that we work
with modal formulas requiring the introduction of a new state one by one.
Hence, we need to store the subformulas of $\phi$ and their values $O(|\phi|)$
times, i.e., we need $O(|\phi|^{2})$ space.

Now, if no rule is applicable and no contradiction is reached, we mark
$w_{0}:\Box\chi=\frac{k}{r}$ as ‘safe’ and _delete all entries of the tableau
below_. After that, we guess another unmarked modal formula that requires an
introduction of a new state and repeat the process. Dealing with the modal
formulas one by one allows for the construction of the model branch by branch.
But again, the length of the _branch of the model_ is $O(|\phi|)$ and we
delete the _branches of the model_ generated by ‘safe’ formulas after having
checked that they do not have contradictions, we need only polynomial space. ∎

##  6 Conclusion

In this paper, we axiomatised crisp modal expansions of the bi-Gödel logic and
the paraconsistent Gödel logic $\mathsf{G}^{2}$ in the bi-modal language with
$\triangle$. We also established their complexity and investigated their
semantical properties. Namely, we showed that (among others) Sahlqvist
formulas and implications of monotone formulas define the same classes of
frames in $\mathbf{K}$, $\mathbf{K}\mathsf{biG}$, and
$\mathbf{K}\mathsf{G}^{2}$. Moreover, we established that Glivenko’s theorem
holds in the $\mathbf{K}\mathsf{biG}$ ($\mathbf{K}\mathsf{G}^{2}$) logic of a
class of frames $\mathbb{F}$ iff $\mathbb{F}$ contains only finitely branching
frames.

In the future work, we plan to further investigate modal logics arising from
$\mathsf{biG}$ and $\mathsf{G}^{2}$. First of all, we plan to axiomatise fuzzy
versions of $\mathbf{K}\mathsf{biG}$ and $\mathbf{K}\mathsf{G}^{2}$. And while
the axiomatisation of $\mathbf{K}\mathsf{biG}^{\mathsf{f}}$ may happen to be
relatively straightforward, it seems to be not the case with
${\mathbf{K}\mathsf{G}^{2}}^{\mathsf{f}}$. Indeed, recall the proof of
proposition 3.10. There, by means of $\mathbf{K}\mathsf{G}^{2}$, we reduced
the $\triangle\Box$ definition of crisp frames to the formula valid in all
frames. This means that the standard definitions of $\Box$ and $\lozenge$ in
${\mathbf{K}\mathsf{G}^{2}}^{\mathsf{f}}$ will produce the logic that _does
not_ extend $\mathbf{K}\mathsf{biG}^{\mathsf{f}}$. We leave its axiomatisation
for the future research.

Secondly, as in $\mathbf{K}\mathsf{G}^{2}$, we treat truth and falsity of
statements independently, it makes sense to have not one but two accessibility
relations on a frame: $R^{+}$ and $R^{-}$ that designate the degree of trust
the agent puts in the assertions and denials given by sources. This also makes
sense in the analysis of statistical evidence: assume that $w$ is some test
that gives many false positives but almost no false negatives, while
$w^{\prime}$ is another test that gives few false positives and many false
negatives. Thus, one would tend to believe in positive results provided by $w$
less in the ones provided by $w^{\prime}$ and vice versa for the negative
results.

The third direction of the further research would be to devise description
logics expanding $\mathsf{G}^{2}$. Description Gödel logics [10, 11, 12] are
useful in the representation of vague or uncertain data which is not possible
in the classical ontologies. In fact [2, 13], Gödel description logics are the
only121212Note that even though, generalised concept inclusion of Łukasiewicz
description logics, and hence, its global entailment is undecidable, the local
entailment still is [30]. decidable fuzzy description logics. On the other
hand, there is a considerable amount of work done on paraconsistent
description logics, i.e., logics whose underlying propositional fragment is
paraconsistent. For example, description logics expanding $\mathsf{N4}$ are
presented in [27], description logics over Belnap–Dunn logics are studied in
[23], and the ones over Priest’s logic of paradox in [32]. Still, to the best
of our knowledge, there is no work done on paraconsistent fuzzy logics which
would enable one to non-trivially reason with data which is both vague and
contradictory.

## References

  * [1] J.P. Aguilera, M. Diéguez, D. Fernández-Duque, and B. McLean.  Time and Gödel: Fuzzy Temporal Reasoning in PSPACE.  In Logic, Language, Information, and Computation, Lecture notes in computer science, pages 18–35. Springer International Publishing, Cham, 2022\.
  * [2] F. Baader and R. Peñaloza.  On the undecidability of fuzzy description logics with GCIs and product t-norm.  In International Symposium on Frontiers of Combining Systems, pages 55–70. Springer, 2011.
  * [3] M. Baaz.  Infinite-valued Gödel logics with $0$-$1$-projections and relativizations.  In Gödel’96: Logical foundations of mathematics, computer science and physics—Kurt Gödel’s legacy, Brno, Czech Republic, August 1996, proceedings, volume 6, pages 23–34. Association for Symbolic Logic, 1996\.
  * [4] G. Bezhanishvili.  Glivenko type theorems for intuitionistic modal logics.  Studia Logica, 67(1):89–109, 2001.
  * [5] M. Bílková, S. Frittella, and D. Kozhemiachenko.  Constraint tableaux for two-dimensional fuzzy logics.  In A. Das and S. Negri, editors, Automated Reasoning with Analytic Tableaux and Related Methods, pages 20–37. Springer International Publishing, 2021.
  * [6] M. Bílková, S. Frittella, and D. Kozhemiachenko.  Paraconsistent Gödel modal logic.  In Automated Reasoning, Lecture notes in computer science, pages 429–448. Springer International Publishing, Cham, 2022.
  * [7] M. Bílková, S. Frittella, D. Kozhemiachenko, and O. Majer.  Qualitative reasoning in a two-layered framework (submitted).  arXiv, 2022.
  * [8] M. Bílková, S. Frittella, O. Majer, and S. Nazari.  Belief based on inconsistent information.  In International Workshop on Dynamic Logic, pages 68–86. Springer, 2020.
  * [9] P. Blackburn, M. de Rijke, and Y. Venema.  Modal logic.  Cambridge tracts in theoretical computer science 53. Cambridge University Press, 4. print. with corr. edition, 2010.
  * [10] F. Bobillo, M. Delgado, J. Gómez-Romero, and U. Straccia.  Fuzzy description logics under Gödel semantics.  International Journal of Approximate Reasoning, 50(3):494–514, March 2009.
  * [11] F. Bobillo, M. Delgado, J. Gómez-Romero, and U. Straccia.  Joining Gödel and Zadeh fuzzy logics in fuzzy description logics.  International Journal of Uncertainty Fuzziness and Knowledge-Based Systems, 20(04):475–508, August 2012.
  * [12] S. Borgwardt, F. Distel, and R. Peñaloza.  Decidable Gödel description logics without the finitely-valued model property.  In Fourteenth International Conference on the Principles of Knowledge Representation and Reasoning, 2014.
  * [13] S. Borgwardt and R. Peñaloza.  Undecidability of fuzzy description logics.  In Thirteenth International Conference on the Principles of Knowledge Representation and Reasoning, pages 232–242, 2012.
  * [14] X. Caicedo, G. Metcalfe, R. Rodríguez, and J. Rogger.  A finite model property for Gödel modal logics.  In International Workshop on Logic, Language, Information, and Computation, pages 226–237. Springer, 2013.
  * [15] X. Caicedo, G. Metcalfe, R. Rodríguez, and J. Rogger.  Decidability of order-based modal logics.  Journal of Computer and System Sciences, 88:53–74, September 2017\.
  * [16] X. Caicedo and R.O. Rodriguez.  Standard Gödel modal logics.  Studia Logica, 94(2):189–214, 2010.
  * [17] X. Caicedo and R.O. Rodríguez.  Bi-modal Gödel logic over [0,1]-valued Kripke frames.  Journal of Logic and Computation, 25(1):37–55, 2015.
  * [18] R. Ertola, F. Esteva, T. Flaminio, L. Godo, and C. Noguera.  Paraconsistency properties in degree-preserving fuzzy logics.  Soft Computing, 19(3):531–546, 2015.
  * [19] V. Glivenko.  Sur quelques points de la logique de M. Brouwer.  Bulletins de la classe des sciences, 15(5):183–188, 1929.
  * [20] R. Grigolia, T. Kiseliova, and V. Odisharia.  Free and projective bimodal symmetric Gödel algebras.  Studia Logica, 104(1):115–143, 2016.
  * [21] S.C. Kleene.  Introduction to metamathematics.  North-Holland, Amsterdam, 1952.
  * [22] H. Leitgeb.  Hype: A system of hyperintensional logic (with an application to semantic paradoxes).  Journal of Philosophical Logic, 48(2):305–405, 2019.
  * [23] Y. Ma, P. Hitzler, and Z. Lin.  Algorithms for paraconsistent reasoning with OWL.  In Lecture Notes in Computer Science, Lecture notes in computer science, pages 399–413. Springer Berlin Heidelberg, Berlin, Heidelberg, 2007\.
  * [24] G.M. Moisil.  Logique modale.  Disquisitiones mathematicae et physicae, 2:3–98, 1942.
  * [25] D. Nelson.  Constructible falsity.  The Journal of Symbolic Logic, 14(1):16–26, 1949.
  * [26] S. Odintsov and H. Wansing.  Routley star and hyperintensionality.  Journal of Philosophical Logic, 50:33–56, 2021.
  * [27] S.P. Odintsov and H. Wansing.  Inconsistency-tolerant description logic: Motivation and basic systems.  In Trends in Logic, pages 301–335. Springer Netherlands, Dordrecht, 2003.
  * [28] H. Ono.  Glivenko theorems revisited.  Annals of Pure and Applied Logic, 161(2):246–250, November 2009\.
  * [29] R.O. Rodriguez and A. Vidal.  Axiomatization of Crisp Gödel Modal Logic.  Studia Logica, 109:367–395, 2021.
  * [30] A. Vidal.  On transitive modal many-valued logics.  Fuzzy Sets and Systems, 407:97–114, March 2021.
  * [31] H. Wansing.  Constructive negation, implication, and co-implication.  Journal of Applied Non-Classical Logics, 18(2–3):341–364, 2008\.
  * [32] X. Zhang, Z. Lin, and K. Wang.  Towards a paradoxical description logic for the semantic web.  In Lecture Notes in Computer Science, Lecture notes in computer science, pages 306–325. Springer Berlin Heidelberg, Berlin, Heidelberg, 2010\.