# Modal logic for reasoning about uncertainty and confusion

Marta Bílková, Thomas Ferguson, Daniil Kozhemiachenko

► To cite this version:

Marta Bílková, Thomas Ferguson, Daniil Kozhemiachenko. Modal logic for reasoning about uncertainty and confusion. 2025. hal-05348621

HAL Id: hal-05348621

https://hal.science/hal-05348621v1

Preprint submitted on 5 Nov 2025

HAL is a multi-disciplinary open access
archive for the deposit and dissemination of sci-
entific research documents, whether they are pub-
lished or not. The documents may come from
teaching and research institutions in France or
abroad, or from public or private research centers.

L'archive ouverte pluridisciplinaire HAL, est
destinée au dépôt et à la diffusion de documents
scientifiques de niveau recherche, publiés ou non,
émanant des établissements d'enseignement et de
recherche français ou étrangers, des laboratoires
publics ou privés.

<figure><img src="image_1.png" /></figure>

Distributed under a Creative Commons Attribution 4.0 International License
# Modal logic for reasoning about uncertainty and confusion

Marta Bílková*

The Czech Academy of Sciences, Institute of Philosophy, Prague, Czech Republic

bilkova@cs.cas.cz

Thomas M. Ferguson

Department of Cognitive Science, Rensselaer Polytechnic Institute, Troy, USA

tferguson@gradcenter.cuny.edu

Daniil Kozhemiachenko

Aix-Marseille Université, CNRS, LIS, UMR 7020, Marseille, France

daniil.kozhemiachenko@lis-lab.fr

We consider a modal logic that can formalise statements about uncertainty and beliefs such as *I think that my wallet is in the drawer rather than elsewhere or I am confused whether my appointment is on Monday or Tuesday.* To do that, we expand Gödel modal logic KG with the involutive negation ~ defined as $v(\sim\phi, w) = 1 - v(\phi, w)$. We provide semantics with the finite model property for our new logic that we call KGinv and show its equivalence to the standard semantics over [0, 1]-valued Kripke models. Namely, we show that $\phi$ is valid in the standard semantics of KGinv iff it is valid in the new semantics. Using this new semantics, we construct a constraint tableaux calculus for KGinv that allows for an explicit extraction of countermodels from complete open branches and then employ the tableaux calculus to obtain the PSPACE-completeness of the validity in KGinv.

## 1 Introduction

When people evaluate their uncertainty or beliefs, they can do it in two ways: either quantitatively, by assigning a specific number to the value of the belief, e.g., ‘the chance of rain today is 73%’ or qualitatively, by comparing degrees of two beliefs without explicitly mentioning their numerical values as in ‘I think that my wallet is more likely to be in the drawer than in the bag’. Usually, a person does not assign exact values to their beliefs and thus reasons qualitatively. Qualitative reasoning can be formalised, e.g., in Gödel modal logic KG or, if one interprets ‘rather’ as ‘strictly more likely’, its expansion with Δ (Baaz’ Delta [3]) or ≺ (co-implication [25, 21]) KbiG (modal bi-Gödel logic).

Comparing degrees of beliefs is possible in KbiG because the semantics of its propositional fragment — bi-Gödel logic (biG) — is characterised by the Gödel t-norm $\wedge_G$ and its residuum $\to_G$ and their duals $\vee_G$ and $\prec_G$ defined on [0, 1] by:

$$ a \wedge_G b = \min(a, b) \quad a \to_G b = \begin{cases} 1 & \text{if } a \le b \\ b & \text{otherwise} \end{cases} \quad a \vee_G b = \max(a, b) \quad a \prec_G b = \begin{cases} 0 & \text{if } a \le b \\ a & \text{otherwise} \end{cases} \quad (1) $$

Propositional Gödel logic is a prominent many-valued logic whose semantics defined on [0, 1] is suitable for formalising relative comparisons of degrees of truth. Gödel modal logics expand propositional Gödel logic with modalities □ and ◦ and are usually interpreted on [0, 1]-valued Kripke frames. There,

<footnote>*The first author is supported by the project Logical Structure of Information Channels, no. 21-23610M of the Czech Science Foundation.</footnote>
propositional variables in states are evaluated with numbers from [0, 1], the propositional connectives correspond to Gödel semantics shown in (1), and the values of □φ and ◊φ are defined as, respectively, the infimum and supremum of the values of φ in the accessible states.

Note that it is natural not only to compare degrees of certainty in two different events but also to assert whether the statement is *more likely to be true* or *more likely to be false*. This can be expressed by statements such as ‘*my wallet is likely in the drawer*’, meaning ‘*I think that my wallet is in the drawer rather than elsewhere*’. I.e., the (subjective) likelihood of the wallet being in the drawer is greater than 1/2. Furthermore, an agent may be *confused* about a statement *p*, i.e., not be able to discern *p* with its negation.

As biG can express only 0 and 1, the first kind of statements cannot be formalised in KbiG. However, 1/2 is expressible with the involutive negation ~ defined as $v(\sim\phi, w) = 1 - v(\phi, w)$: $v(p \leftrightarrow \sim p, w) = 1$ iff $v(p, w) = \frac{1}{2}$. Moreover, since $\neg p$ — the Gödelian negation of $p$ — is defined as $p \rightarrow_G 0$, $p$ and $\neg p$ can never have the same value, and thus, can always be distinguished. I.e., the second kind of statements is not formalisable either.

In this paper, we will present a modal logic that allows us to express such statements. Let us now provide a broader context of our work.

**Gödel logics with involution** The modal logic that we consider in our paper expands $G_{inv}$ — the propositional Gödel logic with involutive negation ~ that was introduced in [20]. Adding ~ greatly enhances the expressivity of the Gödel logic. Not only can 1/2 be expressed, but also coimplication (pseudo-difference, interpreted as φ excludes χ) and the Baaz Delta (the 1-detecting operator) can be defined.

$$ \phi \prec \chi := \sim(\sim\chi \rightarrow \sim\phi) $$

$$ \Delta\phi := 1 \prec (1 \prec \phi) $$

We observe briefly that ~ is closer than ¬ to the intuitive reading of ‘not’ in contexts involving truth degrees. Indeed, if the truth degree of *p* (‘Peter is tall’) is 1/2, it is reasonable to assume that the truth degree of ~*p* (Peter is not tall) is also 1/2. Similarly, if Peter is shorter than average (i.e., the truth degree of *p* is smaller than 1/2), one may safely accept that the truth degree of ‘not-*p*’ should be greater than 1/2. On the other hand, the truth degree of $\neg p$ would be 0 whenever the truth degree of *p* is positive. Thus, using $\neg p$ to stand for ‘Peter is not tall’ is counterintuitive as it says that ‘Peter is tall is contradictory’.

Note, moreover, that $G_{inv}$ is *paraconsistent* in the following sense: (1) $(p \wedge \sim p) \rightarrow q$ is not valid; (2) $p, \sim p \nvdash_{G_{inv}} q$ if entailment is defined via the preservation of order on [0, 1]. These properties were investigated in [19, 18].

Paraconsistency of the propositional fragment is a useful property when it comes to the analysis of beliefs. Indeed, from a classical standpoint, *all contradictions are equivalent* (because they are all universally false). Hence, □(p ∧ ~p) ↔ □(q ∧ ~q) is valid in every classical modal logic. If one interprets □ as a belief modality, this means that the agent cannot differentiate between contradictions. This, however, is counterintuitive since a person can (implicitly) believe in one contradiction but not the other or reject one contradiction with more conviction than the other. In paraconsistent logics, however, contradictions are *not* equivalent, and thus, are not indistinguishable under □.

**Gödel modal logics** Modal expansions of Gödel logics and their applications have been extensively studied. The □ and ◊ fragments<fnref n="1" /> of KG were axiomatised in [16]. Hypersequent calculi were constructed in [23, 24] and used to obtain the PSPACE-completeness of both fragments. KG in the bi-modal language

<footnote n="1">¹Note that □ and ◊ are not interdefinable in Gödel modal logic.</footnote>
was axiomatised in [17, 27] (for fuzzy and crisp<fnref n="2" /> frames, respectively). Moreover, it was shown in [14, 15] that crisp and fuzzy KG are PSPACE-complete.

The applications of Gödel modal logics and its expansions are well researched. In [26], the completeness of K45 and KD45 extensions of KG with respect to non-normalised and normalised possibilistic frames was established. In [1, 2], a temporal logic expanding the Gödel logic with co-implication was proposed. In addition, paraconsistent expansions of KG that can be used to reason about contradictory beliefs were proposed and studied in [4, 5, 6].

**Gödel description logics** Gödel description logics (DLs) were proposed in [8] to represent graded information in the ontologies and were further studied in [9]. Just as the classical description logics are notational variants of the classical logics with the global (universal) modality, Gödel DLs can be considered a notational variant of global Gödel modal logics. Moreover, Gödel DLs are usually equipped with the involutive negation. They differ from Łukasiewicz and Product fuzzy DLs because they are decidable and often have the same complexity as their classical counterparts even in the cases of expressive logics [12, 11, 10, 13]. Note, however, that since infinite-valued Gödel DLs lack the finite model property, their decision procedures do not produce explicit (counter-)models.

**Contributions and plan of the paper** In this paper, we consider KGinv — an expansion of KG with involutive negation and construct a tableaux calculus that allows for the extraction of finite countermodels from failed proofs and can be used to establish its PSPACE-completeness. Our contribution is two-fold. First, following [14, 15], we present an alternative semantics for KGinv that possesses the finite model property. In particular, we show that the sets of validities with respect to the standard and the alternative semantics coincide (both in the case of crisp and arbitrary frames). Second, using this semantics, we construct a tableaux calculus by combining the techniques from [22] and [28] that allows us to read off countermodels from complete open branches. We then use this calculus to establish PSPACE-completeness of KGinv.

The remainder of the text is structured as follows. In Section 2, we present KGinv and its standard semantics. We also discuss the formalisation of reasoning about uncertainty and confusion in KGinv. Section 3 is dedicated to the alternative semantics with the finite model property. In Section 4, we construct a tableaux calculus for KGinv and show its soundness and completeness. Then, in Section 5, we use the tableaux to obtain the PSPACE-completeness of KGinv. Finally, we summarise our results and provide a plan for future work in Section 6.

## 2 Language and standard semantics

Let us present the language and standard semantics of KGinv. We fix a countable set Prop of propositional variables and define the language $\mathcal{L}_{\square, \diamond}$ using the grammar below.

$$ \mathcal{L}_{\square, \diamond} \models \phi ::= p \in \text{Prop} \mid \sim\phi \mid (\phi \land \phi) \mid (\phi \rightarrow \phi) \mid \Box\phi \mid \Diamond\phi $$

The next definitions introduce the notions of frames and KGinv models.

**Definition 1 (Frames).**

* A fuzzy frame is a tuple $\mathfrak{F} = \langle W, R \rangle$ with $W \neq \emptyset$ and $R: W \times W \to [0, 1]$.

<footnote n="2">²A frame $\langle W, R \rangle$ is called fuzzy if $R: W \times W \to [0, 1]$ and crisp if $R: W \times W \to \{0, 1\}$.</footnote>
• A crisp frame is a tuple $\mathfrak{F} = \langle W, R \rangle$ with $W \neq \emptyset$ and $R : W \times W \to \{0, 1\}$.
For a frame $\mathfrak{F} = \langle W, R \rangle$ and $w \in W$, we set $R(w) = \{w' : wRw' > 0\}$.

**Definition 2** (Semantics of $\mathbf{KG}_{\text{inv}}$). A $\mathbf{KG}_{\text{inv}}$-model is a tuple $\mathfrak{M} = \langle W, R, v \rangle$ with $\langle W, R \rangle$ being a frame and $v : \text{Prop} \times W \to [0, 1]$ (a $\mathbf{KG}_{\text{inv}}$-valuation) extended to the complex formulas as follows (cf. (1) for the definition of $\wedge_G$ and $\to_G$).

$$v(\sim\phi, w) = 1 - v(\phi, w)$$
$$v(\phi \to \chi, w) = v(\phi, w) \to_G v(\chi, w)$$

$$v(\phi \wedge \chi, w) = v(\phi, w) \wedge_G v(\chi, w)$$
$$v(\Box\phi, w) = \inf_{w' \in W} \{wRw' \to_G v(\phi, w')\}$$
$$v(\Diamond\phi, w) = \sup_{w' \in W} \{wRw' \wedge_G v(\phi, w')\}$$

We say that $\phi \in \mathcal{L}_{\square, \diamond}$ is $\mathbf{KG}_{\text{inv}}$-valid on a pointed frame $\langle \mathfrak{F}, w \rangle$ ($\mathfrak{F} \models_{\mathbf{KG}_{\text{inv}}} \phi$) iff $v(\phi, w) = 1$ for any model $\mathfrak{M}$ on $\mathfrak{F}$. $\phi$ is $\mathbf{KG}_{\text{inv}}$-valid on frame $\mathfrak{F}$ ($\mathfrak{F} \models_{\mathbf{KG}_{\text{inv}}} \phi$) iff $\mathfrak{F}, w \models_{\mathbf{KG}_{\text{inv}}} \phi$ for any $w \in \mathfrak{F}$. Finally, $\phi$ is $\mathbf{KG}_{\text{inv}}$-valid (or simply valid) iff $\mathfrak{F} \models_{\mathbf{KG}_{\text{inv}}} \phi$ for every $\mathfrak{F}$.

**Convention 1.** Given a formula $\phi$, we use $\ell(\phi)$ to denote the number of occurrences of symbols in $\phi$. We will write $\phi \leftrightarrow \chi$ as a shorthand for $(\phi \to \chi) \wedge (\chi \to \phi)$ and use the following defined connectives:

$$\mathbf{1} := p \to p$$
$$\phi \lor \chi := (\sim\phi \wedge \sim\chi)$$

$$\mathbf{0} := \sim\mathbf{1}$$
$$\phi \prec \chi := (\sim\chi \to \sim\phi)$$

$$\neg\phi := \phi \to \mathbf{0}$$
$$\triangle\phi := \mathbf{1} \prec (\mathbf{1} \prec \phi)$$

One can see from (1) and Definition 2 that $v(\phi \leftrightarrow \chi, w) = 1$ if $v(\phi, w) = v(\chi, w)$ and $\min(v(\phi, w), v(\chi, w))$, otherwise; $v(\phi \lor \chi, w) = v(\phi, w) \lor_G v(\chi, w)$; $v(\phi \prec \chi, w) = v(\phi, w) \prec_G v(\chi, w)$; and $v(\triangle\phi, w) = 1$ if $v(\phi, w) = 1$ and $v(\triangle\phi, w) = 0$, otherwise.

Let us now look at how we can use $\mathbf{KG}_{\text{inv}}$ to formalise the contexts we considered in the previous section. First, we consider the assertion that $\phi$ is more likely to be true than false.

**Example 1.** Consider the following statement from the Introduction.

wal.: *I think that my wallet is in the drawer rather than elsewhere.*

We write $d$ for ‘my wallet is in the drawer’ and use $\Box$ for ‘I think that’. Now, we need to formalise that the degree of subjective likelihood of $d$ is greater than $\frac{1}{2}$. That is, we should write a formula that is true at $w$ when $v(\Box d, w) > \frac{1}{2}$. We formalise wal. as follows: $\phi_{\text{wal.}} := \sim\triangle(\Box d \to \sim\Box d)$. By Definition 2, and Convention 1, one can see that $v(\phi_{\text{wal.}}, w) = 1$ iff $v(\Box d \to \sim\Box d, w) < 1$. This means that $v(\Box d, w) > v(\sim\Box d, w)$, i.e., $v(\Box d, w) > 1 - v(\Box d, w)$, whence, $v(\Box d, w) > \frac{1}{2}$, as required.

Let us now see how to formalise situations involving confusion using $\mathbf{KG}_{\text{inv}}$.

**Example 2.** Assume that Ann wants to come to Brittney’s birthday party. Unfortunately, the only piece of information Ann has about the party is that it is held this weekend and lasts one evening. Thus, Ann cannot discern between the birthday party happening on Saturday ($s$) or Sunday ($\sim s$).

Formally, this means that in every accessible state, the values of $s$ and $\sim s$ must be the same. Thus, we write the following formula: $\phi_{\text{bd}} := \Box\triangle(s \leftrightarrow \sim s)$. It is easy to verify that $v(\phi_{\text{bd}}, w) = 1$ iff $v(s, w') = \frac{1}{2} = v(\sim s, w')$ in every $w' \in R(w)$. Indeed, the value of $\triangle(s \leftrightarrow \sim s)$ always belongs to $\{0, 1\}$. Thus, $v(\phi_{\text{bd}}, w) = 1$ iff $v(\triangle(s \leftrightarrow \sim s), w') = 1$ in every accessible state. That is, $v(s \leftrightarrow \sim s, w') = 1$, and hence, $v(s, w) = v(\sim s, w) = 1 - v(s, w)$.

We finish the section with the following observations. First, $\Box p \leftrightarrow \sim\Diamond\sim p$ is valid on $\mathfrak{F}$ iff $\mathfrak{F}$ is crisp. Second, $\Box$ and $\Diamond$ are not interdefinable on the class of all frames.

**Proposition 1.** $\mathfrak{F} \models_{\mathbf{KG}_{\text{inv}}} \Box p \leftrightarrow \sim\Diamond\sim p$ iff $\mathfrak{F}$ is crisp.
**Proof.** Observe that on crisp frames, the semantics of modalities can be simplified as follows: $v(\square\phi, w) = \inf\{v(\phi, w') : wRw'\}$ and $v(\diamond\phi, w) = \sup\{v(\phi, w') : wRw'\}$. From here, it is evident that $\square p \leftrightarrow \sim\diamond\sim p$ is valid on crisp frames. For the converse, assume that $\mathfrak{F}$ is not crisp, i.e., there are $w, w' \in \mathfrak{F}$ s.t. $wRw' = x$ for some $0 < x < 1$. Now for every $w'' \in W$, set $v(p, w'') = wRw''$ and $v(p, w'') = 1$ only if $wRw'' = 1$. It is clear that $v(\square p, w) = 1$. On the other hand, we have that $v(\diamond\sim p, w) > 0$ since $0 < v(\sim p, w') \le 1 - x < 1$ and $wRw' = x$. But then, $v(\sim\diamond\sim p, w) \ne 1$, as required. $\square$

**Proposition 2.** $\square$ and $\diamond$ are not interdefinable on the class of all frames. That is, there is a model $\mathfrak{M}$ and $w \in \mathfrak{M}$ s.t. (1) there is no $\diamond$-free formula $\chi$ s.t. $v(\chi, w) = v(\diamond p, w)$; (2) there is no $\square$-free formula $\psi$ s.t. $v(\psi, w) = v(\square p, w)$.

*Proof.* Consider Fig. 1 and note that $v(\square p, w) = \frac{1}{5}$ and $v(\diamond p, w) = \frac{1}{4}$. We show by induction on $\tau$ that

$$ \forall \tau \in \mathcal{L}_{\square, \diamond} : v(\tau, w') \in \{0, 1/5, 4/5, 1\} \text{ and } v(\tau, w'') \in \{0, 1/4, 3/4, 1\} \quad (2) $$

The basis cases in (2) hold by the construction of the model and the cases of propositional connectives are obtained by applying the induction hypothesis. Finally, as $R(w') = R(w'') = \emptyset$, for $\tau = \diamond\sigma$, we have $v(\diamond\sigma, w') = v(\diamond\sigma, w'') = 0$; and for $\tau = \square\sigma$, we have that $v(\square\sigma, w') = v(\square\sigma, w'') = 1$.

Then, we can show for every $\tau \in \mathcal{L}_{\square, \diamond}$ that

$$ \begin{aligned} v(\tau, w'') &= 0 &\Rightarrow v(\tau, w') &= 0 & v(\tau, w'') &= \frac{1}{4} &\Rightarrow v(\tau, w') &= \frac{1}{5} \\ v(\tau, w'') &= \frac{3}{4} &\Rightarrow v(\tau, w') &= \frac{4}{5} & v(\tau, w'') &= 1 &\Rightarrow v(\tau, w') &= 1 \end{aligned} \quad (3) $$

and

$$ \begin{aligned} v(\tau, w') &= 0 &\Rightarrow v(\tau, w'') &= 0 & v(\tau, w') &= \frac{1}{5} &\Rightarrow v(\tau, w'') &= \frac{1}{4} \\ v(\tau, w') &= \frac{4}{5} &\Rightarrow v(\tau, w'') &= \frac{3}{4} & v(\tau, w') &= 1 &\Rightarrow v(\tau, w'') &= 1 \end{aligned} \quad (4) $$

For (3), we proceed by induction. The basis case of $\tau = p$ holds by the construction of the model. If $\tau = \diamond\sigma$, then $v(\diamond\sigma, w') = v(\diamond\sigma, w'') = 0$. If $\tau = \square\sigma$, then $v(\square\sigma, w') = v(\square\sigma, w'') = 1$.

Let $\tau = \rho \wedge \sigma$. The cases of $v(\tau, w'') \in \{0, 1\}$ are straightforward. Assume that $v(\rho \wedge \sigma, w'') = \frac{1}{4}$, then w.l.o.g. $v(\rho, w'') = \frac{1}{4}$ and $v(\sigma, w'') \in \{\frac{1}{4}, \frac{3}{4}, 1\}$. By the induction hypothesis, we have that $v(\rho, w'') = \frac{1}{5}$ and $v(\sigma, w'') \in \{\frac{1}{5}, \frac{4}{5}, 1\}$, whence, $v(\rho \wedge \sigma, w') = \frac{1}{5}$. The case when $v(\rho \wedge \sigma, w'') = \frac{3}{4}$ is tackled in the same way.

Consider $\tau = \rho \to \sigma$. We deal only with the most instructive case of $v(\rho \to \sigma, w'') = \frac{1}{4}$. Here, we have $v(\sigma, w'') = \frac{1}{4}$ and $v(\rho, w'') \in \{1, \frac{3}{4}\}$. By the induction hypothesis, we have $v(\sigma, w') = \frac{1}{5}$ and $v(\rho, w') \in \{\frac{4}{5}, 1\}$. Hence, $v(\rho \to \sigma, w') = \frac{1}{5}$.

Other propositional connectives can be dealt with similarly.

For (4), the case of $\tau = p$ holds by construction; if $\tau = \square\sigma$, then $v(\square\sigma, w') = v(\square\sigma, w'') = 1$; if $\tau = \diamond\sigma$, then $v(\diamond\sigma, w') = v(\diamond\sigma, w'') = 0$. The cases of propositional connectives can be dealt with in the same way as for (3).

We now show by induction on formulas $\chi$ and $\psi$ that (i) there is no $\square$-free formula $\chi$ s.t. $v(\chi, w) \in \{\frac{1}{5}, \frac{4}{5}\}$ and (ii) there is no $\diamond$-free formula $\psi$ s.t. $v(\psi, w) \in \{\frac{1}{4}, \frac{3}{4}\}$.

For (i), the basis case holds by the construction of the model. The cases of propositional connectives can be established by a straightforward application of the induction hypothesis. Now let $\chi = \diamond\tau$. It is clear that $v(\diamond\tau, w) \ne \frac{4}{5}$ since $wRw' = wRw'' = \frac{2}{3}$. We check that $v(\diamond\tau, w) \ne \frac{1}{5}$. Assume for contradiction
$$w'' : p = 1/4 \leftarrow \frac{2}{3} \rightarrow w : p = 0 \leftarrow \frac{2}{3} \rightarrow w' : p = 1/5$$

Figure 1: All variables have the same values as p.

that $v(\diamond\tau, w) = \frac{1}{5}$. Then, $v(\tau, w') = \frac{1}{5}$ from (2). But using (3), we have that $v(\tau, w'') = \frac{1}{4}$, whence $v(\diamond\tau, w) = \frac{1}{4}$. Contradiction.

For (ii), the basis case holds by the construction of the model and the cases of propositional connectives can be proven by the application of the induction hypothesis. We show that $v(\Box\tau, w) \notin \{\frac{1}{4}, \frac{3}{4}\}$. Observe that $wRw' = wRw'' = \frac{2}{3}$, whence, $v(\Box\tau, w) \neq \frac{3}{4}$. We are going to check that $v(\Box\tau, w) \neq \frac{1}{4}$. The proof is similar to the one of (i) but we use (4). If $v(\Box\tau, w) = \frac{1}{4}$, then $v(\tau, w'') = \frac{1}{4}$ by (2). But from here, we obtain $v(\tau, w') = \frac{1}{5}$ by (4). Contradiction. □

### 3 Semantics for $KG_{inv}$ with the finite model property

It is well-known (cf., e.g., [16]) that the standard semantics of $KG$ (modal Gödel logic) and thus, of $KG_{inv}^3$, lack the finite model property (FMP). Still, semantics over so-called F-models (F stands for ‘finitary’) satisfying the finite model property can be provided to any expansion of $KG$ with order-based connectives (i.e., connectives expressible via infima and suprema of lattice operations) [15].

One can see, however, that $\sim$ is not an order-based connective. Thus, we cannot use the general result of [15] to provide a semantics over F-models. Still, we can adapt the approach from [14]. Namely, we will redefine the models in such a way that in a given state $w$, there is only a finite set of values that formulas of the form $\Box\phi$ or $\Diamond\phi$ are allowed to have. Then modal formulas will be ‘witnessed’ in $w$ if there is an accessible state $w'$ where the value of $\phi$ is sufficiently close to the value of $\Box\phi$ or $\Diamond\phi$.

**Definition 3 (F-models).** An F-model is a tuple $\mathfrak{M} = (W, R, T, v)$ with $\langle W, R \rangle$ being a frame and $T : W \to \mathcal{P}_{<\omega}([0, 1])^4$ be s.t. for all $w \in W$, it holds that: $\{0, \frac{1}{2}, 1\} \subseteq T(w)$, and if $x \in T(w)$, then $1 - x \in T(w)$. Finally, $v$ (valuation) is a map $v : \text{Prop} \times W \to [0, 1]$ that is extended to the complex formulas as in $KG_{inv}$ (Definition 2) in the cases of propositional connectives and in the modal cases, as follows:

$$v(\Box\phi, w) = \max\{x \in T(w) \mid x \le \inf_{w' \in W} \{wRw' \to_G v(\phi, w')\}$$

$$v(\Diamond\phi, w) = \min\{x \in T(w) \mid x \ge \sup_{w' \in W} \{wRw' \wedge_G v(\phi, w')\}\}$$

We say that $\phi \in \mathcal{L}_{\Box, \Diamond}^\sim$ is F-valid iff $v(\phi, w) = 1$ in every F-model $\mathfrak{M}$ and every $w \in \mathfrak{M}$.

In the definition above, $T$ assigns a finite subset of $[0, 1]$ to each state in the model. This way, $T(w)$ is the set of values that modal formulas can have at $w$. Note also that the value of $\Box\phi$ in an F-model can be interpreted as an approximation from below of its ‘real’ value in a standard model. Dually, the value of $\Diamond\phi$ is an approximation from above. It is important to observe that we need the $1 - x$ closure of $T(w)$ and the presence of $\frac{1}{2}$. Otherwise, we could have the following ‘models’.

$$\mathfrak{R} : w_0 \xrightarrow{R=1/2} w_1 : p = \frac{1}{2} \quad T(w_0) = \{0, 1\} \quad \|\|\| \quad \mathfrak{R}' : w'_0 \xrightarrow{R=1} w'_1 : p = \frac{1}{3} \quad T(w'_0) = \{0, 1/3, 1/2, 1\}$$

<footnote n="3">³As Gödel negation is expressible in $\mathcal{L}_{\Box, \Diamond}^\sim$ (Convention 1), $KG_{inv}$ is a conservative extension of $KG$ with $\sim$.</footnote>

<footnote n="4">⁴We use $\mathcal{P}_{<\omega}([0, 1])$ to denote the set of all finite subsets of $[0, 1]$.</footnote>
One can see that $v(\square p \wedge \diamond \sim p, w_0) = 1$ in $\mathfrak{N}$ which is impossible in $\mathbf{KG}_{\text{inv}}$-models. Furthermore, $\mathfrak{N}'$ is crisp but $v'(\square p \leftrightarrow \sim \diamond \sim p, w'_0) = 0$. By Proposition 1, this is impossible crisp in $\mathbf{KG}_{\text{inv}}$-models.
Let us now state the main result of the section.

**Theorem 1.**

1. $\phi$ is $\mathbf{KG}_{\text{inv}}$-valid iff it is F-valid on all finite models.

2. $\phi$ is $\mathbf{KG}_{\text{inv}}$-valid on crisp frames iff it is F-valid on all finite crisp models.

We adapt the proof of [14, Theorem 1]. We begin with some technical notions.

**Definition 4 (Generated models).**

• A frame $\tilde{\mathfrak{F}} = \langle \tilde{W}, \tilde{R} \rangle$ is a subframe of $\mathfrak{F} = \langle W, R \rangle$ if $\tilde{W} \subseteq W$ and $\tilde{R}$ is the restriction of $R$ on $\tilde{W}$.

• $\tilde{\mathfrak{M}} = \langle \tilde{W}, \tilde{R}, \tilde{v} \rangle$ is a submodel of $\mathfrak{M} = \langle W, R, v \rangle$ if $\langle \tilde{W}, \tilde{R} \rangle$ is a subframe of $\langle W, R \rangle$ and $\tilde{v}$ is the restriction of $v$ on $\tilde{W}$.

• $\tilde{\mathfrak{M}} = \langle \tilde{W}, \tilde{R}, \tilde{T}, \tilde{v} \rangle$ is a submodel of $\mathfrak{M} = \langle W, R, T, v \rangle$ if $\langle \tilde{W}, \tilde{R} \rangle$ is a subframe of $\langle W, R \rangle$ and $\tilde{v}$ and $\tilde{T}$ are the restrictions of $v$ and $T$ on $\tilde{W}$.

• $\tilde{\mathfrak{M}}$ is generated by $X \subseteq W$ if it is the smallest submodel containing $X$ s.t. if $w \in \tilde{W}$ and $wRw' > 0$, then $w' \in \tilde{W}$, as well.

**Convention 2.**

• A model $\mathfrak{M} = \langle W, R, v \rangle$ (or $\mathfrak{M} = \langle W, R, T, v \rangle$) is tree-like if $\langle W, R \rangle$ is a directed rooted tree.

• Given a tree-like model $\mathfrak{M}$, $\mathfrak{h}(\mathfrak{M})$ denotes its height.

First, we can establish the analogue of [14, Lemma 1]. We show that to verify the validity of a formula (with respect to $\mathbf{KG}_{\text{inv}}$-models and F-models), it suffices to consider only tree-like models of finite height. The proof is standard, so we omit it here.

**Lemma 1.** Let $\mathfrak{M} = \langle W, R, v \rangle$ and $\tilde{\mathfrak{M}} = \langle \tilde{W}, \tilde{R}, \tilde{v} \rangle$ be $\mathbf{KG}_{\text{inv}}$-models. Let further $\mathfrak{M}^F = \langle W^F, R^F, T, v^F \rangle$ and $\tilde{\mathfrak{M}}^F = \langle \tilde{W}^F, \tilde{R}^F, \tilde{T}, \tilde{v}^F \rangle$ be F-models. Then the following statements hold.

(a) If $\tilde{\mathfrak{M}}$ (resp., $\tilde{\mathfrak{M}}^F$) is a generated submodel of $\mathfrak{M}$ ($\tilde{\mathfrak{M}}$), then $\tilde{v}(\phi, w) = v(\phi, w)$ for all $w \in \tilde{W}$ (resp., $\tilde{v}^F(\phi, w) = v^F(\phi, w)$ for all $w \in \tilde{W}^F$) and $\phi \in \mathcal{L}_{\square, \diamond}$.

(b) For all $\phi \in \mathcal{L}_{\square, \diamond}$ and $w \in \mathfrak{M}$ ($w \in \mathfrak{M}^F$), there is a tree-like submodel $\tilde{\mathfrak{M}}$ of $\tilde{\mathfrak{M}}$ ($\tilde{\mathfrak{M}}^F$ of $\mathfrak{M}$) generated by $w$ s.t. $v(\phi, w) = \tilde{v}(\phi, w)$ ($v^F(\phi, w) = \tilde{v}^F(\phi, w)$) and $\mathfrak{h}(\tilde{\mathfrak{M}}) \le \ell(\phi)$.

(c) Let $g: [0, 1] \to [0, 1]$ be s.t. $g(0) = 0$, $g(1) = 1$, $g(1-x) = 1-g(x)$, and $x \le x'$ iff $g(x) \le g(x')^5$. Let further $\mathfrak{N} = \langle W_{\mathfrak{N}}, R_{\mathfrak{N}}, v_{\mathfrak{N}} \rangle$ (resp., $\mathfrak{N}^F = \langle W_{\mathfrak{N}}^F, R_{\mathfrak{N}}^F, T_{\mathfrak{N}}, v_{\mathfrak{N}}^F \rangle$) be s.t. $W_{\mathfrak{N}} = W$, $wR_{\mathfrak{N}}w' = g(wRw')$, and $v_{\mathfrak{N}}(p, w) = g(v(p, w))$ ($W_{\mathfrak{N}}^F = W^F$, $wR_{\mathfrak{N}}^Fw' = g(wR^Fw')$, $T_{\mathfrak{N}}(w) = g(T(w))$, $v_{\mathfrak{N}}^F(p, w) = g(v^F(p, w))$) for every $w, w' \in W$ ($w, w' \in W^F$) and $p \in \text{Prop}$. Then it holds that $v_{\mathfrak{N}}(\phi, w) = g(v(\phi, w))$ (resp., $v_{\mathfrak{N}}^F(\phi, w) = g(v^F(\phi, w))$) for every $\phi \in \mathcal{L}_{\square, \diamond}$ and $w \in W$ ($w \in W^F$).

We remark quickly that because of $\sim$, we need the underlined part of (c) that was not present in the original statement. Otherwise, we could have $g(\frac{1}{2}) = \frac{2}{3}$ which would fail (c) since $v_{\mathfrak{N}}(p \leftrightarrow \sim p, w) = 1$ if $v_{\mathfrak{N}}(p, w) = \frac{1}{2}$ but $v_{\mathfrak{N}}(p \leftrightarrow \sim p, w) = \frac{1}{3}$ since $v_{\mathfrak{N}}(p, w) = \frac{2}{3}$.

The next statements are analogous to [14, Lemmas 2 and 3].

**Lemma 2.** For any tree-like F-model $\mathfrak{M} = \langle W, R, T, v \rangle$ of finite height with root $x_0$ there is a tree-like $\mathbf{KG}_{\text{inv}}$-model $\tilde{\mathfrak{M}} = \langle \tilde{W}, \tilde{R}, \tilde{v} \rangle$ with root $\hat{x}_0$ s.t. $v(\phi, x_0) = \tilde{v}(\phi, \hat{x}_0)$ for each $\phi \in \mathcal{L}_{\square, \diamond}$. In addition, if $\mathfrak{M}$ is crisp, so is $\tilde{\mathfrak{M}}$.

<footnote n="5">⁵Observe that this, in particular, means that $x > x'$ implies $g(x) > g(x')$.</footnote>
**Proof.** The statement may be proven by induction on $\mathcal{H}(\mathfrak{M})$. The case in which $\mathcal{H}(\mathfrak{M}) = 0$ serves as basis, setting $\hat{W} = W$, $\hat{R} = \emptyset$, and $\hat{v} = v$; in this case, the statement follows trivially. As induction step, suppose that $\mathcal{H}(\mathfrak{M}) = n+1$. By the induction hypothesis, for each $y \in R(x_0)$, the submodel of $\mathfrak{M}$ generated by $\{y\}$ — the model $\mathfrak{M}_y = (W_y, R_y, v_y)$ — there is a $\mathbf{KG}_{\text{inv}}$ tree model $\widehat{\mathfrak{M}} = (\widehat{W}_y, \widehat{R}_y, \widehat{v}_y)$ such that $\hat{v}_y(\phi, \hat{y}) = v_y(\phi, y) = v(\phi, y)$.

Take $T(x_0) = \{\alpha_0, ..., \alpha_m\}$ and for each $k \in \mathbb{N}$, pick an order embedding $h_k: [0, 1] \to [0, 1]$ such that $h_k(0) = 0$, $h_k(1) = 1$, and $h(1-j) = 1-h(j)$ for all $j \in [0, 1]$ such that:

$$h_k(\alpha_i) = \alpha_i \text{ for all } i \le m \text{ and } k \in \mathbb{N}$$
$$h_k[(\alpha_i, \alpha_{i+1})] = (\alpha_i, \min(\alpha_i + 1/k, \alpha_{i+1})) \text{ for all } i \le m-1 \text{ and even } k \in \mathbb{N}$$
$$h_k[(\alpha_i, \alpha_{i+1})] = (\max(\alpha_i - 1/k, \alpha_{i+1}), \alpha_{i+1}) \text{ for all } i \le m-1 \text{ and odd } k \in \mathbb{N}$$

For each $y \in R(x_0)$ and $k \in \mathbb{N}$, there exists an F-model $\widehat{\mathfrak{M}}_y^k$ defined so that $\widehat{W}_y^k$ includes for each $\hat{x}_y \in \widehat{W}_y$ a point $\hat{x}_y^k$ with root $\hat{y}_y^k$ and for all $\hat{x}_y, \hat{z}_y$, and $\phi \in \mathcal{L}_{\square, \diamond}^{\sim}, \hat{x}_y^k, \hat{R}_y^k, \hat{z}_y^k = h_k(\hat{x}_y, \hat{R}_y, \hat{z}_y)$ and $\hat{V}_y^k(\psi, \hat{x}_y^k) = h_k(\hat{v}_y(\psi, \hat{x}_y))$. We can define a $\mathbf{KG}_{\text{inv}}$-tree-model $\widehat{\mathfrak{M}}$ where

$$\hat{W} = \bigcup_{y \in R(x_0)} \bigcup_{k \in \mathbb{N}} \hat{W}_y^k \cup \{\hat{x}_0\}$$
$$x \hat{R} z = \begin{cases} h_k(x_0 R y) & \text{if } x = \hat{x}_0 \text{ and } z = \hat{y}^k \text{ for some } y \in R(x_0) \text{ and } k \in \mathbb{N} \\ x \hat{R}_y^k z & \text{if } x, z \in \hat{W}_y^k \text{ for some } y \in R(x_0) \text{ and } k \in \mathbb{N} \\ 0 & \text{otherwise} \end{cases}$$
$$\hat{v}(p, x) = \begin{cases} v(p, x_0) & \text{if } x = x_0 \\ \hat{v}_y^k(p, x) & \text{if } x \in \hat{W}_y^k \text{ for some } y \in R(x_0) \text{ and } k \in \mathbb{N} \end{cases}$$

The induction hypothesis ensures that for each $\phi \in \mathcal{L}_{\square, \diamond}^{\sim}$ and $\hat{x}_y^k \in \hat{W}$ distinct from $\hat{x}_0, \hat{v}_y^k(\phi, \hat{x}_y^k) = \hat{v}(\phi, \hat{x}_y^k)$. What remains is then to prove that $\hat{v}(\phi, \hat{x}_0) = \hat{v}(\phi, x_0)$.

This is proven by induction on $\ell(\phi)$. In case $\phi$ is an atom, this follows by construction of $\hat{v}$. The non-modal connectives (including involutive negation) follow standardly. We consider the case of $\phi = \square \psi$.

Suppose that $\phi = \square \psi$. Then in case that $v(\square \psi, x_0) = 1$, for all $y \in R(x_0)$, $x_0 R y \le v(\psi, y)$, whence by Lemma 1, $v(\psi, y) = v_y(\psi, y) = \hat{v}_y(\psi, \hat{y})$. As for any $y$ $x_0 R y \le \hat{v}_y(\psi, \hat{y})$, it follows that for any $k$, $\hat{x}_0 \hat{R} \hat{y}^k \le \hat{v}_y^k(\psi, \hat{y}^k)$, entailing that $\hat{v}(\square \psi, \hat{x}_0) = 1$ as well. Suppose then that $v(\square \psi, x_0) = \alpha_i \ne 1$. Then for all $z \in W$, $x_0 R z \to_G v(\psi, z) \ge \alpha_i$ and by construction of the order embeddings, we get the important feature that for all $z \in \hat{W}$, $\hat{x}_0 \hat{R} z \to_G \hat{v}(\psi, z) \ge \alpha_i$. We consider two cases. In case there is a $y_0 \in W$ for which $x_0 R y \to_G v(\psi, y) = \alpha_i$, then $x_0 R y_0 > v(\psi, y_0) = \alpha_i$ and the order embeddings ensure that for all $k \in \mathbb{N}$, $\hat{x}_0 \hat{R} \hat{y}^k_0 > \hat{v}(\psi \hat{y}^k_0) = \alpha_i$. Otherwise, there must be some $y_0 \in W$ for which $x_0 R y_0 \to_G v(\psi, y_0) \in (\alpha_i, \alpha_{i+1})$. By construction of the order embeddings, for any $\varepsilon > 0$ there is some $k \in \mathbb{N}$ for which $h_k(x_0 R y_0 \to_G v(\psi, y_0)) = \hat{x}_0 \hat{R} \hat{y}^k_0 \to_G \hat{v}(\psi, \hat{y}^k_0) \in (\alpha_i, \alpha_i + \varepsilon)$. In either case, $\hat{v}(\square \psi, \hat{x}_0) = \alpha_i = v(\square \psi, x_0)$.

Finally, we note that if $\mathfrak{M}$ is crisp, so is each $\widehat{\mathfrak{M}}_y$ and thus so is each $\widehat{\mathfrak{M}}_y^k$, whence $\widehat{\mathfrak{M}}$ is crisp. $\square$

**Definition 5** (Fragments). A fragment is a set $\Sigma \subseteq \mathcal{L}_{\square, \diamond}^{\sim}$ s.t. it is closed under taking subformulas and $\{0, 1\} \subseteq \Sigma$. Now let $\mathcal{F}: \mathcal{L}_{\square, \diamond}^{\sim} \to \mathcal{L}_{\square, \diamond}^{\sim}$ be as follows:

$$\phi^{\mathcal{F}} = \begin{cases} \sim \phi & \text{if there is no } \xi \in \mathcal{L}_{\square, \diamond}^{\sim} \text{ such that } \phi = \sim \xi \\ \xi & \text{if there is a } \xi \in \mathcal{L}_{\square, \diamond}^{\sim} \text{ such that } \phi = \sim \xi \end{cases}$$
We say that $\Sigma \subseteq \mathcal{L}_{\square, \diamond}$ is an involutively closed fragment (ICF) if it is a fragment and for every $\phi, \chi \in \Sigma, \circ \in \{\wedge, \rightarrow\}$, and $\diamond \in \{\square, \diamond\}$, it holds that:

* if $\phi \in \Sigma$, then $\phi^{\mathcal{J}} \in \Sigma$;

* if $\phi \circ \chi \in \Sigma$, then $\{\phi^{\mathcal{J}} \circ \chi, \phi \circ \chi^{\mathcal{J}}, \phi^{\mathcal{J}} \circ \chi^{\mathcal{J}}\} \subseteq \Sigma$;

* if $\heartsuit\phi \in \Sigma$, then $\heartsuit\phi^{\mathcal{J}} \in \Sigma$.

Given an involutively closed fragment $\Sigma$, we define:

$$ \Sigma_{\square} = \{\square\phi \mid \square\phi \in \Sigma\} \qquad \Sigma_{\diamond} = \{\diamond\phi \mid \diamond\phi \in \Sigma\} \qquad \Sigma_{\text{Lit}} = \{l \mid l \in \Sigma \text{ and } l \text{ is a literal}\} $$

$$ \Sigma_{\square}^{\sim} = \{\sim\square\phi \mid \sim\square\phi \in \Sigma\} \qquad \Sigma_{\diamond}^{\sim} = \{\sim\diamond\phi \mid \sim\diamond\phi \in \Sigma\} $$

**Lemma 3.** Let $\Sigma$ be a finite ICF and $\mathfrak{M} = \langle W, R, v \rangle$ a tree-like $\mathbf{KG}_{\text{inv}}$-model of finite height with root $x_0$. Then there is a tree-like F-model $\tilde{\mathfrak{M}} = \langle \tilde{W}, \tilde{R}, \tilde{T}, \tilde{v} \rangle$ with root $x_0$ s.t. $\langle \tilde{W}, \tilde{R} \rangle \subseteq \langle W, R \rangle$, $|W| \le |\Sigma|^{\mathcal{h}(\mathfrak{M})}$, $|\tilde{T}(w')| \le |\Sigma|$, and $v(\phi, x_0) = \tilde{v}(\phi, x_0)$ for every $\phi \in \Sigma$ and $w' \in \tilde{\mathfrak{M}}$. In addition, if $\mathfrak{M}$ is crisp, so is $\tilde{\mathfrak{M}}$.

*Proof.* The statement may be proven by induction on $\mathcal{h}(\mathfrak{M})$. As the basis, letting $\tilde{W} = W, \tilde{R} = \emptyset, \tilde{v} = v$, and $\tilde{T}(x_0) = \{0, \frac{1}{2}, 1\}$ establishes the statement immediately.

As induction step, suppose that $\mathcal{h}(\mathfrak{M}) = n + 1$. For each $y \in R(x_0)$, we note that the submodel $\mathfrak{M}_y$ generated by $\{y\}$ is a $\mathbf{KG}_{\text{inv}}$ model with $\mathcal{h}(\mathfrak{M}_y) \le n$ and by induction hypothesis there exists an accompanying finite F-tree-model $\tilde{\mathfrak{M}}_y$ with root $y$ such that for all $\phi \in \Sigma$, $\tilde{v}_y(\phi, y) = v_y(\phi, y) = v(\phi, y)$. Additionally, by induction hypothesis, $|\tilde{W}_y| \le |\Sigma|^n$ and $|\tilde{T}_y(x)| \le |\Sigma| + 1$ for each $x \in \tilde{W}_y$. We build an appropriate finite F-model by selecting a set of appropriate $y \in R(x_0)$.

For a $\Delta \subseteq \mathcal{L}_{\square, \diamond}$ let $v_x[\Delta] = \{v(\phi, x) \mid \phi \in \Delta\}$; the set $v_{x_0}[\Sigma_{\square} \cup \Sigma_{\square}^{\sim} \cup \Sigma_{\diamond} \cup \Sigma_{\diamond}^{\sim}] \cup \{0, \frac{1}{2}, 1\}$ is a finite set $\{\alpha_1, \dots, \alpha_m\}$ closed under $1-x$ where if $i < j$ then $\alpha_i < \alpha_j$. For each $\square\phi \in \Sigma_{\square}$ such that $v(\square\phi, x_0) = \alpha_i < 1$ and $\alpha_j = 1 - \alpha_i$, fix points $y_{\square\phi}, y_{\sim\square\phi} \in R(x_0)$ for which $x_0Ry_{\square\phi} \rightarrow_G v(\phi, y) < \alpha_{i+1}$ and $x_0Ry_{\sim\square\phi} \rightarrow_G v(\phi, y_{\sim\phi}) < \alpha_{j+1}$. Similarly, for each $\diamond\phi \in \Sigma_{\diamond}$ such that $v(\diamond\phi, x_0) = \alpha_i > 0$ and $\alpha_j = 1 - \alpha_i$, fix points $y_{\diamond\phi}, y_{\sim\diamond\phi} \in R(x_0)$ such that $\min(x_0Ry_{\diamond\phi}, v(\phi, y_{\diamond\phi})) \ge \alpha_{i-1}$ and $\min(x_0Ry_{\sim\diamond\phi}, v(\phi, y_{\sim\diamond\phi})) \ge \alpha_{j-1}$. Then let $Y = \{y_{\psi} \mid \psi \in \Sigma_{\square} \cup \Sigma_{\square}^{\sim} \cup \Sigma_{\diamond} \cup \Sigma_{\diamond}^{\sim}\}$.

Now, define an F model $\tilde{\mathfrak{M}} = \langle \tilde{W}, \tilde{R}, \tilde{T}, \tilde{v} \rangle$ such that

$$ \tilde{W} = \bigcup_{y \in W} \tilde{W}_y \cup \{x_0\} \\ x \tilde{R}_z = \begin{cases} x_0 R_z & \text{if } x = x_0 \text{ and } z \in R(x_0) \\ x \tilde{R}_y z & \text{if } x, z \in \tilde{W}_y \text{ for some } y \in Y \\ 0 & \text{otherwise} \end{cases} \\ \tilde{T}(x) = \begin{cases} v_{x_0}[\Sigma_{\square} \cup \Sigma_{\square}^{\sim} \cup \Sigma_{\diamond} \cup \Sigma_{\diamond}^{\sim}] \cup \{0, \frac{1}{2}, 1\} & \text{if } x = x_0 \\ \tilde{T}_y(x) & \text{if } x \in \tilde{W}_y \text{ for some } y \in Y \end{cases} \\ \tilde{v}(p, x) = \begin{cases} v(p, x_0) & \text{if } x = x_0 \\ \tilde{v}_y(p, x) & \text{if } x \in \tilde{W}_y \text{ for some } y \in Y \end{cases} $$

Importantly, note that $\tilde{R}^+[x_0] = Y$ where $Y \subseteq R(x_0)$ and that for each $y \in Y$ and $\phi \in \mathcal{L}_{\square, \diamond}$, $x_0 \tilde{R}y = x_0 R y$ and $\tilde{v}(\phi, y) = v(\phi, y)$. Now, we prove that for all $\phi, \tilde{v}(\phi, x_0) = v(\phi, x_0)$ by induction on length of $\phi$. The atomic case follows by construction of $\tilde{v}$ and the non-modal connectives (including involutive negation) are standard. We thus prove the case in which $\phi = \square\psi$.
In case $v(\Box\psi, x_0) = 1$, for each $y \in R^+[x_0]$, $x_0Ry \to_G v(\psi, y) = 1$, whence for each such $y$, $x_0Ry \le v(\psi, y)$. As $\hat{R}^+[x_0] \subseteq R(x_0)$, the induction hypothesis ensures that $x_0\hat{R}y \to_G \hat{v}(\psi, y) = 1$ for all $y \in \hat{R}^+[x_0]$ whence, as $1 \in \hat{T}(x_0)$, $\hat{v}(\Box\psi, x_0) = 1$. In case $v(\Box\psi, x_0) = \alpha_i < 1$, by construction, $\alpha_i \in \hat{T}(x)$. Then for all $y \in \hat{W}$, $\alpha_i \le \inf\{x_0\hat{R}y \to_G \hat{v}(\psi, y) \mid y \in \hat{W}\}$. But given the choice of $y\Box\psi \in \hat{W}$, $x_0\hat{R}y\Box\psi \to_G \hat{v}(\psi, y\Box\psi) < \alpha_{i+1}$. Then by construction of $\hat{T}$, $\hat{v}(\Box\psi, x_0) = \alpha_i$. The case of $\Diamond\psi$ is similar.

Note, now, that $|\hat{W}| \le |Y| \cdot |\sigma|^n \le |\Sigma|^{n+1} = |\Sigma^{\mathcal{H}(\mathfrak{M})}|$ and that as $|\hat{T}(x_0)| \le |\Sigma_{\Box} \cup \Sigma_{\Box}^{\sim} \cup \Sigma_{\Diamond} \cup \Sigma_{\Box}^{\sim}| + 3$, $|\hat{T}(x_0)| \le |\Sigma| + 1$. Finally, as $\langle\hat{W}, \hat{R}\rangle \subseteq \langle W, R\rangle$, the new model inherits crispness. $\square$

Theorem 1 is now immediate from Lemmas 1, 2, and 3 as for any given $\phi$ there exists a finite ICF containing it.

We finish the section with a short remark. Note from the proof Lemma 3 that we could not have assumed a ‘global’ $T$ (i.e., that $T(w) = T(w')$ for every $w, w' \in \mathfrak{M}$). Indeed, we need to form $T(w)$’s according to the values of modal formulas in the corresponding states of the standard model. These values, however, are independent and thus, cannot be simulated by one $T$.

# 4 Tableaux

In Section 3, we used the result of [14] to obtain that $KG_{inv}$ has the finite model property with respect to F-models. This, however, does not give a decision algorithm. Thus, we will construct a tableaux calculus that allows us to extract countermodels from open branches and use it to define a decision procedure that takes polynomial space. In [28], tableaux for $KG$ are presented but they use the fact that all its connectives are order-based which is not the case for $\mathcal{L}_{\Box, \diamond}$. To incorporate $\sim$, we follow [22] and provide a constraint tableaux calculus. We begin by giving formal definitions of the needed notions. We will then explain them in further detail.

**Definition 6** (Structures and constraints). We fix countable sets WL = {$w, w', w_0, ...$} of state-labels and Var = {$c, d, e, c', ...$} of variables, define the set of T-symbols $T = \{t_i(w) \mid w \in WL, i \in \mathbb{N}\} \cup \{t_i^s(w) \mid w \in WL, i \in \mathbb{N}\} \cup \{\emptyset, 1\}$, and let $\nabla \in \{\leq, <, \geq, >, =\}$.

We define sets of labelled formulas (LF) and relational terms (RT) as follows:

$$ \text{LF} = \{w : \phi \mid w \in \text{WL}, \phi \in \mathcal{L}_{\Box, \diamond}^{\sim}\} \qquad \text{RT} = \{wRw' \mid w, w' \in \text{WL}\} $$

The set VT of value terms and Str of structures are defined as follows:

$$ VT \supset T ::= c \in \text{Var} \mid t \in T \mid \rho \in RT \mid 0 \mid 1 \mid 1 - T \qquad \text{Str} = VT \cup LF $$

Finally, constraints have the form $\Sigma \nabla T$ s.t. $\Sigma \in \text{Str}, T \in \text{VT}$.

**Definition 7** ($\mathcal{T}(KG_{inv})$ — tableaux for $KG_{inv}$). A tableau is a downward-branching tree whose nodes are constraints. Each branch can be extended by one of the rules listed below. We apply the following conventions: vertical bars denote branching; $\vee$, $\nabla \in \{\leq, <, \geq, >\}$, if $\nabla$ is $\leq$, then $\vee$ is $\geq$ and vice versa (likewise for $<$); $\triangleright \in \{\geq, >\}$, $\triangleleft \in \{\leq, <\}$; $c, w', t(w)$, and $t^s(w)$ are fresh on the branch; $wRu$ occurs on the branch.

$$ \sim : \frac{w : \sim \phi \nabla T}{w : \phi \triangleleft 1 - T} $$

$$ \wedge_{\triangleright} : \frac{w : \phi \wedge \chi \triangleright T}{w : \phi \triangleright T} $$

$$ \wedge_{\triangleleft} : \frac{w : \phi \wedge \chi \triangleleft T}{w : \phi \triangleleft T \mid w : \chi \triangleleft T} $$
$$ \rightarrow_{\succ} : \frac{w : \phi \rightarrow \chi \triangleright \mathbb{T}}{w : \chi \triangleright \mathbb{T} \mid \begin{array}{l} \mathbb{T} \triangleleft 1 \\ w : \chi \geq c \\ w : \phi \leq c \end{array}} $$

$$ \rightarrow_{\prec} : \frac{w : \phi \rightarrow \chi \leq \mathbb{T}}{1 \leq \mathbb{T} \mid \begin{array}{l} w : \chi \leq \mathbb{T} \\ w : \phi \geq c \\ w : \chi < c \end{array}} $$

$$ \rightarrow_{<} : \frac{w : \phi \rightarrow \chi < \mathbb{T}}{w : \chi < \mathbb{T} \mid \begin{array}{l} w : \phi \geq c \\ w : \chi < c \end{array}} $$

$$ \Box_{\succ} : \frac{w : \Box \phi \triangleright \mathbb{T}}{w : \Box \phi = 1 \mid \begin{array}{l} w : \Box \phi = t(w) \\ \mathbb{T} \triangleleft t(w) \\ 1 \triangleright \mathbb{T} \end{array}} \quad \Box_{\prec} : \frac{w : \Box \phi \leq \mathbb{T}}{1 \leq \mathbb{T} \mid \begin{array}{l} \mathbb{T} \geq t(w) \\ w' : \phi > w R w' \\ w' : \phi < t^s(w) \end{array}} $$

$$ \Box_{<} : \frac{w : \Box \phi < \mathbb{T}}{\mathbb{T} > t(w) \mid \begin{array}{l} w' : \phi > w R w' \\ w' : \phi < t^s(w) \end{array}} $$

$$ \Box_{>}: \frac{w : \Box \phi > \mathbb{T}}{\mathbb{T} < t^s(w) \mid \begin{array}{l} w R w' > t(w) \\ w' : \phi > t(w) \end{array}} $$

$$ \Diamond_{\prec} : \frac{w : \Diamond \phi \triangleleft \mathbb{T}}{w : \Diamond \phi = 0 \mid \begin{array}{l} w : \Diamond \phi = t^s(w) \\ t^s(w) \triangleleft \mathbb{T} \\ w R w' > t(w) \\ w' : \phi > t(w) \end{array}} $$

$$ \Diamond_{\succ} : \frac{w : \Diamond \phi \geq \mathbb{T}}{\mathbb{T} \leq 0 \mid \begin{array}{l} \mathbb{T} \leq t^s(w) \\ w R w' > t(w) \\ w' : \phi > t(w) \end{array}} $$

$$ \Diamond_{>}: \frac{w : \Diamond \phi > \mathbb{T}}{\mathbb{T} < t^s(w) \mid \begin{array}{l} w R w' > t(w) \\ w' : \phi > t(w) \end{array}} $$

$$ \Box_{=} : \frac{w : \Box \phi = \mathbb{T}}{u : \phi \geq \mathbb{T} \mid \begin{array}{l} u : \phi < \mathbb{T} \\ u : \phi \leq w R u \end{array}} $$

$$ \Box_{=} : \frac{w : \Diamond \phi = \mathbb{T}}{w R u \leq \mathbb{T} \mid \begin{array}{l} u : \phi \leq \mathbb{T} \\ w R u > \mathbb{T} \end{array}} $$

Let $\mathcal{B} = \{c_1, \dots, c_n\}$ be a branch with constraints $c_1, \dots, c_n$ and let further, $e^t$ be the result of replacing every $\mathbb{T} \in \text{VT}$ and $\lambda \in \text{LF}$ with variables $x_{\mathbb{T}}$ and $x_{\lambda}$, respectively, and every $\mathfrak{n} \in \{0, 1\}$ with $\mathfrak{n} \in \{0, 1\}$. Furthermore, for every $w \in \text{WL}$ occurring on $\mathcal{B}$, we set

$$ \mathbb{T}(w) = \{t(w) \mid t(w) \text{ is on } \mathcal{B}\} \cup \{t^s(w) \mid t^s(w) \text{ is on } \mathcal{B}\} \cup \{\mathfrak{n} \mid \exists \phi \ w : \phi = \mathfrak{n} \in \mathcal{B}\} $$

and define $\mathcal{B}$ to be closed iff the following system of inequalities

$$ \{e_1^t, \dots, e_n^t\} \cup \{x_{t(w)} < x_{t^s(w)} \mid t(w) \text{ and } t^s(w) \text{ occur on } \mathcal{B}\} $$

does not have a solution over $[0, 1]$ s.t. for every $w \in \text{WL}$, the following properties hold:

$$ \begin{align} \mathbb{T}(w) = \{t(w), t^s(w)\} &\Rightarrow \left[ \begin{array}{l} x_{t(w)} = 0 \ \& \ x_{t^s(w)} = \frac{1}{2} \\ x_{t(w)} = \frac{1}{2} \ \& \ x_{t^s(w)} = 1 \end{array} \right. \text{ or } \nonumber \\ |\mathbb{T}(w)| \ge 3 &\Rightarrow \left[ \begin{array}{l} \forall \mathbf{t} \in \mathbb{T}(w) \ \exists \mathbf{t}' \in \mathbb{T}(w) : x_{\mathbf{t}} = 1 - x_{\mathbf{t}'} \text{ and} \\ \exists \mathbf{t}_1, \mathbf{t}_2, \mathbf{t}_3 : x_{\mathbf{t}_1} = 0 \ \& \ x_{\mathbf{t}_2} = \frac{1}{2} \ \& \ x_{\mathbf{t}_3} = 1 \end{array} \right] \nonumber \\ \neg \exists t(w), t^s(w), t'(w) : x_{t(w)} < x_{t'(w)} < x_{t^s(w)} \tag{5} \end{align} $$

A branch is *open* if it is not closed. A branch $\mathcal{B}$ is *complete* when for every premise of any rule occurring on $\mathcal{B}$, its conclusion also occurs in $\mathcal{B}$. The only exceptions are branches containing constraints $w : \phi < \mathbb{T}$ and $w : \phi < 1$ or $w : \phi > \mathbb{T}$ and $w : \phi > 0$. In this case, the rules are applied to the constraints containing $\mathbb{T}$, not 0 and 1.

Finally, $\phi \in \mathcal{L}_{\Box, \Diamond}^{\sim}$ has a $\mathcal{T}(\mathbf{K}\mathbf{G}_{\text{inv}})$ proof if there is a tableau beginning with $w : \phi < 1$ s.t. all its branches are closed.
**Definition 8** (Model realising a branch). Let $\mathfrak{M} = \langle W, R, T, v \rangle$ be an F-model and $\mathcal{B}$ a tableau branch. An $\mathfrak{M}$-realisation of $\mathcal{B}$ is a map $rl: WL \cup Str \to W \cup [0, 1]$ s.t. $rl(w) \in W$ and $rl(\Sigma) \in [0, 1]$ for every $\Sigma \in Str$ and $w \in WL$ occurring on $\mathcal{B}$, and the following properties hold:

1. $rl(\emptyset) = 0$ and $rl(1) = 1$;

2. $rl(wRw') = rl(w)Rrl(w')$;

3. if $rl(T) = x$, then $rl(1-T) = 1-x$ for every $T \in VT$;

4. $T(rl(w)) = \{rl(t) \mid t \in T(w)\} \cup \{0, \frac{1}{2}, 1\}$ and $rl(t(w)) < rl(t^s(w))$ for all $w \in WL$;

5. there are no $t'(w), t(w)$, and $t^s(w)$ on $\mathcal{B}$ s.t. $rl(t(w)) < rl(t'(w)) < rl(t^s(w))$;

6. if $T(w) = \{t(w), t^s(w)\}$, then $\frac{1}{2} \in \{rl(t(w)), rl(t^s(w))\}$;

7. if $|T(w)| \ge 3$, then for each $t \in T(w)$ on $\mathcal{B}$, there is $t' \in T(w)$ on $\mathcal{B}$ s.t. $rl(t) = 1-rl(t')$, and there are $t_1, t_2, t_3 \in T(w)$ s.t. $rl(t_1) = 0, rl(t_2) = \frac{1}{2}$, and $rl(t_3) = 1$.

A constraint $w: \phi \triangleright T$ is realised by $\mathfrak{M}$ under $rl$ if $v(\phi, rl(w)) \triangleright rl(T)$. A constraint $T \triangleright T'$ is realised by $\mathfrak{M}$ under $rl$ if $rl(T) \triangleright rl(T')$. $\mathcal{B}$ is realised by $\mathfrak{M}$ under $rl$ if $rl$ realises all constraints occurring on $\mathcal{B}$.

Note that each application of a modal rule to a structure $w: \square\phi$ or $w: \diamond\chi$ that introduces a witnessing state $w'$ to the branch also produces two value terms: $t(w)$ and $t^s(w)$. Each pair of such terms denotes the two consecutive elements of $T(w)$ between which $v(\phi, w')$ lies. Note also that to guarantee the soundness of such rules, we demand (cf. items 4 and 5 in Definition 8) that the intervals do not overlap in a non-trivial way. I.e., we prohibit the situations such as $rl(t_0(w)) < rl(t_1(w)) < rl(t_1^s(w)) < rl(t_0^s(w))$. On the other hand, the intervals can coincide if this does not contradict other constraints on the branch.

For $\square$ rules, this condition guarantees that the introduced $t(w)$ is indeed the maximal member of $T(w)$ that is still less or equal to the 'real' value of $\square\phi$ according to the standard semantics. Dually, for $\diamond$ rules, the condition ensures that the introduced $t^s(w)$ is the minimal member of $T(w)$ that is greater or equal to the value of $\diamond\phi$ according to the standard semantics.

Let us now look at how the tableau proofs work. In the next example, we provide a failed tableau proof of $\square p \rightarrow \sim\diamond\sim p$ and show how to read off countermodels from complete open branches.

*Example 3.* Cf. Fig. 2. The tableau has three closed branches marked with $\times$ and a complete open branch marked with $\ominus$. Let us check the closure of branches. In the leftmost branch, we use the fact that $rl(t(w)) \in [0, 1]$. Steps **17** and **20** directly contradict each other. In the rightmost branch, we use that the values of $t(w)$'s should be closed under $1-x$. Namely, we have that $t_0(w) > 0$ (otherwise, it would contradict $c \le t_0(w)$ and $w: \sim\diamond\sim p < c$). Hence, the values of $t(w)$'s are ordered as follows: $t_1(w), t_1^s(w), t_0(w), t_0^s(w)$. As $\emptyset$ and $1$ do not occur on the branch, we have either (I) $t_1(w) = 0, t_1^s(w) = t_0(w) = \frac{1}{2}, t_0^s(w) = 1$ or (II) $t_0(w) = 0, t_0^s(w) = t_1(w) = \frac{1}{2}, t_1^s(w) = 1$. Observe, however, that $t_1^s(w) = t_0(w) = \frac{1}{2}$ in (I) would contradict **16** and **22**, and $t_0(w) = 0$ in (II) would contradict **4** and **16**.

Thus, $w': p \ge t_0(w)$ and $w': p < 1-t_1(w)$ cannot be realised at the same time.

Let us now discuss how to construct a realising model of the open branch $\ominus$. We note quickly that in the general case, each complete open branch can produce uncountably many models because constraints give order relations, not precise values.<fnref n="6" /> Thus, we will provide just one example of a countermodel.

Observe that $t(w) < wRw' \le v(p, w') < 1$. As there are no other constraints on $t(w)$ and $t^s(w)$, we put $rl(t(w)) = 0, rl(t^s(w)) = \frac{1}{2}$, and $rl(1) = 1$. We now choose any value between 0 and 1 for $v(p, w')$ and set $wRw' = v(p, w')$ as the inequality is not strict. A countermodel can be seen in Fig. 2. Using Definition 3, we see that $v(\square p, w) = 1$ and $v(\sim\diamond\sim p, w) = \frac{1}{2}$ which falsifies $\square p \rightarrow \sim\diamond\sim p$ at $w$.

We are now ready to show the soundness and completeness of our tableaux calculus.

<footnote n="6">⁶Note that this is not a problem from the practical standpoint as systems of linear inequalities over reals often have uncountably many solutions. Yet, they are algorithmically solvable.</footnote>
<figure><img src="image_2.png" /><figcaption>Figure 2: A failed $\mathcal{T}(\mathbf{K}\mathbf{G}_{\text{inv}})$ proof of $\Box p \rightarrow \sim\Diamond\sim p$ and a model of the open branch (marked with $\odot$).</figcaption></figure>

**Theorem 2.** $\phi \in \mathcal{L}_{\Box, \Diamond}^{\sim}$ is $\mathbf{K}\mathbf{G}_{\text{inv}}$-valid iff it has a $\mathcal{T}(\mathbf{K}\mathbf{G}_{\text{inv}})$ proof.

*Proof.* The proof is standard and follows [28, Theorems 6.19 and 6.21], so we only give a sketch thereof. For the soundness part, we show that if a tableau beginning with $w : \phi < 1$ is closed, then $\phi$ is $\mathbf{K}\mathbf{G}_{\text{inv}}$-valid. We show that if $\mathfrak{M}$ realises the premises of a rule, then it should also realise at least one of its conclusions (note that branching rules have two conclusions). The soundness will follow since there is no F-model $\mathfrak{M}$ and realisation $rl$ s.t. $\mathfrak{M}$ realises a closed branch $\mathcal{B}$ under $rl$.

We consider the case of the $\Box \le$ rule as an example. Let $\mathfrak{M} = \langle W, R, T, v \rangle$ realise $w : \Box \phi \le T$. If $rl(T) = 1$, then $1 \le T$ (the left conclusion) is realised. Consider the case where $rl(T) < 1$. Then (cf. Definition 3) $\max\{x \in T(w) \mid x \le \inf_{w' \in W} \{rl(w)Rw' \rightarrow_G v(\phi, w')\}} \le rl(T)$. This means that there is a state $w'$ s.t. $v(\phi, w') < wRw'$ and there are $x, x' \in T(w)$ s.t. $x'$ is the immediate successor of $x$, $v(\Box\phi, w) = x$, and $v(\phi, w') < x'$. Now setting $rl(t(w)) = x$, $rl(t^s(w)) = x'$, and $rl(w') = w'$, we have that $t(w) \le T$ and $w' : \phi < t^s(w)$ are realised. Hence, the right conclusion is realised.

For the completeness part, we prove that for every complete open branch, there is an F-model $\mathfrak{M}$ and a realisation $rl$ s.t. $\mathfrak{M}$ realises $\mathcal{B}$ under $rl$. Let $\mathcal{B}$ be a complete open branch and consider the system of inequalities $\mathcal{B}^t$ as shown in (5) and its solution as specified in Definition 7. Now define $\mathfrak{M}$ as follows: $W = \{w \mid w \text{ occurs in } \mathcal{B}\}$, $wRw' = x_{wRw'}$, $T(w) = \{x_{t(w)} \mid t(w) \text{ occurs in } \mathcal{B}\} \cup \{x_{t^s(w)} \mid t^s(w) \text{ occurs in } \mathcal{B}\} \cup \{0, \frac{1}{2}, 1\}$ and $v(p, w) = x_{w:p}$ for every $w, w'$, and $p \in \text{Prop}$ occurring in $\mathcal{B}$. We also define $rl(w) = w$, $rl(T) = x_T$, and $rl(w : \chi) = x_{w:\chi}$ for every $w \in \text{WL}$, $T \in \text{VT}$, and $w : \chi \in \text{LF}$ occurring on $\mathcal{B}$. It remains to show that all constraints are realised by $\mathfrak{M}$ under $rl$.

For all constraints of the form $T \triangleright T'$ that do not contain labelled formulas, we have $rl(T) \triangleright rl(T')$ by the construction of $\mathfrak{M}$ since $\mathcal{B}$ is a complete open branch. Let us now show that all constraints $u : \psi \triangleright T$
on $\mathcal{B}$ are realised. We proceed by induction on formulas. Constraints of the form $w : p \nabla T$ are realised by construction of $\mathfrak{M}$. The cases of constraints whose principal connective is $\sim$, $\wedge$, or $\to$ can be shown by simple applications of the induction hypothesis.

Let us consider the case of $w : \Box \phi \leq T$ as an example and show that $v(\Box\phi, w) \leq rl(T)$. Since $w : \Box\phi \leq T$ is in $\mathcal{B}$ and $\mathcal{B}$ is complete and open, then it also contains (a) $1 \leq T$ or (b) $t(w) \leq T$, $w' : \phi < wRw'$, and $w' : \phi < t^s(w)$. If (a) is the case, $T$ is a value term (observe from Definition 6 that constraints can contain at most one labelled formula), whence $1 \leq T$ is realised by the construction of $\mathfrak{M}$. Thus, $rl(T) = 1$ and $v(\Box\phi, w) \leq rl(T)$, as required. If (b) is the case, then by the induction hypothesis $t(w) \leq T$, $w' : \phi < wRw'$, and $w' : \phi < t^s(w)$ are realised, whence, $v(\phi, w') < wRw'$, $x_{t(w)} \leq rl(T)$, and $v(\phi, w') < x_{t^s(w)}$ with $\{x_{t(w)}, x_{t^s(w)}\} \subseteq T(w)$ and $x_{t^s(w)}$ being the immediate successor of $x_{t(w)}$. But in this case, it is clear that $v(\Box\phi, w) = \max\{x \in T(w) \mid x \leq \inf_{w' \in W} \{wRw' \to_G v(\phi, w')\}} \leq x_{t(w)}$, whence, $v(\Box\phi, w) \leq rl(T)$, as required. $\Box$

# 5 Complexity

Let us now use $\mathcal{T}(\mathbf{KG}_{\text{inv}})$ to obtain the PSPACE-completeness of $\mathbf{KG}_{\text{inv}}$. Our proof adapts the standard algorithm for $\mathbf{K}$ from [7].

**Theorem 3.** Validity of $\mathbf{KG}_{\text{inv}}$ is PSPACE-complete.

*Proof.* PSPACE-hardness is immediate since $\mathbf{KG}$ is PSPACE-hard [15, Theorem 21] and $\mathbf{KG}_{\text{inv}}$ is a conservative extension of $\mathbf{KG}$. Let us now tackle the upper bound.

First of all, we observe that all tableaux terminate. Indeed, the branching factor of rules is at most 2, and every rule except for $\Box \vdash$ and $\Diamond \vdash$ reduces the number of connectives in the labelled formula in the premise. If $\Box \vdash$ or $\Diamond \vdash$ is applied, then $w : \Box\phi = t(w)$ or $w : \Diamond\phi = t^s(w)$, respectively, is introduced to which one can apply $\Box =_=$ or $\Diamond =_=$ which does decompose the formula. Thus, at some point, all formulas will be decomposed into atoms. We note, moreover, that given a branch $\mathcal{B}$, it takes us nondeterministic polynomial time to find a solution to $\mathcal{B}^t$ over $[0, 1]$ s.t. (5) holds with respect to it.

Let us now provide a decision procedure that uses only polynomial space with respect to $\ell(\phi)$. We aim to build the model realising $w_1^0 : \phi < 1$ ‘on the fly’ (in which case, $\phi$ is not valid) or to show that it is impossible. Fig. 3 illustrates the process of building the model. As one sees, we *do not* build model branch-by-branch but rather generate all children of a given node, then pick one child, and again, generate all its children. This is because we need to apply rules $\Box =_=$ and $\Diamond =_=$ using generated states *all at once*. But these rules can be applied *only after* $\Box \vdash$ and $\Diamond \vdash$.

We begin with $w_1^0 : \phi < 1$. In what follows, if a rule introduces branching to the tableau, we pick one branch, say, $\mathcal{B}$, and work with it depth-first. If the branch with which we are working is closed, we delete it and choose the next one. First, we apply propositional rules. Then we apply modal rules for constraints containing $\leq$ or $<$. This adds new states $w_{1,1}^1, \dots, w_{n_1^0,1}^1$ (we will call them *children* of $w_1^0$), new members of $T(w_1^0)$ of the form $t_i(w_1^0), t_i^s(w_1^0), \emptyset$, and $1$, relational terms $w_1^0 R w_{i,1}^1$, and new constraints of the form $\Box\chi = t_i(w_1^0)$ or $\Diamond\chi = t_i^s(w_1^0)$ for $i \in \{1, \dots, n_1^0\}$. Note that $n_1^0 = \mathcal{O}(\ell(\phi))$, whence, we need only $\mathcal{O}(\ell(\phi))$ space to store the ‘content’ of $w_1^0$.

If $\mathcal{B}$ is still open, mark $w_{1,1}^1$ as ‘active’ and apply all rules for constraints of the form $\Box\chi = t_i(w_1^0)$ and $\Diamond\chi = t_i^s(w_1^0)$ using $w_{1,1}^1$ in the conclusion. Note that $\Box =_=$ and $\Diamond =_=$ are the only modal rules that can become applicable after the application of $\Box \vdash$ and $\Diamond \vdash$. Once all $\Box =_=$ and $\Diamond =_=$ rules are applied, we apply the propositional rules to formulas labelled with $w_{1,1}^1$. We then apply modal rules for constraints
<figure><img src="image_3.png" /><figcaption>Figure 3: Building the model on the fly: red states are active; green states are safe.</figcaption></figure>

with $\le$ and $<$. As on the previous stage, we generate new states $w_{1,1}^2, \dots, w_{n_2^2,1}^2$, constraints of the form $\Box \chi = t_i(w_{1,1}^1)$ or $\Diamond \chi = t_i^s(w_{1,1}^1)$, and members of $\mathcal{T}(w_{1,1}^1)$ and relational terms corresponding to them. We repeat the procedure until we produce a state $w_{1,1}^m$ s.t. all constraints $w_{1,1}^m : \chi \nabla \mathcal{T}$ are atomic. If the branch is not closed, we mark $w_{1,1}^m$ as ‘safe’, delete all $w_{1,1}^m : \chi \nabla \mathcal{T}$’s and go to $w_{2,1}^m$ and repeat the procedure. Once all states $w_{1,1}^m, \dots, w_{n_m^m,1}^m$ are marked as ‘safe’, we delete constraints containing them, mark $w_{1,1}^{m-1}$ as ‘safe’, and delete all its children. Then we proceed to $w_{2,1}^{m-1}$. The procedure is repeated until either all tableau branches are closed (which means that $\phi$ is valid) or $w_1^0$ is marked as ‘safe’ (and thus, we have a complete open branch, whence, $\phi$ is not valid).

Note that the length of the branch of the constructed model is bounded from above by the modal depth of $\phi$ and is thus $\mathcal{O}(\ell(\phi))$. In addition, each state of the branch of the model can have at most $\mathcal{O}(\ell(\phi))$ children because their number is bounded from above by the number of modalities on the same level of nesting. Thus, we have to store $\mathcal{O}((\ell(\phi))^2)$ states each of which contains constraints taking up to $\mathcal{O}(\ell(\phi))$ space. Thus, our decision procedure utilises $\mathcal{O}((\ell(\phi))^3)$ space. $\square$

# 6 Conclusion

We presented an expansion of the Gödel modal logic with the involutive negation and showed how one can use it to formalise reasoning about uncertainty. We also constructed an alternative semantics for KG$_{inv}$ following [14, 15] with respect to which KG$_{inv}$ has the finite model property. We then used these semantics to provide the tableaux calculus $\mathcal{T}(KG_{inv})$ that allows us to read off finite countermodels from complete open branches. Finally, we proved PSPACE-completeness of KG$_{inv}$-validity using $\mathcal{T}(KG_{inv})$.

Our next steps are as follows. First, we want to continue the systematic study of KG$_{inv}$. In particular, we plan to provide a complete Hilbert-style axiomatisation of KG$_{inv}$ over crisp and fuzzy frames. This will help investigate the correspondence between the classes of crisp and fuzzy frames on the one side
and the $\mathcal{L}_{\square, \diamond}$-formulas that define these classes of frames, on the other. Furthermore, in [23, 24], hypersequent calculi for $\square$- and $\diamond$-fragments of KG are presented. Since these calculi are cut-free, they can serve as a syntactical decision procedure (i.e., the one that does not directly produce a countermodel) for the fragments of KG. It thus makes sense to construct hypersequent cut-free calculi for the bi-modal KG and its expansions and obtain an alternative, syntactical, decision procedure for KG.

Second, in [4, 5, 6], we considered $KG^2$ — an expansion of KG with a so-called ‘strong negation’ from [30] with semantics defined on $[0, 1]^{\square}$ — a bi-lattice product of $[0, 1]$ with itself. In particular, it was shown that a class of frames is $KG^2$-definable iff it is KG-definable by a self-dual formula (i.e., a formula equivalent to the negation of the result of replacing every connective with its dual: $\wedge$ with $\vee$, $\to$ with $\prec$, and $\sqcap$ with $\diamond$). Note, however, that $KG^2$ does not introduce connectives defined w.r.t. the second order on $[0, 1]^{\square}$. On the other hand, in [29], it is shown that the modal logic on $\{0, 1\}^{\square}$ in the language with all bi-lattice connectives and modalities and the bi-modal classical modal logic have the same expressivity. It would be thus instructive to consider a full bi-lattice expansion of $KG^2$ with semantics on $[0, 1]^{\square}$ and compare its expressivity to KG and its expansions.

## References

[1] J.P. Aguilera, M. Diéguez, D. Fernández-Duque & B. McLean (2022): *Time and Gödel: Fuzzy Temporal Reasoning in PSPACE*. In: Logic, Language, Information, and Computation, Lecture notes in computer science 13368, Springer International Publishing, Cham, pp. 18–35, doi:10.1007/978-3-031-15298-6_2.

[2] J.P. Aguilera, M. Diéguez, D. Fernández-Duque & B. McLean (2022): *A Gödel Calculus for Linear Temporal Logic*. In: Proceedings of the 19th International Conference on Principles of Knowledge Representation and Reasoning, pp. 2–11, doi:10.24963/kr.2022/1.

[3] M. Baaz (1996): *Infinite-valued Gödel logics with 0-1-projections and relativizations*. In: Gödel’96: Logical foundations of mathematics, computer science and physics—Kurt Gödel’s legacy, Brno, Czech Republic, August 1996, proceedings, Association for Symbolic Logic, pp. 23–33.

[4] M. Bílková, S. Frittella & D. Kozhemiachenko (2022): *Paraconsistent Gödel Modal Logic*. In: Automated Reasoning, Lecture notes in computer science 13385, Springer International Publishing, Cham, pp. 429–448, doi:10.1007/978-3-031-10769-6_26.

[5] M. Bílková, S. Frittella & D. Kozhemiachenko (2023): *Crisp bi-Gödel modal logic and its paraconsistent expansion*. Logic Journal of the IGPL, doi:10.1093/jigpal/jzad017.

[6] M. Bílková, S. Frittella & D. Kozhemiachenko (2025): *Fuzzy bi-Gödel modal logic and its paraconsistent relatives*. Journal of Logic and Computation 35(2), doi:10.1093/logcom/exae011.

[7] P. Blackburn, M. de Rijke & Y. Venema (2010): *Modal logic*, 4th edition. Cambridge tracts in theoretical computer science 53, Cambridge University Press.

[8] F. Bobillo, M. Delgado, J. Gómez-Romero & U. Straccia (2009): *Fuzzy description logics under Gödel semantics*. International Journal of Approximate Reasoning 50(3), pp. 494–514, doi:10.1016/j.jcss.2017.03.012.

[9] F. Bobillo, M. Delgado, J. Gómez-Romero & U. Straccia (2012): *Joining Gödel and Zadeh fuzzy logics in fuzzy description logics*. International Journal of Uncertainty Fuzziness and Knowledge-Based Systems 20(04), pp. 475–508, doi:10.1142/S0218488512500249.

[10] S. Borgwardt (2014): *Fuzzy Description Logics with General Concept Inclusions*. Ph.D. thesis, Technische Universität Dresden, Dresden.

[11] S. Borgwardt, F. Distel & R. Peñaloza (2014): *Decidable Gödel description logics without the finitely-valued model property*. In: Fourteenth International Conference on the Principles of Knowledge Representation and Reasoning, pp. 228–237, doi:10.5555/3031929.3031959.
[12] S. Borgwardt, F. Distel & R. Peñaloza (2014): *Gödel description logics with general models*. In: DL 2014: Informal Proceedings of the 27th International Workshop on Description Logics, Vienna, Austria, July 17–20, 2014, 1193, CEUR, pp. 391–403.

[13] S. Borgwardt & R. Peñaloza (2017): *Algorithms for reasoning in very expressive description logics under infinitely valued Gödel semantics*. International Journal of Approximate Reasoning 83, pp. 60–101, doi:10.1016/j.ijar.2016.12.014.

[14] X. Caicedo, G. Metcalfe, R. Rodríguez & J. Rogger (2013): *A finite model property for Gödel modal logics*. In L. Libkin, U. Kohlenbach & R. de Queiroz, editors: *International Workshop on Logic, Language, Information, and Computation, Lecture Notes in Computer Science* 8071, Springer, Berlin, Heidelberg, pp. 226–237, doi:10.1007/978-3-642-39992-3_20.

[15] X. Caicedo, G. Metcalfe, R. Rodríguez & J. Rogger (2017): *Decidability of order-based modal logics*. Journal of Computer and System Sciences 88, pp. 53–74, doi:10.1016/j.jcss.2017.03.012.

[16] X. Caicedo & R.O. Rodriguez (2010): *Standard Gödel modal logics*. Studia Logica 94(2), pp. 189–214, doi:10.1007/s11225-010-9230-1.

[17] X. Caicedo & R.O. Rodríguez (2015): *Bi-modal Gödel logic over [0,1]-valued Kripke frames*. Journal of Logic and Computation 25(1), pp. 37–55, doi:10.1093/logcom/exs036.

[18] M.E. Coniglio, F. Esteva, J. Gispert & L. Godo (2021): *Degree-preserving Gödel logics with an involu-tion: Intermediate logics and (ideal) paraconsistency*. In O. Arieli & A. Zamansky, editors: *Arnon Avron on Semantics and Proof Theory of Non-Classical Logics, Outstanding contributions to logic* 21, Springer International Publishing, Cham, pp. 107–139, doi:10.1007/978-3-030-71258-7_6.

[19] R. Ertola, F. Esteva, T. Flaminio, L. Godo & C. Noguera (2015): *Paraconsistency properties in degree-preserving fuzzy logics*. Soft Computing 19(3), pp. 531–546, doi:10.1007/s00500-014-1489-0.

[20] F. Esteva, L. Godo, P. Hájek & M. Navara (2000): *Residuated fuzzy logics with an involutive negation*. Archive for Mathematical Logic 39(2), pp. 103–124, doi:10.1007/s001530050006.

[21] R. Goré (2000): *Dual Intuitionistic Logic Revisited*. In R. Dyckhoff, editor: *Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2000, Lecture notes in computer science* 1847, Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 252–267, doi:10.1007/10722086_21.

[22] R. Hähnle (1994): *Many-valued logic and mixed integer programming*. Annals of Mathematics and Artificial Intelligence 12(3-4), pp. 231–263, doi:10.1007/BF01530787.

[23] G. Metcalfe & N. Olivetti (2009): *Proof systems for a Gödel modal logic*. In: *International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Lecture Notes in Artificial Intelligence* 5607, Springer, pp. 265–279, doi:10.1007/978-3-642-02716-1_20.

[24] G. Metcalfe & N. Olivetti (2011): *Towards a Proof Theory of Gödel Modal Logics*. Logical Methods in Computer Science 7(2), doi:10.2168/LMCS-7(2:10)2011.

[25] C. Rauszer (1974): *A Formalization of The Propositional Calculus of H-B Logic*. Studia Logica 33, pp. 23–34.

[26] R.O. Rodriguez, O.F. Tuyt, F. Esteva & L. Godo (2022): *Simplified Kripke semantics for K45-like Gödel modal logics and its axiomatic extensions*. Studia Logica 110(4), pp. 1081–1114, doi:10.1007/s11225-022-09987-0.

[27] R.O. Rodriguez & A. Vidal (2021): *Axiomatization of Crisp Gödel Modal Logic*. Studia Logica 109, pp. 367–395, doi:10.1007/s11225-020-09910-5.

[28] J. Rogger (2016): *Decidability of Order-Based Modal Logics*. Ph.D. thesis, University of Bern.

[29] S.O. Speranski (2022): *Modal Bilattice Logic and its Extensions*. Algebra and Logic 60(6), pp. 407–424, doi:10.1007/s10469-022-09667-x.

[30] H. Wansing (2008): *Constructive negation, implication, and co-implication*. Journal of Applied Non-Classical Logics 18(2-3), pp. 341–364, doi:10.3166/jancl.18.341-364.