11institutetext: Departamento de Computación, FCEyN - UBA, Argentina
11email<EMAIL_ADDRESS>
22institutetext: Mathematical Institute, University of Bern, Switzerland
22email<EMAIL_ADDRESS>33institutetext: Artificial Intelligence
Research Institute, IIIA - CSIC, Bellaterra, Spain 33email:
<EMAIL_ADDRESS>
# Simplified Kripke semantics for K45-like Gödel modal logics and its
axiomatic extensions

Ricardo Oscar Rodriguez 11 Olim Frits Tuyt 22 Francesc Esteva 33 Lluís Godo 33

##  0.1 Introduction

Possibilistic logic [9, 10] is a well-known uncertainty logic to reason with
graded (epistemic) beliefs on classical propositions by means of necessity and
possiblity measures. In this setting, epistemic states of an agent are
represented by possibility distributions. If $W$ is a set of classical
evaluations or possible worlds, for a given propositional language, a
normalized possibility distribution on $W$ is a mapping
$\pi:W\mathop{\rightarrow}[0,1]$, with $\sup_{w\in W}\pi(w)=1$. This map $\pi$
ranks interpretations according to its plausibility level: $\pi(w)=0$ means
that $w$ is rejected, $\pi(w)=1$ means that $w$ is fully plausible, while
$\pi(w)<\pi(w^{\prime})$ means that $w^{\prime}$ is more plausible than $w$. A
possibility distribution $\pi$ induces a pair of dual possibility and
necessity measures on propositions, defined respectively as:

$\Pi(\varphi)=\sup\\{\pi(w)\mid w\in W,w(\varphi)=1\\}$

$N(\varphi)=\inf\\{1-\pi(w)\mid w\in W,w(\varphi)=0\\}$

$N(\varphi)$ measures to what degree $\varphi$ can be considered certain given
the given epistemic, while $\Pi(\varphi)$ measures the degree in which
$\varphi$ is plausible or possible. Both measures are dual in the sense that
$\Pi(\varphi)=1-N(\neg\varphi)$, so that the degree of possibility of a
proposition $\varphi$ equates the degree in which $\neg\varphi$ is not
certain. If the normalized condition over possibility distribution is dropped,
then we gain the ability to deal with inconsistency. In [11], a possibility
distribution which satisfies $\sup_{w\in W}\pi(w)<1$ is called sub-normal. In
this case, given a set $W$ of classical interpretations, a degree of
inconsistency can be defined in the following way:

$inc(W)=1-\sup_{w\in W}\pi(w)$

When the normalised possibility distribution $\pi$ is $\\{0,1\\}$-valued, i.e.
when $\pi$ is the characteristic function of a subset $\emptyset\neq
E\subseteq W$, then the structure $\langle W,\pi\rangle$, or better $\langle
W,E\rangle$, can be seen in fact as a K45 frame. Indeed, it is folklore that
modal logic K45, which is sound and complete w.r.t. the class of Kripke frames
$\langle W,R\rangle$ where $R$ is a euclidean and transitive binary relation,
also has a simplified semantics given by the subclass of frames $\langle
W,E\rangle$, where $E$ is a non-empty subset of $W$ (understanding $E$ as its
corresponding binary relation $R_{E}$ defined as $R_{E}(w,w^{\prime})$ iff
$w^{\prime}\in E$).

When we go beyond the classical framework of Boolean algebras of events to
many-valued frameworks, one has to come up with appropriate extensions of the
notion of necessity and possibility measures for many-valued events [8].

In the particular context of Gödel fuzzy logic [14], natural generalizations
that we will consider in this paper are the following. A possibility
distribution is as before a function $\pi\colon W\mathop{\rightarrow}[0,1]$
but now, $W$ is a set of Gödel propositional interpretations that induces the
following generalized possibility and necessity measures over Gödel logic
propositions:

$\Pi(\varphi)=\sup_{w\in W}\\{\min(\pi(w),w(\varphi))\\}$
$N(\varphi)=\inf_{w\in W}\\{\pi(w)\Rightarrow w(\varphi)\\},$

where $\Rightarrow$ is Gödel implication, that is, for each $x,y\in[0,1]$,
$x\Rightarrow y=1$ if $x\leq y$, $x\Rightarrow y=y$, otherwise.111Strictly
speaking, the possibility measure is indeed a generalization of the classical
one, but the necessity measure is not, since $x\Rightarrow 0\neq 1-x$. These
expressions agree with the ones commonly used in many-valued modal Kripke
frames $\langle W,R\rangle$ to respectively evaluate modal formulas
$\Diamond\varphi$ and $\Box\varphi$ (see for example [1] and references
therein) when the $[0,1]$-valued accessibility relation $R:W\times
W\mathop{\rightarrow}[0,1]$ is replaced by a possibility distribution
$\pi:W\mathop{\rightarrow}[0,1]$ as $R(w,w^{\prime})=\pi(w^{\prime})$, for any
$w,w^{\prime}\in W$.

Actually, modal extensions of Gödel fuzzy logic have been studied by Caicedo
and Rodríguez [5], providing sound and complete axiomatizations for different
classes of $[0,1]$-valued Kripke models. These structures are triples
$\mathfrak{M}=\langle W,R,e\rangle$, where $W$ is a set of worlds, $R$ is a
$[0,1]$-valued accessibility relation, as above, and $e:W\times
Var\mathop{\rightarrow}[0,1]$ is such that, for every $w\in W$, $e(w,\cdot)$
is a Gödel $[0,1]$-valued evaluation of propositional variables (more details
in next section) that extends to modal formulas as follows:

$\displaystyle e(w,\Diamond\varphi)$ $\displaystyle=\sup_{w^{\prime}\in
W}\\{\min(R(w,w^{\prime}),e(w^{\prime},\varphi))\\}$ $\displaystyle
e(w,\Box\varphi)$ $\displaystyle=\inf_{w^{\prime}\in
W}\\{R(w,w^{\prime})\Rightarrow e(w^{\prime},\varphi)\\}.$

We will denote by ${\cal K}45(\mathbf{G})$ the class of $[0,1]$-models
$\mathfrak{M}=\langle W,R,e\rangle$ where $R$ satisfies the following many-
valued counterpart of the classical properties:

  * •

Transitivity: $\forall w,w^{\prime},w^{\prime\prime}\in W$,
$\min(R(w,w^{\prime}),R(w^{\prime},w^{\prime\prime}))\leq
R(w,w^{\prime\prime})$

  * •

Euclidean: $\forall w,w^{\prime},w^{\prime\prime}\in W$,
$\min(R(w,w^{\prime}),R(w,w^{\prime\prime}))\leq
R(w^{\prime},w^{\prime\prime})$

In this setting, the class $\Pi\mathcal{G}$ of possibilistic Kripke models
$\langle W,\pi,e\rangle$, where $\pi\colon W\mathop{\rightarrow}[0,1]$ is a
possibility distribution (not necessarily normalized) on the set of worlds
$W$, can be considered as the subclass of ${\cal K}45(\mathbf{G})$ models
$\langle W,R,e\rangle$ where $R$ is independent of the world in its first
argument, in the sense that $R(w,w^{\prime})=\pi(w^{\prime})$. Since
$\Pi\mathcal{G}\subsetneq{\cal K}45(\mathbf{G})$, it follows that the set
$Val({\cal K}45(\mathbf{G}))$ of valid formulas in the class of ${\cal
K}45(\mathbf{G})$ is a subset of the set $Val(\Pi\mathcal{G})$ of valid
formulas in the class $\Pi\mathcal{G}$, i.e. $Val({\cal
K}45(\mathbf{G}))\subseteq Val(\Pi\mathcal{G})$. The interesting question is
therefore whether the converse inclusion $Val(\Pi\mathcal{G})\subseteq
Val({\cal K}45(\mathbf{G}))$ holds, and thus whether the class
$\Pi\mathcal{G}$ provides a simplified possibilistic semantics for the modal
logic $K45(\mathbf{G})$.

In [2] the authors claim to provide a positive answer, not for the class
${\cal K}45(\mathbf{G}))$ models but for the subclass of ${\cal
KD}45(\mathbf{G}))$ models, i.e. those ${\cal K}45(\mathbf{G}))$ models
$\mathfrak{M}=\langle W,R,e\rangle$ further satisfying the many-valued
counterpart of seriality:

  * •

Seriality: $\forall w\in W$, $\sup_{w^{\prime}\in W}R(w,w^{\prime})=1$

Indeed, they prove that the logic $KD45(\mathbf{G})$, complete w.r.t. the
class of ${\cal KD}45(\mathbf{G}))$ models, is also complete w.r.t. the class
$\Pi^{*}\mathcal{G}$ of possibilistic models $\langle W,\pi,e\rangle$, where
$\pi:W\mathop{\rightarrow}[0,1]$ is a normalized possibility distribution on
$W$. Unfortunately, it has to be noted that the completeness proof in [2] has
some flaws. In this paper we provide a correct proof, not only for the
completeness of $KD45(\mathbf{G})$ w.r.t. to its corresponding class of
possibilistic frames, but also for the weaker logic $K45(\mathbf{G})$
accounting for partially inconsistent possibilistic Kripke frames.

This paper is organized as follows: Section 0.2 introduces the main notions
about minimum propositional modal Gödel logic and its relational semantics;
Section 0.3 then formally introduces a calculus for the logic $K45(G)$, some
of its extensions and several of its main theorems; Section 0.4 presents our
simplified possibilistic semantics and the results of completeness; Section
0.5 is devoted to analyze the finite model property for the new semantics;
finally, Section 0.6 provides some conclusions.

##  0.2 Preliminaries on propositional and modal Gödel fuzzy logic

This section is devoted to preliminaries on the Gödel fuzzy logic G. We
present their syntax and semantics, their main logical properties and the
notation we use throughout the article.

The language of Gödel propositional logic $\mathcal{L}(V)$ is built as usual
from a countable set of propositional variables $V$, the constant $\bot$ and
the binary connectives $\land$ (conjunction) and $\mathop{\rightarrow}$
(implication). Further connectives are defined as follows:

$\displaystyle\top$ is $\displaystyle\bot\rightarrow\bot$
$\displaystyle\varphi\vee\psi$ is
$\displaystyle((\varphi\rightarrow\psi)\rightarrow\psi)\wedge((\psi\rightarrow\varphi)\rightarrow\varphi),$
$\displaystyle\lnot\varphi$ is $\displaystyle\varphi\rightarrow\bot,$
$\displaystyle\varphi\equiv\psi$ is
$\displaystyle(\varphi\rightarrow\psi)\wedge(\psi\rightarrow\varphi).$

The following are the axioms of $G$:

(A1) | $(\varphi\rightarrow\psi)\rightarrow((\psi\rightarrow\chi)\rightarrow(\varphi\rightarrow\chi))$
---|---
(A2) | $(\varphi\wedge\psi)\rightarrow\varphi$
(A3) | $(\varphi\wedge\psi)\rightarrow(\psi\wedge\varphi)$
(A4a) | $(\varphi\rightarrow(\psi\rightarrow\chi))\rightarrow((\varphi\wedge\psi)\rightarrow\chi)$
(A4b) | $((\varphi\wedge\psi)\rightarrow\chi)\rightarrow(\varphi\rightarrow(\psi\rightarrow\chi))$
(A6) | $\varphi\mathop{\rightarrow}(\varphi\wedge\varphi)$
(A7) | $((\varphi\rightarrow\psi)\rightarrow\chi)\rightarrow(((\psi\rightarrow\varphi)\rightarrow\chi)\rightarrow\chi)$
(A8) | $\bot\rightarrow\varphi$

The deduction rule of $G$ is modus ponens.

Gödel logic can be obtained in fact as the axiomatic extension of Hájek’s
Basic Fuzzy Logic BL [14] (which is the logic of continuous t-norms and their
residua) by means of the contraction axiom (A6)
$\varphi\mathop{\rightarrow}(\varphi\land\varphi)$. Since the unique
idempotent continuous t-norm is the minimum, this yields that Gödel logic is
strongly complete with respect to its standard fuzzy semantics that interprets
formulas over the structure
$[0,1]_{\mathrm{G}}:=\langle[0,1],\min,\Rightarrow_{\mathrm{G}},0,1\rangle$222Called
standard Gödel algebra., i.e. semantics defined by truth-evaluations $e$ such
that $e(\varphi\land\psi)=\min(e(\varphi),e(\psi))$,
$e(\varphi\mathop{\rightarrow}\psi)=e(\varphi)\Rightarrow_{\mathrm{G}}e(\psi)$
and $e(\bot)=0$.

Gödel logic can also be seen as the axiomatic extension of intuitionistic
propositional logic by the prelinearity axiom
$(\varphi\mathop{\rightarrow}\psi)\lor(\psi\mathop{\rightarrow}\varphi)$. Its
algebraic semantics is therefore given by the variety of prelinear Heyting
algebras, also known as Gödel algebras. In fact, it is sound and complete in
the following stronger sense, see [4].

######  Proposition 0.2.1.

  * i)

If $T\cup\\{\varphi\\}\subseteq\mathcal{L}(X),$ then $T\vdash_{G}\varphi$
implies $\inf v(T)\leq v(\varphi)$ for any valuation $v:X\rightarrow[0,1]$.

  * ii)

If $T$ is countable, and
$T\nvdash_{G}\varphi_{i_{1}}\vee..\vee\varphi_{i_{n}}$ for each finite subset
of a countable family $\\{\varphi_{i}\\}_{i\in I}$ there is an evaluation
$v:\mathcal{L}(X)\rightarrow[0,1]$ such that $v(\theta)=1$ for all $\theta\in
T$ and $v(\varphi_{i})<1$ for all $i\in I$.

We mention in passing that the algebraic semantics of Gödel algebra is is
given by the variety of prelinear Heyting algebras, also known as Gödel
algebras. A Gödel algebra is a structure ${\bf A}=\langle
A,*,\Rightarrow,0,1\rangle$ which is a (bounded, integral, commutative)
residuated lattice satisfying the contraction equation

$x*x=x,$

and pre-linearity equation

$(x\Rightarrow y)\lor(y\Rightarrow x)=1,$

where $x\lor y=((x\Rightarrow y)\Rightarrow y)*((y\Rightarrow x)\Rightarrow
x)$).

Let us consider a modal expansion of Gödel logic with two operators $\Box$ and
$\Diamond$. The set of formulas $\mathcal{L}_{\Box\Diamond}(V)$ is built as
$\mathcal{L}(V)$ (always assuming countability of the set of propositional
variables $V$) but extending the set of operations with two unary symbols
$\Box$ and $\Diamond$. Whenever $V$ is clear from the context we will simply
write $\mathcal{L}_{\Box\Diamond}$.

In the style introduced by Fitting [12, 13] and studied in the works mentioned
in the introduction, we define the Gödel Modal Logic as arising from its
semantic definition. This is given by enriching usual Kripke models with
evaluations over the previous standard algebra, as in [4, 5] and others.
Formally:

######  Definition 0.2.1.

A Gödel-Kripke model is a structure $\langle W,R,e\rangle$ where $W$ is a non-
empty set of so-called worlds, and $R\colon W\times W\rightarrow[0,1]$ and
$e\colon V\times W\rightarrow[0,1]$ are arbitrary mappings.

The evaluation $e$ can be uniquely extended to a map with domain
$W\times\mathcal{L}_{\Box\Diamond}$ in such a way that it is a propositional
Gödel homomorphism (for the propositional connectives) and where the modal
operators are interpreted as infima and suprema, namely:

  * •

$e(v,\bot)\coloneqq 0$,

  * •

$e(v,\varphi\star\psi)\coloneqq e(v,\varphi)\star e(v,\psi)$ for
$\star\in\\{\wedge,\vee,\rightarrow\\}$,

  * •

$e(v,\Box\varphi)\coloneqq\bigwedge_{w\in W}(R(v,w)\rightarrow e(w,\varphi)),$

  * •

$e(v,\Diamond\varphi)\coloneqq\bigvee_{w\in W}(R(v,w)\wedge e(w,\varphi)).$

A formula $\varphi$ is _valid_ in a Gödel-Kripke model $\langle W,R,e\rangle$,
if $e(w,\varphi)=1$ for all $w\in W$. We will denote by $\cal G$ the class of
Gödel Kripke models and will say that a formula $\varphi$ is _$\cal G$
-valid_, written $\models_{\mathcal{G}}\varphi$, if $\varphi$ is valid in all
Gödel Kripke models.

In their paper [5] Caicedo and Rodriguez define the logic $K(\mathbf{G})$ as
the smallest set of formulas containing some axiomatic version of Gödel-Dummet
propositional calculus, that is, Heyting calculus plus the prelinearity law,
and the following additional axioms and rule:

$(K_{\Box})$ | $\Box(\varphi\mathop{\rightarrow}\psi)\mathop{\rightarrow}(\Box\varphi\mathop{\rightarrow}\Box\psi)$ | $(K_{\Diamond})$ | $\Diamond(\varphi\lor\psi)\mathop{\rightarrow}(\Diamond\varphi\lor\Diamond\psi)$
---|---|---|---
$(F_{\Box})$ | $\Box\top$ | $(P)$ | $\Box(\varphi\mathop{\rightarrow}\psi)\mathop{\rightarrow}(\Diamond\varphi\mathop{\rightarrow}\Diamond\psi)$
$(FS2)$ |  $(\Diamond\varphi\mathop{\rightarrow}\Box\psi)\mathop{\rightarrow}\Box(\varphi\mathop{\rightarrow}\psi)$ | $(Nec)$ | from $\varphi$ infer $\Box\varphi$

They denote deduction in this system as $\vdash_{K(\mathbf{G})}$ and they show
the following result:

######  Theorem 0.2.1 ([5, Theorem 3.1]).

Let $\varphi\in\mathcal{L}_{\Box\Diamond}$. Then

$\vdash_{K(\mathbf{G})}\varphi\text{ if and only if
}\models_{\mathcal{G}}\varphi.$

Proofs with assumptions are allowed with the restriction that $(Nec)$ may be
applied only when the premise is a theorem. This restriction allows for the
following convenient reduction (see [4]).

######  Lemma 0.2.1.

Let $ThK(\mathbf{G})$ be the set of theorems of $K(\mathbf{G})$ with no
assumptions, then for any theory $T$ and formula $\varphi$ in
$\mathcal{L}_{\Box\Diamond}:T\vdash_{K(\mathbf{G})}\varphi$ if and only if
$T\cup ThK(G)\vdash_{\mathbf{G}}\varphi$ where $\vdash_{\mathbf{G}}$ denotes
deduction in Gödel fuzzy logic G.

The following are some theorems of $K(\mathbf{G})$, see [5]:

$\begin{array}[]{rlrl}T1.&\lnot\Diamond\theta\leftrightarrow\square\lnot\theta&\\\
T2.&\lnot\lnot\square\theta\rightarrow\square\lnot\lnot\theta&\\\
T3.&\Diamond\lnot\lnot\varphi\rightarrow\lnot\lnot\Diamond\varphi&\\\
T4.&(\square\varphi\rightarrow\Diamond\psi)\vee\square((\varphi\rightarrow\psi)\rightarrow\psi)\\\
T5.&\Diamond(\varphi\mathop{\rightarrow}\psi)\mathop{\rightarrow}(\square\varphi\mathop{\rightarrow}\Diamond\psi)\\\
\end{array}$

The first one is an axiom in Fitting’s systems in [12], the next two were
introduced in [5], the fourth one will be useful in our completeness proof and
is the only one depending on prelinearity. The last is known as the first
connecting axiom given by Fischer Servi. In addition, it is interesting to
notice that the following rule is derivable:

$\begin{array}[]{rl}(Nec_{\Diamond})&\mbox{from
}\varphi\mathop{\rightarrow}\psi\mbox{ infer
}\Diamond\varphi\mathop{\rightarrow}\Diamond\psi\\\ \end{array}$

Indeed, if $\vdash_{K(\mathbf{G})}\varphi\mathop{\rightarrow}\psi$, then
$\vdash_{K(\mathbf{G})}\Box(\varphi\mathop{\rightarrow}\psi)$ by $Nec$, and by
using axiom $(P)$ and modus ponens we get
$\vdash_{K(\mathbf{G})}\Diamond\varphi\mathop{\rightarrow}\Diamond\psi$.

In the next section, we will focus on an extension of $K(\mathbf{G})$ for
which we are able to simplify the Gödel Kripke semantics introduced in this
section.

##  0.3 The logic $K45(\mathbf{G})$

The logic $K45(\mathbf{G})$ is defined by adding to $K(\mathbf{G})$ the
following axioms:

$(4_{\Box})$ |  $\Box\varphi\mathop{\rightarrow}\Box\Box\varphi$ |  $(4_{\Diamond})$ | $\Diamond\Diamond\varphi\mathop{\rightarrow}\Diamond\varphi$
---|---|---|---
$(5_{\Box})$ |  $\Diamond\Box\varphi\mathop{\rightarrow}\Box\varphi$ |  $(5_{\Diamond})$ | $\Diamond\varphi\mathop{\rightarrow}\Box\Diamond\varphi$

We define the logic $KD45(\mathbf{G})$ by adding to $K45(\mathbf{G})$ the
following axiom:

$(D)$ |  $\Diamond\top$ |
---|---|---

and $KT45(\mathbf{G})$ if we add the following axioms to $K45(\mathbf{G})$:

$(T_{\Box})$ |  $\Box\varphi\mathop{\rightarrow}\varphi$ |  $(T_{\Diamond})$ | $\varphi\mathop{\rightarrow}\Diamond\varphi$
---|---|---|---

On the other hand, the following is a theorem of $KD45(\mathbf{G})$:

$\begin{array}[]{rl}(D^{\prime})&\Box\varphi\mathop{\rightarrow}\Diamond\varphi\\\
\end{array}$

Indeed, we can replace $\top$ by $\varphi\mathop{\rightarrow}\varphi$ in Axiom
(D) and then use T5. In fact, (D) and (D’) are interderivable in
$K(\mathbf{G})$, that is, we have both
$\Diamond\top\vdash_{K(\mathbf{G})}\Box\varphi\mathop{\rightarrow}\Diamond\varphi$
and
$\Box\varphi\mathop{\rightarrow}\Diamond\varphi\vdash_{K(\mathbf{G})}\Diamond\top$,
the latter holding by first instantiating (D’) with $\varphi=\top$ and getting
$\Box\top\mathop{\rightarrow}\Diamond\top$, and then using that $\Box\top$ is
an axiom of $K(\mathbf{G})$.

Next we show that in $K45(\mathbf{G})$ some iterated modalities can be
simplified. This is in accordance with our intended simplified semantics for
$K45(\mathbf{G})$ that will be formally introduced in the next section.

######  Proposition 0.3.1.

The logic $K45(\mathbf{G})$ proves the following schemes:

$\begin{array}[]{llll}\hskip
5.69054pt({F}_{\Diamond\Box})&\Diamond\Box\top\leftrightarrow\Diamond\top&\hskip
56.9055pt{(G45)}&{(\Box\varphi\mathop{\rightarrow}\Diamond\psi)\mathop{\rightarrow}\Box(\Box\varphi\mathop{\rightarrow}\Diamond\psi)}\\\
\hskip
5.69054pt({U}_{\Diamond})&\Diamond\Diamond\varphi\leftrightarrow\Diamond\varphi&\hskip
56.9055pt({U}_{\Box})&\square\square\varphi\leftrightarrow\square\varphi\\\
\hskip
5.69054pt(T4_{\Box})&(\Box\varphi\mathop{\rightarrow}\Diamond\Box\varphi)\vee\Box\varphi&\hskip
56.9055pt(T4_{\Diamond})&(\Box\Diamond\varphi\mathop{\rightarrow}\Diamond\varphi)\vee\Box\Diamond\varphi\\\
\hskip
5.69054pt(Sk_{\Diamond})&(\Diamond\top\mathop{\rightarrow}\Diamond\varphi)\leftrightarrow\Box\Diamond\varphi&\hskip
56.9055pt(T4^{\prime}_{\Diamond})&(\Box\Diamond\varphi\mathop{\rightarrow}\Diamond\varphi)\vee(\Diamond\top\mathop{\rightarrow}\Diamond\varphi)\par\end{array}$

  * Proof:

$({F}_{\Diamond\Box})$ is an immediate consequence of $F_{\Box}$ and
$Nec_{\Diamond}$. As for schemes $U_{\Diamond}$ and $U_{\Box}$, axioms
$4_{\Box}$ and $4_{\Diamond}$ give one direction of them. The opposite
directions, together with the rest of schemes, are obtained as follows:

$\begin{array}[]{ll}\text{Proof $(U_{\Diamond})$:}&\text{Proof
$(U_{\Box})$:}\\\\[3.99994pt]
\begin{array}[]{@{}ll@{}}\Diamond\varphi\mathop{\rightarrow}\Box\Diamond\varphi&\text{
axiom }(5_{\Diamond})\\\
\Box(\varphi\mathop{\rightarrow}\Diamond\varphi)&\text{ by }MP\text{ and
}(FS2)\\\ \Diamond\varphi\mathop{\rightarrow}\Diamond\Diamond\varphi&\text{ by
}MP\text{ and
}(P)\end{array}&\begin{array}[]{@{}ll@{}}\Diamond\Box\varphi\mathop{\rightarrow}\Box\varphi&\text{
axiom }(5_{\Box})\\\ \Box(\Box\varphi\mathop{\rightarrow}\varphi)&\text{ by
}MP\text{ and }(FS2)\\\ \Box\Box\varphi\mathop{\rightarrow}\Box\varphi&\text{
by }MP\text{ and }(K_{\Box})\end{array}\\\\[20.00003pt] \mbox{Proof
$(T4_{\Box})$:}&\mbox{Proof $(T4_{\Diamond})$:}\\\
\begin{array}[]{@{}ll@{}}\Box\Box\varphi\mathop{\rightarrow}\Diamond\Box\varphi\vee\Box\Box\varphi&\text{(T4)
with }\Box\varphi\\\
\Box\varphi\mathop{\rightarrow}\Diamond\Box\varphi\vee\Box\varphi&\text{by
}(U_{\Box})\end{array}&\begin{array}[]{@{}ll@{}}(\Box\Diamond\varphi\mathop{\rightarrow}\Diamond\Diamond\varphi)\vee\Box((\Diamond\varphi\mathop{\rightarrow}\Diamond\varphi)\mathop{\rightarrow}\Diamond\varphi)&\text{(T4)}\\\
(\Box\Diamond\varphi\mathop{\rightarrow}\Diamond\Diamond\varphi)\vee\Box(\top\mathop{\rightarrow}\Diamond\varphi)&\text{equiv}\end{array}\\\\[20.00003pt]
\text{Proof $(G45)$:}&\\\\[3.99994pt]
\lx@intercol\begin{array}[]{@{}ll@{}}(\Box\varphi\mathop{\rightarrow}\Diamond\psi)\mathop{\rightarrow}(\Box\varphi\mathop{\rightarrow}\Box\Diamond\psi)&\text{by
applying }(5_{\Diamond})\\\
(\Box\varphi\mathop{\rightarrow}\Box\Diamond\psi)\mathop{\rightarrow}(\Diamond\Box\varphi\mathop{\rightarrow}\Box\Diamond\psi)&\text{by
applying }(5_{\Box})\\\
(\Diamond\Box\varphi\mathop{\rightarrow}\Box\Diamond\psi)\mathop{\rightarrow}\Box(\Box\varphi\mathop{\rightarrow}\Diamond\psi)&\text{by
<EMAIL_ADDRESS>\text{Proof
$(Sk_{\Diamond})$:}&\\\\[3.99994pt]
\lx@intercol\begin{array}[]{@{}ll@{}}\Box(\top\mathop{\rightarrow}\Diamond\varphi)\mathop{\rightarrow}(\Diamond\top\mathop{\rightarrow}\Diamond\Diamond\varphi)&\text{by
(P)}\\\
\Box\Diamond\varphi\mathop{\rightarrow}(\Diamond\top\mathop{\rightarrow}\Diamond\varphi)&\text{by
$(U_{\Diamond})$ and equivalences}\\\
(\Diamond\top\mathop{\rightarrow}\Box\Diamond\varphi)\mathop{\rightarrow}\Box(\top\mathop{\rightarrow}\Diamond\varphi)&\text{by
}(FS2)\\\
(\Diamond\top\mathop{\rightarrow}\Diamond\varphi)\mathop{\rightarrow}\Box\Diamond\varphi&\text{by
<EMAIL_ADDRESS>\text{Proof
$(T4^{\prime}_{\Diamond})$: using }(T4_{\Diamond})\text{ and
}(Sk_{\Diamond})\end{array}$

$\blacksquare$

Moreover, if we restrict ourselves to formulas starting with $\Box$ or
$\Diamond$ we can prove the following property.

######  Lemma 0.3.1.

Let $X=\\{\Box\theta,\Diamond\theta:\theta\in\mathcal{L}_{\Box,\Diamond}\\}$.
If $\varphi\in X$ then the schemas

$\varphi\mathop{\rightarrow}\Box\varphi\hskip 14.22636pt\mbox{ and }\hskip
14.22636pt\Diamond\varphi\mathop{\rightarrow}\varphi$

are theorems of $K45(\mathbf{G})$.

###### Proof.

We check that $K45(\mathbf{G})$ derives
$\varphi\mathop{\rightarrow}\Box\varphi$ if $\varphi\in X$, the other schema
is similar. In fact, we have two cases: if $\varphi=\Box\psi$, then
$\varphi\mathop{\rightarrow}\Box\varphi$ is in fact one direction of
$(U_{\Box})$; if $\varphi=\Diamond\psi$, then this is axiom $(5_{\Diamond})$.
∎

From now on we will use $ThK45(\mathbf{G})$ to denote the set of theorems of
$K45(\mathbf{G})$. We close this section with the following observation:

######  Lemma 0.3.2.

If $T$ is a finite set of formulas, $T\vdash_{K45(\mathbf{G})}\varphi$ iff
$\vdash_{K45(\mathbf{G})}T^{\land}\mathop{\rightarrow}\varphi$, where
$T^{\land}=\bigwedge\\{\psi\mid\psi\in T\\}$.

  * Proof:

By Lemma 0.2.1, we have $T\vdash_{K45(\mathbf{G})}\varphi$ iff $T\cup
ThK45(\mathbf{G})\vdash_{G}\varphi$. By the deduction theorem of Gödel logic,
the latter is equivalent to
$ThK45(\mathbf{G})\vdash_{G}T^{\land}\mathop{\rightarrow}\varphi$, and by (i)
again, this is equivalent to
$\vdash_{K45(\mathbf{G})}T^{\land}\mathop{\rightarrow}\varphi$. $\blacksquare$

######  Remark 0.3.1.

It is worth noting that for any valuation $v$ such that
$v(ThK45(\mathbf{G}))=1$ there is no formula $\varphi$ such that
$v(\Diamond\top)<v(\nabla\varphi)<1$ with $\nabla\in\\{\Box,\Diamond\\}$
because both formulae
$(\Box\varphi\mathop{\rightarrow}\Diamond\varphi)\vee\Box\varphi$ and
$\Diamond\varphi\mathop{\rightarrow}\Diamond\top$ are in $ThK45(\mathbf{G})$.

##  0.4 Simplified Kripke semantics and completeness

In this section we will show that $K45(\mathbf{G})$ is complete with respect
to a class of simplified Kripke Gödel frames.

######  Definition 0.4.1.

A possibilistic Kripke frame, or $\Pi$-frame, is a structure $\langle
W,\pi\rangle$ where $W$ _is a non-empty set of worlds_ , and
$\pi:W\rightarrow[0,1]$ is a possibility distribution over $W$.

A possibilistic Gödel Kripke model, _$\Pi G$ -model_ for short, is a triple
$\langle W,\pi,e\rangle$ where $\langle W,\pi\rangle$ is a $\Pi$-frame and
$e:W\times Var\mathop{\rightarrow}[0,1]$ provides a Gödel evaluation of
variables in each world. For each $w\in W$, $e(w,-)$ extends to arbitrary
formulas in the usual way for the propositional connectives and for modal
operators in the following way:

$e(w,\Box\varphi):=\inf_{w^{\prime}\in W}\\{\pi(w^{\prime})\Rightarrow
e(w^{\prime},\varphi)\\}$

$e(w,\Diamond\varphi):=\sup_{w^{\prime}\in
W}\\{\min(\pi(w^{\prime}),e(w^{\prime},\varphi))\\}$.

If $\pi$ is normalised, i.e. if $\sup_{w\in W}\pi(w)=1$, then $\langle
W,\pi,e\rangle$ will be called a normalised possibilistic Gödel Kripke model,
or _$\Pi^{*}G$ -model_. A formula $\varphi$ is _valid_ in a $\Pi G$-model
$\langle W,\pi,e\rangle$ if $e(w,\varphi)=1$ for all $w\in W$.

We will denote by $\Pi\cal G$ the class of possibilistic Gödel Kripke models,
and by $\Pi^{*}\cal G$ the subclass of normalised models. We say that a
formula $\varphi$ is _$\Pi\cal G$ -valid_, written
$\models_{\Pi\mathcal{G}}\varphi$, if $\varphi$ is valid in all possibilistic
Gödel Kripke models, and _$\Pi^{*}\cal G$ -valid_, written
$\models_{\Pi^{*}\mathcal{G}}\varphi$, if $\varphi$ is valid in all normalised
possibilistic Gödel Kripke model.

Observe that the evaluation of formulas beginning with a modal operator is in
fact independent from the current world. Also note that the
$e(\cdot,\Box\varphi)$ and $e(\cdot,\Diamond\varphi)$ are in fact
generalisations for Gödel logic propositions of the necessity and possibility
degrees of $\varphi$ introduced in Section 0.1 for classical propositions,
although now they are not dual (with respect to Gödel negation) any longer.

In the rest of this section we are going to show in detail a weak completeness
proof of the logic $K45(\mathbf{G})$ (resp. $KD45(\mathbf{G})$) with respect
to the class $\Pi\mathcal{G}$ (resp. the subclass $\Pi^{*}\mathcal{G}$) of
possibilistic Gödel Kripke models. In fact one can prove a slightly stronger
result, namely completeness for deductions from finite theories.

We start with the case of $K45(\mathbf{G})$. In what follows, for any formula
$\varphi$ we denote by $Sub(\varphi)\subseteq\mathcal{L}_{\square\Diamond}$
the set of subformulas of $\varphi$ and containing the formula $\bot$.
Moreover, let
$X:=\\{\square\theta,\Diamond\theta:\theta\in\mathcal{L}_{\square\Diamond}\\}$
be the set of formulas in $\mathcal{L}_{\square\Diamond}$ beginning with a
modal operator; then $\mathcal{L}_{\square\Diamond}(Var)=\mathcal{L(}Var\cup
X)$. That is, any formula in $\mathcal{L}_{\square\Diamond}(Var)$ may be seen
as a propositional Gödel formula built from the extended set of propositional
variables $Var\cup X$. In addition, for a given formula $\varphi$, let
$\sim_{\varphi}$ be the equivalence relation on $[0,1]^{Var\cup
X}\times[0,1]^{Var\cup X}$ defined as follows:

$u\sim_{\varphi}w\mbox{ iff }\forall\psi\in
Sub(\varphi):u(\Box\psi)=w(\Box\psi)\mbox{ and
}u(\Diamond\psi)=w(\Diamond\psi).$

Now, assume that a formula $\varphi$ is not a theorem of $K45(\mathbf{G})$.
Hence by completeness of Gödel calculus and Lemma 0.2.1, there exists a Gödel
valuation $v$ such that $v(ThK45(\mathbf{G}))=1$ and $v(\varphi)<1$. With the
valuation $v$ now fixed, we follow the usual canonical model construction,
defining a canonical $\Pi G$-model $\mathfrak{M}^{v}_{\varphi}$ in which we
will show $\varphi$ is not valid.

The _canonical model_ __ $\mathfrak{M}^{v}_{\varphi}=\langle
W^{v}_{\varphi},\pi^{v}_{\varphi},e^{v}_{\varphi}\rangle$ is defined as
follows:

  * •

$W^{v}_{\varphi}$ is the set $\\{u\in[0,1]^{Var\cup X}\mid
u\sim_{\varphi}v\mbox{ and }u(ThK45(\mathbf{G}))=1\\}$.

  * •

$\pi^{v}_{\varphi}(u)=\inf_{\psi\in
Sub(\varphi)}\\{\min(v(\Box\psi)\rightarrow u(\psi),u(\psi)\rightarrow
v(\Diamond\psi))\\}.$

  * •

$e^{v}_{\varphi}(u,p)=u(p)$ for any $p\in Var$.

In this context, we call the elements of
$\Delta_{\varphi}:=\\{\square\theta,\Diamond\theta:\theta\in Sub(\varphi)\\}$
the fixed points of the Canonical Model. Note that having
$\nu(ThK45(\mathbf{G}))=1$ does not guarantee that $\nu$ belongs to the
canonical model because it may not take the appropriated values for the fixed
points, i.e. it may be that $u\not\sim_{\varphi}\nu$. However, the next lemma
shows how to, under certain conditions, transform such an evaluation into
another belonging to the canonical model.

######  Lemma 0.4.1.

Let $u\in W^{v}_{\varphi}$ and let $\nu:{Var\cup X}\mathop{\rightarrow}[0,1]$
be a Gödel valuation. Define $\delta=\max\\{u(\lambda):\nu(\lambda)<1\mbox{
and }\lambda\in\Delta_{\varphi}\\}$ and
$\beta=\min\\{u(\lambda):\nu(\lambda)=1\mbox{ and
}\lambda\in\Delta_{\varphi}\\}$. If $\nu$ satisfies the following conditions:

a.

$\nu(ThK45(\mathbf{G}))=1$.

b.

For all $\lambda\in X$, we have $u(\lambda)>\delta\Rightarrow\nu(\lambda)=1$.

c.

For any $\psi,\phi\in\\{\lambda:u(\lambda)\leq\delta\mbox{ and }\lambda\in
X\\}$: $u(\psi)<u(\phi)$ implies $\nu(\psi)<\nu(\phi)$.

d.

For any $\psi,\phi\in\Delta_{\varphi}:u(\psi)\leq u(\phi)$ implies
$\nu(\psi)\leq\nu(\phi)$.

then, there exists a Gödel valuation $w\in W^{v}_{\varphi}$ such that for any
$\varepsilon>0$ with $\delta+\varepsilon<\beta$, and for any formulae $\psi$
and $\phi$, the following conditions hold:

  1. 1.

$\nu(\psi)=1$ implies $w(\psi)\geq\delta+\varepsilon$.

  2. 2.

$\nu(\psi)<1$ implies $w(\psi)<\delta+\varepsilon$.

  3. 3.

$1\neq\nu(\psi)\leq\nu(\phi)$ implies $w(\psi)\leq w(\phi)$.

  4. 4.

$\nu(\psi)<\nu(\phi)$ implies $w(\psi)<w(\phi)$.

  * Proof:

First of all, notice that if $\nu$ satisfies the conditions c and d, then
necessarily $\delta<\beta$. Indeed, suppose $\delta\geq\beta$. Then there are
at least two formulas $\theta_{1}$ and $\theta_{2}$ in $\Delta_{\varphi}$ such
that $\nu(\theta_{1})<1$, $\nu(\theta_{2})=1$ and $\delta\geq
u(\theta_{1})\geq u(\theta_{2})\geq\beta$. Note that the case
$u(\theta_{1})>u(\theta_{2})$ is not possible because it would violate
condition c, and the case $u(\theta_{1})=u(\theta_{2})$ is also imposible
because it would then violate condition d.

Let
$B=\\{\nu(\lambda):\lambda\in\Delta_{\varphi},\nu(\lambda)<1\\}\cup\\{0\\}=\\{b_{0}=0<b_{1}<\ldots<b_{N}\\}$.
Obviously, $b_{N}<1$. For each $0\leq i\leq N$, pick
$\lambda_{i}\in\Delta_{\varphi}$ such that $\nu(\lambda_{i})=b_{i}$. Define
now a continuous strictly function
$g:[0,1]\mapsto[0,\delta+\varepsilon)\cup\\{1\\}$ such that

$g(1)=1$

$g(b_{i})=u(\lambda_{i})$ for every $0\leq i\leq N$

$g[(b_{N},1)]=(\delta,\delta+\varepsilon)$

Notice that $\delta=g(b_{N})$. In addition, define another continuous strictly
increasing function $h:[0,1]\mapsto[\delta+\varepsilon,1]$ such that

$h(0)=\delta+\varepsilon$

$h[(0,\beta)]=(\delta+\varepsilon,\beta)$

$h(x)=x$, for $x\in[\beta,1]$

Then we define the valuation $w:Var\cup X\mathop{\rightarrow}[0,1]$ as
follows:

$w(p)=\left\\{\begin{array}[]{ll}g(\nu(p)),&\mbox{if }\nu(p)<1,\\\
h(u(p)),&\mbox{if }\nu(p)=1.\end{array}\right.$

Next step is to prove that $w$ satisfies the required Properties 1–4. And we
are going to prove it by induction on the maximum of the complexity of both
formulae $\psi,\phi$.

First, we consider the base case when both $\psi$ and $\phi$ belong to
$Var\cup X$. Then

  1. 1.

By definition of $w$, $\nu(\psi)=1$ implies
$w(\psi)=h(u(\psi))\geq\delta+\varepsilon$. The same happens for $\phi$.

  2. 2.

By definition of $w$, $\nu(\psi)<1$ implies
$w(\psi)=g(\nu(\psi))<\delta+\varepsilon$. The same happens for $\phi$.

  3. 3.

Suppose $1\neq\nu(\psi)\leq\nu(\phi)$. Since $\nu(\psi)<1$, by definition of
$w$, we have $w(\psi)=g(\nu(\psi))<\delta+\varepsilon$. Now, we analyse
different cases. If $\nu(\phi)<1$ then $w(\phi)=g(\nu(\phi))\geq
g(\nu(\psi))=w(\psi)$ because $g$ is strictly increasing. Otherwise, If
$\nu(\phi)=1$ then
$w(\phi)=h(u(\phi))\geq\delta+\varepsilon>w(\psi)=g(\nu(\psi))$.

  4. 4.

Suppose $\nu(\psi)<\nu(\phi)$. In this case, the proof is similar to the
previous one. If $\nu(\psi)<1$ and $\nu(\phi)=1$ then
$w(\phi)=h(u(\phi))\geq\delta+\varepsilon>g(\nu(\psi))=w(\psi)$. On the
contrary, if both $\nu(\psi)<1$ and $\nu(\phi)<1$ then
$w(\phi)=g(\nu(\phi))>g(\nu(\psi))=w(\psi)$ because $g$ is strictly
increasing. This case will become important when we try to prove that $w$
satisfies the axioms of $K45(\mathbf{G})$.

In fact, in the case both formulae $\psi$ and $\phi$ belong to $Var\cup X$ we
can prove that two further conditions hold:

  1. 5.

If $\nu(\psi)=\nu(\phi)=1$ and $u(\psi)\leq u(\phi)$ then $w(\psi)\leq
w(\phi)$.

  2. 6.

If $\nu(\psi)=\nu(\phi)=1$ and $u(\psi)<u(\phi)$ then $w(\psi)<w(\phi)$.

Indeed, by definition of $w$, we have $w(\psi)=h(u(\psi))$ and
$w(\phi)=h(u(\phi))$, and since $h$ is strictly increasing, $u(\psi)\leq
u(\phi)$ (resp. $u(\psi)<u(\phi)$) implies $h(u(\psi))\leq h(u(\phi))$ (resp.
$h(u(\psi))<h(u(\phi))$), as desired. These properties will become important
when proving that $w$ satisfies the axioms of $K45(\mathbf{G})$.

Now, we consider the inductive step.

Claim: Induction hypothesis (IH): if Properties 1–4 are satisfied by formulas
with complexity at most $n$, then these properties also hold for formulae with
complexity at most $n+1$.

The proof of this claim is quite technical and it is moved to the appendix.

Finally, we prove that $w\in W^{v}_{\varphi}$, i.e. we prove that both
$w\sim_{\varphi}v$ and $w(ThK45({\cal G}))=1$.

  * (i)

By definition, $w\sim_{\varphi}v$ iff $w(\Box\phi)=v(\Box\phi)$ and
$w(\Diamond\phi)=v(\Diamond\phi)$ for all $\phi\in Sub(\varphi)$. Let
$A\in\\{\Box\phi,\Diamond\phi\\}\subseteq\Delta_{\varphi}$. By definition of
$w$, $w(A)=g(\nu(A))$ if $\nu(A)<1$, and $w(A)=h(u(A))$, otherwise. Since
$A\in\Delta_{\varphi}$, if $\nu(A)<1$ then, by construction
($u(A)\leq\delta$), we have $g(\nu(A))=u(A)\leq\delta$, and if $\nu(A)=1$,
again by construction ($(u(A)\geq\beta$), we have $h(u(A))=u(A)$. So, we have
proved that $w\sim_{\varphi}u$, but by hypothesis $u\sim_{\varphi}v$ as well,
thus $w\sim_{\varphi}v$ as well.

  * (ii)

We first prove that all axioms of $K45(\mathbf{G})$ are evaluated to 1 by $w$.
The axioms of $\mathcal{G}$ are evaluated to $1$ by any Gödel valuation. As
for the specific axioms of $K45(\mathbf{G})$ (i.e. axioms
$(4_{\Box}),(4_{\Diamond}),(5_{\Box}),(5_{\Diamond})$), observe that all these
axioms are of the form $\phi\mathop{\rightarrow}\psi$ for some $\phi,\psi\in
X$. Then it is enough to prove that for any $\varphi,\psi\in X$, if
$\nu(\phi\mathop{\rightarrow}\psi)=1$ then
$w(\phi\mathop{\rightarrow}\psi)=1$. Indeed, if
$\nu(\phi\mathop{\rightarrow}\psi)=1$, then $\nu(\phi)\leq\nu(\psi)$ and we
have two possibilities:

    * *

if $1\neq\nu(\phi)\leq\nu(\psi)$, then by Property 3, we have $w(\phi)\leq
w(\psi)$.

    * *

if $\nu(\phi)=\nu(\psi)=1$, then by definition of $w$, $w(\phi)=h(u(\phi))$
and $w(\psi)=h(u(\psi))$. But since $u\in W^{v}_{\varphi}$, we have
$u(\phi\mathop{\rightarrow}\psi)=1$, because we assume that
$\phi\mathop{\rightarrow}\psi\in K45(\mathbf{G})$ with $\phi,\psi\in X$. Thus
$u(\phi)\leq u(\psi)$ and, by Property 5, we know $w(\phi)=h(u(\phi))\leq
h(u(\psi))=w(\psi)$.

Finally, let us consider the axioms of $K(\mathbf{G})$ (Section 2). We have to
prove that $w(\chi)=1$ for each of such axioms $\chi$, knowing by assumption
that $\nu(\chi)=1$. The case of $(F_{\Box})$ is easy since $(F_{\Box})\in X$,
and then, by definition, $w(F_{\Box})=h(u(F_{\Box}))=1$. As for axiom
$(K_{\Box})$, note that, using propositional reasoning, it can be equivalently
expressed first as
$(\Box(\phi\mathop{\rightarrow}\psi)\land\Box\phi)\mathop{\rightarrow}\Box\psi$,
and then as
$(\Box(\phi\mathop{\rightarrow}\psi)\mathop{\rightarrow}\Box\psi)\lor(\Box\phi\mathop{\rightarrow}\Box\psi)$.
Therefore, if $\nu(K_{\Box})=1$, it means either
$\nu(\Box(\phi\mathop{\rightarrow}\psi)\mathop{\rightarrow}\Box\psi)=1$ or
$\nu(\Box\phi\mathop{\rightarrow}\Box\psi)=1$. But these two cases concern
implications of formulas from $X$, and hence we are in the same situation
above as with the specific axioms of $K45(\mathbf{G})$, and hence using the
same reasoning, we can conclude that either
$w(\Box(\phi\mathop{\rightarrow}\psi)\mathop{\rightarrow}\Box\psi)=1$ or
$w(\Box\phi\mathop{\rightarrow}\Box\psi)=1$.

The case of axioms $(K_{\Diamond})$ and $(P)$ can be dealt in an analogous
way, as they can be written as a disjunction of implications of formulas from
$X$. So the case left is that of axiom $(FS2)$,
$(\Diamond\phi\mathop{\rightarrow}\Box\psi)\mathop{\rightarrow}\Box(\phi\mathop{\rightarrow}\psi)$.

By hypothesis, we know $\nu(FS2)=1$, that is
$\nu(\Diamond\phi)\Rightarrow\nu(\Box\psi)\leq\nu(\Box(\phi\mathop{\rightarrow}\psi))$.
According to that, we have to prove $w(FS2)=1$ is as well. Notice that, since
$\psi\mathop{\rightarrow}(\phi\mathop{\rightarrow}\psi)$ is a tautology,
$u(\Box(\psi\mathop{\rightarrow}(\phi\mathop{\rightarrow}\psi)))=\nu(\Box(\psi\mathop{\rightarrow}(\phi\mathop{\rightarrow}\psi)))=1$.
Then, by definition,
$w(\Box(\psi\mathop{\rightarrow}(\phi\mathop{\rightarrow}\psi)))=1$ as well
and because axiom (K) is valid for $w$, we have
$w(\Box\psi\mathop{\rightarrow}\Box(\phi\mathop{\rightarrow}\psi))=1$, i.e.
$w(\Box\psi)\leq w(\Box(\phi\mathop{\rightarrow}\psi))$.
Now, we consider the following cases:

    * *

Case $u(\Diamond\phi)\leq u(\Box\psi)$. Then
$u(\Box(\phi\mathop{\rightarrow}\psi))=1$ which implies
$\nu(\Box(\phi\mathop{\rightarrow}\psi))=1$. Hence, by construction,
$w(\Box(\phi\mathop{\rightarrow}\psi))=h(u(\Box(\phi\mathop{\rightarrow}\psi)))=1$.

    * *

Case $u(\Diamond\phi)>u(\Box\psi)$. Here we distinguish three subcases:

      * ·

$u(\Box\psi)\leq\delta<u(\Diamond\phi)$: by Conditions b and c,
$\nu(\Diamond\phi)=1$ and $\nu(\Box\psi)<1$, respectively. Therefore, by
Property 4, $w(\Box\psi)<w(\Diamond\phi)$ and thus
$w(\Diamond\varphi\mathop{\rightarrow}\Box\psi)=w(\Box\psi)\leq
w(\Box(\phi\mathop{\rightarrow}\psi))$ and hence $w(FS2)=1$.

      * ·

$\delta<u(\Box\psi)<u(\Diamond\phi)$: by Condition b,
$1=\nu(\Diamond\phi)=\nu(\Box\psi)\leq\nu(\Box(\phi\mathop{\rightarrow}\psi))$.
Thus, by construction, $w(FS2)=(h(u(\Diamond\varphi))\Rightarrow
h(u(\Box\psi)))\Rightarrow h(u(\Box(\phi\mathop{\rightarrow}\psi))=1$.

      * ·

$u(\Box\psi)<u(\Diamond\phi)\leq\delta$: by Condition c,
$\nu(\Box\psi)<\nu(\Diamond\phi)$, and by Property 4,
$w(\Box\psi)<w(\Diamond\phi)$, and hence
$w(\Diamond\varphi\mathop{\rightarrow}\Box\psi)=w(\Box\psi)\leq
w(\Box(\phi\mathop{\rightarrow}\psi))$, and hence $w(FS2)=1$.

So far, we have proved that $w(\phi)=1$ if $\phi$ is a $K45(\mathbf{G})$
axiom. To conclude the proof, we need to extend this result to the rest of the
formulas in $ThK45({\mathbf{G}})$. Recall that a formula $\phi$ in the set
$ThK45({\mathbf{G}})$ is either an axiom of $K45(\mathbf{G})$ or $\phi$ can be
proved from the axioms and rules of inference $K45(\mathbf{G})$. In the latter
case, there is non-empty finite sequence of formulae
$\phi_{1},\phi_{2},\dots,\phi_{n}$, with $\phi_{n}=\psi$, and each $\phi_{i}$
is either an axiom or it has been obtained by application of an inference rule
on some of the preceding formulae $\phi_{1},\dots,\phi_{i-1}$. We proceed by
induction on the length $n$ of the sequence. The unique interesting case is
when $\phi_{n}$ is obtained by applying the (Nec) rule to some $\phi_{j}$ with
$1\leq j<n$, i.e. $\phi_{n}=\Box\phi_{j}$. It is clear that $\phi_{j}\in
ThK45({\mathbf{G}})$, and by the inductive hypothesis, $w(\phi_{j})=1$. Of
course, $\Box\phi_{j}\in ThK45({\mathbf{G}})$ as well, and thus
$\nu(\Box\xi)=1$ too. But since $\Box\phi_{j}\in X$, by definition of $w$, we
hace $w(\psi)=w(\Box\phi_{j})=h(u(\Box\phi_{j}))=1$. This finishes the proof
of the lemma. $\blacksquare$

Completeness will follow from the next truth-lemma.

######  Lemma 0.4.2 (Truth-lemma).

$e^{v}_{\varphi}(u,\psi)=u(\psi)$ for any $\psi\in Sub(\varphi)$ and any $u\in
W^{v}_{\varphi}$.

  * Proof:

For simplicity, we will write $W^{c}$, $\pi^{c}$ and $e^{c}$ for
$W^{v}_{\varphi},\pi^{v}_{\varphi}$ and $e^{v}_{\varphi}$, respectively. We
prove the identity by induction on the complexity of the formulas in
$Sub(\varphi)$, considered now as elements of
$\mathcal{L}_{\square\Diamond}(Var)$. For $\bot$ and the propositional
variables in $Sub(\varphi)$ the equation holds by definition. The only non
trivial inductive steps are: $e^{c}(u,\Box\psi)=u(\Box\psi)$ and
$e^{c}(u,\Diamond\psi)=u(\Diamond\psi)$ for $\Box\psi,\Diamond\psi\in
Sub(\varphi).$ By the inductive hypothesis we may assume that
$e^{c}(u^{\prime},\psi)=u^{\prime}(\psi)$ for every $u^{\prime}\in W^{c};$
thus we must prove

$\displaystyle\inf_{u^{\prime}\in W^{c}}\\{\pi^{c}(u^{\prime})\Rightarrow
u^{\prime}(\psi)\\}=u(\Box\psi)$ (1) $\displaystyle\sup_{u^{\prime}\in
W^{c}}\\{\min(\pi^{c}(u^{\prime}),u^{\prime}(\psi))\\}=u(\Diamond\psi)$ (2)

By definition, $\pi^{c}(u^{\prime})\leq(v(\Box\psi)\Rightarrow
u^{\prime}(\psi))$ and $\pi^{c}(u^{\prime})\leq(u^{\prime}(\psi)\Rightarrow
v(\Diamond\psi))$ for any $\psi\in Sub(\varphi)$ and $u^{\prime}\in W;$
therefore, $u(\Box\psi)=v(\Box\psi)\leq(\pi^{c}(u^{\prime})\Rightarrow
u^{\prime}(\psi))$ and $\min(\pi^{c}(u^{\prime}),u^{\prime}(\psi))\leq
v(\Diamond\psi)=u(\Diamond\psi).$ Taking infimum over $u^{\prime}$ in the
first inequality and the supremum in the second we get

$u(\Box\psi)\leq\inf_{u^{\prime}\in W^{c}}\\{\pi^{c}(u^{\prime})\Rightarrow
u^{\prime}(\psi)\\},\ \sup_{u^{\prime}\in
W^{c}}\\{\min(\pi^{c}(u^{\prime}),u^{\prime}(\psi))\\}\leq u(\Diamond\psi).$

Hence, if $u(\Box\psi)=1$ and $u(\Diamond\psi)=0$ we directly obtain (1) and
(2), respectively. Therefore, it only remains to prove the next two claims for
$\Box\psi,\Diamond\psi\in Sub(\varphi)$.

Claim 1. _If $u(\Box\psi)=\alpha<1$ then, for every $\varepsilon>0$, there
exists a valuation $w\in W^{c}$ such that $\pi^{c}(w)>w(\psi)$ and
$w(\psi)<\alpha+\varepsilon$, and thus $(\pi^{c}(w)\Rightarrow
w(\psi))<\alpha+\varepsilon$_.

Claim 2. _If $u(\Diamond\psi)=\alpha>0$ then, for any small enough
$\varepsilon>0,$ there exists a valuation $w^{\prime}\in W^{c}$ such that
$\min(w^{\prime}(\psi),\pi^{c}(w^{\prime}))\geq\alpha-\varepsilon$_.

The proofs of these two claims are rather involved and they can be found in
the appendix. $\blacksquare$

######  Theorem 0.4.1 (Weak completeness $K45(\mathbf{G})$).

For any formula $\varphi$ in $\mathcal{L}_{\square\Diamond}$,
$\models_{\Pi\mathcal{G}}\varphi$ iff $\vdash_{K45(\mathbf{G})}\varphi.$

  * Proof:

One direction is soundness, and it is easy to check that the axioms are valid
in the class $\Pi\mathcal{G}$ of models. As for the other direction, assume
$\not\vdash_{K45(\mathbf{G})}\varphi.$ Then
$ThK45(\mathbf{G})\not\vdash_{G}\varphi$ by Lemma 0.2.1, and thus there is, by
Proposition [4, Proposition 3.1], a Gödel valuation $v:Var\cup
X\rightarrow[0,1]$ such that $v(\varphi)<v(ThK45(\mathbf{G}))=1.$ Then $v$ is
a world of the canonical model $\mathfrak{M}_{\varphi}^{v}$ and by Lemma
0.4.2, $e_{\varphi}^{v}(v,\varphi)=v(\varphi)<1.$ Thus $\not\models_{\Pi\cal
G}\varphi$. $\blacksquare$

In addition, it is also easy to generalize last proof for getting completeness
for deductions from finite theories as it is shown by the next theorem:

######  Theorem 0.4.2 (Finite strong completeness $K45(\mathbf{G})$).

For any finite theory $T$ and formula $\varphi$ in
$\mathcal{L}_{\square\Diamond}$, we have: $T\models_{\Pi\mathcal{G}}\varphi$
iff $T\vdash_{K45(\mathbf{G})}\varphi$.

  * Proof:

The proof is an easy adaptation of the one of weak completeness. We will only
mention the main differences. If $T\not\vdash_{K45(\mathbf{G})}\varphi$, by
completeness of Gödel logic and Lemma 0.3.2, there exists a Gödel valuation
$v$ such that $v(ThK45(\mathbf{G}))=1$, $v(T)=1$ and $v(\varphi)<1$. Now, in
order to build a canonical model, we need to take into account not only $v$
and $\varphi$ but also $T$. To do that we have to follow the very same steps
as before but replacing everywhere the set $Sub(\varphi)$ of subformulas of
$\varphi$ by the larger set $Sub(T,\varphi)$ of subformulas of
$T\cup\\{\varphi\\}$, i.e. $Sub(T,\varphi)=\bigcup_{\psi\in
T\cup\\{\varphi\\}}Sub(\psi)$. Let us denote by
$\mathfrak{M}^{v}_{T,\varphi}=\langle W^{c},\pi^{c},e^{c}\rangle$ the
canonical model built accordingly, where $v\in W^{c}$. Note that there is no
need of any modification in neither Lemma 0.4.1 nor the Truth Lemma 0.4.2
(except for replacing $Sub(\varphi)$ by $Sub(T,\varphi)$ in its statement).
Then the theorem follows by observing that Lemma 0.4.2 guarantees that
$e^{c}(v,\psi)=v(\psi)=1$ for all $\psi\in T$ while
$e^{c}(v,\varphi)=v(\varphi)<1$. Therefore,
$T\not\models_{\Pi\mathcal{G}}\varphi$. $\blacksquare$

Actually, the proofs for weak and finite strong completeness of
$K45(\mathbf{G})$ with respect to the class of simplified possibilistic models
$\Pi\mathcal{G}$ easily generalize to completeness of $KD45(\mathbf{G})$, the
axiomatic extension $K45(\mathbf{G})$ with axiom $D$, with respect to the
class of normalized possibilistic models $\Pi^{*}\mathcal{G}$.

######  Corollary 0.4.1 (Finite strong completeness $KD45(\mathbf{G})$).

For any finite theory $T$ and formula $\varphi$ in
$\mathcal{L}_{\square\Diamond}$, we have:
$T\models_{\Pi^{*}\mathcal{G}}\varphi$ iff
$T\vdash_{KD45(\mathbf{G})}\varphi$.

###### Proof.

We only consider the proof of weak completeness, its extension to a proof of
finite strong completeness can be then devised as in Theorem 0.4.2. Indeed,
the proof only needs small adaptations to the one for the case of
$K45(\mathbf{G})$. To start with, for technical reasons that will become clear
later, we will actually prove that
$\not\vdash_{KD45(\mathbf{G})}\varphi^{\prime}$ implies
$\not\models_{\Pi^{*}\mathcal{G}}\varphi^{\prime}$, where
$\varphi^{\prime}=\Diamond\top\mathop{\rightarrow}\varphi$. Note that since
$\Diamond\top$ is an axiom of $KD45(\mathbf{G})$ and is valid in the class of
frames $\Pi^{*}\mathcal{G}$, the former condition is indeed equivalent to
prove that $\not\vdash_{KD45(\mathbf{G})}\varphi$ implies
$\not\models_{\Pi^{*}\mathcal{G}}\varphi$. Next, in the definition of the set
of worlds $W^{v}_{\varphi^{\prime}}$ of the canonical model
$\mathfrak{M}^{v}_{\varphi^{\prime}}$, we need to replace the condition
$u(ThK45(\mathbf{G}))=1$ by $u(ThKD45(\mathbf{G}))=1$, i.e. we define

$W^{v}_{\varphi^{\prime}}=\\{u\in[0,1]^{Var\cup X}\mid
u\sim_{\varphi^{\prime}}v\mbox{ and }u(ThKD45(\mathbf{G}))=1\\},$

and analogously in the condition $\bf a.$ of Lemma 0.4.1. Then in the proof of
this lemma (item (ii) after the Claim), one has to further check that
$w(\Diamond\top)=1$. Observe that $\Diamond\top$ is provably equivalent to
$\square\top\mathop{\rightarrow}\Diamond\top$, but this formula is of the form
$\phi\mathop{\rightarrow}\psi$ for some $\phi,\psi\in X$, and hence it falls
under the cases already considered in the proof. Thus Lemma 0.4.1 holds, and
the same happens with Lemma 0.4.2, that holds as well without any
modification. Moreover, Lemma 0.4.2 allows us to prove that the canonical
model belongs in fact to the class $\Pi^{*}\mathcal{G}$ of normalized
possibilistic models. Indeed, by (2) it follows that

$\sup_{u^{\prime}\in
W^{v}_{\varphi^{\prime}}}\\{\min(\pi^{c}(u^{\prime}),u^{\prime}(\psi))\\}=u(\Diamond\psi)$

for every $\Diamond\psi\in Sub(\varphi^{\prime})$, and since $\Diamond\top\in
Sub(\varphi^{\prime})$ and $u\in W^{v}_{\varphi^{\prime}}$ (and hence
$u(\Diamond\top)=1$), we finally have

$1=u(\Diamond\top)=\sup_{u^{\prime}\in
W^{v}_{\varphi^{\prime}}}\\{\min(\pi^{c}(u^{\prime}),u^{\prime}(\top))\\}=\sup_{u^{\prime}\in
W^{v}_{\varphi^{\prime}}}\pi^{c}(u^{\prime}),$

in other words, $\pi^{c}$ is normalized and thus
$\mathfrak{M}^{v}_{\varphi^{\prime}}\in\Pi^{*}\mathcal{G}$. In summary, we
have found a model $\mathfrak{M}^{v}_{\varphi^{\prime}}=\langle
W^{v}_{\varphi^{\prime}},\pi^{c},e_{\varphi^{\prime}}^{v}\rangle\in\Pi^{*}\mathcal{G}$
and a world $v\in W^{v}_{\varphi^{\prime}}$ such that
$e_{\varphi^{\prime}}^{v}(v,\varphi^{\prime})=e_{\varphi^{\prime}}^{v}(v,\varphi)<1$,
and therefore $\not\models_{\Pi^{*}\mathcal{G}}\varphi$. ∎

We would like to finish this section by noticing that the same kind of proof
for weak and finite strong completeness for $K45$ can also be easily adapted
for the logic $KT45(\mathbf{G})$, that is in fact equivalent to
$KT5(\mathbf{G})$, since Axiom (4) is derivable in $KT5(\mathbf{G})$. For
that, we need to adapt some details of our original proof. First, we can take
the same definition of the canonical model but considering $ThKT5(\mathbf{G})$
instead of $ThK45(\mathbf{G})$. Next, we follow with Lemma 0.4.1 where we
change condition a. by $\nu(ThKT5(\mathbf{G}))=1$. It is easy to check that
the same proof goes through except that we need to prove now that
$w(\Box\varphi\mathop{\rightarrow}\varphi)=w(\varphi\mathop{\rightarrow}\Diamond\varphi)=1$.
But again this is easy to be verified, and the rest of the proof is working
well. Then, we are are able to prove the following:

######  Theorem 0.4.3 (Weak completeness $KT45(\mathbf{G})$).

For any formula $\varphi$ in $\mathcal{L}_{\square\Diamond}$:

$\models_{\Pi^{5}\mathcal{G}}\varphi\mbox{ iff
}\vdash_{KT5(\mathbf{G})}\varphi$

where $\Pi^{5}\mathcal{G}$ is the class of possibilistic frames $(W,\pi)$ that
validate axioms $(T_{\Box})$ and $(T_{\Diamond})$. However this result is not
new, since it turns out that $(W,\pi)$ validates $(T_{\Box})$ and
$(T_{\Diamond})$ iff $\pi$ is such that $\pi(w)=1$ for every $w\in W$. In
other words, $\Pi^{5}\mathcal{G}$ is in fact the class of universal models,
the simplified semantics for $S5(\mathbf{G})$, a result that is well-known in
the literature [7].

##  0.5 Decidability

So far, we have shown that $Val(\Pi{\mathcal{G}})=ThK45(\mathbf{G})$, i.e. the
set of valid formulas in $\Pi\mathcal{G}$, the class of all $\Pi G$-frames,
coincides with the set of theorems of the logic $K45(\mathbf{G})$, or in other
words, the logic $K45(\mathbf{G})$ is sound and complete with respect to $\Pi
G$-frames. It is natural to ask whether the logic $K45(\mathbf{G})$ is
decidable. Unfortunately, it is easy to check that under the possibilistic
semantics the logic $K45(\mathbf{G})$ does not satisfy the finite model
property. Indeed, consider the formula

$\square\lnot\lnot p\rightarrow\lnot\lnot\square p$

where $p$ is a propositional variable. This formula is not valid in the model
$\mathfrak{M}=\langle\mathbb{N},\pi,e\rangle,$ where for all $n\in\mathbb{N}$,

$\pi(n)=1\mbox{ and }e(p,n)=\tfrac{1}{n+1}.$

Then, for all $n\in\mathbb{N}$ we have:

$e(\lnot\lnot p,n)=(\frac{1}{n+1}\Rightarrow 0)\Rightarrow 0=1,$

$e(\Box p,n)=\inf_{n\in\mathbb{N}}\\{\pi(n)\Rightarrow
e(p,n)\\}=\inf_{n\in\mathbb{N}}\\{1{\Rightarrow}\frac{1}{n+1}\\}=0,$
$e(\Box\neg\neg p,n)=\inf_{n\in\mathbb{N}}\\{\pi(n)\Rightarrow e(\neg\neg
p,n)\\}=\inf_{n\in\mathbb{N}}\\{1{\Rightarrow}1\\}=1,$

and hence $e(\square\lnot\lnot p\rightarrow\lnot\lnot\square p,n)=0$. However,
$\Box\lnot\lnot p\rightarrow\lnot\lnot\Box p$ is valid in any $\Pi G$-model
$\langle W,\pi,e\rangle$ where $W$ is finite.

Nevertheless, in [6], an alternative semantics was provided for
$K(\mathbf{G})$ which admits the finite model property. In this section, we
are going to adapt that semantics in order to obtain an equivalent class of
$\Pi G$-models. For that, we are going to use the same strategy used in [6],
i.e. by limiting the truth-values of modal formulae to a finite number of
possibilities. According to this idea, we propose the following adaptation of
the original semantics given in [6].

######  Definition 0.5.1.

A ${\Pi GF}$-model is a quadruple $\mathfrak{M}=\langle W,\pi,T,e\rangle$,
where $\langle W,\pi,e\rangle$ is a $\Pi G$-model and
$T\in\mathcal{P}_{<\omega}(\left[0,1\right])$ is a finite set of truth values
satisfying $\\{0,1\\}\subseteq T\subseteq[0,1]$. The valuation $e$ is extended
to formulas using the same clauses for non-modal connectives as for $\Pi
G$-models, and using the following revised clauses for modal connectives:

$\displaystyle e(\Box\varphi,x)$ $\displaystyle=$
$\displaystyle\max\left\\{r\in T:r\leq\inf_{y\in W}\\{\pi(y){\Rightarrow}\
e(\varphi,y)\\}\right\\}$ $\displaystyle e(\Diamond\varphi,x)$
$\displaystyle=$ $\displaystyle\min\left\\{r\in T:r\geq\sup_{y\in
W}\\{\min(\pi(y),e(\varphi,y))\\}\right\\}.$

A formula $\varphi$ is said to be _valid_ in $\mathfrak{M}$ if
$e(\varphi,x)=1$ for all $x\in W$. We will denote by $\Pi\mathcal{GF}$ the
class of all $\Pi GF$-models.

Notice that now the formula $\varphi=\Box\neg\neg
p\mathop{\rightarrow}\neg\neg\Box p$ has a finite $\Pi GF$-counter-model.
Indeed, consider the $\Pi GF$-model $\mathfrak{M}_{0}=\langle
W,\pi,T,e\rangle$ with $W=\\{a\\}$, $\pi(a)=1$, $T=\\{0,1\\}$, and such that
$e(p,a)=\frac{1}{2}$. Then we have:

  * •

$e(\neg p,a)=0$, $\pi(a)\Rightarrow e(\neg\neg p,a)=1$, and so $e(\Box\neg\neg
p,a)=1$.

  * •

Further, $e(\Box p,a)=0$ (since $\pi(a){\Rightarrow}\ e(p,a)=\frac{1}{2}$, and
$0$ is the next smallest element of $T$);

  * •

Hence, $e(\neg\Box p,a)=1$ and $e(\neg\neg\Box p,a)=0$.

  * •

Therefore, $1=e(\Box\neg\neg p,a)>e(\neg\neg\Box p,a)=0$ and $\Box\neg\neg
p\mathop{\rightarrow}\neg\neg\Box p$ is not valid in $\mathfrak{M}_{0}$.

Next, we are going to prove that both semantics characterize the same logic.
First we need the following lemmas to prove the main result.

######  Lemma 0.5.1.

Let $\mathfrak{M}=\langle W,\pi,T,e\rangle$ be an $\Pi GF$-model. Given an
order-embedding $h\colon[0,1]\mathop{\rightarrow}[0,1]$ satisfying $h(0)=0$ ,
$h(1)=1$, and for any $t\in T:h(t)=t$, consider
$\widehat{\mathfrak{M}}=\langle\widehat{W},\widehat{\pi},\widehat{T},\widehat{e}\rangle$,
with $\widehat{W}=W_{\mathfrak{M}}$, $\widehat{\pi}(x)=h(\pi(x))$,
$\widehat{T}(x)=T(x)$, and $\widehat{e}(p,x)=h(e(p,x))$ for all $x\in W$ and
$p\in\rm{Var}$. Then, for all $\varphi\in\mathcal{L}_{\Box\Diamond}(Var)$ and
$x\in W$:

$\widehat{e}(\varphi,x)=h(e(\varphi,x))$

  * Proof:

It is a special case of part (c) of Lemma 1 in [6]. $\blacksquare$

Now, we provide the key construction of a $\Pi G$-model taking the same truth
values for formulae as a given $\Pi GF$-model.

######  Lemma 0.5.2.

For any $\Pi GF$-model $\mathfrak{M}=\langle W,\pi,T,e\rangle$, there is a
$\Pi G$-model
$\widehat{\mathfrak{M}}=\langle\widehat{W},\widehat{\pi},\widehat{e}\rangle$
with $W\subseteq\widehat{W}$, such that $\widehat{e}(\varphi,x)=e(\varphi,x)$
for all $\varphi\in\mathcal{L}_{\Box\Diamond}(Var)$ and $x\in
W_{\mathfrak{M}}$.

  * Proof:

We proceed similarly to the proof of Lemma 4 in [6]. Given a $\Pi GF$-model
$\mathfrak{M}=\langle W,\pi,T,e\rangle$, we construct its associated $\Pi
G$-model $\widehat{\mathfrak{M}}$ directly by taking infinitely many copies of
$\mathfrak{M}$. Consider $T=\\{\alpha_{1},\ldots,\alpha_{n}\\}$ with
$0=\alpha_{1}<\ldots<\alpha_{n}=1$ and, using Lemma 0.5.1, define a family of
order-embeddings $\\{h_{k}\\}_{k\in\mathbb{Z}^{+}}$ from $[0,1]$ into $[0,1$]
satisfying $h_{k}(0)=0$ and $h_{k}(1)=1$, such that

$h_{k}(\alpha_{i})$ | $=$ | $\alpha_{i}$ | for all $i\leq n-1$ and $k\in\mathbb{Z}^{+}$
---|---|---|---
$h_{k}[(\alpha_{i},\alpha_{i+1})]$ | $=$ | $(\alpha_{i},\min(\alpha_{i}+\frac{1}{k},\alpha_{i+1}))$ | for all $i\leq n-1$ and even $k\in\mathbb{Z}^{+}$
$h_{k}[(\alpha_{i},\alpha_{i+1})]$ | $=$ | $(\max(\alpha_{i},\alpha_{i+1}-\frac{1}{k}),\alpha_{i+1})$ | for all $i\leq n-1$ and odd $k\in\mathbb{Z}^{+}$.

For all $k\in\mathbb{Z}^{+}$, we define a $\Pi G$-model
$\widehat{\mathfrak{M}}_{k}=\langle\widehat{W}_{k},\widehat{\pi}_{k},\widehat{e}_{k}\rangle$
such that each $\widehat{W}_{k}$ is a copy of $W$ with distinct worlds,
$\widehat{\pi}_{k}=h_{k}(\pi)$ and
$\widehat{e}_{k}(\varphi,x^{k})=h_{k}(e(\varphi,x))$ for each copy $x^{k}$ of
$x\in W$ and $\varphi\in\mathcal{L}_{\Box\Diamond}(Var)$. We also let
$\widehat{W}_{0}=W$, $\widehat{\pi}_{0}=\pi$ and $\widehat{e}_{0}=e$. Then
$\widehat{\mathfrak{M}}=\langle\widehat{W},\widehat{\pi},\widehat{e}\rangle$
where

$\widehat{W}=\bigcup_{k\in\mathbb{N}}\widehat{W}_{k}\qquad{\rm and}\ \text{
for
}\widehat{x}\in\widehat{W}_{k}:\qquad\widehat{\pi}(\widehat{x})=\widehat{\pi}_{k}(\widehat{x})\qquad;\qquad\widehat{e}(p,\widehat{x})=\widehat{e}_{k}(p,\widehat{x}).$

Now, It then suffices to prove that $\widehat{e}(\varphi,x)=e(\varphi,x)$ for
all $\varphi\in\mathcal{L}_{\Box\Diamond}(Var)$ and $x\in W$, proceeding by an
induction on $\ell(\varphi)$. The base case $\ell(\varphi)=1$ follows directly
from the definition of $\widehat{e}$. For the inductive step, the cases for
the non-modal connectives follow easily using the induction hypothesis. Let us
just consider the case $\varphi=\Box\psi$, the case $\varphi=\Diamond\psi$
being very similar. There are two possibilities. Suppose first that

$e(\Box\psi,x)=\max\\{r\in T:r\leq\inf\\{\pi(y)\Rightarrow e(\psi,y):y\in
W\\}\\}=1.$

That means for all $y\in W\ :\ \pi(y)\leq e(\psi,y)$ and hence, for all
$k\in\mathbb{Z}^{+}$ and $\widehat{y}\in\widehat{W}$:
$h_{k}(\pi(y))=\widehat{\pi}_{k}({y}^{k})=\widehat{\pi}(\widehat{y})\leq
h_{k}(e(\psi,y))=\widehat{e}_{k}(\psi,y^{k})=\widehat{e}(\psi,\widehat{y})$.
It follows that

$\widehat{e}(\Box\psi,\widehat{x})=\inf\\{\widehat{\pi}(\widehat{y})\Rightarrow\widehat{e}(\psi,\widehat{y}):\widehat{y}\in\widehat{W}\\}=1=e(\Box\psi,x).$

Now suppose that $e(\Box\psi,x)=\alpha_{i}<1$ for some $i\leq m-1$. Then
$\pi(z)\Rightarrow e(\psi,z)\geq\alpha_{i}$ for all $z\in W$, and thus,
$(\star)$,
$\widehat{\pi}(\widehat{z})\Rightarrow\widehat{e}(\psi,\widehat{z})\geq\alpha_{i}$
for all $\widehat{z}\in\widehat{W}$, by construction using the order-
embeddings $\\{h_{k}\\}_{k\in\mathbb{Z}^{+}}$.

There are two subcases. First, suppose that there is at least one $y\in W$
such that $\pi(y)\Rightarrow e(\psi,y)=\alpha_{i}$; call it $y_{0}$. This
means that $\pi(y_{0})>e(\psi,y_{0})=\alpha_{i}$ and for all
$k\in\mathbb{Z}^{+}$,
$\widehat{e}(\psi,\widehat{y}_{0})=\widehat{e}_{k}(\psi,{y}_{0}^{k})=h_{k}(e(\psi,y_{0}))=h_{k}(\alpha_{i})=\alpha_{i}$.
Since $\pi(y_{0})>\alpha_{i}$, also for all $k\in\mathbb{Z}^{+}$,
$\widehat{\pi}(\widehat{y}_{0})=\widehat{\pi}_{k}({y}_{0}^{k})=h_{k}(\pi(y_{0}))>\alpha_{i}=\widehat{e}(\psi,\widehat{y}_{0})$,
and hence, using $(\star)$,

$\widehat{e}(\Box\psi,\widehat{x})=\inf\\{\widehat{\pi}(\widehat{z})\Rightarrow\widehat{e}(\psi,\widehat{z}):\widehat{z}\in\widehat{W}\\}=\alpha_{i}=e(\Box\psi,x).$

Now suppose that $\pi(y)\Rightarrow e(\psi,y)>\alpha_{i}$ for all $y\in W$.
Since $e(\Box\psi,x)=\max\\{r\in T:r\leq\inf\\{\pi(y)\Rightarrow
e(\psi,y):y\in W\\}\\}=\alpha_{i}$, there is at least one $y\in W$ such that
$\pi(y)\Rightarrow e(\psi,y)\in(\alpha_{i},\alpha_{i+1})$; call it $y_{0}$.
Then, by construction, for any $\epsilon>0$ there is a $k\in\mathbb{Z}^{+}$
such that
$\widehat{\pi}({y}^{k}_{0})\Rightarrow\widehat{e}(\psi,{y}^{k}_{0})\in(\alpha_{i},\alpha_{i}+\epsilon)$.
Using $(\star)$, this ensures that

$\widehat{e}(\Box\psi,\widehat{x})=\inf\\{\widehat{\pi}(z)\Rightarrow\widehat{e}(\psi,z):z\in\widehat{W}\\}=\alpha_{i}=e(\Box\psi,x)$.

$\blacksquare$

As an immediate consequence of Lemma 0.5.2, we have the next corollary.

######  Corollary 0.5.1.

$Val(\Pi{\mathcal{G}})\subseteq Val(\Pi{\mathcal{GF}})$.

The next lemma paves the way to prove in Theorem 0.5.1 that the logic
$K45(\mathbf{G})$ has the finite model property and offers a bound on the
complexity. We call a set $\Sigma\subseteq\mathcal{L}_{\Box\Diamond}(Var)$ a
_fragment_ if it is closed under subformulas.

######  Lemma 0.5.3.

Let $\mathrm{\Sigma}\subseteq\mathcal{L}_{\Box\Diamond}(Var)$ be a finite
fragment. Then, for any $\Pi G$-model $\mathfrak{M}$, there is a finite $\Pi
GF$-model $\widehat{\mathfrak{M}}$ with $\widehat{W}\subseteq W$, such that
$\widehat{e}(\varphi,x)=e(\varphi,x)$ for all $\varphi\in\mathrm{\Sigma}$ and
$x\in\widehat{W}$. Moreover, $|\widehat{W}|+|\widehat{T}|\leq
2|\mathrm{\Sigma}|$.

  * Proof:

Let $\mathrm{\Sigma}\subseteq\mathcal{L}_{\Box\Diamond}(Var)$ be a finite
fragment, $\mathfrak{M}=\langle W,\pi,e\rangle$ a $\Pi G$-model. First, define
$\mathrm{\Sigma}_{\Box}$ as the set of all box-formulas in $\mathrm{\Sigma}$,
$\mathrm{\Sigma}_{\Diamond}$ as the set of all diamond-formulas in
$\mathrm{\Sigma}$, and $\mathrm{\Sigma}_{\rm{Var}}$ as the set of all
variables in $\mathrm{\Sigma}$. Let us also define
$e_{x}[\mathrm{\Delta}]=\\{e(\varphi,x):\varphi\in\mathrm{\Delta}\\}$ for any
$x\in W$ and $\mathrm{\Delta}\subseteq\mathcal{L}_{\Box\Diamond}(Var)$. In
addition, let
$e_{x}[\mathrm{\Sigma}_{\Box}\cup\mathrm{\Sigma}_{\Diamond}]\cup\\{0,1\\}=\\{\alpha_{1},\ldots,\alpha_{n}\\}$
with $0=\alpha_{1}<\ldots<\alpha_{n}=1$.

Next, we choose a finite number of $y\in W$. For each
$\Box\psi\in\mathrm{\Sigma}_{\Box}$ such that $e(\Box\psi,x)=\alpha_{i}<1$,
choose a $y=y_{\Box\psi}\in W$ such that $e(\psi,y_{\Box\psi})<\alpha_{i+1}$,
and for each $\Diamond\psi\in\mathrm{\Sigma}_{\Diamond}$, such that
$e(\Diamond\psi,x)=\alpha_{i}>0$, choose a $y=y_{\Diamond\psi}\in W$ such that
$e(\psi,y_{\Diamond\psi})>\alpha_{i-1}$. Then let
$\widehat{W}=\\{x\\}\cup\\{y_{\Box\psi}\in
W:\Box\psi\in\mathrm{\Sigma}_{\Box}\\}\cup\\{y_{\Diamond\psi}\in
W:\Diamond\psi\in\mathrm{\Sigma}_{\Diamond}\\}$. Clearly $\widehat{W}\subseteq
W$ is finite. We define
$\widehat{\mathfrak{M}}=\langle\widehat{W},\widehat{\pi},\widehat{T},\widehat{e}\rangle$
where
$\widehat{T}=e_{x}[\mathrm{\Sigma}_{\Box}\cup\mathrm{\Sigma}_{\Diamond}]\cup\\{0,1\\}$,
and both $\widehat{\pi}$ and $\widehat{e}$ are equal to $\pi$ and $e$
restricted to $\widehat{W}$, respectively. It then follows by induction on
$\ell(\varphi)$ that $\widehat{e}(\varphi,x)=e(\varphi,x)$ for all
$x\in\widehat{W}$ and $\varphi\in\mathrm{\Sigma}$. The base case follows from
the definition of $\widehat{e}$. For the inductive step, let
$\varphi\in\mathrm{\Sigma}$ be of the form $\varphi=\Box\psi$ (the non-modal
cases follow directly, using the induction hypothesis). We need to consider
the same two cases it was considered in previous Lemma 0.5.2. First, note that
always it is true that:

$\inf\\{\pi(y)\Rightarrow e(\psi,y):{y\in
W}\\}\leq\inf\\{\widehat{\pi}(\widehat{y})\Rightarrow\widehat{e}(\psi,\widehat{y}):\widehat{y}\in\widehat{W}\\}$

because of $\widehat{W}\subseteq W$. Now suppose that $1=e(\Box\psi,x)$. Then,
because $1\in\widehat{T}$,

$\displaystyle 1=e(\Box\psi,x)$ $\displaystyle=\inf\\{\pi(y)\Rightarrow
e(\psi,y):{y\in W}\\}$
$\displaystyle\leq\inf\\{\widehat{\pi}(\widehat{y})\Rightarrow\widehat{e}(\psi,\widehat{y}):\widehat{y}\in\widehat{W}\\}$
$\displaystyle\leq\max\\{r\in\widehat{T}:r\leq\inf\\{\widehat{\pi}(\widehat{y})\Rightarrow\widehat{e}(\psi,\widehat{y}):\widehat{y}\in\widehat{W}\\}\\}$
$\displaystyle=\widehat{e}(\Box\psi,x).$

For the second case, $e(\Box\psi,x)=\inf\\{\pi(y)\Rightarrow e(\psi,y):y\in
W\\}=\alpha_{i}<1$ for some $i\in\\{1,\ldots,n-1\\}$. According to our choise,
there exists a $y_{\Box\psi}\in\widehat{W}$ such that
$\alpha_{i}\leq\widehat{\pi}(y_{\Box\psi})\Rightarrow\widehat{e}(\psi,y_{\Box\psi})<\alpha_{i+1}$.
Hence,

$\alpha_{i}\leq\inf\\{\widehat{\pi}(\widehat{y})\Rightarrow\widehat{e}(\psi,\widehat{y}):\widehat{y}\in\widehat{W}\\}\\}\leq\widehat{\pi}(y_{\Box\psi})\Rightarrow\widehat{e}(\psi,y_{\Box\psi})<\alpha_{i+1}$

Thus

$\widehat{e}(\Box\psi,x)=\max\\{r\in\widehat{T}:r\leq\inf\\{\widehat{\pi}(\widehat{y})\Rightarrow\widehat{e}(\psi,\widehat{y}):\widehat{y}\in\widehat{W}\\}\\}=\alpha_{i}$

The diamond-case case follows similarly to the box-case and is therefore
omitted.

Finally, we note that by the construction of $\widehat{\mathfrak{M}}$,
$|\widehat{W}|\leq|\mathrm{\Sigma}_{\Box}\cup\mathrm{\Sigma}_{\Diamond}|+1\leq|\mathrm{\Sigma}|$
and
$|\widehat{T}|\leq|\mathrm{\Sigma}_{\Box}\cup\mathrm{\Sigma}_{\Diamond}|+2\leq|\mathrm{\Sigma}|$,
and therefore $|\widehat{W}|+|\widehat{T}|\leq 2|\mathrm{\Sigma}|$.

$\blacksquare$

As a direct consequence of the above lemma we have the converse inclusion of
Corollary 0.5.1.

######  Corollary 0.5.2.

$Val(\Pi{\mathcal{GF}})\subseteq Val(\Pi{\mathcal{G}})$.

Finally, we can state the main result of this section.

######  Theorem 0.5.1 (main).

For each $\varphi\in\mathcal{L}_{\Box\Diamond}(Var)$:
$\models_{\mathsf{\Pi\mathcal{G}}}\varphi$ iff $\varphi$ is valid in all
(finite) $\Pi GF$-models $\mathfrak{M}=\langle W,\pi,T,e\rangle$ satisfying
$|W|+|T|\leq 2(\ell(\varphi)+2)$.

As a direct consequence we get the decidability of $K45({\bf G})$.

######  Corollary 0.5.3.

The logic $K45({\bf G})$ is decidable.

Similarly, one can prove that the logic $KD45({\bf G})$ is decidable as well.

######  Corollary 0.5.4.

The logic $KD45({\bf G})$ is decidable.

##  0.6 Conclusions

In this paper we have studied the logic over Gödel fuzzy logic arising from
many-valued Gödel Kripke models with possibilistic semantics, and have shown
that it actually corresponds to a simplified semantics for the logic $K45({\bf
G})$, the extension of Caicedo and Rodriguez’s bi-modal Gödel logic with many-
valued versions of the well-known modal axioms $4$ and $5$. We have also
considered the extension with the axiom $D$, the logic $KD45({\bf G})$, and
have shown to be captured by normalised possibilistic Gödel Kripke models. In
this way, we have obtained many-valued Gödel generalizations of the results
reported by Pietruszczak in [15] about simplified semantics for several
classical modal logics. We have also shown the decidability of those logics.

It is worth noticing that the truth-value of a formula $\Diamond\varphi$ in a
possibilistic Kripke model is indeed a proper generalization of the
possibility measure of $\varphi$ when $\varphi$ is a classical proposition,
however the semantics of $\Box\varphi$ is not. This is due to the fact that
the negation in Gödel logic is not involutive. Therefore, a first open problem
we leave for further research is to consider to extension of the logic
$K45({\bf G})$ with an involutive negation and investigate its possibilistic
semantics. Finally, we would like to study the connection between our
simplified possiblistic semantics and the pseudomonadic algebras proposed in
[3].

### Acknowledgments

Rodriguez acknowledges partial support of Argentinean projects:
PICT-2019-2019-00882, UBA-CyT-20020190100021BA and PIP 112-2015-0100412 CO.
Tuyt is supported by Swiss National Science Foundation (SNF) grant
200021_184693. Esteva and Godo acknowledge partial support by the Spanish
project PID2019-111544GB-C21.

## References

  * [1] F. Bou, F. Esteva, L. Godo, R. Rodríguez. On the Minimum Many-Valued Modal Logic over a Finite Residuated Lattice. Journal of Logic and Computation, vol. 21, issue 5, pp. 739-790, 2011.
  * [2] F. Bou, F. Esteva, L. Godo and R. Rodriguez. Possibilistic semantics for a modal KD45 extension of Gödel fuzzy logic. Proc. of IPMU 2016 (Part II), J.P. Carvalho et al. (eds.), Communications in Computer and Information Science, vol. 611, pp. 123–135, 2016.
  * [3] M. Busaniche, P. Cordero and R. Rodriguez. Pseudo-monadic BL Algebras. Special Issue of Soft Computing Journal (2019) 23:2199–2212. https://doi.org/10.1007/s00500-019-03810-0.
  * [4] X. Caicedo and R. Rodriguez, Standard Gödel modal logics. Studia Logica, Volume 94, No. 2 (2010), 189-214.
  * [5] X. Caicedo and R. Rodriguez, Bi-modal Gödel modal logics. Journal of Logic and Computation, Volume 25-1, pages 37-55, 2015.
  * [6] X. Caicedo, G. Metcalfe, R. Rodriguez and J. Rogger.  A Finite Model Property for Gödel Modal Logics.  In Proc. of WOLLIC 2013, L. Libkin et al. (eds.), Lecture Notes in Computer Science, vol. 8071, pp. 226–237, 2013.
  * [7] X. Caicedo, G. Metcalfe, R. Rodriguez and O. Tuyt  The One-Variable Fragment of Corsi Logic.  In Proc. of WOLLIC 2019, Lecture Notes in Computer Science, vol. 11541, pp. 70–83, 2019.
  * [8] P. Dellunde, L. Godo, E. Marchioni. Extending possibilistic logic over Gödel logic. Int. J. Approx. Reasoning 52(1): 63-75 (2011)
  * [9] D. Dubois, J. Lang, H. Prade. Possibilistic logic, in: Gabbay et al. (Eds.), Handbook of Logic in Artificial Intelligence and Logic Programming, Non monotonic Reasoning and Uncertain Reasoning, vol. 3, Oxford UP, 1994, pp. 439–513.
  * [10] D. Dubois, H. Prade. Possibilistic logic: a retrospective and prospective view. Fuzzy Sets and Systems, 144:3-23, 2004.
  * [11] D. Dubois and H. Prade. Inconsistency management from the standpoint of possibilistic logic. International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems, Vol. 23 (Suppl. 1). pp. 15-30, 2015.
  * [12] M. Fitting. Many-valued modal logics. Fundamenta Informaticae 15 (1991) 325-254.
  * [13] M. Fitting. Many-valued modal logics II, _Fundamenta Informaticae_ , 17 (1992), pp. 55–73.
  * [14] P. Hájek. Metamathematics of Fuzzy Logic. Trends in Logic, 4, Kluwer, 1998.
  * [15] A. Pietruszczak.  Simplified Kripke style semantics for modal logics K45, KB4 and KD45.  Bulletin of the Section of Logic 38, 3/4 (2009), 163–171.

## Appendix

Claim from Lemma 0.4.1. Induction hypothesis (IH): if Properties 1–4 are
satisfied by formulas with complexity at most $n$ then these properties keep
holding for formulae with complexity at most $n+1$.

  * Proof:

This case will become important when we try to prove that $w$ satisfies the
axioms of $K45(\mathbf{G})$.

We consider different cases according to the main operator being either
$\wedge$ or $\mathop{\rightarrow}$. First, we prove Properties 1 and 2, that
involve only one formula:

Case $\psi=\psi_{1}\wedge\psi_{2}$.

    1. 1.

Let $\nu(\psi_{1}\wedge\psi_{2})=1$. Then $\nu(\psi_{1})=\nu(\psi_{2})=1$. In
such a case, from the inductive hypothesis, we conclude that
$w(\psi_{1})\geq\delta+\varepsilon$ and $w(\psi_{2})\geq\delta+\varepsilon$.
Therefore, $w(\psi_{1}\wedge\psi_{2})\geq\delta+\varepsilon$.

    2. 2.

Let $\nu(\psi_{1}\wedge\psi_{2})<1$. Then, without loss of generality, we can
assume that $\nu(\psi_{1}\wedge\psi_{2})=\nu(\psi_{1})\leq\nu(\psi_{2})$. In
the case that $\nu(\psi_{1})<1$, we can apply the inductive hypothesis and
conclude that $w(\psi_{1})<\delta+\varepsilon$ and $w(\psi_{1})\leq
w(\psi_{2})$, according to Properties 2 and 3, respectively. Therefore, we
obtain $w(\psi_{1}\wedge\psi_{2})=w(\psi_{1})<\delta+\varepsilon$.

Case $\psi=\psi_{1}\mathop{\rightarrow}\psi_{2}$.

    1. 1.

Let $\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})=1$. Then
$\nu(\psi_{1})\leq\nu(\psi_{2})$. First, we consider the case
$\nu(\psi_{1})<1$ where we can apply Property 3 by the inductive hypothesis,
obtaining that $w(\psi_{1})\leq w(\psi_{2})$ and, hence,
$w(\psi_{1}\mathop{\rightarrow}\psi_{2})=1\geq\delta+\varepsilon$. Now, we
turn to the case $\nu(\psi_{1})=1=\nu(\psi_{2})$. In this situation, by
applying Property 1 on $\psi_{2}$, we conclude that
$w(\psi_{1}\mathop{\rightarrow}\psi_{2})\geq
w(\psi_{2})\geq\delta+\varepsilon$.

    2. 2.

Let $\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})<1$. Then
$\nu(\psi_{1})>\nu(\psi_{2})$. By inductive hypothesis, by applying Property
4, we have that $w(\psi_{1})>w(\psi_{2})$, and hence
$w(\psi_{1}\mathop{\rightarrow}\psi_{2})=w(\psi_{2})$, but since
$\nu(\psi_{2})<1$, then by Property 2, $w(\psi_{2})<\delta+\varepsilon$.

Next we prove Properties 3 and 4, that involve two formulas. We proceed by
considering the four possible combinations.

Case $\psi=\psi_{1}\wedge\psi_{2}$ and $\phi=\phi_{1}\wedge\phi_{2}$.

In this case the proof is easy because, without loss of generality, we can
assume that $\nu(\psi_{1}\wedge\psi_{2})=\nu(\psi_{1})$ and
$\nu(\phi_{1}\wedge\phi_{2})=\nu(\phi_{1})$.

$3.$

Let $1\neq\nu(\psi_{1}\wedge\psi_{2})\leq\nu(\phi_{1}\wedge\phi_{2})$.
According to our assumption, this means $1\neq\nu(\psi_{1})\leq\nu(\phi_{1})$,
and by applying induction hypothesis we obtain $w(\psi_{1})\leq w(\phi_{1})$
and $w(\psi_{1})<\delta+\varepsilon$. Now, we need to consider two additional
cases:

$a.$

If $\nu(\psi_{2})=1$ then, by IH, $w(\psi_{2})\geq\delta+\varepsilon$. Thus,
we obtain $w(\psi_{1}\wedge\psi_{2})=w(\psi_{1})<\delta+\varepsilon$. In
addition, if $\nu(\phi_{1})<1$ then, by IH (Property 3), $w(\phi_{1})\leq
w(\phi_{2})$ and $w(\psi_{1}\wedge\psi_{2})\leq w(\phi_{1}\wedge\phi_{2})$. On
the contrary, if $\nu(\phi_{1})=1$ then, $\nu(\phi_{2})=1$ and
$w(\phi_{1}\wedge\phi_{2})\geq\delta+\varepsilon>w(\psi_{1}\wedge\psi_{2})$.

$b.$

If $\nu(\psi_{2})<1$ then, by IH on Properties 2 and 3, $w(\psi_{1})\leq
w(\psi_{2})<\delta+\varepsilon$ which implies
$w(\psi_{1})=w(\psi_{1}\wedge\psi_{2})\leq w(\phi_{1})$. The proof of this
case is completed by reproducing the both alternatives when $\nu(\phi_{1})<1$
and $\nu(\phi_{1})=1$, which were analyzed in the previous item.

$4.$

Let $\nu(\psi_{1}\wedge\psi_{2})<\nu(\phi_{1}\wedge\phi_{2})$. Again, this
means $\nu(\psi_{1})<\nu(\phi_{1})$. By IH, we obtain
$w(\psi_{1})<w(\phi_{1})$ and $w(\psi_{1})<\delta+\varepsilon$ (Properties 4
and 2, respectively). The rest of the proof runs as before.

Case $\psi=\psi_{1}\mathop{\rightarrow}\psi_{2}$ and
$\phi=\phi_{1}\wedge\phi_{2}$.

Again, without loss of generality, we can assume that
$\nu(\phi_{1}\wedge\phi_{2})=\nu(\phi_{1})$.

$3.$

Let
$1\neq\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})\leq\nu(\phi_{1}\wedge\phi_{2})$.
Since $\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})<1$, we conclude that
$\nu(\psi_{1})>\nu(\psi_{2})$ and $1\neq\nu(\psi_{2})\leq\nu(\phi_{1})$. By
IH, we know that $w(\psi_{2})\leq w(\phi_{1})$ and $w(\psi_{1})>w(\psi_{2})$.
In addition, if $1\neq\nu(\phi_{1})\leq\nu(\phi_{2})$ then, by IH, we have
$w(\psi_{1}\mathop{\rightarrow}\psi_{2})=w(\psi_{2})\leq
w(\phi_{1})=w(\phi_{1}\wedge\phi_{2})$. On the contrary, if
$\nu(\phi_{1})=1=\nu(\phi_{2})$ then
$w(\phi_{1}\wedge\phi_{2})\geq\delta+\varepsilon>w(\psi_{2})=w(\psi_{1}\mathop{\rightarrow}\psi_{2})$.

$4.$

Let $\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})<\nu(\phi_{1}\wedge\phi_{2})$.
As in the previous proof, we can conclude that $\nu(\psi_{1})>\nu(\psi_{2})$
and so by Property 4, $w(\psi_{1})>w(\psi_{2})$, i.e.
$w(\psi_{1}\mathop{\rightarrow}\psi_{2})=w(\psi_{2})$. Moreover, as
$\nu(\psi_{2})<\nu(\phi_{1})$, $w(\psi_{2})<w(\phi_{1})$ again by Property 4.
If $1\neq\nu(\phi_{1})\leq\nu(\phi_{2})$ then, by IH,
$w(\phi_{1})=w(\phi_{1}\wedge\phi_{2})$. On the contrary, if
$\nu(\phi_{1})=1=\nu(\phi_{2})$ then, by IH,
$w(\phi_{1}\wedge\phi_{2})\geq\delta+\varepsilon>w(\psi_{2})=w(\psi_{1}\mathop{\rightarrow}\psi_{2})$.

Case $\psi=\psi_{1}\wedge\psi_{2}$ and
$\phi=\phi_{1}\mathop{\rightarrow}\phi_{2}$.

Again, without loss of generality, we can assume that
$\nu(\psi_{1}\wedge\psi_{2})=\nu(\psi_{1})$.

$3.$

Let
$1\neq\nu(\psi_{1}\wedge\psi_{2})\leq\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})$.
According to our assumption, we know
$\nu(\psi_{1}\wedge\psi_{2})=\nu(\psi_{1})<1$. Then, by IH, we obtain
$w(\psi_{1}\wedge\psi_{2})=w(\psi_{1})<\delta+\varepsilon$. If
$\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})<1$ then
$\nu(\phi_{1})>\nu(\phi_{2})\geq\nu(\psi_{1})$ and, by IH, we know
$w(\phi_{1}\mathop{\rightarrow}\phi_{2})=w(\phi_{2})\geq
w(\psi_{1})=w(\psi_{1}\wedge\psi_{2})$. On the contrary,
$\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})=1$ implies
$\nu(\phi_{1})\leq\nu(\phi_{2})$. In this case, if $\nu(\phi_{1})<1$ then, by
IH $w(\phi_{1})\leq w(\phi_{2})$ which implies
$w(\phi_{1}\mathop{\rightarrow}\phi_{2})=1$. If
$\nu(\phi_{1})=1=\nu(\phi_{2})$ then, by IH,
$w(\phi_{1}\mathop{\rightarrow}\phi_{2})\geq
w(\phi_{2})\geq\delta+\varepsilon>w(\psi_{1})=w(\psi_{1}\wedge\psi_{2})$.

$4.$

Let $\nu(\psi_{1}\wedge\psi_{2})<\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})$.
In this case, we can proceed analogously to the previous proofs. For this
reason, we leave to the reader to complete the details.

Case $\psi=\psi_{1}\mathop{\rightarrow}\psi_{2}$ and
$\phi=\phi_{1}\mathop{\rightarrow}\phi_{2}$.

$3.$

Let
$1\neq\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})\leq\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})$.
As $\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})\neq 1$, we conclude
$\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})=\nu(\psi_{2})<1$. In addition, if
$\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})<1$ then
$\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})=\nu(\phi_{2})$. Thus, if the truth
values of both implications are less than one, we have
$1\neq\nu(\psi_{2})\leq\nu(\phi_{2})$. By IH, we know $w(\psi_{2})\leq
w(\phi_{2})$, $w(\psi_{1})>w(\psi_{2})$ and $w(\phi_{1})>w(\phi_{2})$.
Therefore, $w(\psi_{1}\mathop{\rightarrow}\psi_{2})=w(\psi_{2})\leq
w(\phi_{2})=w(\phi_{1}\mathop{\rightarrow}\phi_{2})$. On the contrary, if
$\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})=1$ then
$\nu(\phi_{1}\leq\nu(\phi_{2})$. If $\nu(\phi_{1})<1$ then, by IH,
$w(\phi_{1}\mathop{\rightarrow}\phi_{2})=1$. In the opposite case, if
$\nu(\phi_{1})=1=\nu(\phi_{2})$ then, by IH,
$w(\phi_{1}\mathop{\rightarrow}\phi_{2})\geq
w(\phi_{2})\geq\delta+\varepsilon>w(\psi_{2})=w(\psi_{1}\mathop{\rightarrow}\psi_{2})$.

$4.$

Let
$\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})<\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})$.
If both $\nu(\psi_{1}\mathop{\rightarrow}\psi_{2})<1$ and
$\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})<1$ then we can proceed as in the
previous proof and we can apply IH concluding that
$w(\psi_{1}\mathop{\rightarrow}\psi_{2})=w(\psi_{2})<w(\phi_{2})=w(\phi_{1}\mathop{\rightarrow}\phi_{2})$.
On the contrary, if $\nu(\phi_{1}\mathop{\rightarrow}\phi_{2})=1$ then we need
to consider two alternatives. First, $1\neq\nu(\phi_{1})\leq\nu(\phi_{2})$
implies by IH that
$w(\psi_{1}\mathop{\rightarrow}\psi_{2})=w(\psi_{2})<\delta+\varepsilon<1=w(\phi_{1}\mathop{\rightarrow}\phi_{2})$.
Second, if $\nu(\phi_{1})=1=\nu(\phi_{2})$ then, by IH,
$w(\phi_{1}\mathop{\rightarrow}\phi_{2})\geq
w(\phi_{2})\geq\delta+\varepsilon>w(\psi_{2})=w(\psi_{1}\mathop{\rightarrow}\psi_{2})$.

This finishes the proof of the claim. $\blacksquare$

Claim 1 from Lemma 0.4.2. _If $u(\Box\psi)=\alpha<1$, for every
$\varepsilon>0$, there exists a valuation $w\in W^{c}$ such that
$\pi^{c}(w)>w(\psi)$ and $w(\psi)<\alpha+\varepsilon$, and thus
$\pi^{c}(w)\Rightarrow w(\psi)=w(\psi)<\alpha+\varepsilon$_.

  * Proof:

The proof is achieved in two stages:

  * –

first producing a valuation $\nu\in W$ satisfying $\nu(\psi)<1$ and preserving
the relative ordering conditions the values $w(\theta)$ must satisfy,
conditions which may be coded by a theory $\Gamma_{\psi,u}$;

  * –

and then moving the values $\nu(\theta)$, for $\theta\in Sub(\varphi)$, to the
correct valuation $w$ by composing $\nu$ with an increasing function of [0,1],
using Lemma 0.4.1.

Assume $u(\Box\psi)=\alpha<1$, and define the following set of formulas (all
formulas involved ranging in $\mathcal{L}_{\square\Diamond}(Var)$):

$\begin{array}[]{ll}\Gamma_{\psi,u}=&\\{\chi:\chi\in X\mbox{ and
}u(\chi)>\alpha\\}\\\
&\cup\\{\lambda\rightarrow\theta:\lambda\in\Delta_{\varphi}\mbox{ and
}u(\lambda)\leq u(\Box\theta)\\}\\\
&\cup\\{(\theta\rightarrow\lambda)\rightarrow\lambda:\lambda\in\Delta_{\varphi}\mbox{
and }u(\lambda)<u(\Box\theta)<1\\}\\\
&\cup\\{\theta\rightarrow\lambda:\lambda\in\Delta_{\varphi}\mbox{ and
}u(\Diamond\theta)\leq u(\lambda)\\}\\\
&\cup\\{(\lambda\rightarrow\theta)\rightarrow\theta:\lambda\in\Delta_{\varphi}\mbox{
and }u(\Diamond\theta)<u(\lambda)<1\\}\\\
&\cup\\{(\chi_{1}\rightarrow\chi_{2})\rightarrow\chi_{2}:\chi_{1},\chi_{2}\in
X\mbox{ and }u(\chi_{2})<u(\chi_{1})\leq\alpha\\}\\\ \end{array}$

Then we can check that $u(\square\xi)>\alpha$ for each
$\xi\in\Gamma_{\psi,u}$. Indeed, first recall that, by $U_{\Box}$ and
$U_{\Diamond}$ of Proposition 0.3.1, for any $\lambda\in X$ (in particular
$\Delta_{\varphi}$) we have $u(\Diamond\lambda)\leq{u(\lambda)}\leq
u(\Box\lambda)$ in $\mathsf{K45(\mathbf{G})}$. We analyse case by case. For
the first set of formulas, it is clear by construction. For the second set, we
have $u(\square(\lambda\rightarrow\theta))\geq
u(\Diamond\lambda\rightarrow\square\theta)=u(\Diamond\lambda)\Rightarrow
u(\Box\theta)\geq u(\lambda)\Rightarrow u(\Box\theta)=1$, by $FS2$. For the
third, by FS2 and P, we have

$\displaystyle u(\square((\theta\rightarrow\lambda)\rightarrow\lambda))\geq
u(\Diamond(\theta\mathop{\rightarrow}\lambda)\mathop{\rightarrow}\Box\lambda)$
$\displaystyle\geq
u((\Box\theta\mathop{\rightarrow}\Diamond\lambda)\mathop{\rightarrow}\Box\lambda)$
$\displaystyle\geq
u((\Box\theta\mathop{\rightarrow}\lambda)\mathop{\rightarrow}\Box\lambda)$
$\displaystyle={u(\lambda)\mathop{\rightarrow}u(\Box\lambda)}=1,$

since $u(\Diamond\lambda)\leq u(\lambda)\leq u(\Box\lambda)$ and
$u(\lambda)<u(\Box\theta)$. The fourth and fifth cases are very similar to the
second and third ones. As for the sixth case, by (T4), either
$u(\Box\chi_{1}\mathop{\rightarrow}\Diamond\chi_{2})=1$ or
$u(\Box((\chi_{1}\mathop{\rightarrow}\chi_{2})\mathop{\rightarrow}\chi_{2}))=1$.
According to $(U_{\Box})$, $(U_{\Diamond})$, $(5_{\Box})$ and
$(5_{\Diamond})$, we have that, for any $\varphi$,
$\Diamond\Box\varphi\mathop{\rightarrow}\Box\varphi$ and
$\Diamond\varphi\mathop{\rightarrow}\Box\Diamond\varphi$ are theorems of
$K45(G)$, and thus $u(\Box\chi_{1})\geq u(\chi_{1})$ and
$u(\Diamond\chi_{2})\leq u(\chi_{2})$, from where it follows that

$u(\Box\chi_{1}\mathop{\rightarrow}\Diamond\chi_{2})=u(\Box\chi_{1})\mathop{\rightarrow}u(\Diamond\chi_{2})\leq
u(\chi_{1})\mathop{\rightarrow}u(\chi_{2})=u(\chi_{2})<1.$

Therefore, it holds that
$u(\Box((\chi_{1}\mathop{\rightarrow}\chi_{2})\mathop{\rightarrow}\chi_{2}))=1$.

The fact that $u(\square\xi)>\alpha$ for each $\xi\in\Gamma_{\psi,u}$ implies

$\Gamma_{\psi,u}\not\vdash_{K45(\mathbf{G})}\psi,$

otherwise there would exist $\xi_{1},\ldots,\xi_{k}\in\Gamma_{\psi,u}$ such
that $\xi_{1},\ldots,\xi_{k}\vdash_{K45(\mathbf{G})}\psi.$ In such a case, we
would have $\Box\xi_{1},\ldots,\Box\xi_{k}\vdash_{K45(\mathbf{G})}\Box\psi$ by
$Nec$ and $K_{\square}$. Then
$\Box\xi_{1},\ldots,\Box\xi_{k},ThK45(\mathbf{G})\vdash_{G}\Box\psi$ by Lemma
0.2.1, and thus by Proposition 0.2.1 (i), and recalling that
$u(ThK45(\mathbf{G}))=1$, we would have

$\alpha<\inf u(\\{\Box\xi_{1},\ldots,\Box\xi_{k}\\}\cup ThK45(\mathbf{G}))\leq
u(\square\psi)=\alpha,$

a contradiction. Therefore, by Proposition 0.2.1 (ii) there exists a valuation
$\nu:Var\cup X\mapsto[0,1]$ such that $\nu(\Gamma_{\psi,u}\cup
ThK45(\mathbf{G}))=1$ and $\nu(\psi)<1$. This implies the following relations
between $u$ and $\nu,$ that we list for further use. Given
$\lambda,\lambda_{1},\lambda_{2}\in\Delta_{\varphi},\
\theta\in\mathcal{L}_{\square\Diamond}(Var)$ and $\chi,\chi_{1},\chi_{2}\in
X$, we have:

#1.

If $u(\chi)>\alpha$ then $\chi\in\Gamma_{\psi,u}$, and hence $\nu(\chi)=1$.

#2.

If $u(\lambda)\leq u(\square\theta)$ then $\nu(\lambda)\leq\nu(\theta)$ (since
then $\lambda\rightarrow\theta\in\Gamma_{\psi,u})$. In particular, if
$\lambda_{1},\lambda_{2}\in\Delta_{\varphi}$ and $u(\lambda_{1})\leq
u(\Box\lambda_{2})$ then $\nu(\lambda_{1})\leq\nu(\lambda_{2})$. Furthermore,
if $\Box\theta\in\Delta_{\varphi}$ then $\nu(\Box\theta)\leq\nu(\theta)$. That
means, taking $\theta=\psi$, $\nu(\Box\psi)\leq\nu(\psi)<1$.

#3.

If $u(\lambda)<u(\square\theta)<1$ then $\nu(\lambda)<\nu(\theta)$ or
$\nu(\lambda)=1$ (since then
$(\theta\rightarrow\lambda)\rightarrow\lambda)\in\Gamma_{\psi,u}$). In
particular, if $\lambda_{1},\lambda_{2}\in\Delta_{\varphi}$,
$u(\lambda_{1})<u(\lambda_{2})$ and $u(\lambda_{2})\leq u(\Box\psi)=\alpha$
then $\nu(\lambda_{1})<\nu(\psi)<1$ and thus
$\nu(\lambda_{1})<\nu(\lambda_{2})$. This means that $\nu$ preserves in a
strict sense the order values by $u$ of the formulas
$\lambda\in\Delta_{\varphi}$ such that $u(\lambda)\leq\alpha$.

#4.

If $u(\Diamond\theta)\leq u(\lambda)$ then $\nu(\theta)\leq\nu(\lambda)$
(because $\theta\mathop{\rightarrow}\lambda\in\Gamma_{\psi,u}$). In
particular, if $\Diamond\theta\in\Delta_{\varphi}$ then
$\nu(\theta)\leq\nu(\Diamond\theta)$.

#5.

If $u(\Diamond\theta)<u(\lambda)<1$ then $\nu(\theta)<\nu(\lambda)$ or
$\nu(\theta)=1$. In particular, if
$\lambda_{1},\lambda_{2}\in\Delta_{\varphi}$ and $u(\Diamond\lambda_{1})\leq
u(\lambda_{1})<u(\lambda_{2})\leq\alpha=u(\Box\psi)$ then
$\nu(\lambda_{1})<\nu(\lambda_{2})$. Furthermore, if $u(\lambda_{2})>0$ then
$\nu(\lambda_{2})>0$ (taking $\lambda_{1}:=\Diamond\bot$ since
$u(\bot)=u(\Diamond\bot)=0$).

#6.

If $u(\chi_{2})<u(\chi_{1})\leq\alpha$ then $\nu(\chi_{2})<\nu(\chi_{1})<1$.
Indeed, note that, by construction, $\nu(\psi)<1$, that implies, by #2,
$\nu(\Box\psi)<1$. In addition, we know $\Box\psi\in\Delta_{\phi}$ and
$u(\Box\psi)=\alpha$. Therefore, according to #4, if $\chi_{1}\in X$ and
$u(\Diamond\chi_{1})\leq u(\chi_{1})\leq u(\Box\psi)=u(\Box\Box\psi)$, then
$\nu(\chi_{1})\leq\nu(\Box\Box\psi)=\nu(\Box\psi)<1$. Finally, since
$(\chi_{1}\mathop{\rightarrow}\chi_{2})\mathop{\rightarrow}\chi_{2}\in\Gamma_{\psi,u}$
we have $\nu(\chi_{2})<\nu(\chi_{1})<1$.

#7.

If $u(\lambda_{1})\leq u(\lambda_{2})$ then
$\nu(\lambda_{1})\leq\nu(\lambda_{2})$. Note that this is a particular case of
#2. Certainly, if $\lambda_{1},\lambda_{2}\in\Delta_{\varphi}$, then by Lemma
0.3.1 we have $u(\lambda_{2})\leq u(\Box\lambda_{2})$, and, hence, by #2,
$\nu(\lambda_{1})\leq\nu(\lambda_{2})$.

According to the properties #1–#7, it is clear that $\nu$ satisfies the
conditions a-d of Lemma 0.4.1. Indeed, from #1 and #2 it follows that

$\alpha=\max\\{u(\lambda):\nu(\lambda)<1\mbox{ and
}\lambda\in\Delta_{\varphi}\\},$

because, by construction of $\Gamma_{\psi,u}$ and by #1,
$\forall\lambda\in\Delta_{\varphi}$, if $u(\lambda)>\alpha$ then
$\nu(\lambda)=1$ and by #2, $\nu(\Box\psi)<1$. Therefore $\alpha$ coincides
with the value $\delta$ defined in Lemma 0.4.1.

Consequently, for all $\varepsilon>0$ such that $\alpha+\varepsilon<\beta$,
where $\beta$ is defined as in Lemma 0.4.1, there exists a valuation $w\in
W^{v}$ such that $w(\psi)<\alpha+\varepsilon$. Then in order to finish our
proof, it remains to show that:

$\pi^{c}(w)=\inf_{\lambda\in sub(\varphi)}\min(v(\Box\lambda)\Rightarrow
w(\lambda),w(\lambda)\Rightarrow v(\Diamond\lambda))>w(\psi)$ (3)

To do so, we will prove that, for any $\lambda\in sub(\varphi)$, both
implications in (3) are greater than or equal to
$\alpha+\varepsilon$.333Remember that $u\sim_{\varphi}v\sim_{\varphi}w$. First
we prove it for the first implication by cases:

-

If $\ v(\Box\lambda)\leq\alpha<1$ then $v(\Box\lambda)\Rightarrow
w(\lambda)=1$. Indeed, first of all, by #2, from
$u(\Box\lambda)=v(\Box\lambda)\leq\alpha=u(\Box\psi)$ it follows
$\nu(\Box\lambda)\leq\nu(\psi)<1$. Now, since $u(\Box\lambda)\leq
u(\Box\lambda)$, by #2, we have $1\neq\nu(\Box\lambda)\leq\nu(\lambda)$, and
by 3 of Lemma 0.4.1 we have $v(\Box\lambda)=w(\Box\lambda)\leq w(\lambda)$.
Then $v(\Box\lambda)\Rightarrow w(\lambda)=1$.

-

If $v(\Box\lambda)>\alpha$ then by #1 and #2,
$1=\nu(\Box\lambda)\leq\nu(\lambda)$. Therefore, by 1 of Lemma 0.4.1,
$w(\lambda)\geq\alpha+\varepsilon$ which implies $v(\Box\lambda)\Rightarrow
w(\lambda)>\alpha$.

For the second implication we also consider two cases:

-

If $v(\Diamond\lambda)=u(\Diamond\lambda)>\alpha$ then
$\nu(\Diamond\lambda)=1$ by #1, so $w(\lambda)\geq
w(\Diamond\lambda)\geq\alpha+\varepsilon$. it is obvious that
$w(\lambda)\Rightarrow v(\Diamond\lambda)>\alpha$ because by Lemma 0.4.1 we
know $w(\lambda)\geq\alpha+\varepsilon$.

-

If $u(\Diamond\lambda)\leq\alpha$ then we obtain by #4, that
$\nu(\lambda)\leq\nu(\Diamond\lambda)<1$. Then by Lemma 0.4.1 we have
$w(\lambda)\leq w(\Diamond\lambda)=v(\Diamond\lambda)$ and thus
$w(\lambda)\Rightarrow v(\Diamond\lambda)=1$.

$\blacksquare$

Claim 2 from Lemma 0.4.2. _If $u(\Diamond\psi)=\alpha>0$ then, for any small
enough $\varepsilon>0,$ there exists a valuation $w^{\prime}\in W$ such that
$\min(w^{\prime}(\psi),\pi^{c}(w^{\prime}))\geq\alpha-\varepsilon$_.

  * Proof:

Assume $u(\Diamond\psi)=\alpha>0$444In this context, $\alpha$ plays the role
of $\beta$ in Lemma 0.4.1. Then, we take
$\delta=\max\\{u(\lambda)<\alpha:\lambda\in\Delta_{\varphi}\\}$ (note that the
last set is not empty because $\Diamond\bot$ belongs to it) and define
$\Gamma^{\prime}_{\psi,u}$ in a similar way that it was defined in the proof
of Claim 1:

$\begin{array}[]{ll}\Gamma^{\prime}_{\psi,u}=&\\{\chi:\chi\in X\mbox{ and
}u(\chi)>\delta\\}\\\
&\cup\\{\lambda\rightarrow\theta:\lambda\in\Delta_{\varphi}\mbox{ and
}u(\lambda)\leq u(\Box\theta)\\}\\\
&\cup\\{(\theta\rightarrow\lambda)\rightarrow\lambda:\lambda\in\Delta_{\varphi}\mbox{
and }u(\lambda)<u(\Box\theta)<1\\}\\\
&\cup\\{\theta\rightarrow\lambda:\lambda\in\Delta_{\varphi}\mbox{ and
}u(\Diamond\theta)\leq u(\lambda)\\}\\\
&\cup\\{(\lambda\rightarrow\theta)\rightarrow\theta:\lambda\in\Delta_{\varphi}\mbox{
and }u(\Diamond\theta)<u(\lambda)<1\\}\\\
&\cup\\{(\chi_{1}\rightarrow\chi_{2})\rightarrow\chi_{2}:\chi_{1},\chi_{2}\in
X\mbox{ and }u(\chi_{2})<u(\chi_{1})\leq\delta\\}\\\ \end{array}$

If $u(\Diamond\psi)=\alpha>0$, then we let
$U_{\psi,u}=\psi\mathop{\rightarrow}\theta$ where $\theta\in\Delta_{\varphi}$
and $u(\theta)=\delta$. We claim that

$\Gamma^{\prime}_{\psi,u}\not\vdash_{K45(\mathbf{G})}U_{\psi,u}\ ,$

otherwise there would exist
$\theta_{1},\ldots,\theta_{n}\in\Gamma^{\prime}_{\psi,u}$ such that
$\vdash_{K45(\mathbf{G})}(\theta_{1}\wedge\ldots\wedge\theta_{n})\mathop{\rightarrow}U_{\psi,u}$,
and then we would have
$\vdash_{K45(\mathbf{G})}\Box(\theta_{1}\wedge\ldots\wedge\theta_{n})\mathop{\rightarrow}\Box(\psi\mathop{\rightarrow}\theta)$,
which would imply
$\vdash_{K45(\mathbf{G})}(\Box\theta_{1}\wedge\ldots\wedge\Box\theta_{n})\mathop{\rightarrow}(\Diamond\psi\mathop{\rightarrow}\Box\theta)$.
In that case, evaluating with $u$ it would yield
$1=u(\Box\theta_{1}\wedge\ldots\wedge\Box\theta_{n})\Rightarrow
u(\Diamond\psi\mathop{\rightarrow}\theta)$, contradiction, since
$u(\Box\theta_{1}\wedge\ldots\wedge\Box\theta_{n})>\delta$ and
$u(\Diamond\psi\mathop{\rightarrow}\theta)=\delta$ (because by definition
$u(\theta)<u(\Diamond\psi)$).

Therefore, there is an evaluation $\nu^{\prime}$ such that
$\nu^{\prime}(ThK45(\mathbf{G}))=\nu^{\prime}(\Gamma^{\prime}_{\psi,u})=1$,
$\nu^{\prime}(\Diamond\psi)=1$ and
$\nu^{\prime}(\psi\mathop{\rightarrow}\theta)<1$. Hence, Condition $\bf a$, in
Lemma 0.4.1 is satisfied. Condition $\bf b$ is also satisfied because by
definition of $\Gamma^{\prime}_{\psi,u}$ we know that $\nu^{\prime}(\chi)=1$
for every $\chi\in X$ such that $u(\chi)>\delta$. In addition, we can verify
Condition $\bf c$ by considering Property $\\#6$ of Claim 1 with $\delta$
instead of $\alpha$.

Therefore, for any $\varepsilon>0$ with $\delta+\varepsilon<\alpha$ there
exists a valuation $w^{\prime}\in W$ such that
$w^{\prime}(\psi)\geq\delta+\varepsilon$. Note that in this case
$\delta<\alpha=1$. That means we are always able to find an appropriate
valuation $w^{\prime}$ such that $w^{\prime}(\psi)$ is arbitrarily close to
$\alpha$.

It remains to show that $\pi^{c}(w^{\prime})\geq\alpha$. Indeed, by
construction, it holds that $\forall\theta\in\Delta_{\varphi}\mbox{ and
}u(\Box\theta)\leq\delta:u(\Box\theta)\leq w^{\prime}(\theta)\leq
u(\Diamond\theta)$, and hence $\min(u(\Box\theta)\Rightarrow
w^{\prime}(\theta),w^{\prime}(\theta)\Rightarrow
u(\Diamond\theta))\geq\alpha$. This finishes the proof. $\blacksquare$