# A Hypersequent Calculus with Clusters for Linear Frames

David Baelde, Anthony Lick, Sylvain Schmitz

► To cite this version:

David Baelde, Anthony Lick, Sylvain Schmitz. A Hypersequent Calculus with Clusters for Linear Frames. Twelfth Conference on Advances in Modal Logic, Jul 2018, Bern, Switzerland. pp.36–55. [hal-01756126v2](https://hal-01756126v2)

HAL Id: hal-01756126

https://inria.hal.science/hal-01756126v2

Submitted on 31 Jul 2018

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>
# A Hypersequent Calculus with Clusters for Linear Frames

David Baelde, Anthony Lick, Sylvain Schmitz

LSV, ENS Paris-Saclay & CNRS & Inria, Université Paris-Saclay

## Abstract

The logic $K_t^{4.3}$ is the basic modal logic of linear frames. Along with its extensions, it is found at the core of linear-time temporal logics and logics on words. In this paper, we consider the problem of designing proof systems for these logics, in such a way that proof search yields decision procedures for validity with an optimal complexity—$coNP$ in this case. In earlier work, Indrzejczak has proposed an ordered hypersequent calculus that is sound and complete for $K_t^{4.3}$ but does not yield any decision procedure. We refine his approach, using a hypersequent structure that corresponds to weak rather than strict total orders, and using annotations that reflect the model-theoretic insights given by small models for $K_t^{4.3}$. We obtain a sound and complete calculus with an associated $coNP$ proof search algorithm. These results extend naturally to the cases of unbounded and dense frames, and to the complexity of the two-variable fragment of first-order logic over total orders.

Keywords: modal logics, proof systems, hypersequents, clusters.

## 1 Introduction

Modal logics are expressive and intuitive languages for describing properties of relational structures. Accordingly, when investigating properties of linear frames, it is often quite useful to express them using a tense logic [19] able to reason on temporal flows. For instance, LTL [17,20] and CTL [4] are widely used for verifying computer programs.

When studying a logic, a common approach is to design a proof system, such as a sequent calculus. Our own interest in (enriched) sequent calculi, compared to e.g. axiomatisations, is that their associated proof-search procedures often yield decidability and even complexity results for the satisfiability and validity problems. They are also modular, allowing them to be easily adapted to handle extensions or fragments of the logic at hand. However, basic sequent calculi are often ill-suited for modal logics, as the class of frames underlying the logic is typically difficult to capture. Therefore, more expressive variants of the

<footnote>* Work funded by ANR grant ANR-14-CE28-0005 PRODAQ.</footnote>
sequent calculus have been developed, such as labelled sequents [15], nested sequents [3,18], linear nested sequents [12] or hypersequents [1,7,8,9,10].

In this paper, we focus on $K_t4.3$ [5,2], the tense logic of linear frames. Somewhat surprisingly for the logic lying at the heart of LTL with past modalities—which is largely studied in verification [13,11]—, to the best of our knowledge, a sound and complete sequent-style calculus for $K_t4.3$ was only recently proposed by Indrzejczak [9]. This is an *ordered hypersequent calculus*, where the structure of the hypersequents reflects the linear structure of $K_t4.3$ frames. However, this calculus does not yield a proof-search algorithm, even though $K_t4.3$ satisfiability is known to be decidable and even NP-complete [16]. The issue here is that ordered hypersequents correspond to *strictly ordered* linear frames, which are arguably not the most adequate structures for the logic. Although every satisfiable $K_t4.3$ formula has a model whose underling frame is a strict total order, there are examples of invalid formulæ (like $G \perp \vee FG \perp$), whose strictly ordered counter-models are all infinite. On such invalid instances, the hypersequent calculus of Indrzejczak [9] yields a proof tree with some infinite failure branches, thus proof-search does not terminate.

The decidability of the satisfiability problem of $K_t4.3$ comes from its finite model property, shown by Ono and Nakamura [16, Thm. 3]. But this property can only be obtained when working with weak total orders, i.e. allowing some worlds of the models to be equivalent for the order relation. Such groups of nodes are commonly called ‘clusters.’ Note that the logic itself is not able to distinguish between a weakly ordered frame and any of its ‘bulldozed’ strict orders [2, Thm. 4.56].

In the remainder of this paper, we capture the syntactic aspects of these model-theoretic results. In Section 3, we show how to enhance the hypersequent calculus of Indrzejczak [9] by capturing the model-theoretic ideas in hypersequents with *clusters* and *annotations*. This leads to a sound and complete proof system where proof search always terminates, furthermore with a coNP complexity—which is optimal for the validity problem. Moreover, this proof system is also modular: we consider some classical extensions of $K_t4.3$ in Section 4, and provide new rules for our hypersequent calculus to handle these extensions; these new rules still yield an optimal coNP proof search. Finally, Manuel and Sreejith [14] have recently shown that validity in first-order logic with two variables over strict total orders is in coNEXP. The same statement can be derived from our results and further extended to *dense* linear orders, by first converting the first-order formulæ into equivalent exponential-sized $K_t4.3$ formulæ [6]; see Section 5.

We start by recalling the definition of $K_t4.3$ in Section 2.

## 2 Modal Logic on Weak Total Orders

We consider tense logics with two unary temporal operators, over a set $\Phi$ of propositional variables, with the following syntax:

$$ \varphi ::= \perp | p | \varphi \supset \varphi | G\varphi | H\varphi \quad (\text{where } p \in \Phi) $$
Formulæ $G\varphi$ and $H\varphi$ are called *modal formulæ*. Intuitively, $G\varphi$ expresses that $\varphi$ holds ‘globally’ in all future worlds reachable from the current one, while $H\varphi$ expresses that $\varphi$ holds ‘historically’ in all past worlds from which the current world is accessible. Other Boolean connectives may be encoded from $\perp$ and $\supset$, and we define, as is common, $F\varphi = \neg G\neg\varphi$ expressing that $\varphi$ will hold ‘in the future’ and $P\varphi = \neg H\neg\varphi$ expressing that $\varphi$ was true ‘in the past.’

## 2.1 Semantics

As is standard, our formulæ shall be evaluated on *Kripke structures*. A *frame* is a pair $\mathfrak{F} = (W, \preceq)$, where $W$ is a set of worlds, and $\preceq \subseteq W \times W$ is a binary relation over $W$. A *structure* is a pair $\mathfrak{M} = (\mathfrak{F}, V)$, where $\mathfrak{F} = (W, \preceq)$ is a frame, and $V: \Phi \to 2^W$ is a valuation function. Given such a structure, we define the *satisfaction relation* $\mathfrak{M}, w \models \varphi$, where $w \in W$ and $\varphi$ is a formula, by structural induction on $\varphi$:

<table><tr><td>Μ, w &ne; &perp;</td><td></td></tr><tr><td>Μ, w &vdash; p</td><td>iff w &isin; V(p)</td></tr><tr><td>Μ, w &vdash; &varphi; &supset; &psi;</td><td>iff if Μ, w &vdash; &varphi; then Μ, w &vdash; &psi;</td></tr><tr><td>Μ, w &vdash; G&varphi;</td><td>iff &forall;w' &isin; W such that w' &preceq; w', Μ, w' &vdash; &varphi;</td></tr><tr><td>Μ, w &vdash; H&varphi;</td><td>iff &forall;w' &isin; W such that w' &preceq; w, Μ, w' &vdash; &varphi;</td></tr></table>

When $\mathfrak{M}, w \models \varphi$, we say that $(\mathfrak{M}, w)$ is a *model* of $\varphi$.

A formula that is satisfied in all worlds of all structures is said to be *valid*. In this paper, we shall not consider the validity problem in general, but only in restricted classes of structures. Namely, we will consider the logic of *weak total orders*, i.e., the formulæ that hold in all structures whose accessibility relation is transitive and total. This logic can be defined axiomatically, as shown next. Later in Section 4, we will study further restrictions of the logic.

The choice of the symbol $\preceq$ for our frames' accessibility relations is in line with our focus on weak total orders. When working on such orders, it is useful to define $x \prec y$ when $x \preceq y$ but not $y \preceq x$. Note that $\prec$ may not be a strict total order: it is transitive but not necessarily total.

## 2.2 Weak Total Orders

The logic $\mathbf{K}_4.3$ is defined as the set of theorems generated by necessitation, modus ponens and substitution from classical tautologies and the axioms:

$$G(p \supset q) \supset (Gp \supset Gq) \qquad (\mathbf{K}_r)$$

$$H(p \supset q) \supset (Hp \supset Hq) \qquad (\mathbf{K}_\ell)$$

$$p \supset GPp \qquad (t_r)$$

$$p \supset HFp \qquad (t_\ell)$$

$$FFp \supset Fp \qquad (4)$$

$$Fp \wedge Fq \supset F(p \wedge Fq) \vee F(p \wedge q) \vee F(q \wedge Fp) \qquad (.3_r)$$

$$Pp \wedge Pq \supset P(p \wedge Pq) \vee P(p \wedge q) \vee P(q \wedge Pp) \qquad (.3_\ell)$$
The first two axioms are simply the Kripke schema, given for each modality. Next we find the t axioms, which are obviously satisfied in our setting since the two modalities are converses of each other.<fnref n="1" /> The next axiom, dubbed 4, corresponds to the transitivity of ~. More precisely, canonical models of 4 are transitive [2]. Similarly, canonical models of the trichotomy axioms .3 have accessibility relationships that are non-branching to the left and to the right. All together, this implies the following completeness result:

**Fact 2.1** ([2, p. 220]) A formula is a theorem of K<sub>t</sub>4.3 iff it is valid in all structures whose relation is transitive and total, i.e., in weak total orders.

The logic K<sub>t</sub>4.3 is perhaps better known for being complete wrt. the class of strict total orders [2, Thm. 4.56]. As we shall see, focusing on this characterisation would however be counterproductive for our purposes. As a simple illustration of when weak total orders could be beneficial, note that some formulæ admit finite weak total orders as models but only infinite strict total orders. It is the case, for example, of (GF⊤)∧(F⊤), which admits a single-world model that is a weak total order. The use of weak total orders is instrumental in order to derive decidability and complexity results.

## 3 Hypersequents with Clusters

Indrzejczak [9] proposed a complete calculus for K<sub>t</sub>4.3 using the framework of ordered hypersequents (aka. linear nested sequents [12]): his calculus works with lists of sequents rather than the usual multisets of sequents of hypersequent calculi. The semantics of ordered hypersequents relies on a mapping from ordered sequents to worlds that are ordered accordingly. This extension allows for a natural calculus, enjoying the subformula property and extending nicely to accommodate semantic restrictions such as unboundedness and density.

For example, the calculus of [9] allows the following inference:

$$ \frac{\Gamma \vdash \Delta; \vdash \varphi}{\Gamma \vdash \Delta, G\varphi} $$

It expresses that, if $w \not\models G\varphi$ for an arbitrary world $w$, there must be a $w \preceq w'$ such that $w' \not\models \varphi$.

Unfortunately, Indrzejczak's completeness argument is quite complex, and does not yield a decision procedure. The argument is Hintikka-style: if a careful exhaustive proof search fails in his calculus, then some failed proof-search branch yields a counter-model of the conclusion hypersequent. In Indrzejczak's calculus, that failure branch may be infinite, in which case the extracted counter-model is obtained as a limit, and is itself infinite.

**Finite Models and Hypersequents with Clusters.** In fact, the counter-models extracted from failure branches of Indrzejczak's calculus are always strictly (and totally) ordered, hence they must be infinite in some cases. The

<footnote n="1">¹ In a standard bi-modal setting, we would have two a priori unrelated relations. The t axioms would then force the two relations to be converses of each other in canonical models.</footnote>
model theory of K<sub>t</sub>4.3 provides us with a way to circumvent this problem. Indeed, K<sub>t</sub>4.3 enjoys a finite model property for weak total orders [16, Thm. 3]; the desired finite model is obtained from the original model by applying Lemony's filtration (see Appendix A for details).

This insight leads us to consider ordered hypersequents with clusters, corresponding semantically to sets of worlds which are all equivalent with respect to the weak total order, i.e. where w ≲ w' and w' ≲ w for all w, w' in the cluster. In itself, this only complicates the calculus as it only creates more premises (and indeed some rules in our calculus have a large number of premises), and does not allow us to bound failure branches. For example, the inference shown above would be modified as follows:

$$ \frac{\frac{\Gamma \vdash \Delta \parallel \vdash \varphi \qquad \{\Gamma \vdash \Delta\}; \vdash \varphi}{\Gamma \vdash \Delta; \vdash \varphi \qquad \{\Gamma \vdash \Delta, G\varphi\}}}{\Gamma \vdash \Delta, G\varphi} $$

The bottom inference expresses that, if w ≠ Gφ, then either there is w ≺ w' such that w' ≠ φ (first premise) or w is reflexive (second premise). In the latter case, the next inference expresses that there must be a w' such that w' ≠ φ satisfying either w ≲ w' ≲ w (first premise) or w ≺ w' (second one).

**Extremal Models and Annotations.** Crucially, this new formalism allows us to benefit from another model-theoretic insight. It is known that satisfiability in K<sub>t</sub>4.3 is NP-complete because any satisfiable formula φ admits a model of size linear in the size of the formula [16, Thm. 5] (see also [2, Thm. 6.38]). We shall not exploit this result as such, but the construction behind it: the linear-sized model is obtained by keeping, for each subformula Fψ (resp. Pψ) of φ, only the rightmost (resp. leftmost) world of the original model that satisfies ψ.

Viewing our hypersequent calculus as a search for counter-models, we constrain it to search for 'extremal' counter-models as above. Concretely, we annotate some sequents with modal formulæ, requiring that a modal formula occurs at most once as an annotation. For example, the previous inferences are enriched as follows (with the annotations between parentheses and in violet):

$$ \frac{\frac{\Gamma \vdash \Delta \parallel \vdash \varphi (G\varphi) \qquad \{\Gamma \vdash \Delta\}; \vdash \varphi (G\varphi)}{\Gamma \vdash \Delta; \vdash \varphi (G\varphi) \qquad \{\Gamma \vdash \Delta, G\varphi\}}}{\Gamma \vdash \Delta, G\varphi} $$

The annotation indicates a maximal sequent for the contradiction of the considered modal formula. This is then reflected by special inferences, for example

$$ \dots; \Gamma \vdash \Delta (G\varphi); \dots; \Pi \vdash \Sigma, G\varphi; \dots $$

which expresses that, for the (complete) class of counter-models that we are considering, there is no counter-model, since Gφ would have to be contradicted strictly after a rightmost contradicting world.

With this in place, we finally obtain a calculus where failure branches are finite. This allows for an elementary completeness argument, extracting
finite weakly ordered counter-models from failure branches. For the soundness argument, we indirectly make use of the extremal counter-model construction of [16, Thm. 4]. Another consequence is that proof search in our calculus directly yields an optimal coNP procedure for validity.

## 3.1 Definitions and Basic Meta-Theory

We shall now formally describe our calculus. We first define hypersequents with clusters and their semantics in terms of embeddings into weak total orders. We then extend them with annotations, and present our system of deduction rules.

**Hypersequents with Clusters.** A sequent (denoted $S$) is a pair of two finite sets of formulæ, written $\Gamma \vdash \Delta$. It is satisfied in a world $w$ of a model $\mathfrak{M}$ if, in that world, the conjunction of the formulæ of $\Gamma$ implies the disjunction of the formulæ of $\Delta$. In that case, we write $\mathfrak{M}, w \models \Gamma \vdash \Delta$.

In this paper, a hypersequent is a list of cells, each cell being either a sequent or a list of sequents called a (syntactic) cluster. We shall use the following abstract syntax, where both operators ‘;’ and ‘||’ are associative with unit ‘•’:

$$H ::= \bullet | C; H \qquad (\text{hypersequents})$$

$$C ::= S | \{S \parallel Cl\} \qquad (\text{cells})$$

$$Cl ::= \bullet | S \parallel Cl \qquad (\text{clusters})$$

The main feature of hypersequents with clusters is that their structures are weak total orders. The order of cells in a hypersequent is relevant, as it yields a strict ordering in the semantics. The order of sequents inside a cluster is semantically irrelevant; nevertheless, assuming an ordering as part of the syntactic structure of clusters is sometimes useful, as in the upcoming definition.

**Underlying Frames and Embeddings.** Let $H$ be a hypersequent containing $n$ sequents, counting both the sequents found directly in its cells and those in its clusters. We call a natural number $i \in [1; n]$ a *position* of $H$, and we write $H(i)$ for the $i$-th sequent of $H$. We define the *underlying frame* of $H$ as $\mathfrak{F}(H) = ([1; n], \preceq)$ where $i \preceq j$ iff either the $i$-th and $j$-th sequents are in the same cluster, or the $i$-th sequent is in a cell that lies strictly to the left of the cell of the $j$-th sequent. In particular, a position can only be reflexive in the underlying frame of a hypersequent if it is in a cluster.

Let $\mathfrak{F} = (W, \preceq)$ and $\mathfrak{F}' = (W', \preceq')$ be two frames. We say that $\mu: W \to W'$ is an embedding of $\mathfrak{F}$ into $\mathfrak{F}'$ if, for all $(w_1, w_2) \in W^2$,

* $w_1 \preceq w_2$ implies $\mu(w_1) \preceq' \mu(w_2)$ and

* $w_1 < w_2$ implies $\mu(w_1) <' \mu(w_2)$.

In that case, we write $\mathfrak{F} \hookrightarrow_{\mu} \mathfrak{F}'$. We simply write $H \hookrightarrow_{\mu} \mathfrak{F}'$ when $\mathfrak{F}(H) \hookrightarrow_{\mu} \mathfrak{F}'$.

An example embedding is shown in Figure 1. Note that it is possible that $\mu(i)$ is reflexive when $i$ is not. However, positions from distinct cells cannot be embedded into worlds of a same cluster. By contrast, distinct positions belonging to the same cluster may be mapped to the same (reflexive) world.
<figure><img src="image_2.png" /><figcaption>Fig. 1. Embedding of a hypersequent in a weak total order.</figcaption></figure>

**Definition 3.1 (semantics)** Let $\mathfrak{M} = (\mathfrak{F}, V)$ be a structure. Given an embedding $H \hookrightarrow_{\mu} \mathfrak{F}$, we say that $(\mathfrak{M}, \mu)$ is a *model* of a hypersequent $H$, written $\mathfrak{M}, \mu \models H$, when there exists a position $i$ of $H$ such that $\mathfrak{M}, \mu(i) \models H(i)$. We say that a hypersequent is *valid* if for any weak total order $\mathfrak{M} = (\mathfrak{F}, V)$ and any embedding $H \hookrightarrow_{\mu} \mathfrak{F}$, we have $\mathfrak{M}, \mu \models H$. $\square$

**Annotations.** We finally introduce annotations, and their semantics. An *annotated sequent* is a sequent that may be annotated with modal formulæ. We simply write $\Gamma \vdash \Delta$ for a sequent carrying no annotation, otherwise we write, e.g., $\Gamma \vdash \Delta (H \varphi, G \psi, \dots)$. Then, *annotated hypersequents* are hypersequents whose sequents are annotated, with the constraint that an annotation may only occur once in an annotated hypersequent. Formally, we can see annotations as partial functions from the set of modal formulæ to the set of positions of the hypersequent. For instance, $\Gamma \vdash \Delta (G \varphi)$; $\{\Pi \vdash \Sigma (H \varphi)\}$ is an annotated hypersequent but $\Gamma \vdash \Delta (H \varphi, G \varphi)$; $\{\Pi \vdash \Sigma (H \varphi)\}$ is not allowed because of the two occurrences of $H \varphi$ as an annotation.

Since we use these annotations to guide the search for a *finite* counter-model, we only define a semantics for annotated hypersequents over finite structures.

**Definition 3.2 (annotation semantics)** Given an annotated hypersequent $H$ and a *finite* structure $\mathfrak{M} = (\mathfrak{F}, V)$, an embedding $H \hookrightarrow_{\mu} \mathfrak{F}$ is *annotation-respecting* if, for all $i$ such that $H(i)$ carries the annotation $(G \varphi)$ (resp. $(H \varphi)$), there is no $w \in W$ such that $\mathfrak{M}, w \models \neg \varphi$ and $\mu(i) \prec w$ (resp. $w \prec \mu(i)$).

An *annotation-respecting model* of $H$ is a model $((\mathfrak{F}, V), \mu)$ of $H$ where $H \hookrightarrow_{\mu} \mathfrak{F}$ is annotation-respecting. The sequent $H$ is *annotation-respecting valid* if, for any finite weak total order $\mathfrak{M} = (\mathfrak{F}, V)$ and any annotation-respecting embedding $H \hookrightarrow_{\mu} \mathfrak{F}$, we have $\mathfrak{M}, \mu \models H$. $\square$

A peculiarity of our system is that it is sound with respect to the annotation-respecting validity of Definition 3.2, but only complete with respect to the general validity of Definition 3.1: if a hypersequent is annotation-respecting valid but not valid in general, it might not have a derivation. Thus our annotation system may be seen as a proof search strategy over a more standard, annotation-free system.<fnref n="2" /> In any case, our proof system is sound and complete for hypersequents without annotations, since the two notions of validity coincide in that case.

<footnote n="2">² This more standard system simply consists of the rules of figures 2 and 3 without annotations, ignoring the rules of Figure 4. It is obviously sound. For completeness, we conjecture that Indrzejczak's proof could be adapted to weak total orders. However that system is not interesting as it is subsumed by Indrzejczak's original calculus, only adding more branches.</footnote>
$$ \begin{array}{ccc} \text{(ax)} & \frac{H[\varphi \supset \psi, \Gamma \vdash \Delta, \varphi]}{H[\varphi, \Gamma \vdash \Delta, \varphi]} & H[\varphi \supset \psi, \psi, \Gamma \vdash \Delta] \\ \text{(\top)} & \frac{H[\varphi, \Gamma \vdash \Delta, \psi, \varphi \supset \psi]}{H[\Gamma, \perp \vdash \Delta]} & H[\varphi, \Gamma \vdash \Delta, \varphi \supset \psi] \quad (\vdash \top) \end{array} $$

<caption>Fig. 2. Propositional rules of the hypersequent calculus with clusters.</caption>

**Rules of the Hypersequent Calculus.** The rules are given in figures 2 to 4, making use of a few notations.

First, we use hypersequents with *holes*. One hypersequents, cells, and clusters are defined by the syntax

$$ H \] ::= H ; C \] ; H \quad C \] ::= \star | \{ Cl \] \} \quad Cl \] ::= Cl \parallel \star \parallel Cl $$

Two-placeholder cells and hypersequents have two holes identified by $\star_1$ and $\star_2$:

$$ \begin{align*} H \] \] &::= H ; C \] \] ; H \mid H[\star_1] ; H[\star_2] \\ C \] \] &::= \{ Cl[\star_1] \parallel Cl[\star_2] \} \mid \{ Cl[\star_2] \parallel Cl[\star_1] \} \end{align*} $$

As usual, $C[S]$ (resp. $C[Cl]$) denotes the same cell with $S$ (resp. $Cl$) substituted for $\star$; two-placeholder cells and hypersequents with holes behave similarly. In terms of the frames underlying hypersequents with two holes, observe that the positions $i$ and $j$ associated resp. to $\star_1$ and $\star_2$ are such that $i \lesssim j$.

Second, we do not write explicitly the annotations that sequents may carry in rule applications. These annotations are implicitly the same in a conclusion sequent and the corresponding sequents in premises, or updated by adding the explicit annotation; freshly created sequents always have an explicit annotation. Annotations can prevent a rule application if the addition of an annotation would break the single-annotation constraint.

Third, we use a convenient notation for enriching a sequent: if $S$ is a sequent $\Gamma \vdash \Delta$ (*A*), then $S \times (\Gamma' \vdash \Delta' (A'))$ is the sequent $\Gamma, \Gamma' \vdash \Delta, \Delta' (A, A')$. Moreover, we sometimes need to enrich an arbitrary sequent of a cluster $C$ with a sequent $S$; then $C \times S$ denotes the cluster with its leftmost sequent enriched.

**Modal Rules.** After the usual propositional rules of Figure 2, we give in Figure 3 the introduction rules for modalities. The left introduction rules are symmetric for our two modalities. The first two, $(G\vdash)$ and $(G\vdash')$, express that if $G\varphi$ holds at some position, then $\varphi$ must also hold at a position to its right in the underlying frame.

Regarding the right introduction rules for modalities, let us start with the particular case where these modalities occur in extremal cells. In rule $(\vdash G)$, we introduce a formula $G\varphi$ to the right of a principal sequent that is in the rightmost cell of the hypersequent. The premises cover all the ways in which a world could occur to the right of (the embedding of) the principal sequent:

* We always have to consider a possible new cell strictly further to the right; in that case, the cell carries the (single) annotation $(G\varphi)$.
$$ (G \vdash) \frac{H [G \varphi, \Gamma \vdash \Delta] [\varphi, \Pi \vdash \Sigma]}{H [G \varphi, \Gamma \vdash \Delta] [\Pi \vdash \Sigma]} \qquad \frac{H_1; \{Cl_1 \parallel \varphi, G \varphi, \Gamma \vdash \Delta \parallel Cl_2\}; H_2}{H_1; \{Cl_1 \parallel G \varphi, \Gamma \vdash \Delta \parallel Cl_2\}; H_2} \quad (G \vdash') $$

$$ (H \vdash) \frac{H [\varphi, \Pi \vdash \Sigma] [H \varphi, \Gamma \vdash \Delta]}{H [\Pi \vdash \Sigma] [H \varphi, \Gamma \vdash \Delta]} \qquad \frac{H_1; \{Cl_1 \parallel \varphi, H \varphi, \Gamma \vdash \Delta \parallel Cl_2\}; H_2}{H_1; \{Cl_1 \parallel H \varphi, \Gamma \vdash \Delta \parallel Cl_2\}; H_2} \quad (H \vdash') $$

$$ \frac{H; C [\Gamma \vdash \Delta, G \varphi]; \vdash \varphi (G \varphi) \\ H; \{\Gamma \vdash \Delta, G \varphi\} \qquad \text{if } C = \star \\ H; C [\Gamma \vdash \Delta, G \varphi \parallel \vdash \varphi (G \varphi)] \qquad \text{if } C \neq \star}{H; C [\Gamma \vdash \Delta, G \varphi]} \quad (\vdash G) $$

$$ \frac{\vdash \varphi (H \varphi); C [\Gamma \vdash \Delta, H \varphi]; H \\ \{\Gamma \vdash \Delta, H \varphi\}; H \qquad \text{if } C = \star \\ C [\Gamma \vdash \Delta, H \varphi \parallel \vdash \varphi (H \varphi)]; H \qquad \text{if } C \neq \star}{C [\Gamma \vdash \Delta, H \varphi]; H} \quad (\vdash H) $$

$$ \frac{H [C [\Gamma \vdash \Delta, G \varphi]; \vdash \varphi (G \varphi); C'] \\ H [C [\Gamma \vdash \Delta, G \varphi]; C' \times (\vdash G \varphi)] \\ H [C [\Gamma \vdash \Delta, G \varphi]; C' \times (\vdash \varphi (G \varphi))] \qquad \text{if } C' \text{ is not a cluster} \\ H [\{\Gamma \vdash \Delta, G \varphi\}; C'] \qquad \text{if } C = \star \\ H [C [\Gamma \vdash \Delta, G \varphi \parallel \vdash \varphi (G \varphi)]; C'] \qquad \text{if } C \neq \star}{H [C [\Gamma \vdash \Delta, G \varphi]; C']}
\quad (\vdash G') $$

$$ \frac{H [C'; \vdash \varphi (H \varphi); C [\Gamma \vdash \Delta, H \varphi]] \\ H [C' \times (\vdash H \varphi); C [\Gamma \vdash \Delta, H \varphi]] \\ H [C' \times (\vdash \varphi (H \varphi)); C [\Gamma \vdash \Delta, H \varphi]] \qquad \text{if } C' \text{ is not a cluster} \\ H [C'; \{\Gamma \vdash \Delta, H \varphi\}] \qquad \text{if } C = \star \\ H [C'; C [\Gamma \vdash \Delta, H \varphi \parallel \vdash \varphi (H \varphi)]] \qquad \text{if } C \neq \star}{H [C'; C [\Gamma \vdash \Delta, H \varphi]]} \quad (\vdash H') $$

<caption>Fig. 3. Modal rules of the hypersequent calculus with clusters.</caption>

* If the active sequent does not belong to a cluster, i.e., if $C = \star$, it may still be embedded in a cluster in a frame, so we have to consider a premise where the last cell is changed into a single-sequent cluster.

* Alternatively, if $C \neq \star$, the active sequent belongs to a cluster and we need the last premise when $\varphi$ is falsified in an arbitrary world of that cluster.

Rule $(\vdash H)$ is, as expected, symmetric. Note that the $(\vdash G)$ and $(\vdash H)$ rules cannot apply when the principal formula already belongs to the annotations of some sequent of the hypersequent, since it would then create a new cell with that annotation. The rules $(\vdash G')$ and $(\vdash H')$, where the active sequent is not extremal, follow the same idea but have extra premises corresponding to the case where $\varphi$ is falsified in the next cell $C'$ or beyond.

**Annotation Rules.** Finally, the rules of Figure 4 allow special deduction steps based on the annotations, leveraging the annotation-respecting semantics.
$$ ((G)) \qquad \frac{H_1 [\Gamma \vdash \Delta (G \varphi)] ; H_2 [\Pi \vdash \Sigma, G \varphi]}{H_1 ; \Gamma \vdash \Delta, H \varphi (H \varphi)} \qquad \frac{H_1 ; \{\Gamma \vdash \Delta, H \varphi (H \varphi)\} ; H_2}{H_1 ; \Gamma \vdash \Delta, H \varphi (H \varphi) ; H_2} \qquad ((H)) \\ ((H)) \qquad \frac{H_1 [\Pi \vdash \Sigma, H \varphi] ; H_2 [\Gamma \vdash \Delta (H \varphi)]}{H_1 ; \Gamma \vdash \Delta, G \varphi (G \varphi)} \qquad \frac{H_1 ; \{\Gamma \vdash \Delta, G \varphi (G \varphi)\} ; H_2}{H_1 ; \Gamma \vdash \Delta, G \varphi (G \varphi) ; H_2} \qquad ((G)) $$

<caption>Fig. 4. Annotation rules of the hypersequent calculus with clusters.</caption>

The ((G)) rule allows to derive any hypersequent where Gφ occurs strictly to the right of a sequent carrying the annotation (Gφ), and symmetrically for ((H)): such hypersequents cannot have annotation-respecting counter-models. The (({G})) and (({H})) rules express that, if a hypersequent features a sequent containing a modal formula both in its right hand side and in its set of annotations, then that sequent must occur in a cluster for the hypersequent to have an annotation-respecting counter-model.

**Invertibility.** Note that our rules are formulated in an invertible style, keeping the principal formula in the premises. This eases the proof of completeness, where proof search induces a form of saturation. The following weakening rules are admissible in our system, and we shall use them implicitly in examples to avoid carrying around useless formulæ:

$$ \frac{H[\Gamma \vdash \Delta]}{H[\Gamma, \varphi \vdash \Delta]} \qquad \frac{H[\Gamma \vdash \Delta]}{H[\Gamma \vdash \varphi, \Delta]} $$

We prove invertibility with respect to Definition 3.1.

**Lemma 3.3 (invertibility)** For any instance of a deduction rule where the conclusion hypersequent is valid, all premisses are also valid.

**Proof.** Considering a rule instance with a counter-model ($\mathfrak{M}, \mu$) of a premise $H$, we build a counter-model ($\mathfrak{M}, \mu'$) of the conclusion $H'$. Depending on the rule that is applied, $H$ and $H'$ will either have exactly the same structure, or $H$ will have a new cell, or $H$ will have a cluster cell where $H'$ contains a simple sequent cell. Accordingly, we take $\mu'$ to be the restriction of $\mu$ to the positions of $H'$ (and adapt it accordingly for the positions that have been shifted). It is indeed a proper embedding of $H'$ into $\mathfrak{M}$. It is then easy to see that ($\mathfrak{M}, \mu'$) is a counter-model of $H'$, since any sequent $H'(i)$ is contained in the corresponding sequent $H(j): \mathfrak{M}, \mu(j) \not\models H(j)$ implies $\mathfrak{M}, \mu'(i) \not\models H'(i)$. $\square$

**Example 3.4** We provide on the next page a proof of the hypersequent $\{Hp, Gp, p \vdash GHp\}$ in our system. At each inference, the principal formula is indicated in orange and weakenings are implicit.

**Example 3.5** Consider the hypersequent $G \neg G \perp \vdash G \perp$, which has finite counter-models with a weak total order, but no finite counter-models with a strict total order (a counter-model of this sequent must be unbounded to the right). When trying to prove this sequent with the calculus of Indrzejczak [9], the proof search strategy underlying its completeness argument unfolds the
$$ \mathcal{P} \quad \frac{\begin{array}{c} (\mathbf{ax}) \\ (\mathbf{G}\vdash) \end{array}}{\begin{array}{c} \frac{\begin{array}{c} \mathbf{H}p, \mathbf{G}p, p \vdash \parallel \vdash (\mathbf{G}Hp) \parallel p \vdash p (\mathbf{H}p)} \\ \mathbf{H}p, \mathbf{G}p, p \vdash \parallel \vdash (\mathbf{G}Hp) \parallel \vdash p (\mathbf{H}p)} \end{array}}{\begin{array}{c} \mathbf{H}p, \mathbf{G}p, p \vdash \parallel \vdash \mathbf{H}p (\mathbf{G}Hp) \\ \mathbf{H}p, \mathbf{G}p, p \vdash \mathbf{G}Hp \end{array}} \end{array}} \quad \frac{\begin{array}{c} (\mathbf{ax}) \\ (\mathbf{H}\vdash) \end{array}}{\begin{array}{c} \frac{p \vdash p (\mathbf{H}p); \{\mathbf{H}p, \mathbf{G}p, p \vdash \parallel \vdash (\mathbf{G}Hp)\}}{\vdash p (\mathbf{H}p); \{\mathbf{H}p, \mathbf{G}p, p \vdash \parallel \vdash (\mathbf{G}Hp)\}} \end{array}} \quad \begin{array}{c} (\mathbf{H}\vdash) \\ (\mathbf{G}\vdash) \end{array} $$

where $\mathcal{P}$ is:

$$ \frac{\begin{array}{c} (\mathbf{ax}) \\ \frac{\begin{array}{c} \mathbf{H}p, \mathbf{G}p, p \vdash \\ \{\mathbf{H}p, \mathbf{G}p, p \vdash \} ; \vdash (\mathbf{G}Hp) \end{array}}{\begin{array}{c} \mathbf{H}p, \mathbf{G}p, p \vdash \\ \{\mathbf{H}p, \mathbf{G}p, p \vdash \} ; \vdash p (\mathbf{H}p) ; \vdash (\mathbf{G}Hp) \end{array}} \end{array}}{\begin{array}{c} (\mathbf{H}\vdash) \\ \mathbf{P}' \end{array}} \quad \frac{\begin{array}{c} (\mathbf{ax}) \\ (\mathbf{G}\vdash) \end{array}}{\begin{array}{c} \mathbf{H}p, \mathbf{G}p, p \vdash \\ \{\mathbf{H}p, \mathbf{G}p, p \vdash \} ; \vdash \mathbf{H}p (\mathbf{G}Hp) \end{array}} \quad \begin{array}{c} (\mathbf{H}\vdash) \\ (\mathbf{H}'') \end{array} $$

where $\mathcal{P}'$ is:

$$ \frac{\begin{array}{c} (\mathbf{ax}) \\ \frac{\begin{array}{c} \mathbf{H}p, \mathbf{G}p, p \vdash \mathbf{H}p \\ \{\mathbf{H}p, \mathbf{G}p, p \vdash \} ; p \vdash p (\mathbf{H}p) ; \{\vdash (\mathbf{G}Hp)\} \end{array}}{\begin{array}{c} \mathbf{H}p, \mathbf{G}p, p \vdash \\ \{\mathbf{H}p, \mathbf{G}p, p \vdash \} ; \vdash p (\mathbf{H}p) ; \{\vdash (\mathbf{G}Hp)\} \end{array}} \end{array}}{\begin{array}{c} (\mathbf{ax}) \\ (\mathbf{G}\vdash) \end{array}} \quad \frac{\begin{array}{c} (\mathbf{ax}) \\ \frac{\begin{array}{c} \mathbf{H}p, \mathbf{G}p, p \vdash \\ \{\mathbf{H}p, \mathbf{G}p, p \vdash \} ; \{\vdash (\mathbf{G}Hp) \parallel p \vdash p (\mathbf{H}p)\} \end{array}}{\begin{array}{c} \mathbf{H}p, \mathbf{G}p, p \vdash \\ \{\mathbf{H}p, \mathbf{G}p, p \vdash \} ; \{\vdash (\mathbf{G}Hp) \parallel \vdash p (\mathbf{H}p)\} \end{array}} \end{array}}{\begin{array}{c} (\mathbf{G}\vdash) \\ (\mathbf{H}'') \end{array}} \quad \begin{array}{c} (\mathbf{H}\vdash) \\ (\mathbf{H}'') \end{array} $$
following infinite derivation, by alternating the right and left introduction rules
for G (with implicit uses of the left rules for $\supset$ and $\perp$):

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

Principal formulas shown in orange,
useless formulas in gray.

In our calculus, a derivation of that same hypersequent would necessarily
contain several branches. The analogue of the one shown above will quickly
lead to a point where only (`{{G}}`) applies, after which no rule applies:

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

In other words, it is a finite failure branch. As we shall see, we can extract from
it a finite counter-model featuring a reflexive world.
☐

**3.2 Soundness**

We show two soundness statements, relative to definitions 3.2 and 3.1.

**Lemma 3.6 (annotation-respecting soundness)** All the rules of our hypersequent calculus with clusters are sound with respect to the annotation-respecting semantics.

**Proof.** We prove the contrapositive. Considering a rule instance whose conclusion $H$ admits an annotation-respecting counter-model $(\mathfrak{M}, \mu)$, we show that one of its premises also admits an annotation-respecting counter-model $(\mathfrak{M}, \mu')$. Below, embeddings and counter-models are implicitly annotation-respecting.

We first consider the case of rule (`$\vdash G'$`), applied on a principal sequent
$\Gamma \vdash \Delta, G\varphi$ at position $i$ in $H$. Since $\mathfrak{M}, \mu(i) \not\models G\varphi$, there exists $w'$ such that
$\mu(i) \preceq w'$ and $\mathfrak{M}, w' \models \neg\varphi$. Since $\mathfrak{M}$ is finite we can take $w'$ to be a rightmost
world invalidating $\varphi$, i.e., such that there is no $w' \prec w''$ such that $w'' \models \neg\varphi$.

* We first consider the case where $\mu(i)$ and $w'$ are two worlds (distinct or not) of the same cluster. If $i$ is not in a cluster in the underlying frame of $H$, i.e., if $C = \star$, then the rule has a premise $H [{\Gamma \vdash \Delta, G\varphi}; C']$ of which $(\mathfrak{M}, \mu)$ is a counter-model. Otherwise, the premise $H [C [\Gamma \vdash \Delta, G\varphi] \parallel \vdash \varphi (G\varphi)]; C']$ is available. We extend $\mu$ into $\mu'$, mapping the new sequent, at position $i+1$, to the world $w'$: $\mu'(k) = \mu(k)$ for all $k \le i$, $\mu'(i+1) = w'$, and $\mu'(k+1) = \mu(k)$ for all $k > i$. Then $(\mathfrak{M}, \mu')$ is a counter-model of the premise. In particular, the annotation $(G\varphi)$ at position $i+1$ is respected, as we have chosen $\mu'(i+1) = w'$ such that for any $\mu'(i+1) \prec w''$, $w'' \models \varphi$.

* Otherwise, $\mu(i) \prec w'$. Let $j$ be the first position in the cell $C'$. If $w' \prec \mu(j)$, we obtain a counter-model of premise $H [C [\Gamma \vdash \Delta, G\varphi]; \vdash \varphi (G\varphi); C']$
by adapting $\mu$ into an embedding $\mu'$ that assigns $w'$ to the new position. If $\mu(j) \preceq w'$ then we have a counter-model of the second premise $H[C[\Gamma \vdash \Delta, G\varphi] ; C' \times (\vdash G\varphi)]$, with the same embedding $\mu$. Otherwise, $\mu(j) = w'$ and $\mu(j)$ is not reflexive, hence the next premise is available, namely $H[C[\Gamma \vdash \Delta, G\varphi] ; C' \times (\vdash \varphi (G\varphi))]$. Our counter-model $(\mathfrak{M}, \mu)$ is a counter-model of that premise.

In the case of rule $(\{ (G) \})$ applied on a principal sequent $\Gamma \vdash \Delta, G\varphi (G\varphi)$ at position $i$ in $H$, $i$ cannot be in a cluster. Since $(\mathfrak{M}, \mu)$ is a counter-model of $H$, we have $\mathfrak{M}, \mu(i) \models \neg G\varphi$, i.e., there is a world $w$ of $\mathfrak{M}$ such that $\mu(i) \preceq w$ and $\mathfrak{M}, w \models \neg \varphi$. Since $H(i)$ carries the annotation $(G\varphi)$, we cannot have $\mu(i) \prec w$, hence $\mu(i) = w$ or $w \preceq \mu(i)$. Either way, $\mu(i)$ is reflexive, hence $(\mathfrak{M}, \mu)$ is still a counter-model of the premise of the rule, which creates a cluster at position $i$.

We finally consider the case of rule ((G)). We show that there cannot be a counter-model $(\mathfrak{M}, \mu)$ of the conclusion $H_1[\Gamma \vdash \Delta (G\varphi)] ; H_2[\Pi \vdash \Sigma, G\varphi]$. Let $i \prec j$ be the respective positions of the two active sequents in the rule application. Since $\mathfrak{M}, \mu(j) \models \neg G\varphi$, there exists $w$ such that $\mu(j) \preceq w$ and $\mathfrak{M}, w \models \neg \varphi$. Since $\mu(i) \prec w$, this contradicts the fact that $\mu$ was assumed annotation-respecting.

The other rules are analogous, or easy to handle. □

**Theorem 3.7 (soundness)** *Our hypersequent calculus with clusters is sound: if an annotation-free hypersequent is provable, then it is valid.*

**Proof.** We prove the contrapositive. If an annotation-free hypersequent has a counter-model, then it has a finite counter-model $\mathfrak{M}$ as a consequence of the finite model property of $\mathbf{K}_t\mathbf{4.3}$ [16] recalled in Lemma A.2, Appendix A. Since $\mathfrak{M}$ is finite and $H$ does not carry any annotations, $\mathfrak{M}$ is also an annotation-respecting counter-model of $H$. So, by Lemma 3.6, $H$ is not provable. □

## 3.3 Completeness and Complexity

We now turn to establishing completeness for our calculus, and to showing that proof search yields an optimal coNP procedure for deciding $\mathbf{K}_t\mathbf{4.3}$ validity. These results follow from two properties of our calculus: deduction rules are invertible wrt. the (annotation-blind) semantics (recall Lemma 3.3), and proof search branches are polynomially bounded (as shown next in Lemma 3.8).

In this section, we call *partial proof* a finite open derivation tree: each node corresponds to a rule application, but some leaves may be left open. Partial proofs arise from (backward) proof search. We require that the conclusion hypersequent of any rule application differs from all of the premisses of that rule—this amounts to forbidding useless proof search steps.

In general, proof search may diverge by expanding partial proofs infinitely, or require backtracking due to (finite) choices in rule applications. Lemma 3.8 shows that divergence cannot happen with our calculus, regardless of the way rules are applied. Lemma 3.3 shows that backtracking is not necessary either. Hence, proof search in our calculus simply consists in expanding one proof attempt, either reaching a complete proof or obtaining a partial proof with at least one open leaf that cannot be derived by any rule application.
We define $|H|$ to be the maximum of the number of positions in $H$ and the number of distinct subformulæ occurring in $H$.

**Lemma 3.8 (small branch property)** For any partial proof of a hypersequent $H$, any branch of the proof is of length at most $4|H|^2 + 2|H|$.

**Proof.** Let $H$ be a hypersequent of size $|H|$, $\mathcal{P}$ a partial proof of it, and $\beta$ a branch of $\mathcal{P}$. Remark that the number of positions in hypersequents of $\beta$ is bounded by $2|H|$: we have at most $|H|$ positions initially, and a new position may only be created together with a new annotation among at most $|H|$ formulæ. Any rule application adds some subformula among $|H|$ to the left or to the right of the turnstile at a position among $2|H|$, hence with $4|H|^2$ choices, or changes a simple cell among $2|H|$ into a cluster. Thus $\beta$ is of length at most $4|H|^2 + 2|H|$. $\square$

**Theorem 3.9 (completeness)** *Our hypersequent calculus with clusters is complete: every annotation-free valid hypersequent $H$ has a proof.*

**Proof.** Assume that a hypersequent $H$ is not provable. Consider a partial proof $\mathcal{P}$ of $H$ that cannot be expanded any more: its leaves cannot be obtained as the conclusion of a rule instance. Such a partial proof exists by Lemma 3.8. By invertibility, it suffices to exhibit a counter-model for an open leaf of $\mathcal{P}$ to obtain a counter-model of $H$ as required.

We thus consider a leaf hypersequent $H'$, which cannot be derived by any rule (excluding rule applications which would have $H'$ itself as a premise). Let $\mathfrak{F} = (W, \preceq)$ be the underlying frame of $H'$. Let $V$ be the valuation defined for all $i \in W$ by $V(p) = \{i \in W \mid p \text{ appears on the left-hand side of } H'(i)\}$. Finally, let $\mathfrak{M} = (\mathfrak{F}, V)$. We shall establish that $(\mathfrak{M}, \mu)$ is a counter-model of $H'$, where $\mu$ is the identity embedding $H' \hookrightarrow_{\mu} \mathfrak{F}$. More precisely, we prove by structural induction on $\varphi$ that, for every position $i$ of $H'$:

* If $\varphi$ appears on the left of the turnstile in $H'(i)$, then $\mathfrak{M}, i \models \varphi$.

* If $\varphi$ appears on the right of the turnstile in $H'(i)$, then $\mathfrak{M}, i \not\models \varphi$.

We reason by case analysis on $\varphi$. We only detail below the case where $\varphi = G\varphi'$, since the other cases are either standard or analogous.

* If $G\varphi'$ appears on the left-hand side of a sequent $H'(i)$, then, since rules $(G\vdash)$ and $(G\vdash')$ cannot be applied on $H'$, $\varphi'$ appears on the left-hand side of every sequent $H'(j)$ such that $i \preceq j$. By induction hypothesis, $\mathfrak{M}, j \models \varphi'$ for all $i \preceq j$. Hence $\mathfrak{M}, i \models G\varphi'$.

* If $G\varphi'$ appears on the right-hand side of $H'(i)$, there must be some position $j$ such that $H'(j)$ carries the annotation $(G\varphi')$, as otherwise, either $(\vdash G)$ or $(\vdash G')$ would apply. Moreover, by inspection of our rules and since $H$ was initially annotation-free, necessarily $j$ must contain $\varphi'$ on its right-hand side. By totality, we have $i \preceq j, j \preceq i$ or $i = j$. If $i = j$, since rule $((G))$ does not apply, $i$ is in a cluster. If $j \preceq i$, since rule $((G))$ does not apply, $i$ and $j$ must be in the same cluster. So we have $i \preceq j$ in any case. By induction hypothesis on $\varphi'$, we have $\mathfrak{M}, j \not\models \varphi'$, hence $\mathfrak{M}, i \not\models G\varphi'$. $\square$
**Proposition 3.10** *Proof search in our hypersequent calculus is in coNP.*

**Proof.** Proof search can be implemented in an alternating Turing machine maintaining the current hypersequent on its tape, where existential states choose which rule to apply to which principal sequent(s) and formula, and universal states choose a premise of the rule. By Lemma 3.8, the computation branches are of length bounded by a polynomial. By Lemma 3.3, the non-deterministic choices in existential states can be replaced by arbitrary deterministic choices, thus this Turing machine has only universal states, hence is in coNP. □

## 4 Extensions

The logic K<sub>t</sub>4.3 can be extended by additional axioms to further restrict the class of frames. We consider here two examples of such extensions also considered by Indrzejczak [9]: density and unboundedness. For each extension, we show that our calculus can be adapted by adding new rules corresponding to the new axioms, and yields the same coNP upper bound. These new rules are rather different from Indrzejczak's, and exploit our use of hypersequents with clusters. Together, these rules extend our calculus into a sound and complete proof system with a coNP proof search algorithm for K<sub>t</sub>Q, the logic of dense unbounded linear frames, consisting of K<sub>t</sub>4.3 with both extensions.

**Density.** A frame $\mathfrak{F} = (W, \preceq)$ is dense if $\forall (x, y) \in W^2$, if $x \preceq y$ then $\exists z \in W$ such that $x \preceq z \preceq y$. Density is axiomatised by adding the following axiom:

$$Fp \supset FFp \qquad (\mathbf{Den})$$

This new logic also has a finite model property as well as a small model property [16]. Moreover, a finite weak total order is dense if and only if it never has two consecutive worlds that are not in clusters. This last property leads to the following new rule for our calculus to handle density:

$$\frac{H[\{S_1\}; S_2] \quad H[S_1; \{\vdash\}; S_2] \quad H[S_1; \{S_2\}]}{H[S_1; S_2]} \qquad (\mathbf{den})$$

**Proposition 4.1** *Adding (den) to our calculus yields a sound and complete proof system for K<sub>t</sub>4.3 ∪ (Den), where proof search is in coNP.*

**Proof.** Our rule is obviously sound, as it closely reflects the shape of dense finite weak total orders. It is also invertible, since the underlying frame of the conclusion of the rule is always a subframe of its premises. Hence Theorem 3.7 and Lemma 3.3 still hold.

To obtain that proof search is in coNP, it suffices to check that Lemma 3.8 carries over to our extension. This is true because the rule (den) can only be applied on two consecutive non-cluster cells, and whenever the rule (den) is applied on such a bad occurrence, this occurrence is no longer present in the premises. Hence, every time the rule (den) is applied, we reduce at least by one the number of bad occurrences, so we can only apply the rule (den) a finite
number of times between applications of other rules creating new cells such as (†G) and (†H). Finally, since new cells can only be created polynomially many times by those other rules thanks to our initial strategy, the new rule (den) can, in the end, only be applied polynomially many times along a branch. So the branches of our proof tree are still polynomial.

Finally, completeness is obtained as in Theorem 3.9. It only remains to show that the underlying frame of a hypersequent found at the end of a failing branch is dense. Indeed, if its underlying frame was not dense, we could apply the rule (den) which would contradict the fact that no rules can be applied any more on this hypersequent. □

**Unboundedness.** A frame $\mathfrak{F} = (W, \preceq)$ is *unbounded to the right* if $\forall x \in W, \exists y \in W$ such that $x \preceq y$. Symmetrically, a frame $\mathfrak{F} = (W, \preceq)$ is *unbounded to the left* if $\forall x \in W, \exists y \in W$ such that $y \preceq x$. These frame properties can be axiomatised by adding the following axiom(s):

$$ Gp \supset Fp \qquad (D_r) $$

$$ Hp \supset Pp \qquad (D_\ell) $$

The logics we obtain when adding these axioms still have a finite model property and a small model property [16]. Moreover, a finite weak total order is unbounded to the right (resp. left) if and only if its rightmost (resp. leftmost) world is in a cluster. This leads to the following new rules for our calculus to handle unboundedness:

$$ (D_r) \frac{H; \{S\} \quad H; S; \{\vdash\}}{H; S} \qquad \frac{\{S\}; H \quad \{\vdash\}; S; H}{S; H} \qquad (D_\ell) $$

**Proposition 4.2** *Adding $(D_r)$ (resp. $(D_\ell)$) yields a sound and complete proof system for $K_t 4.3 \cup (D_r)$ (resp. $K_t 4.3 \cup (D_\ell)$), where proof search is in coNP.*

**Proof.** It is easy to check that rule $(D_r)$ is sound, as it reflects the shape of right-unbounded finite weak total orders. It is also invertible, since the underlying frame of the conclusion of the rule is always a subframe of its premises. Hence Theorem 3.7 and Lemma 3.3 still hold.

To obtain that proof search is in coNP, it suffices to check that Lemma 3.8 carries over to our extension. This is true because the rule $(D_r)$ can only be applied when the last cell of the hypersequent is not a cluster, and whenever the rule $(D_r)$ is applied, the last cell of its premises is always a cluster. Hence, the rule $(D_r)$ can only be applied once between applications of other rules creating new cells such as (†G) and (†H). Finally, since new cells can only be created polynomially many times by those other rules thanks to our initial strategy, the new rule $(D_r)$ can, in the end, only be applied polynomially many times along a branch. So the branches of our proof tree are still polynomial.

Finally, completeness is obtained as in Theorem 3.9. It only remains to show that the underlying frame of a hypersequent found at the end of a failing branch
is unbounded to the right. Indeed, if its underlying frame was not unbounded to the right, we could apply the rule ($D_r$) which would contradict the fact that no rules can be applied any more on this hypersequent. □

One can see that all rules can be taken together to form a sound and complete calculus for $K_tQ$, with coNP proof search. Note that the rules proposed in this section differ from the ones proposed by Indrzejczak for density and unboundedness [9]. These rules would be sound but would break our polynomial bound on the length of proof branches.

# 5 First-Order Logic with Two Variables

We show here a coNEXP upper bound on the complexity of validity in the two-variable fragment of first-order logic over linear orders, re-proving and extending recent results by Manuel and Sreejith [14].

**Syntax and Semantics.** We consider first-order formulæ with two variables $x$ and $y$ over the signature (=, <, (p)$_{p \in \Phi}$) where = and < are binary relational symbols and each $p$ is a unary relational symbol:

$$ \psi ::= z' \mid z < z' \mid p(z) \mid \perp \mid \psi \supset \psi \mid \forall z.\psi \quad (\text{first-order formulæ}) $$

where $z, z'$ range over $\{x, y\}$ and $p$ over $\Phi$. We call this logic $FO^2(\langle\rangle)$.

We interpret our formulæ over structures $\mathfrak{M} = (W, <, V)$ where = is interpreted as the equality over $W$, < as the strict total ordering of $W$, and each $p$ as $V(p)$ for the valuation $V: \Phi \to 2^W$.

**Equivalence with $K_t4.3$.** Given an $FO^2(\langle\rangle)$ formula $\psi(z)$ with one free variable $z$, Etessami et al. [6] show how to construct a $K_t4.3$ formula $\varphi$ such that, for all strict totally ordered structures $\mathfrak{M} = (W, <, V)$, $\mathfrak{M}, [w/z] \models \psi$ if and only if $\mathfrak{M}, w \models \varphi$, where $[w/z]$ is the variable assignment mapping $z$ to $w$.

**Fact 5.1 ([6, Thm. 2])** Every $FO^2(\langle\rangle)$ formula $\psi(z)$ can be converted to an equivalent $K_t4.3$ formula $\varphi$ with $|\varphi| \in 2^{poly(|\psi|)}$.

Although the proof of [6, Thm. 2] is given for the case of the strict total order $\omega$— i.e., for $\omega$-words over the alphabet $2^\Phi$, it actually does not rely on this specific frame and applies similarly to arbitrary strict total orders.

We have therefore the following, where the NEXP upper bounds in items (i–iii) were already shown by Manuel and Sreejith [14, Thm. 15] using automata-based techniques. Let us reiterate that the complexity bounds on the satisfiability problem for the modal logics in question were already known [16], so the interest here lies in the use of proof search in our hypersequent proof system rather than a brutal enumeration of all potential models up to some bound.

**Theorem 5.2** The following problems are in NEXP: satisfiability of $FO^2(\langle\rangle)$ over (i) arbitrary strict total orders, (ii) countable strict total orders, (iii) scattered strict total orders, and (iv) dense strict total orders.

**Proof.** Regarding (i), given an $FO^2(\langle\rangle)$ formula $\psi$, we first turn it into the equisatisfiable formula $\exists y.\psi$ with one free variable $x$. Fact 5.1 then allows to
construct a $K_t4.3$ formula $\varphi$ of exponential size, which is equisatisfiable over strict total orders. By Fact 2.1, it is also equisatisfiable over weak total orders, and Theorem 3.10 shows that satisfiability can be checked in non-deterministic polynomial time in $|\varphi|$, hence in NEXP overall.

Regarding (ii) and (iii), by [16, Thm. 3], the above-constructed $\varphi$ is satisfiable over weak total orders if and only if it is satisfiable over finite weak total orders. The bulldozing construction used to prove Fact 2.1 (see [2, Thm. 4.56]) consists essentially in turning each cluster into a direct product $\omega^* \cdot \omega$ (i.e., a copy of $\mathbb{Z}$), which shows that $\varphi$ is satisfiable over finite weak total orders if and only if it is satisfiable over countable scattered strict total orders.

Finally, regarding (iv), by adapting [2, theorems 4.41 and 4.56] to bulldoze clusters over $\mathbb{Q}$ rather than $\mathbb{Z}$, $\psi$ is satisfiable over dense strict total orders if and only if the above-constructed $\varphi$ is satisfiable over dense weak total orders as a $K_t4.3 \cup (\text{Den})$ formula. By Proposition 4.1, the latter can be checked in non-deterministic polynomial time in $|\varphi|$, hence in NEXP overall. $\square$

# 6 Discussion

We have designed a sound and complete hypersequent calculus with clusters for the modal logic $K_t4.3$ of linear temporal frames. The proof system relies on the finite model property of our logic in the presence of clusters to bound the length of branches during a proof search, which yields a proof search with optimal coNP complexity for the validity problem. Moreover, the approach is modular, as these results remain true when extending the proof system to handle density and unboundedness, yielding a sound and complete system for $K_tQ$ with the same complexity, and a sound and complete system for $FO^2(\mathbb{<})$ with coNEXP upper bounds. This coNEXP upper bound itself is hardly surprising, but from a proof-theoretic perspective, the two-variable fragment of first-order logic is an unusual beast—eigenvariables must be avoided—, hence our solution through a proof system for a modal logic is arguably a natural one.

An extension we would like to consider in future work is *well-foundedness*, by adding the Gödel-Löb axiom to our logic. Here, the logic of weak total orders well-founded to the left and unbounded to the right does not enjoy a finite model property.

# A Finite Model Property

We recall the result from Ono and Nakamura [16] which yields the finite model property for all logics considered in this paper. Finite models are obtained by using a filtration [2, Def. 2.36] on a structure to obtain a finite structure of the same ‘shape.’ The relevant filtration in this case is called the *Lemmon filtration*.

**Lemmon Filtration.** Let $\mathfrak{M} = (W, \prec, V)$ be a Kripke structure. Let $\Psi$ be a set of $K_t4.3$ formulæ closed under taking subformulæ. We define a binary relation $\equiv$ on $W$ by:

$$w \equiv w' \text{ iff } \forall \psi \in \Psi, \mathfrak{M}, w \models \psi \iff \mathfrak{M}, w' \models \psi$$
The relation $\equiv$ is an equivalence relation, and we note $[w]$ the equivalence class of a world $w \in W$. Note that, if $\Psi$ is finite, then $\equiv$ has finite index. Moreover, if $w \equiv w'$, then $\forall p \in \Phi \cap \Psi, w \in V(p) \iff w' \in V(p)$. Hence, we can define the *Lemmon filtration* of $\mathfrak{M}$ by $\Psi$ as $\mathfrak{M}^f = (W^f, \preceq^f, V^f)$ such that:

$$ W^f = W/\equiv \qquad V^f(p) = V(p)/\equiv \\ [w] \preceq^f [w'] \text{ iff } \left\{ \begin{array}{l} \forall \mathfrak{G} \psi \in \Psi, \text{ if } \mathfrak{M}, w \models \mathfrak{G} \psi \text{ then } \mathfrak{M}, w' \models \mathfrak{G} \psi \text{ and } \mathfrak{M}, w' \models \psi \\ \forall \mathfrak{H} \psi \in \Psi, \text{ if } \mathfrak{M}, w' \models \mathfrak{H} \psi \text{ then } \mathfrak{M}, w \models \mathfrak{H} \psi \text{ and } \mathfrak{M}, w \models \psi \end{array} \right. $$

**Fact A.1 ([16, Thm. 3])** Let $\mathfrak{M} = (W, \preceq, V)$ be a weak total order and $\Psi$ a set of $\mathbf{K}_t\mathbf{4.3}$ formulæ closed under taking subformulæ, and let $\mathfrak{M}^f = (W^f, \preceq^f, V^f)$ be the Lemmon filtration of $\mathfrak{M}$ by $\Psi$. Then (i) $[w] \preceq^f [w']$ if $w \preceq w'$, (ii) $\preceq^f$ is transitive and linear, (iii) $\preceq^f$ is unbounded to the right (resp. left) if $\preceq$ is unbounded to the right (resp. left), and (iv) $\preceq^f$ is dense if $\preceq$ is dense.

Now, if $\mathfrak{M}$ is a model of a $\mathbf{K}_t\mathbf{4.3}$ formula $\varphi$ and $\Psi$ is the set of subformulæ of $\varphi$, then $\mathfrak{M}^f$ is finite since $\Psi$ is finite. Moreover, if we had $\mathfrak{M}, w \models \varphi$, then we also have $\mathfrak{M}^f, [w] \models \varphi$ since it is a filtration [2, Thm. 2.39]. Hence, all the logics presented in this paper have the finite model property.

Finally, we show that our hypersequents with clusters also enjoy the finite counter-model property; the following proof also captures our extensions to dense and unbounded frames.

**Lemma A.2** If $H$ is an invalid annotation-free hypersequent with clusters, then $H$ has a finite counter-model.

**Proof.** Let $(\mathfrak{M}, \mu)$ be a counter-model of $H$ and $\mathfrak{M}^f$ its Lemmon filtration for $\Psi$ the set of subformulæ of $H$. For every position $i$ of $H$, we have $\mathfrak{M}^f, [\mu(i)] \not\models H(i)$. But $\mu^f: i \mapsto [\mu(i)]$ might not be an embedding of $H$ in $\mathfrak{M}^f$, as we could have two positions $i \prec j$ such that $[\mu(i)] \preceq^f [\mu(j)]$ and $[\mu(j)] \preceq^f [\mu(i)]$, i.e., $[\mu(i)] \not\models^f [\mu(j)]$. We can avoid this problem by duplicating such clusters.

Formally, let $i \prec j$ and $[\mu(i)] \not\models^f [\mu(j)]$. Let $C = \{w \in \mathfrak{M}^f | w \not\models^f [\mu(i)]\}$ be the cluster containing $[\mu(i)]$ and $[\mu(j)]$. We define a modified model $\mathfrak{M}_1^f = (W_1^f, \preceq_1^f, V_1^f)$ featuring two copies of $C$ as follows:

$$ W_1^f = (W^f \setminus C) \cup \{(w, b) \mid w \in C, b \in \{0, 1\}\} \\ V_1^f(w) = V^f(w) \quad \forall w \in W^f \setminus C \\ V_1^f((w, b)) = V^f(w) \quad \forall (w, b) \in C \times \{0, 1\} \\ (w, b) \preceq_1^f (w', b) \quad \forall (w, w', b) \in C^2 \times \{0, 1\} \quad (w, 0) \preceq_1^f (w', 1) \quad \forall (w, w') \in C \\ w \preceq_1^f (w', b) \quad \text{whenever } w \preceq^f w' \quad (w, b) \preceq_1^f w' \quad \text{whenever } w \preceq^f w' \\ w \preceq_1^f w' \quad \text{whenever } w \preceq^f w' $$

We now have $([\mu(i)], 0) \preceq_1^f ([\mu(j)], 1)$ and we still have $\mathfrak{M}_1^f, ([\mu(i)], 0) \not\models H(i)$ and $\mathfrak{M}_1^f, ([\mu(j)], 1) \not\models H(j)$, because $[\mu(i)]$ and $([\mu(i)], 0)$ (resp. $[\mu(j)]$ and $([\mu(j)], 1)$)
are bisimilar [2, Thm. 2.20]. The mapping $\mu^f$ can be modified into $\mu_1^f$ as follows:

$$ \mu_1^f(k) = \begin{cases} ([\mu(k)], 0) & \text{if } k \in C \text{ and } k \preceq i \\ ([\mu(k)], 1) & \text{if } k \in C \text{ and } i \prec k \\ [\mu(k)] & \text{if } k \notin C \end{cases} $$

This fixes the failure of the second condition of embeddings on $i$ and $j$, though not necessarily on other positions.

Finally, let $\mathfrak{M}'$ be the model obtained from $\mathfrak{M}^f$ after performing this duplication for all such $i \prec j$; $\mathfrak{M}'$ is finite, since $\mathfrak{M}^f$ is finite and we only did finitely many copies, and the resulting $\mu'$ is such that $(\mathfrak{M}', \mu')$ is a counter-model of $H$. $\square$

## References

[1] Avron, A., *Hypersequents, logical consequence and intermediate logics for concurrency*, Annals of Mathematics and Artificial Intelligence **4** (1991), pp. 225-248.

[2] Blackburn, P., M. de Rijke and Y. Venema, "Modal Logic," Cambridge Tracts in Theoretical Computer Science **53**, Cambridge University Press, 2001.

[3] Brünnler, K., *Deep sequent systems for modal logic*, Archiv für Mathematische Logik und Grundlagenforschung **48** (2009), pp. 551-577.

[4] Clarke, E. M. and E. A. Emerson, *Design and synthesis of synchronization skeletons using branching time temporal logic*, in: Proc. Workshop on Logic of Programs, Lecture Notes in Computer Science **131** (1981), pp. 52-71.

[5] Cocchiarella, N. B., "Tense and Modal Logic: a Study in the Topology of Temporal Reference," Ph.D. thesis, University of California, Los Angeles (1965).

[6] Etessami, K., M. Y. Vardi and T. Wilke, *First-order logic with two variables and unary temporal logic*, Information and Computation **179** (2002), pp. 279-295.

[7] Indrzejczak, A., *Cut-free hypersequent calculus for S4.3*, Bulletin of the Section of Logic **41** (2012), pp. 89-104.

[8] Indrzejczak, A., *Eliminability of cut in hypersequent calculi for some modal logics of linear frames*, Information Processing Letters **115** (2015), pp. 75-81.

[9] Indrzejczak, A., *Linear time in hypersequent framework*, Bulletin of Symbolic Logic **22** (2016), pp. 121-144.

[10] Indrzejczak, A., *Cut elimination theorem for non-commutative hypersequent calculus*, Bulletin of the Section of Logic **46** (2017), pp. 135-149.

[11] Laroussinie, F., N. Markey and Ph. Schnoebelen, *Temporal logic with forgettable past*, in: Proc. LICS 2002 (2002), pp. 383-392.

[12] Lellmann, B., *Linear nested sequents, 2-sequents and hypersequents*, in: Proc. Tableaux 2015, Lecture Notes in Computer Science **9323** (2015), pp. 135-150.

[13] Lichtenstein, O., A. Pnueli and L. Zuck, *The glory of the past*, in: Proc. Workshop on Logics of Programs, Lecture Notes in Computer Science **193** (1985), pp. 196-218.

[14] Manuel, A. and A. V. Sreejith, *Two-variable logic over countable linear orderings*, in: Proc. MFCS 2016, Leibniz International Proceedings in Informatics **58** (2016), pp. 66:1-66:13.

[15] Negri, S., *Proof analysis in modal logic*, Journal of Philosophical Logic **34** (2005), pp. 507-544.

[16] Ono, H. and A. Nakamura, *On the size of refutation Kripke models for some linear modal and tense logics*, Studia Logica **39** (1980), pp. 325-333.

[17] Pnueli, A., *The temporal logic of programs*, in: FOCS 1977 (1977), pp. 46-57.

[18] Poggiolesi, F., *The method of tree-hypersequents for modal propositional logic*, in: Proc. Trends in Logic IV, Trends in Logic **28** (2009), pp. 31-51.

[19] Prior, A. N., "Time and Modality," Oxford University Press, 1957.

[20] Sistla, A. P. and E. M. Clarke, *The complexity of propositional linear temporal logics*, Journal of the ACM **32** (1985), pp. 733-749.