Tableaux for Epistemic Gödel Logic

Marta Bílková, Thomas Ferguson, Daniil Kozhemiachenko

► To cite this version:

Marta Bílková, Thomas Ferguson, Daniil Kozhemiachenko. Tableaux for Epistemic Gödel Logic. PRIMA 2025: Principles and Practice of Multi-Agent Systems, Dec 2025, Modena, Italy, Italy. Lecture Notes in Artificial Intelligence, 16366, Springer Nature Switzerland, pp.232-250, 2025, Lecture Notes in Computer Science, 10.1007/978-3-032-13562-9_17. http://dx.doi.org/10.1007/978-3-032-13562-9_17

HAL Id: hal-05348706

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

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
Tableaux for epistemic Gödel logic *

Marta Bílková¹[0000-0002-3490-2083], Thomas Ferguson¹,²[0000-0002-6494-1833], and Daniil Kozhemiachenko³[0000-0002-1533-8034]

¹ The Czech Academy of Sciences, Institute of Computer Science, Prague
bilkova@cs.cas.cz

² Department of Cognitive Science, Rensselaer Polytechnic Institute, Troy, USA
tferguson@gradcenter.cuny.edu

³ Aix-Marseille Univ, CNRS, LIS, Marseille, France
daniil.kozhemiachenko@lis-lab.fr

**Abstract.** We propose a multi-agent epistemic logic capturing reasoning with degrees of plausibility that agents can assign to a given statement with 1 interpreted as ‘entirely plausible for the agent’ and 0 as ‘completely implausible’ (i.e., the agent knows that the statement is false). We formalise such reasoning in an expansion of Gödel fuzzy logic with an involutive negation and multiple **S5**-like modalities. As already Gödel single-modal logics are known to lack the finite model property w.r.t. their standard [0, 1]-valued Kripke semantics, we provide an alternative semantics that allows for the finite model property. For this semantics, we construct a strongly terminating tableaux calculus that allows us to produce finite counter-models of non-valid formulas. We then use the tableaux to show that the validity problem in our logic is PSpace-complete when there are two or more agents, and coNP-complete for the single-agent case.

**Keywords:** epistemic logic · constraint tableaux · Gödel logic · involutive negation · modal logic.

# 1 Introduction

Epistemic modal logic deals with reasoning about knowledge and thus usually interprets formulas of the form $\Box_a\phi$ as ‘a knows that $\phi$ is true’. The dual formula $\Diamond_a\phi$ can be then interpreted as ‘$\phi$ is consistent with a’s knowledge’ or ‘a considers $\phi$ plausible’. In the classical epistemic logic, such statements are either true or false; however, in many contexts, it makes sense to assume that a proposition can be true to a degree. E.g., a person can be ‘very tall’, ‘quite tall’, ‘not so tall’, etc. Similarly, an agent can consider a given statement $\phi$ plausible to some degree — from entirely plausible to completely implausible. In the latter case, we can say that a rational agent knows that $\phi$ is false.

There are several approaches to representing degrees of belief and plausibility. The first one is to use graded modal logics as has been done in, e.g., [24]. In this

<footnote>* The research of Marta Bílková was supported by the grant 22-23022L CELIA of Grantová Agentura České Republiky.</footnote>
approach, the language is expanded with modal formulas $\Diamond^{\ge n}\phi$ read as 'φ is true in at least n accessible states'. A similar approach proposed in [25] is to add formulas $\Box_a^n\phi$ interpreted as 'a believes in φ after any removal of at most n pieces of information from their belief base'. Another option [19,23] is to consider a binary modality $\succeq$ s.t. $\phi \succeq \chi$ is interpreted as 'φ is at least as likely / plausible / probable / ... as χ'. Note, however, that these logics usually expand classical propositional logic. Thus, even though a belief statement has degrees, it is still not trivial to formalise statements such as 'the degree to which a finds it plausible that Paula is *very tall* should be lower or equal to the degree to which a finds it possible that she is *quite tall*' because 'very tall' and 'quite tall' do not correspond to classical values of formulas.

Thus, in this paper, we will consider an alternative approach that relies on *non-classical*, namely, *fuzzy logics*. In fuzzy modal logics, both propositional and modal formulas can have values in the [0, 1] real-valued interval. Moreover, we will concentrate on a less formal notion of ‘plausibility’ that one may use in everyday reasoning.

In the context of everyday reasoning, people usually do not assign specific
values to statements about plausibility but can *compare* them — e.g., a hailstorm
can be less plausible than rain. To formalise such contexts, one can use *Gödel
logic* and its modal expansions. An important property of Gödel logic is that
the truth of a formula depends on the *order* of the values, not on the values
themselves. This is because (propositional) Gödel logic is given via the t-norm $\wedge_G$
(Gödel conjunction) and its residuum $\rightarrow_G$ (implication):

$$
a \wedge_G b = \min(a, b) \qquad a \rightarrow_G b = \begin{cases} 1 & \text{if } a \le b \\ b & \text{otherwise} \end{cases}
$$

**Gödel modal and description logics** Gödel modal logics are usually defined on Kripke frames of the form ⟨W, R⟩ where W is a set of states and R is a relation on W (in which case, the frame is called *crisp*) or a function W × W → [0, 1] (in which case, the frame is *fuzzy*).<fnref n="4" /> The values of modal formulas □φ and ◇φ in a given state are defined via, respectively, the infimum and supremum of the values of φ in accessible states. Modal expansions of Gödel logics are well-studied. In particular, □ and ◇ fragments of Gödel modal logic **KG** were axiomatised in [15] and **KG** with both □ and ◇ was axiomatised in [16,31]. Hypersequent calculi were constructed in [26,27] and used to obtain the **PSpace**-completeness of both fragments. Decidability and **PSpace**-completeness of the full logic were shown in [13,14].

In *knowledge representation and reasoning*, modal logics correspond to *de-
scription logics* (DLs). Gödel DLs were proposed in [7] to represent graded infor-
mation in the ontologies and were further studied in [8]. It was shown that even
the most expressive Gödel DLs often have the same complexity as their classical
counterparts [11,10,9,12]. Note, however, that, in contrast to modal logics, the

<footnote n="4">⁴ Note, however, that some temporal Gödel logics [1,2] are constructed over bi-relational frames where one relation is used to define modalities and the other to compute the value of implication.</footnote>
interpretations in fuzzy description logics are often assumed to be witnessed,
that is, if the value of a quantified concept assertion [∀R.A](a) is x, then there
must be some individual b s.t. A(b) has value x.

**Epistemic and doxastic Gödel logics** In classical logic, it is customary (cf., e.g., [22,18,17,6]) to use **S5** (the logic of frames ⟨W, R⟩ where **R** is an equivalence relation) to formalise reasoning about knowledge and **K45** and **KD45** (logics of transitive Euclidean and serial transitive Euclidean frames, respectively) to reason about beliefs. Applications of Gödel modal logics to the reasoning about beliefs and knowledge have also received much attention. In particular, Gödel counterparts of logics **S5** [13,16,32,14,31], **K45**, and **KD45** [30] were axiomatised and shown to be decidable. In fact, the single-agent **S5** turns out to be NP-complete just as the classical version. Moreover, a Gödel analogue of the public announcement logic was proposed in [4].

**Contributions and plan of the paper** Even though epistemic and doxastic Gödel logics are well investigated, to the best of our knowledge, the decidability results concern *single-agent* logics. This is why, in this paper, we will study **S5G**<sup>c</sup><sub>inv</sub> — a Gödel counterpart to **S5<sub>n</sub>** (classical **S5** with *n* agents) over *crisp* frames and expanded with an involutive negation ~ defined as v(~φ, w) = 1 — v(φ, w). This negation not only allows one to define additional connectives but also makes ◊ and □ interdefinable in the expected fashion.

Moreover, the involutive negation is closer to the intuitive reading of ‘not’
in contexts involving truth degrees than the standard Gödelian negation ¬<sub>G</sub>φ :=
φ →<sub>G</sub> 0. Consider the following example, borrowed from [5]. Let the truth degree
of ‘Paula is tall’ (*p*) be 1/2. It is reasonable to assume that the truth degree of
‘Paula is not tall’ is also 1/2. Similarly, if she is shorter than average (i.e., the
truth degree of *p* is smaller than 1/2), it is reasonable that the truth degree of
‘not-*p*’ should be greater than 1/2. On the other hand, the truth degree of ¬<sub>G</sub>p
is 0 when the truth degree of *p* is positive. Thus, using ¬<sub>G</sub>p to stand for ‘Paula
is not tall’ is counterintuitive as it says that ‘Paula is tall is contradictory’.

As Gödel counterpart of S5 lacks finite model property (FMP) w.r.t. standard semantics, we will adapt the approach of [13] and [5] to produce a semantics over finitary models (so-called F-models) w.r.t. which the logic will have the FMP. We will then use these semantics to construct a tableaux calculus for S5G<sub>inv</sub><sup>c</sup> that allows for an explicit construction of countermodels from complete open branches. We will also use this calculus to prove PSpace-completeness of S5G<sub>inv</sub><sup>c</sup> and show that the alternative semantics is equivalent to the standard one.

The remainder of the text is structured as follows. We present and discuss
two semantics of epistemic Gödel logic in Section 2: first, the standard semantics,
then the one based on F-models. In Section 3, we construct a tableaux calculus
and show its soundness and completeness w.r.t. F-models. Section 4 is dedicated
to the complexity of the validity of S5G<sub>inv</sub><sup>c</sup> w.r.t. F-models. In particular, we
establish the finite model property and show that the validity w.r.t. F-models in
*multi-agent* S5G<sub>inv</sub><sup>c</sup> is *PSpace-complete* and *NP-complete* for *single-agent* S5G<sub>inv</sub><sup>c</sup>.
In Section 5, we show that the new semantics is equivalent to the standard one.
Finally, we summarise our results and set goals for future work in Section 6. Omitted proofs can be found in the appendix.

## 2 Two semantics of epistemic Gödel logic

Let us now present the language and semantics of $S5G_{inv}^c$. We fix a countable set $\mathbf{Prop}$ of propositional variables. For a finite set $\mathbf{A}$ of agents, we define the language $\mathcal{L}^{\sim}(\mathbf{A})$ via the following grammar with $p \in \mathbf{Prop}$ and $a \in \mathbf{A}$:

$$ \phi ::= p \mid \sim\phi \mid (\phi \land \phi) \mid (\phi \rightarrow \phi) \mid \Box_a \phi $$

From now on, we will assume a fixed $\mathbf{A}$ and mostly omit explicit reference to it.

**Definition 1 (Epistemic frames).** An epistemic frame for $\mathbf{A}$ is a tuple $\mathfrak{F} = (W, \langle R_a \rangle_{a \in \mathbf{A}})$ s.t. $W \neq \emptyset$ and $R_a$'s are equivalence relations on $W$.

### 2.1 Standard semantics

We begin with the standard semantics of $S5G_{inv}^c$ that generalises the Kripke semantics of $S5$ [6].

**Definition 2 (S5G<sub>inv</sub><sup>c</sup>-models).** An $S5G_{inv}^c$-model for $\mathbf{A}$ is a tuple $\mathfrak{M} = (\mathfrak{F}, v)$ s.t. $\mathfrak{F}$ is an epistemic frame for $\mathbf{A}$ and $v: \mathbf{Prop} \times W \rightarrow [0, 1]$ (valuation).

The valuation is extended to the complex formulas as follows:

$$ \begin{array}{l@{\qquad}l} v(\sim\phi, w) = 1 - v(\phi, w) & v(\phi \land \chi, w) = \min(v(\phi, w), v(\chi, w)) \\ v(\phi \rightarrow \chi, w) = \begin{cases} 1, & \text{if } v(\phi, w) \le v(\chi, w) \\ v(\chi, w), & \text{else} \end{cases} & v(\Box_a \phi, w) = \inf\{v(\phi, w') \mid wR_a w'\} \end{array} $$

We say that a formula $\phi$ is $S5G_{inv}^c$-satisfiable if there is a $S5G_{inv}^c$-model $\mathfrak{M}$ and $w \in \mathfrak{M}$ s.t. $v(\phi, w) = 1$; $\phi$ is $S5G_{inv}^c$-valid if $v(\phi, w) = 1$ for every $\mathfrak{M}$ and $w \in \mathfrak{M}$.

**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 \rightarrow \chi) \land (\chi \rightarrow \phi)$ and use the following defined connectives:<fnref n="5" />

$$ \begin{array}{l@{\qquad}l@{\qquad}l} \mathbf{1} & := p \rightarrow p & \mathbf{0} & := \mathbf{1} & \neg\phi & := \phi \rightarrow \mathbf{0} \\ \phi \lor \chi & := \sim(\sim\phi \land \sim\chi) & \phi \prec \chi & := \sim(\sim\chi \rightarrow \sim\phi) & \Delta\phi & := \mathbf{1} \prec (\mathbf{1} \prec \phi) \\ \Diamond_a \phi & := \sim\Box_a \sim\phi & & & & \\ & & & & & \end{array} $$

Furthermore, in $\Box_a \phi$ or $\Diamond_a \phi$, we call the lower index $a \in \mathbf{A}$ the agent label.

Using Definition 2, we obtain the following semantics of $\prec$, $\prec$, $\leftrightarrow$, $\Delta$, and $\Diamond$:

$$ v(\phi \prec \chi, w) = \begin{cases} v(\phi, w), & \text{if } v(\phi, w) > v(\chi, w) \\ 0, & \text{else} \end{cases} \qquad v(\neg\phi, w) = \begin{cases} 1, & \text{if } v(\phi, w) = 0 \\ 0, & \text{else} \end{cases} $$

<footnote n="5">⁵ Here, $\prec$ is coimplication ($\phi \prec \chi$ is interpreted as '$\phi$ excludes $\chi$'; cf. [29,20] for a detailed study and [33] for the interpretation), and $\Delta$ is 'Baaz Delta operator' (cf. [3] for a discussion in the context of fuzzy logics).</footnote>
$$
\begin{align*}
v(\phi \leftrightarrow \chi, w) &= \begin{cases} 1, & \text{if } v(\phi, w) = v(\chi, w) \\ \min(v(\phi, w), v(\chi, w)), & \text{else} \end{cases} &
v(\Delta\phi, w) &= \begin{cases} 1, & \text{if } v(\phi, w) = 1 \\ 0, & \text{else} \end{cases} \\
v(\phi \lor \chi, w) &= \max(v(\phi, w), v(\chi, w)) &
v(\diamond_a\phi, w) &= \sup_{wR_a w'} v(\phi, w') \quad (1)
\end{align*}
$$

We also observe that non-validity and satisfiability are reducible to one another.
Namely, $\phi$ is valid iff $\sim\Delta\phi$ is unsatisfiable; $\phi$ is satisfiable iff $\sim\Delta\phi$ is not valid.

In the introduction, we mentioned that it makes sense to consider degrees of plausibility in epistemic contexts. Furthermore, agents might know that a proposition is true *to some degree*. The example below illustrates one of such contexts and highlights the differences between Gödel and classical epistemic logics.

*Example 1.* Consider the following formula: $\phi_{\text{plaus}} := (\Box_a(\sim p \rightarrow p) \wedge \Diamond_a p) \rightarrow \Diamond_b p$.
Here, $\phi_{\text{plaus}}$ says that if $a$ knows that the value of $p$ is at least $\frac{1}{2}$ and considers $p$ plausible (does not know that it is false), then $b$ should also consider $p$ plausible.
Observe that $\phi_{\text{plaus}}$ is valid in $S_5_2$ since $p$ and $\sim p \rightarrow p$ are classically equivalent and $\Box_a p$ implies $\Diamond_b p$. On the other hand, it can be easily refuted in $S_5 G^c_{\text{inv}}$, e.g., in the following model:

$$
\mathfrak{M} : w_1 : p = \frac{1}{2} \dashv\!\!\dashv\!\! R_b \quad w_0 : p = \frac{1}{2} \dashv\!\!\dashv\!\! R_a \quad w_2 : p = 1
$$

Let us now present a natural context illustrating $\mathfrak{M}$. Say, there are three people: Alice, Brittney, and Paul. Alice knows that Paul is quite tall (i.e., that the value of $p$ is at least $\frac{1}{2}$) and finds it plausible that he is very tall (value of $p$ equals 1 in some state accessible to Alice). Of course, it does not mean that Brittney also finds it plausible that Paul is very tall. On the other hand, it is easy to see that the following formula is $S_5 G^c_{\text{inv}}$-valid: $\phi'_{\text{plaus}} := (\Box_a(\sim p \rightarrow p) \wedge \Diamond_a p) \rightarrow (\sim \Diamond_b p \rightarrow \Diamond_b p)$. Here, if Alice knows that Paul is quite tall and finds it plausible that he is very tall, the degree of plausibility of $p$ for Brittney is at least $\frac{1}{2}$.

Finally, we observe that degrees of belief also depend on the degrees of truth.
Let us consider such contexts in more detail.

*Example 2.* Consider two statements: *the suitcase is very heavy (s)* and *the suitcase is quite heavy (~s → s — i.e., the truth degree of s is at least as high as that of its negation)*. It is reasonable to assume that the degree of plausibility of *s* for Ann should not be higher (but can be lower) than the degree of plausibility of ~*s* → *s*. Indeed, one can use Definition 2 and 1 to see that ♦<sub>a</sub>*p* → ♦<sub>a</sub>(*~p* → *p*) is S<sub>5</sub>G<sub>inv</sub><sup>c</sup>-valid but ♦<sub>a</sub>(*~p* → *p*) → ♦<sub>a</sub>*p* is not.

On the other hand, in classical logic, one cannot express this connection between different truth degrees of a single statement and degrees of plausibility. Indeed, as *s* and ~*s* → *s* are classically equivalent, it follows that ♦<sub>a</sub>*p* ↔ ♦<sub>a</sub>(*~p* → *p*) is S<sub>5</sub>-valid.

## 2.2 Epistemic F-models

As is well-known [13,32,14], even the single-agent version of the Gödel modal logic over epistemic frames lacks the finite model property. So, will our semantics with Definition 2. In [14], there was given a procedure to define alternative semantics for *order-based* modal logics, i.e., logics whose connectives can be
expressed in the lattice language. Clearly, ~ is not order-based. Still, we can combine the approaches from [13] and [5] to construct such semantics for S5G<sub>inv</sub>.

**Definition 3 (eF-models).** Let $\mathcal{P}_{<\omega}([0, 1]) = \{X \mid X \subseteq [0, 1], |X| < \aleph_0\}$. An epistemic F-model for A (eF-model) is a tuple $\mathfrak{M} = (W, \langle R_a \rangle_{a \in A}, \langle T_a \rangle_{a \in A}, v \rangle$ s.t.

- $\langle W, \langle R_a \rangle_{a \in A} \rangle$ is an epistemic frame;

- $T_a: W \to \mathcal{P}_{<\omega}([0, 1])$ are s.t. (i) $\{0, \frac{1}{2}, 1\} \subseteq T_a(w)$ for each $w \in W$, (ii) if $x \in T_a(w)$, then $1 - x \in T_a(w)$, (iii) if $w R_a w'$, then $T_a(w) = T_a(w')$;

- $v: \text{Prop} \times W \to [0, 1]$.

We call $v$ an F-valuation and extend it to propositional formulas as in Definition 2 and to modal formulas as follows:

$$v(\Box_a \phi, w) = \max\{x \in T_a(w) \mid x \le \inf\{v(\phi, w') \mid w R_a w'\}\}$$

We say that a formula $\phi$ is satisfiable on epistemic F-models (eF-satisfiable) if there is an eF-model $\mathfrak{M}$ and $w \in \mathfrak{M}$ s.t. $v(\phi, w) = 1$; $\phi$ is valid on epistemic F-models (eF-valid) if $v(\phi, w) = 1$ for every $\mathfrak{M}$ and $w \in \mathfrak{M}$.

Let us now discuss F-models in more detail. As in [13,14], $T_a$'s assign finite subsets of $[0, 1]$ to each state in the model that represent sets of values that formulas $\Box_a \phi$ can have at $w$. In a sense, the value of $\Box_a \phi$ in an F-model can be interpreted as an approximation from below of its 'real' value in a standard model. Conditions (i) and (ii) account for the presence of $\sim$ and result in the following semantics of $\Diamond_a \phi$:

$$v(\sim\Box_a \sim\phi, w) = v(\Diamond_a \phi, w) = \min\{x \in T_a(w) \mid x \ge \sup\{v(\phi, w') \mid w R_a w'\}\}$$

This way, the value of $\Diamond_a \phi$ in an F-model is an approximation from above of its 'real' value in a standard model. Finally, condition (iii) ensures the preservation of the following property of S5G<sub>inv</sub>-models: if $w R_a w'$, then $v(\Box_a \phi, w) = v(\Box_a \phi, w')$ for every $\phi \in \mathcal{L}^{\sim}$.

We recall from the introduction that in Gödel description logics, it is customary [10,12] to assume that interpretations of ontologies are witnessed. In modal logic terms, this means that if $v(\Box_a \phi, w) = x$ or $v(\Diamond_a \phi, w) = x$, then there is some accessible $w'$ s.t. $v(\phi, w) = x$. Thus, a natural question is whether epistemic F-models are just witnessed standard models in disguise. The answer is known to be negative [15,13]. For instance, $\phi = \Delta\Diamond_a p \to \Diamond_a \Delta p$ has value 1 in every witnessed model. On the contrary, consider the following eF-model $\mathfrak{M} = (W, R_a, T_a, v)$: $W = \{w\}$, $R_a = \langle w, w \rangle$, $T_a(w) = \{0, \frac{1}{2}, 1\}$, $v(p, w) = \frac{3}{4}$. Now observe from Definition 3 that $v(\Diamond p, w) = 1$ but $v(\Diamond_a \Delta p, w) = 0$. Thus, $v(\Delta\Diamond_a p \to \Diamond_a \Delta p, w) = 0$.

Another question is whether rejecting witnessed models is reasonable in an epistemic context. In the following paragraph, we argue that it does make sense.

Intuitively, $\phi$ tells that if $a$ considers $p$ absolutely plausible, then $a$ should consider it possible that $p$ is true (has value 1). Observe, however, that one might not accept this principle if values of $p$ are considered large enough to infer the (absolute) plausibility of $p$. In the standard semantics, this can be modelled by having infinitely many accessible states where the supremum of the values of $p$ is 1 even though $p$ never has value 1. In the eF-models, given
$T_a(w) = \{0, x_1, \dots, x_n, 1\}$, one can interpret the values of formulas in the interval $(x_n, 1)$ as *large enough*. Note furthermore, that as $\frac{1}{2} \in T_a(w)$, the set of negligibly small values does not trivialise to $\{0, 1\}$. Dually, the values in the interval $(0, x_1)$ can be considered *negligibly small*. This would mean that the following formula $\chi = \Box_a \neg\neg q \rightarrow \neg\neg\Box_a q$ can be invalidated in the eF-model from the previous paragraph by setting $v(q, w) = \frac{1}{4}$. One can interpret $\chi$ as follows: if $a$ knows that the value of $q$ is positive, then $a$ should not consider its negation plausible. Indeed, observe that $v(\neg\neg\Box_a q) = 1$ iff $v(\diamond_a \sim q) < 1$. If, however, some value $x > 0$ of $q$ is *negligibly small* for $a$, they may not accept $\chi$ if $v(q, w') \le x$ in some state $w'$ accessible to $a$.

## 3 Tableaux

Many reasoning techniques are used for Gödel modal and description logics. In particular, there are terminating sequent calculi for $\Box$- and $\Diamond$-fragments of the Gödel modal logic [26,27] (with the standard negation $\neg$, not the involutive negation $\sim$). There are also tableaux for Gödel description logics with witnessed semantics, and it is known that they can be reduced to *classical reasoning in ontologies* (cf. [12] for both approaches applied to expressive Gödel DLs). In the case of *general* (i.e., not necessarily witnessed) interpretations, automata-based decision procedures are used [11]. In addition, there are semantic tableaux systems based on F-models. In particular, tableaux for **KG** and **KG**<sup>c</sup> (Gödel modal logics *without* involutive negation over arbitrary fuzzy and crisp frames, respectively) and for **S5G**<sup>c</sup> (single-agent epistemic Gödel logic *without* $\sim$) are presented in [32]. In [5], a tableaux calculus for **KG**<sub>inv</sub> (a Gödel modal logic with involutive negation over *arbitrary fuzzy frames*) is presented.

In this paper, we are constructing a tableaux calculus for $S5G_{inv}^c$ based on eF-models. As we have seen in the previous section, eF-models *do not* correspond to witnessed models. Thus, it is unreasonable to expect that there is a nice reduction of $S5G_{inv}^c$-satisfiability to classical S5-satisfiability. Furthermore, in contrast to reasoning procedures based on sequent calculi or automata (or on reductions to classical logics), tableaux enable straightforward extraction of finite countermodels from failed proofs. Thus, the finite model property (w.r.t. eF-models) will follow immediately from the completeness of tableaux. We will generalise the tableaux for $GS5^c$ from [32]. One of the features of *mono-modal S5*-like logics is that they can be characterised via frames with *universal relations*. Thus, simple terminating tableaux for them can be defined without encoding accessibility relation (cf., e.g., [28] for the classical S5). Of course, when dealing with *multi-modal S5*, one has to keep track of different relations. This can be done, e.g., with relational terms of the form $wRw'$ [22]. In this case, one sometimes has to propagate modal formulas into the generated states, which might complicate the decision procedure. Note, however, that since $R_a$'s in epistemic frames are equivalence relations, we can represent frames as families of clusters — equivalence classes under $R_a$'s.
We can now use terms of the form $w \in \mathfrak{c}_a$ interpreted as 'w belongs to an $R_a$-cluster $\mathfrak{c}'$ in our tableaux. Furthermore, to account for the involutive negation, we will adapt 'constraint tableaux' from [21] and follow the presentation of the tableaux calculus from [5]. We begin by giving formal definitions of the needed notions. We will then explain them in further detail.

**Definition 4 (Structures and constraints).** We fix a countable set WL = {$w, w', w_0, ...$} of state-labels, $\mathfrak{C} = \bigcup_{a \in A}\{\mathfrak{c}_a, \mathfrak{c}'_a, \mathfrak{c}^1_a, ...\}$ of cluster-labels, and $\mathbf{Var} = \{d, e, d', ...\}$ of variables. We also define the set of T-symbols $T = \{t_i(\mathfrak{c}_a) | \mathfrak{c}_a \in \mathfrak{C}, i \in \mathbb{N}, a \in A\} \cup \{t^s_i(\mathfrak{c}_a) | \mathfrak{c}_a \in \mathfrak{C}, a \in A, i \in \mathbb{N}\} \cup \{\emptyset, 1\},$ and let $\triangledown \in \{\leq, <, \geq, >, =\}$. We define sets of labelled formulas (LF) and relational terms (RT) as follows:

$$ \mathbf{LF} = \{w:\phi | w \in \mathrm{WL}, \phi \in \mathscr{L}^{\sim}_{\square}\} \quad \mathbf{RT} = \{w \in \mathfrak{c}_a | w \in \mathrm{WL}, \mathfrak{c}_a \in \mathfrak{C}, a \in A\} $$

The set VT of value terms is defined as follows:

$$ \mathbf{VT} \ni \mathfrak{T} := c \in \mathbf{Var} | \mathbf{t} \in \mathbf{T} | 0 | 1 | 1 - \mathfrak{T} $$

Finally, constraints have the form $\Sigma \triangledown \mathfrak{T}$ s.t. $\Sigma \in \mathbf{LF} \cup \mathbf{VT}$, $\mathfrak{T} \in \mathbf{VT}$. We will also set $\mathbf{Str} := \mathbf{LF} \cup \mathbf{VT}$ and call its elements structures.

In the definition above, a constraint of the form $w:\phi \leq \mathfrak{T}$ means that the value of $\phi$ in $w$ is less or equal to $\mathfrak{T}$. Note that $\mathfrak{T}$ is never a formula but a 'value term' — either a number, a member of $\mathbf{T}$, or an expression of the form $1 - \mathfrak{T}$. Thus, we never compare the values of formulas to one another. We also need three types of T-symbols — constants ($\emptyset$ and $1$), $t$'s, and $t^s$'s. Here, $t_i(\mathfrak{c}_a)$ is a member of $T_a(w)$ for any $w \in \mathfrak{c}_a$, and $t^s_i(\mathfrak{c}_a)$ is the immediate successor of $t_i(\mathfrak{c}_a)$. This is needed to represent the semantics of $\square$ (recall from Definition 3 that the value of $\square_a \phi$ at $w$ is the maximal element of $T_a(w)$ that still does not exceed the infimum of the values of $\phi$).

**Definition 5 (T(S5G<sup>c</sup><sub>inv</sub>) — tableaux for S5G<sup>c</sup><sub>inv</sub> ).** A tableau is a downward-branching tree whose nodes are constraints and relational terms. Each branch can be extended by one of the rules from Figure 1.

Let $\mathcal{B} = \{c_1, ..., c_n\}$ be a branch with constraints $c_1, ..., c_n$. Given a constraint $c$, let $c^t$ be the result of replacing $\mathfrak{T} \in \mathbf{VT}$, and $\lambda \in \mathbf{LF}$ with variables $x_{\mathfrak{T}}$, and $x_{\lambda}$, respectively, and $\mathfrak{n} \in \{\emptyset, 1\}$ with $n \in \{0, 1\}$. Furthermore, for every $\mathfrak{c}_a \in \mathfrak{C}$ and $a \in A$ occurring on $\mathcal{B}$, we set

$$ \mathfrak{T}(\mathfrak{c}_a) = \{t(\mathfrak{c}_a) | \begin{array}{l} t(\mathfrak{c}_a) \text{ is on } \mathcal{B} \\ t^s(\mathfrak{c}_a) \text{ is on } \mathcal{B} \\ \mathfrak{n} | \exists \phi w:\phi = \mathfrak{n} \in \mathcal{B} \text{ and } w \in \mathfrak{c}_a \text{ occurs on } \mathcal{B} \end{array} \} \cup \{\emptyset | \exists \phi w:\phi = \mathfrak{n} \in \mathcal{B} \text{ and } w \in \mathfrak{c}_a \text{ occurs on } \mathcal{B}\} $$

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

$$ \mathcal{B}^t = \{c_1^t, ..., c_n^t\} \cup \{x_{t(\mathfrak{c}_a)} < x_{t^s(\mathfrak{c}_a)} | t(\mathfrak{c}_a) \text{ and } t^s(\mathfrak{c}_a) \text{ occur on } \mathcal{B}\} $$

does not have a solution over $[0,1]$ s.t. for each $w \in \mathrm{WL}$ and $a \in A$, it holds that:

$$ \begin{align} \mathfrak{T}(\mathfrak{c}_a) &= \{t(\mathfrak{c}_a), t^s(\mathfrak{c}_a)\} \Rightarrow \left[ \begin{array}{l} x_{t(\mathfrak{c}_a)} = 0 \ \& \ x_{t^s(\mathfrak{c}_a)} = \frac{1}{2} \ \text{or} \\ x_{t(\mathfrak{c}_a)} = \frac{1}{2} \ \& \ x_{t^s(\mathfrak{c}_a)} = 1 \end{array} \right] \nonumber \\ |\mathfrak{T}(\mathfrak{c}_a)| \geq 3 &\Rightarrow \left[ \begin{array}{l} \forall \mathbf{t} \in \mathfrak{T}(\mathfrak{c}_a) \ \exists \mathbf{t}' \in \mathfrak{T}(\mathfrak{c}_a) : 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] \tag{2} \\ \neg \exists t(\mathfrak{c}_a), t^s(\mathfrak{c}_a), t'(\mathfrak{c}_a) : x_{t(\mathfrak{c}_a)} < x_{t'(\mathfrak{c}_a)} < x_{t^s(\mathfrak{c}_a)} \nonumber \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

- $w:\phi < \mathfrak{T}$ and $w:\phi < 1$, or

- $w:\phi > \mathfrak{T}$ and $w:\phi > 0$, or

- $u : \square_a \phi = \mathfrak{T}, u' : \square_a \phi = \mathfrak{T}', u \in \mathfrak{c}l_a, \text{ and } u' \in \mathfrak{c}l_a$.

In the first two cases, the rules are applied to the constraints with $\mathfrak{T}$, not 0 and 1. In the third case, we use $\equiv_{\mathfrak{c}l}$ and then apply $\sqsubseteq$ to $u : \square_a \phi = \mathfrak{T}$ only.

Finally, $\phi \in \mathcal{L}^\sim$ has a $\mathcal{T}(\mathbf{S5G}^c_{\text{inv}})$ proof if there is a tableau beginning with $\{w:\phi < 1\} \cup \{w \in \mathfrak{c}l_a \mid a \in A\}$ s.t. all its branches are closed.

$$ \sim : \frac{w:\sim\phi\triangledown\mathfrak{T}}{w:\phi\triangleleft 1-\mathfrak{T}} \qquad \wedge_{\triangleright} : \frac{w:\phi\wedge\chi\triangleright\mathfrak{T}}{w:\phi\triangleright\mathfrak{T}} \qquad \wedge_{\triangleleft} : \frac{w:\phi\wedge\chi\triangleleft\mathfrak{T}}{w:\phi\triangleleft\mathfrak{T} | w:\chi\triangleleft\mathfrak{T}} \\ \rightarrow_{\triangleright} \frac{w:\phi \rightarrow \chi\triangleright\mathfrak{T}}{w:\chi\triangleright\mathfrak{T} \mid \mathfrak{T}\triangleleft 1} \qquad \rightarrow_{\leq} \frac{w:\phi \rightarrow \chi\leq\mathfrak{T}}{1 \leq \mathfrak{T} \mid w:\phi > d} \qquad \rightarrow_{<} \frac{w:\phi \rightarrow \chi < \mathfrak{T}}{w:\phi \geq d} \\ \qquad \qquad \qquad \qquad \begin{array}{l} w:\chi \geq d \\ w:\phi \leq d \end{array} \qquad \qquad \qquad \qquad \begin{array}{l} w:\chi \leq d \\ d \leq \mathfrak{T} \end{array} $$

$$ \begin{array}{c} \Box_{\triangleright} : \quad \left. \begin{array}{l} w:\square_a \phi \triangleright \mathfrak{T} \\ w \in \mathfrak{c}l_a \end{array} \right| \begin{array}{l} w:\square_a \phi = t(\mathfrak{c}l_a) \\ \mathfrak{T} \triangleleft t(\mathfrak{c}l_a) \\ w':\phi < t^s(\mathfrak{c}l_a) \\ w' \in \mathfrak{c}l_a \\ w' \in \mathfrak{c}l'_{a'} \end{array} \\ \Box_{\leq} : \quad \left. \begin{array}{l} w:\square_a \phi \leq \mathfrak{T} \\ w \in \mathfrak{c}l_a \end{array} \right| \begin{array}{l} t(\mathfrak{c}l_a) \leq \mathfrak{T} \\ w':\phi < t^s(\mathfrak{c}l_a) \\ w' \in \mathfrak{c}l_a \\ w' \in \mathfrak{c}l'_{a'} \end{array} \\ \Box_{<} : \quad \left. \begin{array}{l} w:\square_a \phi < \mathfrak{T} \\ w \in \mathfrak{c}l_a \end{array} \right| \begin{array}{l} t(\mathfrak{c}l_a) < \mathfrak{T} \\ w':\phi < t^s(\mathfrak{c}l_a) \\ w' \in \mathfrak{c}l_a \\ w' \in \mathfrak{c}l'_{a'} \end{array} \\ \Box = : \quad \frac{w:\square_a \phi = \mathfrak{T}}{w \in \mathfrak{c}l_a \quad u \in \mathfrak{c}l_a} \\ \qquad \qquad \qquad \qquad \begin{array}{l} u : \square_a \phi = \mathfrak{T} \\ u' : \square_a \phi = \mathfrak{T}' \\ u \in \mathfrak{c}l_a \quad u' \in \mathfrak{c}l_a \end{array} \\ \qquad \qquad \qquad \qquad \equiv_{\mathfrak{c}l} : \quad \frac{u \in \mathfrak{c}l_a \quad u' \in \mathfrak{c}l_a}{\mathfrak{T} \leq \mathfrak{T}' \\ \qquad \qquad \qquad \qquad \qquad \qquad \mathfrak{T}' \leq \mathfrak{T}} \end{array} $$

Fig. 1: Tableaux rules. Vertical bars denote branching; $\triangleright$, $\triangleright \in \{\leq, <, \geq, >\}$, if $\triangleright$ is $\leq$, then $\triangleright$ is $\geq$ and vice versa (likewise for $<$); $\triangleright \in \{\geq, >\}$, $\triangleleft \in \{\leq, <\}$; $d, \mathfrak{c}l'_a, w', t(\mathfrak{c}l_a)$, and $t^s(\mathfrak{c}l_a)$ are fresh on the branch; $a' \in A$ appears on the branch.

Let us briefly explain tableaux rules. First, we note that every generated state is added to a cluster w.r.t. each relation. This is needed because accessibility relations in eF-models are reflexive. Thus, when an application of a $\square\leq$, $\square<$, or a $\Box\triangleright$ rule produces a new state $w'$, we add it to the current cluster $\mathfrak{c}l_a$ and then
also for every $a' \in A$ s.t. $a' \neq a$, create new clusters $cl_a'$ that will contain $w'$. Moreover, $\square_a \psi$ formulas are guaranteed to have the same values in all states of a given $R_a$-cluster because of the $\equiv_{cl}$ rule.

Second, consider the $\square \leq$ rule. There we consider two possibilities: either $\square_a \phi$ has value 1 at $w$ (left branch) or it has some value $t(cl_a)$ from $T_a(w)$ strictly lower than 1 (right branch). In the first case, $\phi$ will have value 1 in all states of the $R_a$-cluster to which $w$ belongs (cf. $\square=$). In the second case, we create $w'$ where $\phi$ has value between $t(cl_a)$ and its successor $t^s(cl_a)$. After the application of $\square \leq$, we can use $\square=$ that stipulates that $\phi$ has value at least $t(cl_a)$ in all states of the current $R_a$-cluster. Note, moreover, that $\square <$ rule is, essentially, a particular case of the $\square \leq$ rule. We keep them separate to avoid unnecessary introductions of constraints $1 < 1$ to the branch.

Third, observe that the clusters allow us to avoid redundant applications of modal rules. E.g., if $\mathcal{B}$ contains $u : \square_a \phi \leq \mathfrak{T}$, $u' : \square_a \phi \leq \mathfrak{T}$, $u \in cl_a$, and $u' \in cl_a$, it is clear that we only need to apply the $\square \lhd$-rule once. This is because the newly generated state $w'$ will belong to the same $R_a$-cluster $cl_a$ as both $u$ and $u'$. Similarly, if $\mathcal{B}$ contains $u : \square_a \phi \geq \mathfrak{T}$, $u' : \square_a \phi \geq \mathfrak{T'}$, $u \in cl_a$, and $u' \in cl_a$, we use the $\equiv_{cl}$ rule to avoid redundant applications of modal rules.

**Definition 6 (Model realising a branch).** Let $\mathfrak{M} = (W, \langle R_a \rangle_{a \in A}, \langle T_a \rangle_{a \in A}, v)$ be an eF-model and $\mathcal{B}$ a tableau branch. An $\mathfrak{M}$-realisation of $\mathcal{B}$ is a map $\mathfrak{r} : WL \cup \text{Str} \to W \cup [0, 1]$ s.t. $\mathfrak{r}(w) \in W$ and $\mathfrak{r}(\Sigma) \in [0, 1]$ for each $w \in WL$ and $\Sigma \in \text{Str}$ occurring on $\mathcal{B}$, and the following properties hold:

1. $\mathfrak{r}(\emptyset) = 0$, $\mathfrak{r}(1) = 1$;

2. $\mathfrak{r}(w)R_a\mathfrak{r}(w')$ if $w \in cl_a$ and $w' \in cl_a$ occur in $\mathcal{B}$ for some cluster-label $cl_a$;

3. if $\mathfrak{r}(\mathfrak{T}) = x$, then $\mathfrak{r}(1 - \mathfrak{T}) = 1 - x$ for every $\mathfrak{T} \in \mathfrak{T}$;

4. $(\{\mathfrak{r}(t) \mid t \in \mathfrak{T}(cl_a)\} \cup \{0, \frac{1}{2}, 1\}) \subseteq T_a(\mathfrak{r}(w))$ and $\mathfrak{r}(t(cl_a)) < \mathfrak{r}(t^s(cl_a))$ for all $w \in WL$ and $a \in A$ s.t. $w \in cl_a$ occurs on $\mathcal{B}$;

5. there are no $t'(cl_a)$, $t(cl_a)$, $t^s(cl_a)$ on $\mathcal{B}$ s.t. $\mathfrak{r}(t(cl_a)) < \mathfrak{r}(t'(cl_a)) < \mathfrak{r}(t^s(cl_a))$;

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

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

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

Let us now give an example of a failed proof in $\mathcal{T}(\mathfrak{S}\mathfrak{5}\mathfrak{G}_{\text{inv}}^c)$. We will see how to construct a realising model from a complete open branch.

**Example 3.** Recall the formula $\phi_{\text{plaus}}$ from Example 1 and replace $\diamond$'s with $\square$'s as follows: $(\square_a(\sim p \to p) \wedge \sim \square_a \sim p) \to \sim \square_b \sim p$. A failed proof is given in Fig. 2.

First, consider the closed branches. All of them but the ones marked $\times_A$ and $\times_B$ contain constraints whose incompatibility is evident. In the leftmost branch: $w_0:p \geq 1$ and $w_0:p \leq 1 - 1$. In the second branch from the left: $w_0:p \leq 1 - 1$, $w_0:p \geq d_1$, and $w_0:p \geq 1 - d_1$. In the third branch: $w_0:p \geq t(cl_a^0)$, $t(cl_a^0) \geq d_0$, $w_0:p \leq 1 - 1$, and $w_0:\sim \square_b \sim p < d_0$; etc. To see why $\times_A$ is closed, observe
that $w_3:p < d_1$ and $w_3:p \le 1 - d_1$ imply that $v(p, w_3) < \frac{1}{2}$. Now as $d_0 > 0$ (because of $w_0:\sim \Box_b \sim p < d_0$), we know that $t_1(\mathbf{cl}_a^0) > 0$ as well. Note that $\mathbf{T}(\mathbf{cl}_a^0) = \{t_0(\mathbf{cl}_a^0), t_0^s(\mathbf{cl}_a^0), t_1(\mathbf{cl}_a^0), t^s(\mathbf{cl}_a^0)\}$. $\mathbf{T}(\mathbf{cl}_a^0)$ should be closed under $1-x$ and contain $0, \frac{1}{2}$, and $1$. Thus, $\mathbf{rl}(t_1(\mathbf{cl}_a^0)) = \frac{1}{2}$. But as we have $w_3:p \ge t_1(\mathbf{cl}_a^0)$, there is a contradiction. Similarly, for $\times_B$, $w_3:p \ge d_2$ and $w_3:p \ge 1 - d_2$ imply that $v(p, w_3) \ge \frac{1}{2}$ which again contradicts $w_3:p < d_1$ and $w_3:p \le 1 - d_1$.

Let us build an eF-model that realises $\Box_A$. We have three states — $w_0$, $w_1$, and $w_2$ — joined into the following clusters: $\mathbf{cl}_a^0 = \{w_0, w_2\}$, $\mathbf{cl}_b^0 = \{w_0, w_1\}$, $\mathbf{cl}_a^1 = \{w_1\}$, and $\mathbf{cl}_b^1 = \{w_2\}$. We also have $\mathbf{T}(\mathbf{cl}_a^0) = \{t_0(\mathbf{cl}_a^0), t_0^s(\mathbf{cl}_a^0), 1\}$ and $\mathbf{T}(\mathbf{cl}_b^0) = \{t(\mathbf{cl}_b^0), t^s(\mathbf{cl}_b^0)\}$ while $\mathbf{T}(\mathbf{cl}_a^1)$ and $\mathbf{T}(\mathbf{cl}_b^1)$ are not specified. For simplicity, we put $\mathbf{rl}(w_i) = w_i$ with $i \in \{0, 1, 2\}$. It is clear that $\mathbf{rl}(t_0(\mathbf{cl}_a^0)) = 0$ and $\mathbf{rl}(t_0^s(\mathbf{cl}_a^0)) = \frac{1}{2}$. As for the realisation of $\mathbf{T}(\mathbf{cl}_b^0)$, we have $\mathbf{rl}(t(\mathbf{cl}_b^0)) = \frac{1}{2}$ and $\mathbf{rl}(t^s(\mathbf{cl}_b^0)) = 1$ since $t(\mathbf{cl}_b^0) \ge d_0$ and $w_0:\sim \Box_b \sim p < d_0$ occur on the branch. Finally, we have $v(p, w_2) = 1$ because of $w_2:p \ge 1$; $v(p, w_0) \ge \frac{1}{2}$ because of $w_0:p \ge d_1$ and $w_0:p \ge 1 - d_1$; $v(p, w_1) \in (0, \frac{1}{2}]$. A model can be seen in Fig. 3.

A straightforward check gives us that $v(\Box_a(\sim p \rightarrow p), w_0) = 1$, $v(\sim \Box_a \sim p, w) = 1$ but $v(\sim \Box_b \sim p, w_0) = \frac{1}{2}$. Thus, $v(\phi_{\text{plaus}}, w_0) = \frac{1}{2} < 1$.

We are now ready to obtain the completeness of tableaux w.r.t. eF-models. The proof is standard and follows [32, Theorems 6.9 and 6.11] and [5, Theorem 2].

**Theorem 1.** $\phi \in \mathcal{L}_{\Box}^{\sim}$ is eF-valid iff it has a $\mathcal{T}(\mathbf{S5G}_{\text{inv}}^{c})$ proof.

# 4 Complexity

In the previous section, we constructed a tableaux calculus that allows us to check whether a given formula is valid on eF-models. Let us now produce a polynomial space decision procedure on its basis. We adapt the proof of the PSpace-completeness of $KG_{\text{inv}}$ from [5].

**Theorem 2.**

1. Let $|A| \ge 2$. Then it is PSpace-complete to decide whether $\phi \in \mathcal{L}_{\Box}^{\sim}(A)$ is valid on eF-models for A.

2. Let $|A| = 1$. Then it is coNP-complete to decide whether $\phi \in \mathcal{L}_{\Box}^{\sim}(A)$ is valid on eF-models for A.

*Proof.* We show Item 1 only (cf. the appendix for Item 2). Consider first PSpace-hardness. We provide a polynomial-time reduction from the validity in classical S5 which is known to be coNP-complete if $|A| = 1$ and PSpace-complete if $|A| \ge 2$ [22]. Let $\phi \in \mathcal{L}_{\Box}^{\sim}$, and denote $\phi^{\Delta}$ the result of replacing every occurrence $p$ of every propositional variable $p$ with $\Delta p$ (recall Convention 1 for the definition and semantics of $\Delta$). It is clear from Convention 1 that $\mathcal{L}(\phi^{\Delta}) = \mathcal{O}(\mathcal{L}(\phi))$.

Now let $\mathfrak{F} = \langle W, \langle R_a \rangle_{a \in A} \rangle$ be an epistemic frame. Let further, $v$ be a classical valuation on $\mathfrak{F}$ and denote $\mathfrak{M} = \langle W, \langle R_a \rangle_{a \in A}, v \rangle$. We define an eF-model $\mathfrak{M}^{\Delta} = \langle W, \langle R_a \rangle_{a \in A}, \langle T_a^{\Delta} \rangle_{a \in A}, v^{\Delta} \rangle$ as follows: $T_a^{\Delta}(w) = \{0, \frac{1}{2}, 1\}$ for every $w \in W$
<figure><img src="image_2.png" /><figcaption>Fig. 2: A failed proof of $(\square_a(\sim p \to p) \land \sim \square_a \sim p) \to \sim \square_b \sim p$. ⊙'s denote complete open branches.</figcaption></figure>

$$ w_1 : p = \frac{1}{2} \quad \ldots \quad R_b \quad \ldots \quad w_0 : p = \frac{1}{2} \quad \ldots \quad R_a \quad \ldots \quad w_2 : p = 1 \\ \forall w : T_a(w) = T_b(w) = \{0, \frac{1}{2}, 1\} $$

<caption>Fig. 3: A countermodel for ⊙<sub>A</sub> (cf. Fig. 2). Reflexive arrows are not shown.</caption>
and $a \in A$; $v^\Delta(p, w) = v(p, w)$. We can now check by induction on $\phi$ that $v^\Delta(\phi^\Delta, w) = v(\phi, w)$ for every $\phi \in \mathcal{L}_{\square}^\sim$ and $w \in W$.

The basis case of $\phi = p$ and $\phi^\Delta = \Delta p$ is evident from (1). The cases of propositional connectives $\sim$, $\wedge$, and $\rightarrow$ follow by a straightforward application of the induction hypothesis since propositional connectives behave classically on $\{0, 1\}$, $\Delta$ behaves trivially on $\{0, 1\}$, and $v^\Delta$ assigns only 0 and 1. Thus, it suffices to check that $v^\Delta(\phi^\Delta, w) = 1$ iff $v(\phi, w) = 1$. Consider now $\phi = \Box_a \chi$ and $\phi^\Delta = \Box_a \chi^\Delta$. We have

$$ 
\begin{array}{l}
v(\Box_a \chi, w) = 1 \quad \text{iff } \forall w' : w R_a w' \Rightarrow v(\chi, w') = 1 \\
\qquad \text{iff } \forall w' : w R_a w' \Rightarrow v^\Delta(\chi^\Delta, w') = 1 \quad (\text{by IH}) \\
\qquad \text{iff } v^\Delta(\Box_a \chi^\Delta) = 1
\end{array}
$$

For the converse direction, let $\mathfrak{M} = \langle W, \langle R_a \rangle_{a \in A}, \langle T_a \rangle_{a \in A}, v \rangle$ be an eF-model. We define a classical S5-model $\mathfrak{M} = \langle W, \langle R_a \rangle_{a \in A}, v^{\text{cl}} \rangle$ as follows: $v^{\text{cl}}(p, w) = 1$ if $v(p, w) = 1$ and $v^{\text{cl}}(p, w) = 0$, otherwise. Again, by induction on $\phi$, we show that $v(\phi^\Delta, w) = v^{\text{cl}}(\phi, w)$. First, observe that since every variable of $\phi^\Delta$ is in the scope of a $\Delta$, $v(\phi^\Delta, w) \in \{0, 1\}$ in every $w \in W$. Now, let $\phi = p$ and $\phi^\Delta = \Delta p$. If $v(\Delta p, w) = 1$, then $v(p, w) = 1$ whence, $v^{\text{cl}}(p, w) = 1$. If $v(\Delta p, w) = 0$, then $v(p, w) < 1$, whence, $v^{\text{cl}}(p, w) = 0$. The cases of propositional connectives can be dealt with by direct applications of the induction hypothesis. Finally, let $\phi = \Box_a \chi$ and $\phi^\Delta = \Box_a \chi^\Delta$. If $v(\Box_a \chi^\Delta, w) = 1$, then $v(\chi^\Delta, w') = 1$ in every $w'$ s.t. $w R_a w'$. Thus, $v^{\text{cl}}(\chi, w') = 1$ in all such $w'$'s by the induction hypothesis, whence $v^{\text{cl}}(\Box_a \chi, w) = 1$. If $v(\Box_a \chi^\Delta, w) = 0$, then recall that $\chi^\Delta$ can have only values in $\{0, 1\}$. Thus, there is some $w'$ s.t. $w R_a w'$ and $v(\chi^\Delta, w') = 0$. Again, by the induction hypothesis, we obtain $v^{\text{cl}}(\chi, w') = 0$, whence, $v^{\text{cl}}(\Box_a \chi, w) = 0$, as required.

For the PSpace-membership, we begin by observing that every tableau terminates. Indeed, all rules except for $\Box_\Delta$ are finitely branching and decompose the formulas in the premise. If $\Box_\Delta$ is applied, then a constraint of the form $w:\Box_a \psi = \mathfrak{T}$ is introduced to which we can apply $\Box_\Delta$ which does decompose the formula. Moreover, as we have noticed in Section 3, if a branch contains several instances of a modal constraint in different states of the same cluster, it suffices to apply a modal rule to only one such instance.

For simplicity, we assume that $A = \{a, b\}$. Decision procedures for larger A's can be obtained in a similar manner. The algorithm runs as follows: given $\phi$, we start building a tableau for $\mathfrak{T}(\phi) = \{w:\phi < 1, w \in \mathfrak{cl}_a^0, w \in \mathfrak{cl}_b^0\}$. If a rule introduces branching, we pick one branch of the tableau and work with it depth-first. If the branch we are working with is closed, we delete it and choose the next one. Our goal is to build a model realising $\mathfrak{T}(\phi)$ 'on the fly' (cf. Fig. 4 for an illustration). As we proceed depth-first on the tableau, we denote the branch we are working on with $\mathcal{B}$.

We begin with applying propositional rules until all labelled formulas in $\mathcal{B}$ have $\Box$'s as principal connectives. Once all propositional rules are applied, we pick $a \in A$ and apply modal rules for $\Box_a$-formulas. We begin with $\Box_\Delta$, $\Box_\leq$, and $\Box_<$ rules. After all such rules are applied, we apply $\equiv_{\text{cl}}$ rules and propositional rules if needed. This adds $\mathcal{O}(\ell(\phi))$ states to the $R_a$-cluster $\mathfrak{cl}_a^0$. Then we apply
□= rules using the generated states. Note that □= uses the states generated by the applications of other modal rules. Moreover, as we apply all instances of □= in $cl_a^0$ at once, we have to first apply all rules □> , □< , □< , and $≡_{cl}$ in $cl_a^0$ (otherwise, some instances of □= might not be applicable). Note that □= is the only modal rule that can become applicable after the application of □> . Observe also that we avoid generating new (proper) clusters until all modal rules are applied in $cl_a^0$.

Once done, we pick one state (say, $u$) in $cl_a^0$ s.t. $u : \Box_b \psi \triangledown \mathcal{T}$ is present on $\mathcal{B}$ and mark $u$ as ‘active’. We then apply modal rules for $\Box_b$ in the described manner but to $u$ only. This generates an $R_b$-cluster (say, $cl_b^1$) that also contains at most $\ell(\phi)$ states. In this cluster, we pick a state $u'$ s.t. $u' : \Box_a \psi' \triangledown \mathcal{T}' \in \mathcal{B}$, mark $u'$ ‘active’, and repeat the process until we obtain a cluster that does not contain labelled formulas of the form $\Box_a \chi \triangledown \mathcal{X}$ (say, $cl_b'$ that was generated by a state $s$ in an $R_a$-cluster $cl_a'$). We will generate at most $\ell(\phi)$ clusters: there will be as many clusters as alternations of agent labels of nested modalities$^6$ and each of these will have at most $\ell(\phi)$ states. We check whether $\mathcal{B}$ is closed. Note that a model satisfying $\mathcal{B}$ can be guessed in non-deterministic polynomial time.

If $\mathcal{B}$ is open, we mark every state $u''$ s.t. $u'' \in cl_b'$ occurs on $\mathcal{B}$ as ‘safe’. Then we delete all labelled formulas of the form $u' : \chi \triangledown \mathcal{X}$ s.t. $u' \in cl_b'$ occurs on $\mathcal{B}$ from $\mathcal{B}$. Furthermore, we delete all non-active states in $cl_b'$ and remove the ‘active’ mark from $s$. Then we pick another state in $cl_a'$ and repeat the process. The algorithm runs until either $w$ is marked as ‘safe’ (whence, $\phi$ is not valid) or all branches of the tableau are closed (in which case, $\phi$ is valid). Since, as we have remarked earlier, all tableaux terminate, we will stop at some point. Note furthermore, that at any given time the branch of the tableau contains at most $\ell(\phi)$ proper clusters each with at most $\ell(\phi)$ states (i.e., $\mathcal{O}(\ell(\phi)^2)$ states in total). Each state contains subformulas of $\phi$ occurring in constraints, constraints consisting of two value terms, and relational terms indicating to which clusters it belongs. Thus, we need $\mathcal{O}(\ell(\phi)^3)$ space to execute the algorithm.

# 5 Equivalence with the standard semantics

In Sections 3 and 4, we provided a sound and complete tableaux calculus for $S5G_{inv}^c$ and obtained the complexity of validity. We can also obtain the finite model property for the eF-model based semantics.

**Corollary 1.** A formula $\phi \in \mathcal{L}_{\square}^{\sim}$ is valid on all eF-models iff it is valid on all finite eF-models.

*Proof.* As $\mathcal{T}(S5G_{inv}^c)$ is sound and complete and each complete open branch in the failed proof of $\phi$ contains a finite eF-countermodel of $\phi$, the statement follows.

It remains to show that the sets of formulas valid on $S5G_{inv}^c$-models and eF-models coincide. To do this, we adapt the approaches of [13] and [5].

<footnote>$^6$ E.g., it suffices to use one cluster for $\Box_a \Box_{ap}$, but we need two clusters for $\Box_a \Box_b q$.</footnote>
<figure><img src="image_3.png" /><figcaption>Fig. 4: Building an eF-model from a tableau proof on the fly: ellipses denote proper clusters; active states are marked with ○'s; safe states are green.</figcaption></figure>

We begin with a special version of the tree model property. Namely, we show that it suffices to check whether a formula is satisfiable on eF-models whose frame is a tree of proper clusters (cf. Fig. 5 for an illustration).

**Definition 7.** Let $\mathfrak{F} = \langle W, \langle R_a \rangle_{a \in A} \rangle$ be an epistemic frame for A. Given two proper clusters $cl$ and $cl'$ in $\mathfrak{F}$, we write $cl \prec cl'$ if $cl \neq cl'$ and $|cl \cap cl'| = 1$.

We say that $\mathfrak{F}$ is a cluster tree if it holds that:

- any two distinct proper clusters have at most one state in common;

- $\langle cl(\mathfrak{F}), \emptyset \rangle$ is a tree.

If we designate $cl$ as the root of $\mathfrak{F}$, we say that the height of $\mathfrak{F}$ ($\mathcal{H}(\mathfrak{F})$) is the number of proper clusters in the longest branch originating from $cl$.

An epistemic (F-)model $\mathfrak{M}$ whose underlying frame is a cluster tree is called an epistemic cluster tree (F-)model. The height of $\mathfrak{M}$ ($\mathcal{H}(\mathfrak{M})$) is the height of its underlying frame.

The following statement now follows from Theorem 1 since the models produced by tableaux are cluster trees.

**Corollary 2.** For any $\phi \in \mathcal{L}_{\square}^{\sim}$, it holds that $v(\phi, w) = x$ in some eF-model $\mathfrak{M}$ and $w \in \mathfrak{M}$ iff there are a cluster tree eF-model $\mathfrak{M}'$ and $w' \in \mathfrak{M}'$ s.t. $v(\phi, w') = x$, $\mathcal{H}(\mathfrak{M}) = \mathcal{O}(l'(\phi))$, and the root of $\mathfrak{M}'$ is the proper cluster to which $w'$ belongs.
<figure><img src="image_4.png" /><figcaption>Fig. 5: Two epistemic frames for $A = \{\text{red, blue}\}$. $\mathfrak{F}$ a cluster tree; $\mathfrak{G}$ is **not**.</figcaption></figure>

We can now use Corollary 2 to obtain the equivalence between the semantics.
The next statement can be shown similarly to [5, Theorem 1].

**Theorem 3.** An $\mathcal{L}^{\sim}_{\square}$-formula $\phi$ is $\mathbf{S5G}^{c}_{\text{inv}}$-valid iff it is eF-valid.

*Proof.* If $\phi$ is invalidated in an $\mathbf{S5G}^c_{\text{inv}}$-model $\mathfrak{M}$, we reuse it as an eF-model. We define $T_a(w)$'s as the sets of values of $\square_a$-subformulas of $\phi$ and their $\sim$-negations at $w$, adding $\{0, \frac{1}{2}, 1\}$ if needed. This way, $T_a$'s will be finite and satisfy the conditions from Definition 3, and the values of modal formulas will be preserved. Hence, $\phi$ will be invalidated in an eF-model. For the converse direction, we use the proofs of Lemmas 2 and 4 in [13] and Corollary 2. Given $\phi$, a cluster-tree eF-model $\mathfrak{M}$ and $w \in \mathfrak{M}$ in its root cluster, we construct an $\mathbf{S5G}^c_{\text{inv}}$-model $\mathfrak{M}\tilde{\wedge}$ and $\tilde{w} \in \mathfrak{M}\tilde{\wedge}$ s.t. $v(\phi, w) = \tilde{v}(\phi, \tilde{w})$. We consider countably infinitely many order embeddings $h_k^a : [0, 1] \to [0, 1]$ for each $a \in A$ with $h_k^a(0) = 0$, $h_k^a(1-x) = 1 - h_k^a(x)$, and $h_k^a(1) = 1$ that 'squeeze' the open intervals between members of $T_a(w)$ closer to either their lower or upper bounds. Then we take infinitely many copies of the clusters in the original F-model without $T_a$'s obtained via these embeddings. The resulting infima and suprema will coincide with the next smaller or larger member of $T_a(w)$. Thus, the required values of the formulas at $w$ in the original F-model will be preserved.

**Corollary 3.**

1. It is PSpace-complete to decide whether $\phi \in \mathcal{L}^{\sim}_{\square}(A)$ is $\mathbf{S5G}^{c}_{\text{inv}}$-valid if $|A| \ge 2$.

2. It is coNP-complete to decide whether $\phi \in \mathcal{L}^{\sim}_{\square}(A)$ is $\mathbf{S5G}^{c}_{\text{inv}}$-valid if $|A| = 1$.

# 6 Conclusion

In this paper, we presented an epistemic Gödel logic with involutive nega-
tion $\mathbf{S5G}^c_{\text{inv}}$. We built its semantics with the finite model property and used
it to show that $\mathbf{S5G}^c_{\text{inv}}$-validity is PSpace-complete (coNP-complete in the single
agent case). Our next steps are as follows. First, we are not aware of any ax-
iomatisation of $\mathbf{S5G}^c_{\text{inv}}$ (nor of any Gödel modal logic with $\sim$). Thus, it makes
sense to provide one. Second, we plan to expand the eF-model-based semantics
for the case of *doxastic* Gödel logics. Finally, it would be instructive to adapt the
F-model-based semantics for Gödel modal logics with group knowledge operators
such as distributed or common knowledge.
References

1. Aguilera, J., Diéguez, M., Fernández-Duque, D., McLean, B.: Time and Gödel: Fuzzy Temporal Reasoning in PSPACE. In: Logic, Language, Information, and Computation, Lecture notes in computer science, vol. 13368, pp. 18–35. Springer International Publishing, Cham (2022)

2. Aguilera, J., Diéguez, M., Fernández-Duque, D., McLean, B.: 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 (2022)

3. Baaz, M.: 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, pp. 23–33. Association for Symbolic Logic (1996)

4. Benevides, M., Madeira, A., Martins, M.: Graded epistemic logic with public announcement. Journal of Logical and Algebraic Methods in Programming **125**, 100732 (Feb 2022)

5. Bílková, M., Ferguson, T., Kozhemiachenko, D.: Modal logic for reasoning about uncertainty and confusion. In: Bjorndahl, A. (ed.) Theoretical Aspects of Rationality and Knowledge 2025 (TARK 2025). pp. 211–227. Electronic Proceedings in Theoretical Computer Science (2025), TARK2025:14 (to appear)

6. Blackburn, P., Rijke, M.d., Venema, Y.: Modal logic. Cambridge tracts in theoretical computer science 53, Cambridge University Press, 4. print. with corr. edn. (2010)

7. Bobillo, F., Delgado, M., Gómez-Romero, J., Straccia, U.: Fuzzy description logics under Gödel semantics. International Journal of Approximate Reasoning **50**(3), 494–514 (Mar 2009)

8. Bobillo, F., Delgado, M., Gómez-Romero, J., Straccia, U.: Joining Gödel and Zadeh fuzzy logics in fuzzy description logics. International Journal of Uncertainty Fuzziness and Knowledge-Based Systems **20**(04), 475–508 (Aug 2012)

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

10. Borgwardt, S., Distel, F., Peñaloza, R.: 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 (2014)

11. Borgwardt, S., Distel, F., Peñaloza, R.: 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. vol. 1193, pp. 391–403. CEUR (2014)

12. Borgwardt, S., Peñaloza, R.: Algorithms for reasoning in very expressive description logics under infinitely valued Gödel semantics. International Journal of Approximate Reasoning **83**, 60–101 (Apr 2017)

13. Caicedo, X., Metcalfe, G., Rodríguez, R., Rogger, J.: A finite model property for Gödel modal logics. In: Libkin, L., Kohlenbach, U., Queiroz, R.d. (eds.) International Workshop on Logic, Language, Information, and Computation. Lecture Notes in Computer Science, vol. 8071, pp. 226–237. Springer, Berlin, Heidelberg (2013)

14. Caicedo, X., Metcalfe, G., Rodríguez, R., Rogger, J.: Decidability of order-based modal logics. Journal of Computer and System Sciences **88**, 53–74 (Sep 2017)

15. Caicedo, X., Rodriguez, R.: Standard Gödel modal logics. Studia Logica **94**(2), 189–214 (2010)
16. Caicedo, X., Rodríguez, R.: Bi-modal Gödel logic over [0,1]-valued Kripke frames. Journal of Logic and Computation **25**(1), 37–55 (2015)

17. Ditmarsch, H.v., Hoek, W.v.d., Kooi, B.: Dynamic Epistemic Logic. Synthese Library, Springer, New York, 2008 edn. (Jun 2007)

18. Fagin, R., Halpern, J., Moses, Y., Vardi, M.: Reasoning About Knowledge. MIT Press, Cambridge, MA, USA (2003)

19. Gärdenfors, P.: Qualitative probability as an intensional logic. Journal of Philosophical Logic pp. 171–185 (1975)

20. Goré, R.: Dual Intuitionistic Logic Revisited. In: Dyckhoff, R. (ed.) Automated Reasoning with Analytic Tableaux and Related Methods. TABLEAUX 2000, Lecture notes in computer science, vol. 1847, pp. 252–267. Springer Berlin Heidelberg, Berlin, Heidelberg (2000)

21. Hähnle, R.: Tableaux for many-valued logics. In: D'Agostino, M., Gabbay, D., Hähnle, R., Posegga, J. (eds.) Handbook of Tableaux Methods. pp. 529–580. Springer-Science+Business Media, B.V. (1999)

22. Halpern, J., Moses, Y.: A guide to completeness and complexity for modal logics of knowledge and belief. Artificial Intelligence **54**(3), 319–379 (Apr 1992)

23. Hoek, W.: Qualitative modalities. International Journal of Uncertainty, Fuzziness and Knowledge-Based Systems **04**(01), 45–59 (Feb 1996)

24. Hoek, W., Meyer, J.J.: Graded modalities in epistemic logic. In: Logical Foundations of Computer Science — Tver '92, Lecture notes in computer science, vol. 620, pp. 503–514. Springer Berlin Heidelberg, Berlin, Heidelberg (1992)

25. Lorini, E., Schwarzentruber, F.: A computationally grounded logic of graded belief. In: Logics in Artificial Intelligence. 17th European Conference, Lecture notes in artificial intelligence, vol. 12678, pp. 245–261. Springer International Publishing, Cham (2021)

26. Metcalfe, G., Olivetti, N.: 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, vol. 5607, pp. 265–279. Springer (2009). https://doi.org/10.1007/978-3-642-02716-1_20

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

28. Priest, G.: An Introduction to Non-Classical Logic. From If to Is. Cambridge University Press, 2nd edn. (2008)

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

30. Rodriguez, R., Tuyt, O., Esteva, F., Godo, L.: Simplified Kripke semantics for K45-like Gödel modal logics and its axiomatic extensions. Studia Logica **110**(4), 1081–1114 (Aug 2022)

31. Rodriguez, R., Vidal, A.: Axiomatization of Crisp Gödel Modal Logic. Studia Logica **109**, 367–395 (2021)

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

33. Wansing, H.: Constructive negation, implication, and co-implication. Journal of Applied Non-Classical Logics **18**(2–3), 341–364 (2008)
A Proofs of Section 3

**Theorem 1.** $\phi \in \mathcal{L}^{\sim}_{\square}$ is eF-valid iff it has a $\mathcal{T}(\mathbf{S5G}_{\text{inv}}^{\mathcal{e}})$ proof.

*Proof.* We begin with soundness. It is clear from Definitions 5 and 6 that if $\mathcal{B}$ is a closed branch, then there is no $\mathfrak{M}$ and $\mathfrak{r}$ s.t. $\mathfrak{M}$ realises $\mathcal{B}$ under $\mathfrak{r}$. Thus, it suffices to establish that if $\mathfrak{M}$ realises the premise of a rule, then it should realise at least one conclusion as well. We consider the case of the $\square_{\triangleleft}$ rule as an example. In particular, we assume that the premise is as follows: $\{w:\square_a\phi \leq \mathfrak{T}, w \in \mathfrak{c}_a\}$. Let $\mathfrak{M} = \langle W, \langle R \rangle_{a \in A}, \langle T_a \rangle_{a \in A}, v \rangle$ realise $w:\square_a\phi \leq \mathfrak{T}$. That is, $v(\square_a\phi, w) \leq \mathfrak{r}(\mathfrak{T})$. If $\mathfrak{r}(\mathfrak{T}) = 1$, then $1 \leq \mathfrak{T}$ (the left conclusion) is realised. Consider the case where $\mathfrak{r}(\mathfrak{T}) < 1$. Then (cf. Definition 3) $\max\{x \in T_a(w) \mid x \leq \inf\{v(\phi, w') \mid wR_a w'\}\} \leq \mathfrak{r}(\mathfrak{T})$. This means that there is a state $w'$ $R_a$-accessible from $w$ (i.e., in the same $R_a$-cluster as $w$) and $x, x' \in T_a(w)$ s.t. $x'$ is the immediate successor of $x$, $v(\square_a\phi, w) = x$, and $v(\phi, w') < x'$. Now setting $\mathfrak{r}(t(\mathfrak{c}_a)) = x$ and $\mathfrak{r}(t^s(\mathfrak{c}_a)) = x'$, we have that $t(\mathfrak{c}_a) \leq \mathfrak{T}$ and $w' : \phi < t^s(\mathfrak{c}_a)$ are realised. Hence, as $T_a(w) = T_a(w')$ when $wR_a w'$, the right conclusion is realised.

Let us now proceed to completeness. We will prove that for every complete open branch, there is a model $\mathfrak{M}$ and a realisation $\mathfrak{r}$ s.t. $\mathfrak{M}$ realises $\mathcal{B}$ under $\mathfrak{r}$. Let $\mathcal{B}$ be a complete open branch and consider the system of inequalities $\mathcal{B}^t$ as shown in (2) and its solution as specified in Definition 5. Now define $\mathfrak{M}$ as follows:

$$
\begin{align*}
W &= \{w \mid w \text{ occurs in } \mathcal{B}\} \\
wR_a w' \quad \text{iff} \quad \exists \mathfrak{c}_a \in \mathfrak{C}, a \in A : w \in \mathfrak{c}_a \text{ and } w' \in \mathfrak{c}_a \text{ occur on } \mathcal{B} \\
T_a(w) &= \{x_{t(\mathfrak{c}_a)} \mid w \in \mathfrak{c}_a \text{ and } t(\mathfrak{c}_a) \text{ occur in } \mathcal{B}\} \cup \\
&\phantom{=} \quad \{x_{t^s(\mathfrak{c}_a)} \mid w \in \mathfrak{c}_a \text{ and } t^s(\mathfrak{c}_a) \text{ occur in } \mathcal{B}\} \cup \{0, \frac{1}{2}, 1\} \\
v(p, w) &= x_{w:p}
\end{align*}
$$

for every $w$, $w'$, and $p \in \text{Prop}$ occurring in $\mathcal{B}$. We also set $\mathfrak{r}(w) = w$, $\mathfrak{r}(\mathfrak{T}) = x_{\mathfrak{T}}$, and $\mathfrak{r}(w:\chi) = x_{w:\chi}$ for every $w \in \text{WL}$, $\mathfrak{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 $\mathfrak{r}$.

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

We consider $w:\square_a\phi \leq \mathfrak{T}$ as an example and show that $v(\square_a\phi, w) \leq \mathfrak{r}(\mathfrak{T})$. Since $w:\square_a\phi \leq \mathfrak{T}$ is in $\mathcal{B}$ and $\mathcal{B}$ is complete and open, it also contains (a) $1 \leq \mathfrak{T}$ or (b) $t(\mathfrak{c}_a) \leq \mathfrak{T}$, $w' : \phi < t^s(\mathfrak{c}_a)$, $w' \in \mathfrak{c}_a$, and $w' \in \mathfrak{c}'_{a'}$ for every $a' \in A$. If (a) is the case, $\mathfrak{T}$ is a value term (observe from Definition 4 that constraints can contain at most one labelled formula), whence $1 \leq \mathfrak{T}$ is realised by the construction of $\mathfrak{M}$. Thus, $\mathfrak{r}(\mathfrak{T}) = 1$ and $v(\square_a\phi, w) \leq \mathfrak{r}(\mathfrak{T})$, as required. If (b) is the case, then by the induction hypothesis $t(\mathfrak{c}_a) \leq \mathfrak{T}$ and $w' : \phi < t^s(\mathfrak{c}_a)$ are realised, and $w$ and $w'$ belong to the same $R_a$-cluster. Thus, $x_{t(\mathfrak{c}_a)} \leq \mathfrak{r}(\mathfrak{T})$ and $v(\phi, w') < x_{t^s(\mathfrak{c}_a)}$ with $\{x_{t(\mathfrak{c}_a)}, x_{t^s(\mathfrak{c}_a)}\} \subseteq T(w)$ and $x_{t^s(\mathfrak{c}_a)}$ being the immediate successor of $x_{t(\mathfrak{c}_a)}$.
But in this case, it is clear that $v(\square_a\phi, w) = \max\{x \in T(w) \mid x \le \inf\{v(\phi, w') \mid wR_a w'\}\} \le x_{t(w)}$, whence, $v(\square_a\phi, w) \le \mathrm{rl}(\mathfrak{T})$, as required.

## B Proofs of Section 4

We supply the missing details of the proof of Theorem 2. Namely, we show that the validity of $\mathcal{L}_{\square}^{\sim}(A)$-formulas with $A = \{a\}$ is coNP-complete.

**Theorem 2.**

1. Let $|A| \ge 2$. Then it is PSpace-complete to decide whether $\phi \in \mathcal{L}_{\square}^{\sim}(A)$ is valid on eF-models for A.

2. Let $|A| = 1$. Then it is coNP-complete to decide whether $\phi \in \mathcal{L}_{\square}^{\sim}(A)$ is valid on eF-models for A.

*Proof.* To see that Item 2 holds, observe that if $A = \{a\}$, we will generate only one cluster of size $\mathcal{O}(\ell(\phi))$. Furthermore, every cluster will contain $\mathcal{O}(\ell(\phi))$ T-symbols (at most two for each $\square$ occurring in $\phi$). Thus, applying Theorem 1, we have that if $\phi$ is not valid on eF-models, there is some eF-model $\mathfrak{M}$ of the size $\mathcal{O}(\ell(\phi))$ s.t. $v(\phi, u) \ne 1$ for some $u \in \mathfrak{M}$ and for every $w \in \mathfrak{M}$, it holds that $|T_a(w)| = \mathcal{O}(\ell(\phi))$. It is clear that given such a model and a state $w$, it takes only polynomial time w.r.t. $\ell(\phi)$ to determine whether $v(\phi, w) = 1$. Thus, the validity of single-agent $\mathcal{L}_{\square}^{\sim}$-formulas over eF-models is in coNP.

## C Proofs of Section 5

In this section, we supply the proofs of Corollary 2 and Theorem 3. For the sake of brevity, we assume that $A = \{a, b\}$. The cases of larger sets of agents can be dealt with in a similar manner.

We begin with a technical notion.

**Definition 8 (Modal alternation depth).** Let $\phi \in \mathcal{L}_{\square}^{\sim}(A)$ be represented as a syntactical rooted tree and let further $A = \{a_1, \dots, a_m\}$.

Let $\mathbf{n}$ be a node in the tree for $\phi$. We say that it is modal if $\mathbf{n} \in \{\square_a \mid a \in A\}$ and propositional, otherwise. Let, further, $\mathbf{p}(\mathbf{n})$ be the parent of $\mathbf{n}$. We define the alternation number of $\mathbf{n}$ ($\mathcal{N}(\mathbf{n})$) as follows.

- If $\mathbf{n}$ is the root of the tree and propositional, then $\mathcal{N}(\mathbf{n}) = 0$.

- If $\mathbf{n}$ is the root of the tree and modal, then $\mathcal{N}(\mathbf{n}) = 1$.

- If $\mathbf{n}$ is not the root and propositional, then $\mathcal{N}(\mathbf{n}) = \mathcal{N}(\mathbf{p}(\mathbf{n}))$.

- If $\mathbf{n}$ is not the root, is modal, and the previous modal node $\mathbf{n}$ is s.t. $\mathbf{n}' = \mathbf{n}$, then $\mathcal{N}(\mathbf{n}) = \mathcal{N}(\mathbf{p}(\mathbf{n}))$.

- If $\mathbf{n}$ is not the root, is modal, and the previous modal node $\mathbf{n}$ is s.t. $\mathbf{n}' \ne \mathbf{n}$ or all nodes above $\mathbf{n}$ are propositional, then $\mathcal{N}(\mathbf{n}) = \mathcal{N}(\mathbf{p}(\mathbf{n})) + 1$.

The modal alternation depth of $\phi$ ($\mathcal{A}(\phi)$) is defined as follows:

$$ \mathcal{A}(\phi) = \max\{\mathcal{N}(\mathbf{n}) \mid \mathbf{n} \text{ is a leaf in the tree of } \phi\} $$
<figure><img src="image_5.png" /><figcaption>Fig. 6: Syntactical tree for $\Box_a(\Box_a(p \wedge \sim\Box_a q) \wedge \sim\Box_b(r \rightarrow \sim\Box_b(s \wedge \Box_a t))) \wedge u$.</figcaption></figure>
For example, let $\phi = \square_a(\square_a(p \wedge \sim\square_a q) \wedge \sim\square_b(r \rightarrow \sim\square_b(s \wedge \square_a t))) \wedge u$. Its syntactical tree is given in Fig. 6. To illustrate the definition, we write alternation numbers for each node. One can see that $\mathcal{A}(\phi) = 3$.

We now show that eF-satisfiability can be checked over cluster-tree models.

**Corollary 2.** For any $\phi \in \mathcal{L}_{\square}^{\sim}$, it holds that $v(\phi, w) = x$ in some eF-model $\mathfrak{M}$ and $w \in \mathfrak{M}$ iff there are a cluster tree eF-model $\mathfrak{M}'$ and $w' \in \mathfrak{M}'$ s.t. $v(\phi, w') = x$, $\mathcal{H}(\mathfrak{M}) = \mathcal{O}(\ell(\phi))$, and the root of $\mathfrak{M}'$ is the proper cluster to which $w'$ belongs.

*Proof.* The statement follows immediately from Theorem 1 and the fact that satisfiability and non-validity w.r.t. F-models are reducible to one another. Indeed, observe that our tableaux generate counter-models of $\phi$ that are cluster trees of the needed shape and of the height at most $\mathcal{A}(\phi) + 1$. To obtain a model satisfying $v(\phi, w) = x$, we simply build a tableau starting with $\{w:\phi \leq x, w:\phi \geq x\} \cup \{w \in \mathfrak{cl}_a | a \in \mathfrak{A}\}$. As $\mathcal{A}(\phi) = \mathcal{O}(\ell(\phi))$ for every $\phi \in \mathcal{L}_{\square}^{\sim}$, the result follows.

Let us proceed to the proof of Theorem 3. We begin with some lemmas. The following statement can be obtained in a standard manner by induction on $\phi \in \mathcal{L}_{\square}^{\sim}$.

**Lemma 1.** Fix a function $g : [0, 1] \rightarrow [0, 1]$ such that $g(0) = 0$, $g(1) = 1$, $g(1-x) = 1 - g(x)$, and $x \leq x'$ iff $g(x) \leq g(x')$. For an eF-model $\mathfrak{M} = \langle W, \langle R_a \rangle_{a \in \mathfrak{A}}, \langle T_a \rangle_{a \in \mathfrak{A}}, v \rangle$, define a model $\tilde{\mathfrak{M}}$ such that $\tilde{W} = W$, $\langle \tilde{R}_a \rangle_{a \in \mathfrak{A}} = \langle R_a \rangle_{a \in \mathfrak{A}}$, $\langle \tilde{T}_a \rangle_{a \in \mathfrak{A}} = \langle g[T]_a \rangle_{a \in \mathfrak{A}}$, and $\tilde{v}(p, w) = g(v(p, w))$ for every $w \in W$ and $p \in \mathbf{Prop}$. Then it holds that $\tilde{v}(\phi, w) = g(v(\phi, w))$ for each $\phi \in \mathcal{L}_{\square}^{\sim}$ and $w \in W$.

Next, we show that formulas can be transformed in such a way that one occurrence $\square_a$ is never in the immediate scope of another.

**Definition 9.** A formula is called irredundantly nested if in every branch of its syntactic tree between every two nodes $\square_a$, there is a node $\square_{a'}$ for some $a' \neq a$.

Note that $\mathcal{A}(\square_a \phi) = \mathcal{A}(\phi) + 1$ for every irredundantly nested $\phi$. Moreover, $\mathcal{A}(\phi) = \mathcal{D}(\phi)$ with $\mathcal{D}(\phi)$ being the modal depth of $\phi$. The converse, however, is not true: $\mathcal{D}(\square_a \square_b p \wedge \square_a \square_a q) = \mathcal{A}(\square_a \square_b p \wedge \square_a \square_a q) = 2$ but $\square_a \square_b p \wedge \square_a \square_a q$ is not irredundantly nested.

**Lemma 2.** For every $\phi \in \mathcal{L}_{\square}^{\sim}$, there is an irredundantly nested $\phi^b$ s.t. $\phi \leftrightarrow \phi^b$ is $S5G_{\text{inv}}^{\mathcal{C}}$-valid and eF-valid.

*Proof.* It suffices to check that the following equivalences hold in both semantics.

$$ \begin{array}{l@{\qquad}l} \Box_a \Box_a \chi \leftrightarrow \Box_a \chi & \Box_a \sim \Box_a \chi \leftrightarrow \sim \Box_a \chi & (3) \\ \Box_a (\chi \rightarrow \Box_a \psi) \leftrightarrow (\sim \Box_a \sim \chi \rightarrow \Box_a \psi) & \Box_a \sim (\chi \rightarrow \Box_a \psi) \leftrightarrow \sim (\Box_a \chi \rightarrow \Box_a \psi) & \\ \Box_a (\Box_a \chi \rightarrow \psi) \leftrightarrow (\Box_a \chi \rightarrow \Box_a \psi) & \Box_a \sim (\Box_a \chi \rightarrow \psi) \leftrightarrow \sim (\Box_a \chi \rightarrow \sim \Box_a \sim \psi) & \\ \Box_a (\chi \rightarrow \sim \Box_a \psi) \leftrightarrow (\sim \Box_a \sim \chi \rightarrow \Box_a \psi) & \Box_a \sim (\chi \rightarrow \sim \Box_a \psi) \leftrightarrow \sim (\Box_a \chi \rightarrow \sim \Box_a \psi) & \\ \Box_a (\sim \Box_a \chi \rightarrow \psi) \leftrightarrow (\sim \Box_a \chi \rightarrow \Box_a \psi) & \Box_a \sim (\sim \Box_a \chi \rightarrow \psi) \leftrightarrow \sim (\sim \Box_a \chi \rightarrow \sim \Box_a \sim \psi) & \\ & \Box_a \sim (\chi \wedge \Box_a \psi) \leftrightarrow \sim (\Box_a \sim \chi \wedge \sim \Box_a \psi) & \end{array} $$
$$ \Box_a \sim (\chi \wedge \sim \Box_a \psi) \leftrightarrow (\Box_a \sim \chi \wedge \Box_a \psi) $$

Note that all these equivalences are single-agent. Moreover, we can transform all of them into the negation normal form using the following validities: $\sim \Box_a \phi \leftrightarrow \Diamond_a \sim \phi$ and $\sim (\chi \rightarrow \psi) \leftrightarrow (\sim \psi \leftarrow \sim \chi)$. Thus, (3) can be replaced with the following equivalences.

$$ \begin{array}{l@{\qquad}l} \Box_a \Box_a \chi \leftrightarrow \Box_a \chi & \Box_a \Diamond_a \chi \leftrightarrow \Diamond_a \chi \hfill (4) \\ \Box_a (\chi \rightarrow \Box_a \psi) \leftrightarrow (\Diamond_a \chi \rightarrow \Box_a \psi) & \Box_a (\Diamond_a \psi \leftarrow \chi) \leftrightarrow (\Diamond_a \psi \leftarrow \Diamond_a \chi) \\ \Box_a (\Box_a \chi \rightarrow \psi) \leftrightarrow (\Box_a \chi \rightarrow \Box_a \psi) & \Box_a (\psi \leftarrow \Diamond_a \chi) \leftrightarrow (\Box_a \psi \leftarrow \Diamond_a \chi) \\ \Box_a (\chi \rightarrow \Diamond_a \psi) \leftrightarrow (\Diamond_a \chi \rightarrow \Diamond_a \psi) & \Box_a (\Box_a \psi \leftarrow \chi) \leftrightarrow (\Box_a \psi \leftarrow \Diamond_a \chi) \\ \Box_a (\Diamond_a \chi \rightarrow \psi) \leftrightarrow (\Diamond_a \chi \rightarrow \Box_a \psi) & \Box_a (\psi \leftarrow \Box_a \chi) \leftrightarrow (\Box_a \psi \leftarrow \Box_a \chi) \\ & \Box_a (\chi \vee \Diamond_a \psi) \leftrightarrow (\Box_a \chi \vee \Diamond_a \psi) \\ & \Box_a (\chi \vee \Box_a \psi) \leftrightarrow (\Box_a \chi \vee \Box_a \psi) \end{array} $$

As one can see, all propositional connectives in (4) are order-based (i.e., $\wedge$, $\vee$, $\rightarrow$, or $\leftarrow$). From [14], we know that the single-agent fragment of our semantics is equivalent to the standard semantics. Thus, it suffices to verify the equivalences above in the standard semantics of $\mathbf{S5G}_{\text{inv}}^{\mathbf{c}}$.

The validity of equivalences in (4) without $\leftarrow$ can be easily established by a routine check. Let us now consider $\phi = \underbrace{\Box_a (\Diamond_a \psi \leftarrow \chi)}_{\phi_L} \leftrightarrow \underbrace{(\Diamond_a \psi \leftarrow \Diamond_a \chi)}_{\phi_R}$ as an example. We note briefly that $v(\phi_L, w) \in \{0, v(\Box_a \Diamond_a \psi, w)\}$. Indeed, $v(\Diamond_a \psi \leftarrow \chi, w') \in \{0, v(\Diamond_a \psi, w')\}$ for every $R_a$-accessible $w'$, whence, the infimum of such values is either 0, or is equal to the infimum of the value of $\Diamond_a \psi$, i.e., to the value of $\Box_a \Diamond_a \psi$ at $w$.

Similarly, $v(\phi_R, w) \in \{0, v(\Diamond_a \psi, w)\}$. Note also that $\Box_a \Diamond_a \psi \leftrightarrow \Diamond_a \psi$ is $\mathbf{S5G}_{\text{inv}}^{\mathbf{c}}$-valid. Thus, it remains to see that the following two statements hold:

1. if $v(\Box_a (\Diamond_a \psi \leftarrow \chi), w) = 0$, then $v(\Diamond_a \psi \leftarrow \Diamond_a \chi, w) = 0$;

2. if $v(\Box_a (\Diamond_a \psi \leftarrow \chi), w) = v(\Box_a \Diamond_a \psi, w)$, then $v(\Diamond_a \psi \leftarrow \Diamond_a \chi, w) = v(\Diamond_a \psi, w)$.

For Item 1, we have that

$$ \begin{align*} v(\Box_a (\Diamond_a \psi \leftarrow \chi), w) = 0 &\Rightarrow \left[ \begin{array}{@{}l@{}} \inf\{v(\Diamond_a \psi, w') \mid wR_a w'\} = 0 \\ \text{or} \\ \exists wR_a w' : v(\Diamond_a \psi, w') \le v(\chi, w') \end{array} \right] \\ &\Rightarrow \left[ \begin{array}{@{}l@{}} \inf\{v(\psi, w') \mid wR_a w'\} = 0 \\ \text{or} \\ \exists wR_a w' : \sup\{v(\psi, w'') \mid w'' \in R_a(w)\} \le v(\chi, w') \end{array} \right] \\ &\Rightarrow \left[ \begin{array}{@{}l@{}} v(\Diamond_a \psi, w) = 0 \\ \text{or} \\ \sup_{w'' \in R_a(w)} v(\psi, w'') \le \sup_{wR_a w'} v(\chi, w') \end{array} \right] \\ &\Rightarrow v(\Diamond_a \psi \leftarrow \Diamond_a \chi, w) = 0 \end{align*} $$

For Item 2, we assume w.l.o.g. that $v(\Box_a \Diamond_a \psi, w) = v(\Diamond_a \psi, w) > 0$ and proceed as follows:

$$ \begin{align*} v(\Box_a (\Diamond_a \psi \leftarrow \chi), w) = v(\Diamond_a \psi, w) &\Rightarrow \inf_{wR_a w'} v(\Diamond_a \psi \leftarrow \chi, w) = v(\Diamond_a \psi, w) \\ &\Rightarrow \sup_{wR_a w'} v(\psi, w') > \sup_{w'' \in R_a(w)} v(\chi, w'') \end{align*} $$
$$ \begin{align*} \Rightarrow v(\diamond_a \psi, w) &> v(\diamond_a \chi, w) \\ \Rightarrow v(\diamond_a \psi \prec \diamond_a \chi, w) &= v(\diamond_a \psi, w) \end{align*} $$

The remaining cases can be dealt with in a similar manner.

We recall briefly that a pointed model is a pair $\langle \mathfrak{M}, w \rangle$ with $\mathfrak{M}$ being a model ($\mathbf{S5G}_{\text{inv}}^{\mathfrak{c}}$-model or eF-model, in our case) and $w$ a state in $\mathfrak{M}$. We can now use Lemmas 1 and 2 to show that pointed cluster-tree eF-models $\langle \mathfrak{M}, w \rangle$ can be transformed into pointed $\mathbf{S5G}_{\text{inv}}^{\mathfrak{c}}$-models $\langle \widetilde{\mathfrak{M}}, \hat{w} \rangle$ s.t. $v(\phi, w) = \hat{v}(\phi, \hat{w})$ provided that $\mathcal{A}(\phi)$ is bounded by $\mathcal{H}(\mathfrak{M})$. The next statement can be obtained by combining Lemmas 2 and 4 from [13].

**Lemma 3.** For every pointed cluster tree eF-model $\langle \mathfrak{M}, w_0 \rangle$ with $w_0$ belonging to the root cluster $cl_a$ of $\mathfrak{M}$ and every $\phi \in \mathcal{L}_{\square}^{\sim}$ s.t. $\mathcal{A}(\phi) \le \mathcal{H}(\mathfrak{M})$, there is a pointed $\mathbf{S5G}_{\text{inv}}^{\mathfrak{c}}$-model $\langle \widetilde{\mathfrak{M}}, \hat{w}_0 \rangle$ s.t. $v(\phi, w_0) = \hat{v}(\phi, \hat{w}_0)$.

*Proof.* Note that we can w.l.o.g. assume that $\mathfrak{M} = \langle W, \langle R_a \rangle_{a \in A}, \langle T_a \rangle_{a \in A}, v \rangle$ is finite, that $cl_a = \{w_0, \dots, w_m\}$, and that $\phi$ is irredundantly nested. For simplicity, we will assume here that $A = \{a, b\}$. The proofs for larger sets of agents can be obtained in a similar fashion.

We proceed by double induction on $\mathcal{H}(\mathfrak{M})$ and on $\phi \in \mathcal{L}_{\square}^{\sim}$. First, consider the basis case of $\mathcal{H}(\mathfrak{M}) = 1$. That is, $\mathfrak{M}$ contains one proper cluster, namely, $cl_a$. Moreover, $\mathcal{A}(\phi) \le 1$. If $\mathcal{A}(\phi) = 0$, then $\phi$ is $\square$-free (propositional), and the statement follows immediately since the semantical conditions for propositional formulas in eF-models and $\mathbf{S5G}_{\text{inv}}^{\mathfrak{c}}$-models coincide. Now let $\mathcal{A}(\phi) = 1$.

Note that since $T_a(w) = T_a(w')$ for every $w$ and $w'$ s.t. $wR_a w$, we can assume that $T_a$'s and $T_b$'s are associated with clusters and not states. We let $T_a(cl_a) = \{\alpha_1, \dots, \alpha_n\}$ and $T_b(w_0) = \{\beta_1, \dots, \beta_r\}$<fnref n="7" /> and construct a pointed $\mathbf{S5G}_{\text{inv}}^{\mathfrak{c}}$-model $\langle \widetilde{\mathfrak{M}}, \hat{w}_0 \rangle$ s.t. $\hat{v}(\phi, \hat{w}_0) = v(\phi, w_0)$. It suffices to consider the following cases:

1. $\phi = \square_a \chi$ for some $\chi \in \mathcal{L}_{\square}^{\sim}$ s.t. $\chi$ is propositional;

2. $\phi = \square_b \chi$ for some $\chi \in \mathcal{L}_{\square}^{\sim}$ s.t. $\chi$ is propositional;

3. $\phi = \chi \circ \psi$ s.t. w.l.o.g. $\chi$ contains $\square_a$ and $\psi$ contains $\square_b$ with $\circ \in \{\wedge, \rightarrow\}$.

For Item 1, note that $v(\square_a \chi, w_0) \le \inf\{v(\chi, w') | w_0 R_a w'\}$. Moreover, as $\mathfrak{M}$ is finite, $v(\square_a \chi, w_0) = \inf\{v(\chi, w') | w_0 R_a w'\}$ iff there are some $\alpha_i \in T(cl_a)$ and $w'' \in cl_a$ such that $\inf\{v(\chi, w') | w_0 R_a w'\} = \alpha_i = v(\chi, w'')$. In this case, we can set $\widetilde{\mathfrak{M}} = \langle W, \langle R_a \rangle_{a \in A}, v \rangle$ (i.e., just remove $T_a$'s from $\mathfrak{M}$) because the F-models and $\mathbf{S5G}_{\text{inv}}^{\mathfrak{c}}$-models evaluate propositional formulas in the same way. This also deals with the case of $v(\square \psi, w_0) = 1$.

Now let $v(\square \psi, w_0) = \alpha_i \ne 1$, and, furthermore, $\alpha_i < \inf\{v(\chi, w') | w_0 R_a w'\}$. We define order embeddings $h_k^a$'s for every $k < \omega$. We let $h_0^a(x) = x$ for every $x \in [0, 1]$ and for the remaining ones, we demand that $h_k^a(0) = 0$, $h_k^a(1) = 1$, and $h_k^a(1-j) = 1 - h_k^a(j)$ for all $j \in [0, 1]$.

$$ h_k^a(\alpha_i) = \alpha_i \text{ for all } i \le n \text{ and } k \in \mathbb{N} $$

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

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

<footnote n="7">⁷ Recall that $\mathfrak{M}$ contains only one proper cluster.</footnote>
We then copy $cl_a \omega$ times. I.e., $\tilde{M} = \langle \tilde{W}, \hat{R}_a, \hat{R}_b, \hat{v} \rangle$ is as follows:

$$ 
\begin{aligned}
\tilde{W} &= \bigcup_{k<\omega} \{w_i^k \mid i \le m\} \\
\hat{R}_a &= \tilde{W} \times \tilde{W} \\
\hat{R}_b &= \{\langle \hat{w}, \hat{w} \rangle \mid \hat{w} \in \tilde{W}\} \\
\hat{v}(p, w_i^k) &= h_k^a(v(p, w_i))
\end{aligned}
$$

We have $v(\psi, w_j) \ge \alpha_i$ for all $w_j \in cl_a$, and by the construction of the order embeddings, we get that for all $w' \in \tilde{W}$, $\hat{v}(\psi, w') \ge \alpha_i$. Now, there must be some $w'' \in cl_a$ for which $v(\psi, w'') \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(v(\psi, w'')) = \hat{v}(\psi, \hat{w}''^k) \in (\alpha_i, \alpha_i + \varepsilon)$. Hence, $\hat{v}(\Box\psi, \hat{w}_0^0) = \alpha_i = v(\Box\psi, w_0)$.

We note briefly that if $\mathcal{A}(\phi) = 1$ and $\phi$ contains several subformulas $\Box_a\chi_1, \dots, \Box_a\chi_q$ (but does not contain $\Box_b$'s), the proof proceeds in the same way. The only difference is that we will need to copy $cl_a$ if the value of at least one $\Box_a\chi_i$ is lower than the infimum of values of $\chi_i$ in $cl_a$. Still, one can see from the construction that $h_k^a$'s preserve the value of all formulas of the form $\Box_a\chi_i$ in $w_0$, whence, it suffices to produce $\omega$ copies of $cl_a$ only once.

The case of Item 2 is similar but we need different model and embeddings. Namely, we set $h_0^b(x) = x$, and for $k > 0$, $h_k^b$'s are as follows:

$$ 
\begin{aligned}
h_k^b(\beta_i) &= \beta_i \text{ for all } i \le r \text{ and } k \in \mathbb{N} \\
h_k^b[(\beta_i, \beta_{i+1})] &= (\beta_i, \min(\beta_i + 1/k, \beta_{i+1})) \text{ for all } i \le r-1 \text{ and even } k \in \mathbb{N} \\
h_k^b[(\beta_i, \beta_{i+1})] &= (\max(\beta_i - 1/k, \beta_{i+1}), \beta_{i+1}) \text{ for all } i \le r-1 \text{ and odd } k \in \mathbb{N}
\end{aligned}
$$

$$ 
\begin{aligned}
\tilde{W} &= \{\hat{w}_i \mid i \le m\} \cup \{\hat{w}_0^k \mid 1 \le k < \omega\} \\
\hat{R}_a &= \{\hat{w}_i \mid i \le m\} \times \{\hat{w}_i \mid i \le m\} \cup \{\langle \hat{w}_0^k, \hat{w}_0^k \rangle \mid 1 \le k < \omega\} \\
\hat{R}_b &= \{\langle s, s' \rangle \mid \{s, s'\} \subseteq \{\hat{w}_0\} \cup \{\hat{w}_0^k \mid 1 \le k < \omega\}\} \\
\hat{v}(p, \hat{w}_i) &= v(p, w_i) \\
\hat{v}(p, \hat{w}_0^k) &= h_k^b(v(p, w_0))
\end{aligned}
$$

Here, $h_k^b$'s are essentially the same as $h_k^a$'s but defined w.r.t. $T_b(w_0)$, not $T_a(cl_a)$. Namely, Note, moreover, that since $\mathcal{H}(\tilde{M}) = 1$, $R_b(w) = \{w\}$ for all $w \in cl_a$. The rest of the proof that $v(\phi, w_0) = \hat{v}(\phi, \hat{w}_0)$ is the same as in the previous case.

Finally, in the third case, we combine the two constructions by defining $\tilde{M} = \langle \tilde{W}, \hat{R}_a, \hat{R}_b, \hat{v} \rangle$ is as follows:

$$ 
\begin{aligned}
\tilde{W} &= \bigcup_{k<\omega} \{w_i^k \mid i \le m\} \cup \underbrace{\{\hat{w}_0^k \mid 1 \le k < \omega\}}_{W_{R_b}} \\
\hat{R}_a &= \bigcup_{k<\omega} \{w_i^k \mid i \le m\} \times \bigcup_{k<\omega} \{w_i^k \mid i \le m\} \cup \{\langle \hat{w}_0^k, \hat{w}_0^k \rangle \mid 1 \le k < \omega\} \\
\hat{R}_b &= \{\langle s, s' \rangle \mid \{s, s'\} \subseteq \{w_0^0\} \cup \{\hat{w}_0^k \mid 1 < k < \omega\}\} \cup \bigcup_{1 \le k < \omega} \{\langle w_i^k, w_i^k \rangle \mid i \le m\} \\
\hat{v}(p, w_i^k) &= h_k^a(v(p, w_i))
\end{aligned}
$$
$$ \hat{v}(p, \hat{w}_0^k) = h_k^b(v(p, w_0)) $$

Again, the proof that $v(\phi, w_0) = \hat{v}(\phi, w_0^0)$ is essentially the same as that in the previous cases but now we also use the fact that the value of $\chi$ depends only on $W_{R_a}$ and the value of $\psi$ only on $W_{R_b}$.<fnref n="8" />

Let us now proceed to the induction step. Assume that $\mathcal{H}(\mathfrak{M}) = n+1$ and the statement holds for all cluster-tree eF-models of the height $n$ or lower. Again, we conduct induction on $\phi$. The basis case of $\phi = p$ holds trivially, the cases of $\phi = \sim\chi$, $\phi = \chi \wedge \psi$, and $\phi = \chi \to \psi$ can be obtained by straightforward applications of the induction hypothesis. It remains to consider modal cases.

Let $\phi = \square_a\chi$ and let further, $v(\square_a\chi, w_0) = x$. We now have two cases: (I) $\inf\{v(\chi, w') | wR_a w'\} = x$ or (II) $\inf\{v(\chi, w') | wR_a w'\} > x$. In the case (I), we replace every $w_i \in \mathfrak{cl}_a$ with a pointed $\mathbf{S5G}_{\text{inv}}^c$-model $(\mathfrak{M}_{w_i}, \hat{w}_0^i)$ s.t. $v^{\mathfrak{M}_{w_i}}(\chi, \hat{w}_0^i) = v(\chi, w_i)$. Note that since $\square_a\chi$ is irredundantly nested, we have $\mathcal{A}(\chi) = \mathcal{A}(\square_a\chi) - 1$. Thus, by Corollary 2, we can apply the induction hypothesis to obtain the needed $(\mathfrak{M}_{w_i}, \hat{w}_0^i)'$s. We now extend accessibility relations on $\hat{w}_0^i$'s as expected: $\hat{w}_0^i R_a \hat{w}_0^j$ and $\hat{w}_0^i R_b \hat{w}_0^j$ for every $i, j \in \{0, \dots, m\}$. Clearly, $v(\square_a\chi, w_0) = v^{\mathfrak{M}_{w_0}}(\square_a\chi, \hat{w}_0^0)$.

In the case (II), we replace each $w_i \in \mathfrak{cl}_a$ with countably many pointed $\mathbf{S5G}_{\text{inv}}^c$-models $(\mathfrak{M}_{w_i}^k, \hat{w}_0^{k,i})$ s.t. $v^{\mathfrak{M}_{w_i}^k}(\chi, \hat{w}_0^{k,i}) = h_k^a(v(\chi, w_i))$. Again, this is possible to have by the induction hypothesis because $\mathcal{A}(\chi) = \mathcal{A}(\square_a\chi) - 1$. One can now show that $v(\square_a\chi, w_0) = v^{\mathfrak{M}_{w_0}^k}(\square_a\chi, \hat{w}_0^{0,0})$ utilising the argument in the basis case.

Finally, let $\phi = \square_b\chi$. The procedure is similar to the case of $\phi = \square_a\chi$ but we will need to replace the states in $R_b(w_0)$ and use $h_k^b$'s. The result follows.

**Theorem 3.** An $\mathcal{L}^{\sim}_{\square}$-formula $\phi$ is $\mathbf{S5G}_{\text{inv}}^c$-valid iff it is eF-valid.

*Proof.* The left-to-right direction follows from Corollary 2 and Lemma 3. For right-to-left, suppose that $\phi$ is not $\mathbf{S5G}_{\text{inv}}^c$-valid. Then there exists a $\mathbf{S5G}_{\text{inv}}^c$-countermodel $\mathfrak{M} = \langle W, \langle R_a \rangle_{a \in A}, v \rangle$ with $w \in W$ s.t. $v(\phi, w) = x$ for some $x < 1$. For every $a \in A$, we set

$[\phi]_{\square_a} \sim = \{\square_a\psi | \square_a\psi \text{ is a subformula of } \phi\} \cup \{\sim\square_a\psi | \square_a\psi \text{ is a subformula of } \phi\}$ and define a function $\hat{T}_a$ for each $s \in W$ with the following scheme:

$$ \hat{T}_a(s) = \{\inf\{v(\psi, w') | sR_a w'\} | \psi \in [\phi]_{\square_a} \} \cup \{0, \frac{1}{2}, 1\} $$

Let $\mathfrak{M} = \langle \hat{W}, \langle \hat{R}_a \rangle_{a \in A}, \langle \hat{T}_a \rangle_{a \in A}, \hat{v} \rangle$ where $\hat{W} = W, \hat{R}_a = R_a$ for all $a \in A$, and $\hat{v} = v$. By definition, $\langle \hat{W}, \langle \hat{R}_a \rangle_{a \in A} \rangle$ is a frame and each $\hat{T}_a$ and point $s$, $\hat{T}_a(s)$ is finite and closed under $1-x$, whence $\mathfrak{M}$ is an F-model. We claim that for all $w$ and all $\psi$ a subformula of $\phi$, $\hat{v}(\psi, w) = v(\psi, w)$.

<footnote n="8">⁸ Note that even for formulas such as $\phi = \square_a\chi_1 \to (\square_b\psi_1 \to ((\square_a\chi_2 \wedge \tau_1) \to (\tau_2 \wedge \square_b\psi_2)))$ with $\mathcal{A}(\phi) = 1$, the values of all its $\square_a$-subformulas still depend only on $W_{R_a}$, the values of $\square_b$-subformulas only on $W_{R_b}$, and the values of propositional subformulas only on $w_0^0$. As the values of modal subformulas are preserved using $h_k^a$'s and $h_k^b$'s, it suffices to consider the case when $\phi = \chi \circ \psi$ with $\chi$ and $\psi$ containing $\square_a$ and $\square_b$, respectively.</footnote>
The basis step in case $\phi$ is atomic is immediate and the propositional connectives follow easily, leaving the case of an operator $\square_a$. Let $\psi = \square_a\xi$. Then $v(\square_a\xi, w) = \inf\{v(\xi, w') | wR_a w'\}$, whence by construction, $v(\square_a\xi, w)$ is an element $x$ in $\hat{T}_a(w)$ such that for all $w'$ such that $w\hat{R}_a w'$, $v(\xi, w') \le x$; as it is the greatest such element, $\hat{v}(\square_a\xi, w) = x$, whence $\hat{v}(\square_a\xi, w) = v(\square_a\xi, w)$. The case of $\psi = \square_b\xi$ can be considered in a similar manner. This completes the induction, so $\tilde{M}$ provides an F-countermodel.