1 Introduction
Modal sequent calculi have been developed for K and many of its extensions, but it has historically been difficult to develop sequent systems that have nice proof-theoretic properties. The cut elimination theorem is an important result in structural proof theory: any sequent that is derivable in a calculus can be derived without the use of cut. Notably, the sequent system for S5 given by Ohnishi & Matsumoto (Reference Ohnishi and Matsumoto1957) is not cut-free. Although cut-free sequent systems for S5 were later developed by Ohnishi (Reference Ohnishi1982) and Braüner (Reference Braüner2000), this issue prompted research into extensions of the sequent calculus that could better accommodate modal logics. One such extension is hypersequent calculi, which operate on sets or sequences of sequents. The first hypersequent system, also for S5, was presented by Mints (Reference Mints1971, Reference Mints and Feys1974). There has since been a proliferation of hypersequent approaches to modal logics (Pottinger, Reference Pottinger1983; Avron, Reference Avron, Hodges, Hyland, Steinhorn and Truss1996; Brünnler, Reference Brünnler2009; Restall, Reference Restall2009; Poggiolesi, Reference Poggiolesi2008; Indrzejczak, Reference Indrzejczak2012; Lahav, Reference Lahav2013).
Sequents
can be translated into single formulas:
$\bigwedge \Gamma \to \bigvee \Delta $
, or sometimes
$\Box (\bigwedge \Gamma \to \bigvee \Delta )$
in the case of sequent systems for modal logics. Earlier hypersequent approaches to modal logics interpret hypersequents as disjunctions of the formula interpretations of the individual sequents. Intuitively, a hypersequent is evaluated at a single world, and describes a disjunction. Under this interpretation, the order and multiplicity of sequents in a hypersequent is immaterial, and external contraction, exchange, and weakening are admissible rules. More recent approaches, however, interpret hypersequents in such a way that different sequents in a hypersequent are evaluated at different worlds. If the logic is S5 (and so either no or a universal accessibility relation is assumed), the order and multiplicity of sequents in a hypersequent still does not matter. But for other logics, the worlds at which adjacent sequents in a hypersequent are evaluated must be related. Then the order and multiplicity of sequents in a hypersequent does matter, and external structural rules such as external contraction, weakening, and exchange are not sound in general. Approaches using this interpretation of hypersequents are the linear nested sequent systems of Lellmann (Reference Lellmann and De Nivelle2015), Lellmann & Pimentel (Reference Lellmann and Pimentel2019), and Goré & Lellmann (Reference Goré, Lellmann, Cerrito and Popescu2019), the noncommutative hypersequents of Indrzejczak (Reference Indrzejczak2016, Reference Indrzejczak2018, Reference Indrzejczak2019), and the ordered hypersequents of Baelde, Lick, & Schmitz (Reference Baelde, Lick, Schmitz, D’Agostino, Bezhanishvili, Metcalfe and Studer2018). The 2-sequents of Masini (Reference Masini1992) are a notational variant of hypersequents with the same interpretation as linear nested sequents. Kuznets & Lellmann (Reference Kuznets, Lellmann, D’Agostino, Bezhanishvili, Metcalfe and Studer2018) applied the linear nested sequent approach also to Gödel logic.
The hypersequent system for S5 of Restall (Reference Restall2009), although taking hypersequents as sets of sequents, explicitly interprets individual sequents as describing different possible worlds. Parisi (Reference Parisi2017, Reference Parisi2020) generalized this interpretation by incorporating an accessibility relation into the interpretation of a hypersequent, and offered calculi for K, T, D, S4, and S5. The interpretation of Parisi’s hypersequents is equivalent to the formula interpretation of linear nested sequents. To unify terminology, we’ll call hypersequents relational if their interpretation takes the accessibility relation into account.
In addition to cut elimination, there are other desiderata that one might consider when developing hypersequent calculi. We consider two properties of hypersequent systems that have been proposed as important. One is modularity: each property of the accessibility relation is captured by a single rule or set of rules. Modularity yields a satisfying systematicity for proof systems for various kinds of modal logics. The fact familiar from modal correspondence theory that properties of the accessibility relation can be captured by different modal axioms allows for elegant treatment of large classes of logics and uniform results. Likewise, analogous modularity of proof systems opens up the possibility of dealing with combinations of properties of the accessibility relation not piecemeal, but systematically by combining different structural rules. Another property relational hypersequent systems have is that they obey what’s been called Došen’s principle: hypersequent systems for different modal logics only differ in the presence or absence of structural rules, while the rules for modalities are the same for all systems. This corresponds to a methodological principle that the meaning of a connective should be determined by its rules of inference. So, the rules for modal operators should be the same regardless of the structure of the accessibility relation.
Parisi’s systems are the first candidates for hypersequent calculi for modal logics that are both modular and conform to Došen’s principle. These systems are unique in that they do not require the addition of rules that govern the modal operator when moving between modal systems. Different modalities are treated using only external structural rules.Footnote 1 This is not to say that modular systems obeying Došen’s principle are superior to other approaches. In fact, e.g., Poggiolesi ( Reference Poggiolesi2011 , pp. 32–34) has called Došen’s principle into question, and perhaps the ideal of modularity simply cannot be universally combined with other results such as cut elimination.
The prospects of the relational hypersequent approach to obtain cut-free systems that are modular and obey Došen’s principle is nevertheless an important and interesting question, which this paper aims to shed light on. In §2, we introduce Parisi’s relational hypersequent approach and compare it to Lellman’s linear nested sequents. Lellmann (Reference Lellmann and De Nivelle2015) and Parisi (Reference Parisi2017, Reference Parisi2020) showed completeness for their systems by inductively translating usual sequent derivations into hypersequent derivations. Cut-free completeness for the hypersequent systems then follows from the cut-free completeness of the corresponding sequent system. Exceptions are Parisi’s systems RB, RS4, and RS5, where the translation makes use of the cut rule. Masini (Reference Masini1992) and Parisi (Reference Parisi2017) independently gave syntactic cut-elimination proofs for their (equivalent) systems for D. Restall (Reference Restall2009) shows cut-free completeness for RS5 directly. We improve on these results by providing a direct cut-free completeness proof for RK, the relational hypersequent calculus for K (§3). In §4 we show how this proof can be adapted to obtain cut-free completeness for T and D. Finally, in §5 we discuss the limitations of the method for the cases of logics B and S4.
2 Relational hypersequent calculi
Definition 1. We call any expression of the form
a sequent, where
$\Gamma $
and
$\Delta $
are sets of formulas.
A hypersequent is any expression of the form
, where the
$S_i$
are sequents.
The rules for the calculus RK, sound and complete for K, are found in Table 1. To keep the subsequent proofs simple, we give only the logical rules for
$\lnot $
,
$\land $
, and
$\Box $
. (The rules for
$\lor $
and
$\to $
are as usual, and rules for
$\Diamond $
are symmetrical to those for
$\Box $
.) Below is an example proof in RK.
Rules of RK
Calculi for extensions of K are obtained by adding external structural rules, which each characterize a property of the accessibility relation. The structural rules and resulting calculi are summarized in Tables 2 and 3. As usual, we write
$\vdash _{\mathrm {RX}} H$
to mean that H has a derivation in calculus RX, where X is one of K, T, 4, B, D, S4, S5.Footnote
2
Additional external structural hypersequent rules
Hypersequent calculi for various logics
With the exception of RS5, these systems are modular: each external structural rule represents an axiom characteristic of a property of the accessibility relation. In the case of system RS5, the EE rule does not only capture symmetry, but also transitivity. This way of capturing S5 is equivalent to that of Restall (Reference Restall2009), but one may also straightforwardly replace the EE rule with Sym. The resultant calculus would be complete (Reference ParisiParisi 2017, Reference Parisi2020), but the simulation of sequent derivations in the hypersequent calculus uses cut.
The semantics of relational hypersequents are given in terms of absence of counterexamples.
Definition 2 (Branch of worlds)
Let
$\mathfrak {F} = \langle W, R\rangle $
be a frame. A branch of worlds in
$\mathfrak {F}$
is a sequence
$w_1$
, …,
$w_n$
of worlds such that
$w_i R w_{i+1}$
for
$i=1$
, …,
$n-1$
.
Definition 3 (Countermodel)
A model
$\mathfrak {M}$
is a countermodel to a sequent
at a world w iff for all
$\varphi \in \Gamma , \mathfrak {M}, w \models \varphi $
and for all
.
Definition 4 (Counter-example)
A model
$\mathfrak {M}$
is a counter-example to a hypersequent
iff there is a branch of worlds
$w_1$
, …,
$w_n$
such that
$\mathfrak {M}$
is a countermodel to
at
$w_i$
for all
$1 \leq i \leq n$
.
Definition 5 (Valid hypersequent)
A hypersequent H is valid in a class of frames
$\mathfrak {F}$
just in case there is no counter-example to it that is in
$\mathfrak {F}$
. Otherwise, we say that the hypersequent is invalid.
It is important to note that the interpretation of the relational hypersequent is equivalent to that of the linear nested sequent, as in Lellmann (Reference Lellmann and De Nivelle2015). Whereas the interpretation of the relational hypersequent is given in terms of a branch of worlds along a hypersequent, linear nested sequents interpret the hypersequent as a disjunction of nested modal formulas. This interpretation is given by a mapping I on hypersequents H:
In other words, a linear nested sequent
is interpreted as
$$ \begin{align*} \Big(\bigwedge \Gamma_1 \to \bigvee \Delta_1 \Big) \lor \Box \Big(\Big(\bigwedge \Gamma_2 \to \bigvee \Delta_2\Big) \lor \Box \Big(\cdots \Box \Big(\bigwedge \Gamma_n \to \bigvee \Delta_n\Big) \cdots \Big) \Big). \end{align*} $$
Proposition 6. A relational hypersequent
is valid iff
is valid.
Proof. Prove by induction on n that
iff there is a branch of worlds
$w_1$
, …,
$w_n$
in
$\mathfrak {M}$
with
$w_i R w_{i+1}$
such that for each i,
$\mathfrak {M}$
is a countermodel to
at
$w_i$
. This is clear for
$n=1$
. Let
. Now
iff both
and, for some
$w_2$
such that
$w_1 R w_2$
,
. By induction hypothesis, the latter holds iff there is a branch of worlds
$w_2$
, …,
$w_n$
such that
$\mathfrak {M}$
is a counterexample to
at
$w_i$
for each
$i = 2$
, …, n. Since
just means that
$\mathfrak {M}$
is a countermodel to
at
$w_1$
, the claim follows. □
So Parisi’s relational hypersequents and Lellman’s linear nested sequents have the same semantic interpretation. Their calculi differ, however, in that Parisi’s systems conform to Došen’s principle. The base calculus RK contains a pair of rules for
$\Box $
, and extensions of RK for other systems add structural rules, but no rules that mention
$\Box $
.
Soundness proofs for the relational calculi can be found in Parisi (Reference Parisi2017, Reference Parisi2020). Most of the cases are routine; we give the cases for
$\land $
R,
$\Box $
, EWL and EWR as examples.
Theorem 7 (Soundness)
If
$\vdash _{\mathrm {RK}} H$
, then there is no counter-example to H.
Proof. The proof proceeds by induction on the length of a derivation
$\delta $
.
-
1. Base Case:
$\beta $
is an instance of an axiom, (
). There is no model
$\mathfrak {M}$
and possible world
$w_i$
such that
$\mathfrak {M}, w_i \models \varphi $
and
$\mathfrak {M}, w_i \not \models \varphi $
.Let
$\beta $
be the last inference of
$\delta $
. We show that each rule preserves validity: if the conclusion is not valid, then one of the premises is not valid. We give the details for
$\land $
R,
$\Box $
L,
$\Box $
R, and EWR; the other cases are treated the same. -
2.
$\beta $
is an instance of the
$\land $
R rule:Let
$\mathfrak {M}, w_1, \ldots , w_n$
form a counter-example to the conclusion. So
$w_1, \ldots , w_n$
forms a branch of worlds such that
$w_{k} R w_{k+1}$
and
$\mathfrak {M}$
is a countermodel to each sequent
at
$w_k$
for all
$1 \leq k \leq n$
with
$k\neq i$
, and a countermodel to
at
$w_i$
. So
$\mathfrak {M}, w_i \models \Gamma _i$
, and for each
$\theta \in \Delta _i \cup \{\phi \land \psi \}$
,
. It follows that
or
. In the former case,
$\mathfrak {M}$
,
$w_1$
, …,
$w_n$
is a counter-example to the left premise, in the latter, a counter-example to the right premise. -
3.
$\beta $
is an instance of
$\Box $
L.Suppose
$\mathfrak {M}, w_1, \ldots , w_n$
is a counter-example for the conclusion. Then
$\mathfrak {M}$
is a countermodel to
at
$w_i$
. It follows that
$\mathfrak {M}, w_i \models \Box \varphi $
. So, for all v such that
$w_i R v$
,
$\mathfrak {M}, v \models \varphi $
. Since
$w_i R w_{i+1}$
, we have that
$\mathfrak {M}, w_{i+1} \models \varphi $
. Since
$\mathfrak {M}, w_1, \ldots , w_n$
is a counter-example to the lower hypersequent,
$\mathfrak {M}, w_{i+1} \models \Gamma _{i+1}$
and
for all
$\theta \in \Delta _{i+1}$
. So
$\mathfrak {M}$
is also a countermodel to the sequent (
) at
$w_{i+1}$
. Hence,
$\mathfrak {M}, w_1, \ldots , w_n$
is also a counter-example to the premise. -
4.
$\beta $
is an instance of
$\Box $
R.Suppose that
$\mathfrak {M}, w_1, \ldots , w_n$
forms a counter-example to the conclusion. Then
$\mathfrak {M}$
is a countermodel to
at
$w_n$
. This means that
$\mathfrak {M}, w_n \not \models \Box \varphi $
. So, there is some possible world v such that
$w_n R v$
and
$\mathfrak {M}, v \not \models \varphi $
. But then
$\mathfrak {M}$
is also a countermodel to the sequent (
) at v. So
$\mathfrak {M}, w_1, \ldots , w_n, v$
is a counter-example to the premise. -
5.
$\beta $
is an instance of EWR.Suppose that
$\mathfrak {M}, w_1, \ldots , w_n, w_{n+1}$
forms a counter-example to the conclusion of the inference: If
$\mathfrak {M}$
is a countermodel to
at
$w_k$
for all
$1 \leq k \leq n$
. Of course,
$\mathfrak {M}$
is a countermodel to the empty sequent at any world, in particular
$w_{n+1}$
. It follows that
$\mathfrak {M}, w_1, \ldots , w_{n}$
is a counter-example to G. □
Theorem 8. If
$\vdash _{\mathrm {RT}} H$
, then there is no reflexive counter-example to H.
Proof. We show that the EC rule is sound for reflexive frames. Consider:
Let
$\mathfrak {M}$
be a reflexive counter-example to the conclusion, i.e.,
$\mathfrak {M}$
is a countermodel to
at
$w_k$
for
$1 \leq k \leq n$
. Since the frame is reflexive,
$w_i R w_i$
. So
$w_1, \ldots , w_i, w_i, \ldots , w_n$
is a branch of worlds where
$w_j$
is a counter-example to
for all
$1 \leq j \leq n$
. But this means that
$\mathfrak {M}$
is a counter-example to the premise
. □
Theorem 9. If
$\vdash _{\mathrm {RB}} H$
, then there is no symmetric counter-example to H.
Proof. We show that the Sym rule is sound for symmetric frames.
Let
$\mathfrak {M}, w_1, \ldots , w_n$
be a symmetric counter-example to the conclusion, i.e.,
$w_n, \ldots , w_1$
is a branch of worlds such that
$w_{i+1} R w_{i}$
and
$\mathfrak {M}$
is a countermodel to
at
$w_i$
for
$1 \leq i \leq n$
. Since the frame is symmetric, it follows that
$w_{i} R w_{i+1}$
. So
$w_1, \ldots , w_n$
also forms a branch of worlds such that
$\mathfrak {M}$
is a countermodel to each
at
$w_i$
for all
$1 \leq i \leq n$
, i.e.,
$\mathfrak {M}$
is a counter-example to the premise. □
Theorem 10. If
$\vdash _{\mathrm {RD}} H$
, then there is no serial counter-example to H.
Proof. We show that the Drop rule is sound for serial frames.
Let
$\mathfrak {M}, w_1, \ldots , w_n$
be a serial counter-example to the conclusion. This means that there is a branch of worlds
$w_1, \ldots , w_n$
such that
$w_i R w_{i+1}$
and
$\mathfrak {M}$
is a countermodel to each
at
$w_i$
for all
$1 \leq i \leq n$
. Since the frame is serial, there is some world v such that
$w_{n} R v$
.
$\mathfrak {M}$
is a countermodel to the empty sequent at v. It follows that
$\mathfrak {M}$
,
$w_1$
, …,
$w_n$
, v is a counter-example to the premise. □
Theorem 11. If
$\vdash _{\mathrm {R4}} H$
, then there is no transitive counter-example to H.
Proof. It suffices to show that the EW rule is sound for transitive frames.
Let
$\mathfrak {M}, w_1, \ldots , w_n$
be a transitive counter-example to the conclusion, where
So there is a branch of worlds
$w_1, \ldots , w_i, v, w_{i+1}, \ldots , w_n$
such that
$w_k R w_{k+1}$
for all
$1 \leq k \leq n$
,
$w_{i} R v$
,
$v R w_{i+1}$
and
$\mathfrak {M}$
is a countermodel to each
at
$w_k$
for all
$1 \leq k \leq n$
. Since
$v R w_{i+1}$
,
$w_i R v$
, and the frame is transitive, it follows that
$w_i R w_{i+1}$
. So
$w_1, \ldots , w_i, w_{i+1}, \ldots , w_n$
is also a branch of worlds and
$\mathfrak {M}$
is a countermodel to each
at
$w_k$
for all
$1 \leq k \leq n$
. But this means that
$\mathfrak {M}$
is also a counter-example to the premise.
If either
$i=0$
(that is,
is empty) or
$i=n$
(
is empty), then this is an application of EWL or EWR, respectively, which we have shown are sound. □
Theorem 12. If
$\vdash _{\mathrm {RS5}} H$
, then there is no reflexive, transitive and symmetric counter-example to H.
Proof. We have already shown that EC is sound for all reflexive frames, and EW for all transitive frames. We now show that the EE rule is sound for transitive, symmetric frames. Together this means that there cannot be a reflexive, symmetric, and transitive countermodel to H.
Suppose that
$\beta $
is an application of the EE rule.
Suppose again that
and that the conclusion has a counterexample, i.e., there is a symmetric, transitive model
$\mathfrak {M}, w_1, \ldots , w_n$
and a branch of worlds
$w_1, \ldots , w_{i-1}, w_{i+1}, w_i, w_{i+2}, \ldots , w_n$
such that
$\mathfrak {M}$
is a countermodel to
at
$w_k$
for all
$1 \leq k \leq n$
. We know that
$w_{i-1}Rw_{i+1}$
,
$w_{i+1} R w_{i}$
and
$w_{i} R w_{i+2}$
. Since the frame is transitive,
$w_{i-1} R w_{i}$
and
$w_{i+1} R w_{i+2}$
. Since the frame is also symmetric,
$w_{i} R w_{i+1}$
. It follows that
$w_1$
, …,
$w_{i-1}$
,
$w_i$
,
$w_{i+1}$
,
$w_{i+2}$
, …,
$w_n$
is a branch of worlds in
$\mathfrak {M}$
. Since
at
$w_k$
for
$1 \leq k \leq n$
, there is a counter-example to the premise. If G or H is empty, the argument is similar. □
3 Cut-free completeness for RK
To prove cut-free completeness, we show that for every unprovable hypersequent H, there is a counter-example. The counter-example is obtained by constructing a tree
$T \subseteq \mathbb {N}^*$
ordered by a relation R and assigning labeled hypersequents to elements
$\sigma \in T$
such that (a) each hypersequent is unprovable, (b) it is maximal in this respect (“fully reduced”), (c) component sequents labeled by
$\sigma $
of any two hypersequents assigned to elements of T are identical. We define a model using T, R, and V where
$\sigma \in V(p)$
iff p occurs on the left-hand side (lhs) of any (and thus, by (c), all) component sequents labeled
$\sigma $
). We then show that this model falsifies every component
at
$\sigma $
. This relies on the fact that each hypersequent is fully reduced and on how hypersequents were assigned to successors of
$\sigma $
.
Definition 13. Let
$\mathbb {N}^*$
be the set of finite sequences of natural numbers. If
$\sigma \in \mathbb {N}^*$
, then
$\sigma .n$
is the sequence
$\sigma $
extended by
$n \in \mathbb {N}$
.
A subset T of
$\mathbb {N}^*$
is a tree iff whenever
$\sigma .n \in T$
then
$\sigma \in T$
. We consider four relations on
$\mathbb {N}^*$
and T:
-
1. The successor relation
$R^1$
:
$\sigma R^1 \sigma '$
iff
$\sigma ' = \sigma .n$
. -
2. The reflexive closure
$R^=$
of R. -
3. The transitive closure
$R^+$
of R. -
4. The reflexive transitive closure
$R^*$
of R.
Obviously
$R^=$
is reflexive,
$R^+$
is transitive, and
$R^*$
is reflexive and transitive, both on
$\mathbb {N}^*$
and any tree T.
Definition 14. A sequence
$\Sigma = \sigma _1$
, …,
$\sigma _n$
is an R-branch iff
$\sigma _i R \sigma _{i+1}$
for
$1 \le i < n$
.
$\Sigma $
is an R-path through T if it is an R-branch of T and for all
$\sigma \in T$
, not
$\sigma R^1 \sigma _1$
and not
$\sigma _n R^1 \sigma $
(i.e., R-paths are R-branches that are maximal with respect to
$R^1$
, although they need not be maximal in the order R).
Definition 15. An R-labeled hypersequent is a sequence
where
$\sigma _1$
, …,
$\sigma _n$
is an R-branch.
If H is an R-labeled hypersequent, then
$H(\sigma )$
is the rightmost component sequent
of H or the empty sequent if H has no such component sequent.
$\Sigma (H)$
is the sequence of labels
$\sigma _1,\dots ,\sigma _n$
of the component sequents of H.
We write
$\Gamma (H,\sigma )$
and
$\Delta (H,\sigma )$
for the left-hand side and right-hand side of
$H(\sigma )$
, i.e., the sets of formulas such that
$H(\sigma )$
is
We say a sequent
extends a sequent
iff
$\Gamma \subseteq \Gamma '$
and
$\Delta \subseteq \Delta '$
. If H and
$H'$
are labeled hypersequents, we say
$H'$
extends H iff for all
$\sigma $
occurring as labels in H,
$H'(\sigma )$
extends
$H(\sigma )$
.
Our construction will produce a tree of labels
$\sigma $
and unprovable
$R^1$
-labeled hypersequents. From this tree we will extract a counter-example. We will ensure that new hypersequents added to the tree are always extensions of original ones. In the next section, we will extend the construction to RT, in which case we deal with
$R^+$
-labeled hypersequents which may contain more than one component sequent with the same label
$\sigma $
. However, the construction will guarantee that if a hypersequent contains two component sequents
and
with the same label
$\sigma $
, the component further to the right extends the component to the left in H, by defining reducts (in the following definition) always on the basis of the rightmost component labeled by
$\sigma $
. The definition of the model, specifically, the valuation at
$\sigma $
, then also need only take into account the rightmost component
$H(\sigma )$
. For the remainder of this section, however, we will deal with
$R^1$
-labeled hypersequents only.
Definition 16. Given an R-labeled hypersequent H and a label
$\sigma $
, we define a
$\sigma $
-reduct (corresponding to a rule) of H as the corresponding hypersequent on the right in Table 4.
Reducts of labeled hypersequents
In each case, the displayed component sequent labeled by
$\sigma $
is the rightmost such in H, if there is more than one.
A hypersequent is called
$\sigma $
-reduced if it is identical to all of its
$\sigma $
-reducts, otherwise it is
$\sigma $
-reducible. If it is
$\sigma $
-reduced for all
$\sigma $
occurring in it as labels, it is called fully reduced.
Proposition 17. If H is unprovable, any
$\sigma $
-reduct of it is also unprovable.
Proof. If the
$\sigma $
-reduct of H were provable, the relevant rule would prove H. For instance, suppose
is unprovable. Then one of
must be unprovable. For suppose both were provable. Then we’d have:
Or, suppose the
$\sigma $
-reduct based on the
$\Box $
L-rule were provable. Then we’d have:
□
Proposition 18. Every unprovable labeled hypersequent H is extended by an unprovable, fully reduced hypersequent
$\mathrm {Red}(H)$
(called its full reduction).
Proof. If H is already fully reduced, we have nothing to prove. Otherwise, there is a least
$\sigma $
(in the prefix order
$R^*$
) so that H is not
$\sigma $
-reduced. Any
$\sigma $
-reduction of a reducible hypersequent extends it. So, starting with the set
$\{H\}$
and adding
$\sigma $
-reductions results in a set of unprovable hypersequents, partially ordered by extension. This set is finite, as can easily be seen by induction on the number and degree of formulas in
$H(\sigma )$
and the number of formulas of the form
$\Box \phi $
in
$H(\sigma ')$
. A maximal element in this order is an unprovable
$\sigma $
-reduced hypersequent extending H. The proposition follows by induction on the number of components of H. □
Proposition 19. Let H be
$\mathrm {Red}(H')$
for some unprovable sequent
$H'$
, and let
$H(\sigma )$
be
.
-
1. If
$\lnot \phi \in \Gamma $
, then
$\phi \in \Delta $
. -
2. If
$\lnot \phi \in \Delta $
, then
$\phi \in \Gamma $
. -
3. If
$\phi \land \psi \in \Gamma $
, then
$\phi \in \Gamma $
and
$\psi \in \Gamma $
. -
4. If
$\phi \land \psi \in \Delta $
, then
$\phi \in \Delta $
or
$\psi \in \Delta $
. -
5. If
$\Box \phi \in \Gamma $
,
$\sigma R^1 \tau $
, and
$\tau $
occurs in H, then
$\phi \in \Gamma (H,\tau )$
.
Proof. Since H is
$\sigma $
-reduced,
$H(\sigma )$
is identical to all its
$\sigma $
-reducts. Inspection of the definition of reducts (Table 4) establishes (1)-(4).
For (5), suppose that
$\Box \phi \in \Gamma $
,
$\sigma R^1 \tau $
and
$\tau $
occurs as a label in H. Since H is
$\sigma $
-reduced, H is identical to its
$\Box $
L
$\sigma $
-reducts. Since
$\Sigma (H)$
is an
$R^1$
-branch, the component
$H(\tau )$
occurs immediately to the right of
$H(\sigma )$
, i.e.,
$\Gamma (H,\tau ) \ni \phi $
. □
Definition 20. Suppose
is an unprovable fully reduced hypersequent, and
$\Box \psi \in \Delta $
. The
$\sigma .n$
-
${\kern-0.3pt}\psi $
-successor
$\mathrm {Succ}_{\sigma .n}^\psi (H)$
of H is the hypersequent
.
We record some facts about the successor construction.
-
1. The
$\sigma .n$
-
${\kern-0.3pt}\psi $
-successor of an unprovable fully reduced hypersequent is unprovable. -
2. If
$H^*$
is a
$\sigma .n$
-
${\kern-0.3pt}\psi $
-successor of H and
$\tau R^* \sigma $
, then
$H(\tau ) = H^*(\tau )$
(i.e., passing to successors does not change the sequent labeled
$\sigma $
or any to the left of it).
Proof. Suppose H is a fully reduced hypersequent of the form
-
1. If
$H'$
were provable, then H would be provable:
$\mathrm {Succ}_{\sigma .n}^\psi (H)$
is
$\mathrm {Red}(H')$
, which is unprovable if
$H'$
is by Proposition 18. -
2. Since H is fully reduced,
is the only reducible sequent in
$H'$
. So, for every
$\tau $
in
$\Sigma (H')$
other than
$\sigma .n$
, every
$\tau $
-reduct of
$H'$
is identical to
$H'$
. Moreover, in constructing
$\tau $
-reducts, no formulas are added to component sequents to the left of
$H'(\tau )$
. In particular, reduction of
$H'(\sigma .n)$
does not affect
$H'(\sigma )$
, throughout the construction of
$\mathrm {Red}(H')$
given in the proof of Proposition 18. Hence, for all
$\tau $
with
$\tau R^* \sigma $
,
$H(\tau ) = \mathrm {Red}(H')(\tau ) = H^*(\tau )$
. □
Definition 22. Let H be an unprovable hypersequent
Let
$H'$
be the full reduction of
with
$\sigma _i = 0\dots 0$
with
$i\ 0$
’s, and let
(
$i \le n$
).
We define a partial mapping
$\lambda $
from
$\mathbb {N}^*$
to labeled hypersequents inductively. Assuming
$\lambda (\sigma )$
is already defined, let
be
$\lambda (\sigma )(\sigma )$
, i.e., the (rightmost)
$\sigma $
-labeled component of the hypersequent
$\lambda (\sigma )$
, and let
$\psi _1$
, …,
$\psi _l$
be all the formulas
$\psi _k$
such that
$\Box \psi _k \in \Delta $
.
$$ \begin{align*} \lambda(0) & = H_1' \\ \lambda(\sigma.k) & = \begin{cases} H_{i+1}' &\quad \textrm{if}\ k=0, i < n,\ \textrm{and}\ \sigma=\sigma_{i}\\[2.5pt] \mathrm{Succ}_{\sigma.k}^{\psi_k}(\lambda(\sigma)) & \quad\textrm{if}\ k>0, \lambda(\sigma)\ \textrm{is}\ \textrm{defined,}\ \textrm{and}\ \psi_k\ \textrm{exists}\\[2.5pt] \textrm{undefined} & \quad\textrm{otherwise.} \end{cases} \end{align*} $$
Let T be the set of all
$\sigma \in \mathbb {N}^*$
such that
$\lambda (\sigma )$
is defined and let
$S(H) = \{\lambda (\sigma ) : \sigma \in T\}$
be all labeled hypersequents in the range of
$\lambda $
.
Proposition 23. We record some facts about T,
$\lambda $
, and
$S(H)$
:
-
1. T is a tree.
-
2. If
$G \in S(H)$
, G is unprovable and fully reduced. -
3. If
$G = \lambda (\sigma )$
,
$\tau $
occurs in G iff
$\tau R^*\sigma $
. -
4. If
$G = \lambda (\sigma )$
,
$G' = \lambda (\tau )$
, and
$\sigma R^* \tau $
, then
$G(\sigma ) = G'(\sigma )$
. -
5. If G,
$G' \in S(H)$
and
$\sigma $
occurs in both,
$G(\sigma ) = G'(\sigma )$
. -
6. If
and
$\Box \psi \in \Delta $
, there is a k such that
$\sigma .k \in T$
such that
and
$\psi \in \Delta '$
.
-
1. By construction, if
$\lambda (\sigma )$
is undefined,
$\lambda (\sigma .n)$
is undefined. Hence, if
$\sigma \in T$
has the property that
$\tau \in T$
for all
$\tau R^+ \sigma $
, so does
$\sigma .n \in T$
. -
2. Each
$\lambda (\sigma _i)$
, i.e.,
$H^{\prime }_i$
for
$i = 1$
, …, n, is fully reduced and unprovable (If
$H^{\prime }_i$
is provable, so is
, by EWR.) By induction on
$\sigma $
, and Propositions 18 and 21(1), each
$\lambda (\sigma .k)$
(
$\sigma .k \in T$
and
$k>0$
) is unprovable (and fully reduced by construction). -
3. By induction on
$\sigma \in T$
. There is no
$\tau $
such that
$\tau R^1 0$
. The property holds for
$\sigma _i$
by definition of
$\lambda (\sigma _i)$
. It holds for
$\sigma .k$
(
$k \ge 1$
) by the definition of
$\lambda (\sigma .k)$
and Proposition 21(2). -
4. By induction on
$\sigma \in T$
: The definition of
$H'$
ensures the property holds for
$\lambda (\sigma _i)$
, and the definition of
$\mathrm {Succ}_{\sigma .k}^\psi $
ensures that if it holds for
$\lambda (\sigma )$
it also does for
$\lambda (\sigma .k)$
(
$k \ge 1$
). -
5. Let
$\tau $
,
$\tau '$
be such that
$\lambda (\tau ) = G$
and
$\lambda (\tau ') = G'$
. If
$\sigma $
occurs in both G and
$G'$
, by (3),
$\sigma R^* \tau $
and
$\sigma R^* \tau '$
. Let
$G'' = \lambda (\sigma )$
. Then by (4),
$G''(\sigma ) = G(\sigma )$
and
$G''(\sigma ) = G'(\sigma )$
, and so
$G(\sigma ) = G'(\sigma )$
. -
6.
$H''$
is a
$\sigma .k$
-
${\kern-0.3pt}\psi $
-successor of
$H'$
. □
Since
for any two G,
$G' \in S(H)$
which both contain
$\sigma $
, we can define
$\Gamma (\sigma ) = \Gamma $
and
$\Delta (\sigma ) = \Delta $
independently of the individual hypersequents in
$S(H)$
.
Given an unprovable hypersequent H, let T and
$S(H)$
be as in Definition 22 and let
$\mathfrak {M} = \langle T, R^1, V\rangle $
with
$\sigma \in V(p)$
iff
$p \in \Gamma (\sigma )$
.
Proposition 24. For all
$\phi $
, if
$\phi \in \Gamma (\sigma )$
then
$\mathfrak {M}, \sigma \models \phi $
and if
$\phi \in \Delta (\sigma )$
, then
.
Proof. By induction on
$\phi $
.
If
$p \in \Gamma (\sigma )$
, then
$\sigma \in V(p)$
by definition, so
$\mathfrak {M}, \sigma \models p$
.
If
$p \in \Delta (\sigma )$
, then
$p \notin \Gamma (\sigma )$
(otherwise
and any hypersequent containing it would be provable). So
$\sigma \notin V(p)$
.
If
$\lnot \phi \in \Gamma (\sigma )$
, by Proposition 19(1),
$\phi \in \Delta (\sigma )$
. By induction hypothesis,
, so
$\mathfrak {M}, \sigma \models \lnot \phi $
. Similarly for
$\lnot \phi \in \Delta (\sigma )$
, using Proposition 19(2).
If
$\phi \land \psi \in \Gamma (\sigma )$
, by Proposition 19(3),
$\phi \in \Gamma (\sigma )$
and
$\psi \in \Gamma (\sigma )$
. By induction hypothesis,
$\mathfrak {M}, \sigma \models \phi $
and
$\mathfrak {M}, \sigma \models \psi $
, so
$\mathfrak {M}, \sigma \models \phi \land \psi $
.
If
$\phi \land \psi \in \Delta (\sigma )$
, by Proposition 19(4),
$\phi \in \Delta (\sigma )$
or
$\psi \in \Delta (\sigma )$
. By induction hypothesis,
or
, so
.
Suppose
$\Box \phi \in \Gamma (\sigma )$
and let
$\sigma R^1 \tau $
. By Proposition 23(3) and Proposition 19(5),
$\phi \in \Gamma (\tau )$
. By induction hypothesis,
$\mathfrak {M}, \tau \models \phi $
. Thus,
$\mathfrak {M}, \sigma \models \Box \phi $
.
Suppose
$\Box \phi \in \Delta (\sigma )$
. By Proposition 23(6), there is a
$\tau $
such that
$\sigma R^1 \tau $
(namely,
$\tau = \sigma .k$
for some k) and
$\phi \in \Delta (\tau )$
. By induction hypothesis,
, hence
. □
Corollary 25. The calculus RK is complete for K.
Example 26. Consider the hypersequent
. The counter-example construction begins by labeling the components using the branch
$0$
,
$0.0$
:
It is
$0$
-reduced, but not
$0.0$
-reduced. A
$0.0$
-reduct, using the
$\Box $
L rule, is:
In turn, we can apply a
$\lnot $
L-reduction to the sequent labeled
$0.0$
to obtain
Finally, we apply a
$\land $
R-reduction to obtain
Since
$\Box \lnot q \in \Delta (0)$
, there is a
$0.1$
-
$\lnot q$
-successor, namely
We now have
$T = \{0, 0.0, 0.1\}$
with
The corresponding counter-example is
4 Cut-free completeness of RT and RD
The completeness proof above can be extended to RT. First we extend Definition 16 to include the following:
where the sequent
is the rightmost sequent labeled
$\sigma $
in H and
$\phi \notin \Gamma $
.
Then Proposition 17 still holds, i.e., if H is unprovable, so are its
$\sigma $
-reducts.
Proposition 18 also still holds for the extended definition of “fully reduced” now including reducts for rule EC. A
$\sigma $
-reduct
$H'$
of a hypersequent H also extends it: Suppose
$\Box \phi , \Gamma $
is
$\Gamma (H, \sigma )$
, the left side of the rightmost sequent in H labeled
$\sigma $
. Then
$\Gamma (H',\sigma )$
, the left side of the rightmost sequent labeled
$\sigma $
in
$H'$
, is
$\phi , \Box \phi , \Gamma $
. Clearly, the number of times an EC reduction can be applied to the sequent labeled
$\sigma $
is bounded by the sum of the degrees of the formulas in H.
Proposition 19(5) now holds in the form: If H is
$\mathrm {Red}(H')$
for some hypersequent
$H'$
, and
, then
-
5
$'$
. If
$\Box \phi \in \Gamma $
,
$\sigma R^=\tau $
, and
$\tau $
occurs in H, then
$\phi \in \Gamma (H,\tau )$
.
If
$\sigma R^1 \tau $
, then we just have a case of Proposition 19(5). For the case
$\sigma =\tau $
, we have to show that if
$\Box \phi \in \Gamma $
, then
$\phi \in \Gamma $
. This holds since H is fully reduced, and
is a
$\sigma $
-reduct of
(for rule EC).
Definition 22 yields a tree of unprovable hypersequents
$S(H)$
for any unprovable hypersequent H also when EC-reductions are included in the definition of
$\mathrm {Red}$
. For the definition of the
$\lambda (\sigma .k)$
, note that
is the rightmost
$\sigma $
-labeled component of the hypersequent
$\lambda (\sigma )$
. Thus, successors are computed from the fully reduced hypersequent component.
Proposition 23 still holds since it is independent of the definition of reduction.
Completeness for reflexive models now follows: If H is unprovable,
$S(H)$
is a tree of fully reduced unprovable hypersequents. Define
$\mathfrak {M} = \langle T, R^=, V\rangle $
as before, with the difference that the accessibility relation is the reflexive closure
$R^=$
of R. Proposition 24 holds for
$S(H)$
and
$\mathfrak {M}$
, since the only relevant difference is the case
$\Box \phi \in \Gamma (\sigma )$
, which holds by Proposition 19(5
$'$
).
Example 27. Consider the hypersequent
. Again we begin by labeling the components using the branch
$0$
,
$0.0$
:
This hypersequent is not
$0$
-reduced. A
$0$
-reduct using the RT reduction is:
which further reduces to
This is now
$0$
-reduced. The full reduct, as before, is:
There again is a
$0.1$
-
$\lnot q$
-successor, namely
Its full reduction is
The corresponding counter-example is
To prove completeness of RD for serial models, we have to ensure that the accessibility relation on T is serial. To do this, we extend Definition 20: Suppose
is an unprovable fully reduced hypersequent, and
$\Delta $
contains no formula of the form
$\Box \psi $
(i.e., it has no
$\sigma .n$
-
${\kern-0.3pt}\psi $
-successor, where
$\sigma $
is the label of the rightmost sequent in H). The
$\sigma .n$
-successor
$\mathrm {Succ}_{\sigma .n}(H)$
of H is the hypersequent
.
Proposition 21 also holds for
$\sigma .n$
-successors, by the Drop rule. Definition 22 is extended by including the
$\sigma .n$
-successor of H if there is no
$\sigma .n$
-
${\kern-0.3pt}\psi $
-successor. Proposition 19(5) still holds since the
$\sigma .n$
-successor is fully reduced as in the case for K. Propositions 23 and 24 still hold. The relation R on T in this case is serial, since for every
$\sigma $
that occurs as a label on a sequent either
$\sigma .0$
also occurs as a label in the original labeled hypersequent
$H'$
, or there is a
$\sigma .n$
-
${\kern-0.3pt}\psi $
-successor, or
$\sigma $
is the label of the rightmost sequent without a formula of the form
$\Box \psi $
in the succedent, in which case there is a
$\sigma .n$
-successor.
This method of adding successors results in an infinite tree, but we can do a bit better: only add a
$\sigma .n$
-successor if
$\Box \phi \in \Gamma (\sigma )$
, and add
$\langle \sigma ,\sigma \rangle $
to the accessibility relation. For instance, suppose we start with
. This is completely reduced, and has a
$0.1$
-p successor which reduces to
There is no
$\Box \psi \in \Delta (0.1)$
, so a
$0.1.1$
-successor is
which reduces to
The serial counter-example is
5 Failure of the method for B and 4
The constructions of the K, T, and D counter-examples to RK, RT, and RD-unprovable hypersequents work because once a sequent with label
$\sigma $
is reduced, it remains unchanged in the reduction of successors. This guarantees that in the entire tree of hypersequents, all (rightmost, in the case of RT) components labeled
$\sigma $
are identical. This explains why the construction does not work for RB. The crucial lemma is Proposition 19(5): If
$\Box \phi \in \Gamma (\sigma )$
,
$\sigma R\sigma'$
, and
$\sigma '$
occurs in
$H'$
, then
$\phi \in \Gamma (\sigma ')$
. Suppose we tried to define the counter-example M with the symmetric closure of R as its accessibility relation. Then we would have to change the definition of reduction so as to not only add
$\phi $
to the antecedent of
$H(\sigma ')$
if
$\Box \phi \in \Gamma (\sigma )$
(with
$\sigma R\sigma'$
) but also vice versa. Then Proposition 23(4) would no longer hold. Hence the prospects of extending the method of proving cut-free completeness to RB are dim.
Recently, a cut-free complete linear nested sequent system for B has been developed by Goré & Lellmann (Reference Goré, Lellmann, Cerrito and Popescu2019), though it requires the introduction of a new modal rule and so does not obey Došen’s principle. A cut-free tree hypersequent system for symmetric logics has also been developed by Poggiolesi (Reference Poggiolesi2011). The structure of tree hypersequents provides more structural flexibility, and is thus capable of accommodating symmetric frame properties. However, again we see Došen’s principle violated.
More surprisingly, constructing transitive counter-examples for R4-unprovable hypersequents also causes difficulties. Here the problem is different and resides in the “destructive” nature of the unrestricted EW rule. Suppose we were going to define a transitive counter-example
$\mathfrak {M}$
using the transitive closure of
$R^1$
. Then the definition of reduction would have to take into account not just immediate predecessors of
$\sigma $
(as the
$\Box $
L reduction does), but any predecessor of
$\sigma $
, i.e., we would define
to be a 4-reduct of
However, if
$G''$
is not empty, the unprovability of a hypersequent does not guarantee the unprovability of its 4-reduct. The best we can do is guarantee the unprovability of
using the EW and
$\Box $
L rules. But now the new reduct is no longer an extension of the original hypersequent, and so Proposition 18 fails. The problem, in short, is that EW destroys information that is required in the subsequent reduction of a hypersequent and of its successor hypersequents.
The problem can be circumvented by using rules other than EW to deal with transitivity. One could strengthen the
$\Box $
L to the rule
or add a transitivity rule like
In both cases, the unprovability of a hypersequent would guarantee the unprovability of its reducts which would furthermore be extensions of them. However, the resulting calculi no longer satisfy Došen’s Principle, since the new rules are not purely (external) structural rules. It remains an open question whether or not a cut-free complete hypersequent system for B or S4 which obeys Došen’s principle can be developed. In fact, it is open if RB, R4, and RS4 are cut-free complete.Footnote 3
6 Conclusion
In this paper we have studied the hypersequent systems of Parisi (Reference Parisi2017, Reference Parisi2020), which extend the hypersequent system for S5 due to Restall (Reference Restall2009) to other modal logics. Though these systems require only two modal rules for K and its extensions, there are some issues that arise with this approach to modal hypersequents. In particular, our method for showing cut-free completeness fails for the systems RB and RS4. All known cut-free complete hypersequent calculi for RB and RS4 add additional rules that manipulate modal formulas, and so violate Došen’s principle. We have also noted that the system RS5 is not entirely modular. While it has been shown to be cut-free complete, in order to obtain modularity by replacing EE with Sym, we lose the cut-free completeness result.
Cut-free proofs in RB and R4 of B and 4
Acknowledgments
The authors would like to thank the reviewers for this paper for their helpful comments. The results of in this paper are based on Burns (Reference Burns2018) and were presented at the Society for Exact Philosophy and the Melbourne Logic Group. We would like to thank the audiences for their helpful comments and criticisms. A special thanks to Andrew Parisi, who presented us with an early version of his foundational work on this topic and gave us the opportunity to expand upon it.
