Two Is Enough – Bisequent Calculus for S5

Abstract

We present a generalised sequent calculus based on the use of pairs of ordinary sequents called bisequents. It may be treated as the weakest kind of system in the rich family of systems operating on items being some collections of ordinary sequents. This family covers hypersequent and nested sequent calculi introduced for several non-classical logics. It seems that for many such logics, including some many-valued and modal ones, a reasonably modest generalization of standard sequents is sufficient. In this paper we provide a proof theoretic examination of S5 in the framework of bisequent calculus. Two versions of cut-free calculus are provided. The first version is more flexible for proof search but admits only indirect proof of cut elimination. The second version is syntactically more constrained but admits constructive proof of cut elimination. This result is extended to several versions of first-order S5.

The results reported in this paper are supported by the National Science Centre, Poland (grant number: DEC-2017/25/B/HS1/01268).

1 Introduction

During the last five decades researchers trying to apply sequent calculi (SC) to several non-classical logics faced many serious problems. In order to overcome the difficulties they provided a lot of ingenious solutions, mainly based on the changes in the notion of basic items on which rules are defined. Sometimes the machinery involved in the construction of such generalised forms of SC is quite complicated and in special cases may be reduced. The aim of this paper is to provide the simplest cut-free generalised SC which has strictly syntactical character, i.e. no labels or other external devices are required. Of course the assumption that there is a clear-cut distinction between purely syntactic and semantic-based calculi may be questioned. After all, there are results showing that some of the approaches may be seen as notational variants simply¹ and, on the other hand, a labelled SC of Negri [36] admits purely syntactical methods of proving admissibility of cut and other structural rules. Also the notion of simplicity is rather vague; in Introduction to [24] different, sometimes opposing, criteria are discussed. Below we will try to explain in what sense the proposed solution may be seen as the simplest, at least in one, but quite rich and important group of generalised SC of similar character.

Let us propose a name many-sequent calculi for the class of systems which is under inspection here. This class covers a variety of systems using collections of sequents as the basic items – in particular, two families of calculi operating on hyper- or nested sequents. Moreover, many other approaches, e.g. using structured notion of a sequent (e.g. Sato [41]) or multiple kinds of sequents (e.g. Indrzejczak [21]) may be reduced to this group by suitable translation.

Let us recall that hypersequents are structures of the form $\varGamma _1 \Rightarrow \varDelta _1 \mid ... \mid \varGamma _i \Rightarrow \varDelta _i$ which are usually conceived as sets or multisets of their components². It is commonly believed that hypersequent calculus (HC) was originally introduced by Pottinger [39]. However, this information should be revised since a similar idea was earlier introduced by Mints in [32] and [33] to formalize S5. Unfortunately, these papers were written in Russian and unknown to wider community. Even much later, when English translation of [33] was presented in Mints [34] he did not care to underline his priority in this respect. But it was Avron [1] who not only independently introduced such kind of SC but developed its theory, first for relevant, then for many other non-classical logics (see e.g. [2]). Since then, HC was applied widely in many fields (see e.g. [12] or [31]).

Nested sequents are more complicated structures where, in addition to formulae, the elements of a sequent may be other sequents, containing other sequents. This approach in general form was initiated by Dos̆en [14] where one is dealing with a hierarchy of sequents of order $n+1$ with arguments being finite sets of sequents of order n. In particular, sequents of order 2 consist of finite sets of ordinary sequents (of order 1) on both sides, where elements of the antecedent are treated conjunctively, and elements of the succedent disjunctively. Independently of Dos̆en’s general frame (not well known either) similar ideas were extensively applied, under different names (deep inference calculi, tree-hypersequent calculi), in the field of modal and temporal logics (e.g. Bull [11], Kashima [27], Stouppa [43], Brünnler [10], Poggiolesi [38]).

In fact, HC may be seen as a special, simplified case of Došen’s general framework. In this perspective hypersequents are just sequents of order 2 with empty antecedents. This shows a deep relationship between these approaches. In particular, if hypersequents are defined not as sets or multisets of sequents, but rather as their sequences, then HC may be interpreted as a restricted version of nested sequent calculi, called by Lellmann [30] linear nested SC and by Indrzejczak [26] non-commutative HC.

In particular, if we use just structures which consist of two sequents only, we obtain a limiting case of either HC or nested SC which we call bisequent calculi (BSC). Hence our proposal may be seen as providing the simplest and most restrictive form of all aforementioned systems captured by the general frame of Dos̆en in the sense of simplicity of the basic syntactic structures. Is such restricted calculus of any use? HC already may be seen as quite restrictive form of generalised SC, yet it was shown to be useful in many fields. BSC is even more restrictive but preliminary work on its application is promising. For example, one may apply bisequents successfully to a variety of three- and four-valued logics which may be characterised in terms of Hähnle [19] approach with labels as sets of values (work in progress). In this paper we focus on construction of BSC for modal logic S5. It is an open question if this approach may be extended to other modal logics containing axiom 5 or B. But in case of S5 we obtain an elegant solution which is simple also in the sense of simple modal rules allowing for easy proof search and establishing decidability (in propositional case).

S5 is chosen not only because of its philosophical importance. It is important also for proof theory since it had a remarkable impact on the development of different generalised SC. This well-known and important modal logic was very early recognized as a troublesome case for construction of well-behaving SC (Matsumoto and Ohnishi [37]). It was in the strong contrast with nice semantic, algebraic and many other features of S5. Although it is possible to devise a standard cut-free SC it requires global restrictions on the application of modal rules which make it rather complicated in practical proof search (see e.g. Serebriannikov [42] or Braüner [9]). Several proposals for solving the problem were connected not only with aforementied kinds of generalised SC but also with other approaches based on the application of structured sequents (Sato [41]) or variety of sequents (Indrzejczak [21]) or labels (Fitting [15]), to mention just a few proposed solutions. In nested SC there are systems of Stouppa [43], Brünnler [10] and Poggiolesi [38]. In case of HC the number of different formalizations of S5 is particularly impressive: Mints [32], Pottinger [39], Avron [2], Restall [40], Poggiolesi [38], Lahav [29], Kurokawa [28], Bednarska and Indrzejczak [7].

When we compare different generalised SC for S5 we can observe that although in standard SC this logic is troublesome, in other approaches it often needs the minimum of what is at hand. For example, in labelled approach formalization of S5 requires the most simple solution – labels being natural numbers; no necessity for structured prefixes (Fitting [15]) or relational formulae (Negri [36]). Similarly in the approach based on the use of variety of different sequents (Indrzejczak [22]), S5 requires only two different ones. In what follows we want to show that also in many-sequent approach the overall machinery may be significantly reduced to very simple BSC. One may look at this attempt as a kind of the application of the principle of Ockham’s Razor to generalised SC of some sort. It may also be compared with the principle of shallow formalization proposed by Quine. HC in itself may be seen already as a quite simple form of many-sequent calculi, but sometimes we can go further.

In Sect. 2 we describe the basic propositional system called BSC1 and compare it with some approaches represented in HC. In Sect. 3 we will show that its cut-free version is complete. It is shown indirectly by translation from cut-free proofs in double sequent calculus DSC for S5 which is briefly characterised first. In Sect. 4 we introduce restricted form of BSC1 called BSC2. Although it is less flexible in practical applications we can prove a constructive cut elimination theorem for it. Usually different approaches are restricted to propositional level only, here the last section discusses extensions of BSC to quantified versions with identity. Three variants of modal first-order logics are discussed, one based on classical logic and two on free logic. Surprisingly enough, the first one although unproblematic in the setting of BSC1, cannot be accomodated in BSC2 without addition of axiomatic sequents which destroy full cut elimination. On the other hand, for two variants based on free logic we can still obtain cut elimination theorem in nonrestricted version.

2 The System

We will use standard monomodal language with ordinary boolean connectives and two modal operators of necessity $\Box$ and possibility $\diamondsuit$. Let us recall that one can axiomatize propositional S5 by adding to Hilbert system for classical propositional logic CPL the following schemata of axioms:

• K $\Box (\varphi \rightarrow \psi )\rightarrow (\Box \varphi \rightarrow \Box \psi )$

• T $\Box \varphi \rightarrow \varphi$

• 4 $\Box \varphi \rightarrow \Box \Box \varphi$

• 5 $\lnot \Box \varphi \rightarrow \Box \lnot \Box \varphi$ or $\diamondsuit \varphi \rightarrow \Box \diamondsuit \varphi$

• Pos $\diamondsuit \varphi \leftrightarrow \lnot \Box \lnot \varphi$

Instead of 5 one can use B ($\lnot \varphi \rightarrow \Box \lnot \Box \varphi$ or $\varphi \rightarrow \Box \diamondsuit \varphi$) and dispense with 4 since it is provable from 5 and T. The only primitive rules are modus ponens MP and Gödel’s rule GR. $\varGamma \vdash _{S5}\varphi$ denotes a provability of $\varphi$ from $\varGamma$ where applications of GR is restricted to theses only. Since only syntactic proofs will be presented below we do not recall semantic characterisation of S5.

The basic system which we call BSC1 is essentially a bisequent counterpart of Gentzen’s LK for CPL enriched with special modal rules. Bisequents in BSC1 are simply (unordered) pairs of sequents $\varGamma \Rightarrow \varDelta \mid \varPi \Rightarrow \varSigma$, where $\varGamma , \varDelta , \varPi , \varSigma$ are finite (possibly empty) multisets of formulae. In case when one component of a bisequent is empty (i.e. both arguments of $\Rightarrow$ are empty multisets) we can omit it and a bisequent with single nonempty sequent is just a standard sequent. Most of the rules have active formulae (i.e. side and principal formulae) in one sequent only and this sequent is called active, whereas the second is non-active (for this instance of rule application). For both components of a bisequent we have the same set of rules hence for simplicity in schemata of rules we will state active component always on the left but in the course of the proof respective inferences are allowed in both sequents. As axioms we count all bisequents of the form $\varphi \Rightarrow \varphi \mid S$, where S is any sequent, possibly empty. For classical basis we just take LK (but with all two-premiss rules in multiplicative form):

Note that although in case of logical two-premiss rules we keep the second, non-active component, the same in both premisses, for cut we admit different sequents which are mixed in the conclusion. It simplifies a constructive proof of cut elimination which will be stated in Sect. 4.

Now rules for modal operators:

As we can see all logical modal rules are symmetric, explicit and separate in the sense defined by Wansing [44]. Moreover, they allow for easy proofs of interdefinability of $\Box$ and $\diamondsuit$ hence they satisfy most of the desiderata stated for well behaved logical rules. Only $(\Rightarrow \Box )$ and $(\diamondsuit \Rightarrow )$ are not pure in the sense of Avron. Note also that all rules stated so far are static in the sense that there is no transition of any formula from one sequent to another. In addition to ordinary structural rules W and C we have eight transitional quasi-structural rules:

where M is either $\Box$ or $\diamondsuit$ uniformly in the premiss and the conclusion. These rules are called quasi-structural since no constant is introduced but it is anyway displayed in the schemata of rules.

A proof is defined in the standard way as a tree of bisequents. As an example we provide a proof of B:

One can easily prove other axioms of S5 whereas MP and GR are simulated by cut and $(\Rightarrow \Box )$. In the other direction we can use some translation functions which were developed in general form for nested and hypersequent calculi. Let $\wedge \varGamma , \vee \varGamma$ denote conjunctions and disjunctions of elements of $\varGamma$ and in case $\varGamma$ is empty they are interpreted as $\top$ and $\bot$ respectively. Consider the following translation for bisequents: $\mathfrak {I}(\varGamma \Rightarrow \varDelta \mid \varPi \Rightarrow \varSigma ) := (\wedge \varGamma \rightarrow \vee \varDelta )\vee \Box (\wedge \varPi \rightarrow \vee \varSigma )$. This is a (restricted) form of the translation applied to nested sequents. Alternatively, we may use a translation applied to hypersequents, i.e., $\mathfrak {I}(\varGamma \Rightarrow \varDelta \mid \varPi \Rightarrow \varSigma ) := \Box (\wedge \varGamma \rightarrow \vee \varDelta )\vee \Box (\wedge \varPi \rightarrow \vee \varSigma )$. The former is a bit simpler but has a disadvantage that in fact bisequents are treated here as ordered pairs whereas it was not required for BSC1 (although it will be required for BSC2). The fact that both can be used provides one more evidence that provided calculi may be seen as a limit case of both hypersequent and nested sequent calculi. We left to the reader the task of proving that all rules of BSC1 are admissible in S5 under any of these translations. Alternatively, one may demostrate validity-preservation of translation of rules thereby proving soundness. In consequence we have:

Theorem 1

$\varGamma \vdash _{S5}\varphi$ iff BSC1 $\vdash \varGamma \Rightarrow \varphi$

Before we go to more satisfactory solutions (i.e. cut-free) it is interesting to compare modal rules of BSC1 with several kind of hypersequent rules which were provided so far. Mints [32] is using HLK for CPL with addition of the following rules for $\Box$:

where G denotes a collection of sequents. Two of them, namely $(\Box \Rightarrow ^{T})$ and $(\Rightarrow \Box ^G)$ are just our rules for $\Box$. The remaining rules are transitional but logical, not quasi-structural like in our system. The only rule which is specific for S5 is $(\mathord {\Box \Rightarrow }^5)$. This set of rules is in fact redundant and later approaches, of Restall [40] and Poggiolesi [38], were more economical but also partly static, partly transitional on the side of logical modal rules. Approaches of Avron [2], Kurokawa [28] and Lahav [29] were based rather on special quasi-structural rules. One can find a comparison of all these systems in Bednarska and Indrzejczak [7]. Solutions provided for S5 in the framework of nested calculi are of similar character. What is important is the fact that all proposed rules may be easily simulated in BSC1, if we just take G in the schemata of rules to represent just one sequent, possibly empty. Moreover, the proposed solution seems to be more elegant since all logical rules are static and the only transitional ones are quasi-structural.

3 Cut-Free BSC1

What with cut elimination? Let us call BSC1 without cut BSC1$^-$. It is possible to prove completeness for such cut-free system semantically³ but to save space we will show it indirectly by translation from proofs in some other kind of generalised cut-free SC for S5 which is known to be complete. We finished the previous section with the claim that BSC1 can simulate modal rules from several cut-free hypersequent calculi. But devising a direct translation is harder since hypersequents may have more components than two. There are some other generalised SC where such translation is more straightforward; moreover it shows how bisequents can simulate other kind of systems in addition to hypersequent or nested sequent calculi.

One such possibility is connected with SC operating on structured sequents i.e., having additional components in the antecedent or succedent like in Blamey and Humberstone [8] or Heuerding, Seyfried and Zimmermann [20]. In particular, all rules of Sato [41] from cut-free system for S5 may be simulated in BSC1 under translation $\mathfrak {I}(\varGamma \ [\varSigma ]\Rightarrow [\varPi ] \ \varDelta ) := \varGamma \Rightarrow \varDelta \mid \varSigma \Rightarrow \varPi$. Another possibility is to refer to multisequent calculi in which only one sequent is used at a time but different kinds of sequents are generally applied in the system. In particular, a cut-free system for S5 uses only two kinds of sequents. It is called double SC (DSC) since in addition to ordinary sequents there are modal ones of the form $\varGamma \ \mathord {\Box }\mathord {\Rightarrow } \varDelta$. The latter appear only in proofs but what is proved are only standard sequents. If it is inessential whether standard or modal sequent is applied both kinds are denoted as $\varGamma \ (\Box )\!\!\Rightarrow \varDelta$. The idea of using special kind of sequents is due to Curry [13] and it was also used by Zeman [46]. In both cases additional sequent was introduced to express modal character of suitable operations. In fact, its introduction in Curry’s formulation of S4 is not necessary; in Zeman it is essential for obtaining a modal rule characterising S4.2. Two kinds of sequents were applied also in Avron, Honsell, Miculan and Paravano [3] but in totally different character. In their system two kinds of sequents correspond to two different deducibility relation – global and local one. Indrzejczak introduced a general construction where several types of modal [22] and temporal sequents [23] were applied in one SC but in case of S5 a considerable reduction is possible to the effect that only one type of modal sequent is required. Below we briefly describe this system; in addition to [21] one may find a fuller account and comparison with other approaches in Poggiolesi [38] and Wansing [45].

In addition to modal sequents, a language is enriched with a special structural operation of transition (from one argument of a sequent to another). It is unary like negation but cannot be iterated; it is allowed only to add it in front of a formula or to delete it. We will use a sign ‘−’ for it, so any formula $\varphi$ may be transformed into $-\varphi$. In the schemata we will use a convention $\varphi ^*$ in the sense that for ordinary formula $\varphi$, $\varphi ^*= -\varphi$ and $(-\varphi )^*= \varphi$. Also $\varGamma ^*= \{\varphi ^*: \varphi \in \varGamma \}$.

Most rules are standard and work the same way on both kinds of sequents. However in order to block uncontrolled transition from one side of a sequent to the other for negation and implication we have symmetric variants:

Clearly, $\varGamma$ and $\varDelta$ may contain ordinary formulae as well as formulae with −; the same remark applies to further rules. We need special rules for transition of the form:

and modal rules:

where $M\varDelta$ contains only formulae of the form $\Box \psi , -\Box \psi$ and in (NC) one of the $\varGamma , \varDelta$ is either empty or contains only such modal formulae. If we admit $\diamondsuit$ as a primitive operator, we have dual rules for it and the notion of modal formula is extended to include $\diamondsuit \psi , -\diamondsuit \psi$.

It is easy to prove soundness under syntactic translation where standard sequents are dealt with as Gentzen transforms with the addition that formulae preceded with − are translated as negations. Modal sequents are translated as $\wedge \varGamma \rightarrow \Box (\vee \varDelta )$ with the same proviso for formulae with −.

This system is cut-free and has generalised subformula property in the sense that the only formulae which must occur in any proof of $\varGamma \Rightarrow \varDelta$ are of the form $\varphi , -\varphi$ for every $\varphi \in SF(\varGamma \cup \varDelta )$. Completeness and decidability is proved by Hintikka-style argument in [21].

The obvious translation of modal sequents is: $\mathfrak {I}(\varGamma , -\varDelta \ \Box \!\!\Rightarrow -\varPi , \varSigma ) := \varGamma \Rightarrow \varDelta \mid \varPi \Rightarrow \varSigma$; ordinary sequents are treated as bisequents with one component empty.

Theorem 2

If $\vdash _{DSC}\varGamma \Rightarrow \varDelta$, then BSC1$^-$ $\vdash \mathfrak {I}(\varGamma \Rightarrow \varDelta )$.

Proof

It goes by induction on the height of a proof in DSC. We must provide stepwise simulation of all rules of DSC under the translation. For most of the rules it is obvious so we consider only the case of $(\Rightarrow \Box )$ and (NC). In case of the former by the induction hypothesis we have provable a bisequent in which one component has $\varphi$ in the succedent and the remaining formulae are modal. By transitional rules we move all modal formulae to the next component and then apply $(\Rightarrow \Box )$ (from BSC1) to $\varphi$. The application of $(\mid \Rightarrow TR)$ to $\Box \varphi$ completes the proof. For (NC) one of $\varGamma , \varDelta$ is modal or empty. In the first case a series of application of transitional rules leads to translation of the conclusion; in the second there is nothing to do.    $\square$

This theorem implies completeness of cut-free version of BSC1, that is of BSC1$^-$. It yields, by subformula property, decidability and also admissibility of cut by a simple argument. Since if both premisses of cut are provable, then by soundness they are valid. But cut is validity-preserving, hence the conclusion must be valid either and, by completeness, it is also provable. But we may do even better and prove this result constructively. However, not for a calculus in this shape. Consider the following application of cut:

If we now push cut up to reduce the height of a proof we obtain $\varLambda \Rightarrow \varTheta , \varphi \mid \varGamma , \varPi \Rightarrow \varDelta , \varSigma$ and in general there is no chance to apply $(\Rightarrow \Box )$ to this bisequent. Therefore, for the aim of constructive proof of cut elimination we must modify slightly a calculus to obtain its variant BSC2.

4 Modified System BSC2

First of all let us restrict the application of all static rules to left sequents only. So what in BSC1 was only a convention applied in the schemata of rules, now is a rigid requirement to the effect that in BSC2 bisequents are ordered pairs. Note that in consequence of this restriction the right sequent is either empty or modal and plays only auxiliary role, similarly like in the sequent calculus of Heuerding, Seyfried and Zimmermann [20] for S4; it serves for storing modal data. To simplify things we restrict language to $\Box$ only but the proof works also in the presence of $\diamondsuit$. We also introduce (Mix) instead of (Cut) to deal with C. It looks like this:

where $i, k > 0$ and all occurrences of $\varphi$ are displayed. It is obvious that a system with mix is equivalent to the system with cut by exactly the same argument as stated by Gentzen for LK.

However, to deal with transitional rules we must add the second form of mix. Let (MMix) denote the following rule devised for boxed cut formulae:

with $i+j \ge 1$ and $k+n \ge 1$.

Note that (MMix) similarly like TR-rules works also on the right sequents, even if $i=k=0$. Moreover, we require that (Mix) is restricted only to nonmodal cut formulae and denote it by $(Mix')$. Nothing is lost since if $j=n=0$, then (MMix) works like (Mix). This is the solution similar to applied by Avron [2] in his cut elimination proof for hypersequent calculus for S5. Details of such proof are specified in Bednarska and Indrzejczak [7].

Let us call the system with these two variants of mix BSC2’. One may easily prove that:

Lemma 1

BSC2 $\vdash \varGamma \Rightarrow \varDelta$ iff BSC2’ $\vdash \varGamma \Rightarrow \varDelta$

Proof

From left to right it is enough to show that the application of (Mix) on modal formula is derivable by (MMix). If $j=n=0$ it is the same. Otherwise, after the application of (MMix) we must introduce the lacking number of occurences of cut formula by W to the left sequent and then by TR move them to the right sequent to restore its full shape.

From right to left it is enough to show that (MMix) is derivable by (Mix) in BSC2. Again only the case with $j\ge 1$ or $n\ge 1$ must be considered. We apply (TR) to such occurrences of cut formula to move them to the left sequent in both premisses, then we apply (Mix) so all these occurrences are deleted from resulting bisequent.    $\square$

Before we prove elimination of cut for BSC2 one important thing should be noted. Clearly, in the presence of cut BSC1 and BSC2 are equivalent. It is also easy to observe that without cut everything provable in BSC2 must be provable in BSC1 since the former is just restricted form of the latter. But is BSC2 without cut equivalent to BSC1? An examination of a proof of B in BSC1 shows that rules were applied in both sequents. But in BSC2 the application of static rules in the right sequent is forbidden and without cut we are not able to prove B. If we restrict our interest to the system which is only weakly complete, i.e. where all valid formulae are provable, we can apply the approach of Fitting [15] based on the observation that in S5 it holds that $\vdash \varphi$ iff $\vdash \Box \varphi$. Therefore, at the expense of reducing the problem to weak completeness only we can change slightly a definition of a proof demanding that what we are proving are sequents of the form $\Rightarrow \Box \varphi$. In fact, due to the application of bisequents we may provide more specific formulation. Note first that:

Lemma 2

In BSC2 (without cut) $\vdash \Rightarrow \Box \varphi$ iff $\vdash \Rightarrow \varphi \mid \Rightarrow \Box \varphi$

Proof

From left to right we just apply $(\Rightarrow TR\mid )$ and $(\Rightarrow W)$; conversely we apply $(\Rightarrow \Box )$, then $(\mid \Rightarrow TR)$ (but to the right sequent) and $(\Rightarrow C)$.    $\square$

For illustration sake let us consider again a problem of proving B in so modified BSC2 (without cut). Here is a proof of $\Rightarrow \lnot p \rightarrow \Box \lnot \Box p \mid \Rightarrow \Box (\lnot p \rightarrow \Box \lnot \Box p)$

Now we can prove:

Theorem 3

If BSC2 $\vdash \Rightarrow \varphi \mid \Rightarrow \Box \varphi$, then BSC2$^- \ \vdash \Rightarrow \varphi \mid \Rightarrow \Box \varphi$

Proof

We will use the method of Girard [18] based on the application of cross-cuts. But we apply Gentzen’s overall strategy, i.e., we will prove the result for the case where both premisses of $(Mix')$ or (MMix) are cut-free.

The cases where one premiss, say the left one, is axiomatic are simple; we show it only for (MMix):

is replaced by:

The cases where one cut-formula in one premiss is parametric in all occurrences are similar to reductions in standard LK. For illustration we consider the case of (MMix) when the left premiss is obtained by $(\rightarrow \Rightarrow )$:

is transformed into:

where D replaces:

Note that in case $\varphi = \Box \chi$ we must additionally restore $\varphi$ by $(\Rightarrow W)$ to be able to derive the last sequent by $(\rightarrow \Rightarrow )$. If in this case also some $\Box \chi$ were deleted in the right component we restore them by W in the left component and TR. It should be noted that when TR is performed we can always reduce the height even if left sequents are non-active.

The most troublesome cases are with cut formulae being principal in both premisses. Let us consider the case of $\Box \varphi$:

if $i=j=k=0$ it is enough to perform $(Mix')$ on $\varphi$ and then possibly restore by $(W\Rightarrow )$ some occurences of $\varphi$ in $\varLambda$. Moreover, if $\varphi = \Box \psi$ and there are some occurrences of it in $\varDelta$ or $\varPi$ we actually perform (MMix) and must restore by W also deleted occurrences in these multisets. In case some of $i, j, k\ge 0$ we must first make cross-cuts to delete occurrences of $\Box \varphi$. Of course the most difficult situation is when all of $i, j, k \ge 1$; we perform two cross-cuts:

where both applications of (MMix) have lower height and next:

where the application of $(Mix')$ is of lower complexity. $\varLambda ', \varTheta '$ are like $\varLambda , \varTheta$ but with deleted occurrences of $\varphi$ (if any). Again, if $\varphi = \Box \psi$ and there are some occurrences of it in $\varDelta , \varSigma , \varGamma , \varPi$ we perform rather (MMix). The last step signed with double line should be explained. No rule is to be applied on the right component, including contraction. However, all formulae are modal so we can perform enough transitions to the left component, make required contractions and move these formulae again to the right component.    $\square$

5 Extensions

Recently Avron and Lahav [4] noticed that all HC for S5 are restricted to propositional part. In fact, Mints [32] proposed systems for some first-order version of S5 but, as we mentioned, this work came unnoticed. In general, most of the proposals indeed are restricted to propositional level. However, once we have at our disposal a calculus for which a syntactic cut elimination holds it is possible to extend it to cover at least some first-order versions of S5. We will use a version of first-order language commonly applied in proof theoretic research with denumerable set of bound individual variables $x, y, z, \ldots$ and free individual variables (or parameters) a, b, c, .... Both sorts of variables are rigid but we additionally admit also nonrigid terms $f_1, f_2, f_3, \ldots$.

Let us consider axiomatic formulations of systems Q1, Q1R and QS as stated by Garson [17], all with S5 modalities (hence the last is just QS5 since S is just a label for chosen modality). The first and the second are adequate wrt to semantics with all terms rigid whereas QS5 admits also nonrigid terms being individual concepts in the sense of Carnap. Q1 is the logic of constant domain for all states in models whereas the other two admit varying domains. We do not go deeper into semantical matters here since what is of interest for us is their axiomatic characterization. Q1 is based on standard classical first-order logic CFL hence to obtain its BSC2-counterpart we may use standard rules for quantifiers:

where t is any (rigid) term but a is not in $\varGamma , \varDelta$ and $\varphi$.

Note that Barcan Formula $\forall x\Box \varphi \rightarrow \Box \forall x\varphi$ is provable in axiomatic CFL with S5-modalities hence it need not be added as a separate axiom as in case of weaker modal logics. Unfortunatelly it is not provable in BSC2$^-$ although it is easily provable in BSC1$^-$:

We conjecture that BSC1$^-$ is complete but it needs separate semantic proof since constructive cut elimination theorem does not hold for this calculus. As for BSC2$^-$ to save equivalence with Q1 we must add axiomatic sequents $\forall x\Box \varphi \Rightarrow \Box \forall x\varphi$. This formalization is easily proven to be equivalent to standard axiomatic one under the translation stated for propositional case but note that cuts with additional axioms as one of the premisses are not eliminable.

In case of Q1R and QS5 the situation is clearer. Since both are based on positive free logic FL we must change quantifier rules for their free versions:

with the same stipulations concerning instantiated terms but in case of QS5 they may be nonrigid as well. ‘E’ is an existence predicate. Again proving equivalence with axiomatic formulation of (positive) free logic is unproblematic.

To accomodate identity one may add the following rules to Q1 and QR1:

where $\varphi$ is atomic in $(\Rightarrow =)$. For QS5 only the first two rules are needed since nonrigid terms are admitted. But it should be noted that Et is not counted as atomic formula in case of QS5.

One may in a standard way (see e.g. Negri and von Plato [35]) prove that:

Lemma 3

(Substitution). If $\vdash \varGamma \Rightarrow \varDelta$, then $\vdash (\varGamma \Rightarrow \varDelta )[a/t]$ in the height-preserving manner.

It is then routine to extend our cut elimination to BSC2 counterparts of all these six axiomatic systems (with or without rules for identity) but in case of Q1 in restricted form (see the remarks above concerning Barcan Formula). Reduction of the height in case all occurrences of mix-formula are parametric in one premiss goes as in propositional case. The cases where in both premisses one occurrence of mix formula is principal are also unproblematic. However one should remeber that in case of Q1 and QR1 MMix also takes place when the left premiss is deduced by $(\Rightarrow =\Box )$ or $(\Rightarrow \ne \Box )$ and the right one by $(\Box \Rightarrow )$ or some transitional rule. For the sake of illustration we display one such case:

by two cross-cuts of lesser height we obtain:

and

and finally:

where mix-formula is of lesser complexity and the compact last step is obtained by the series of transitions, contractions and transitions again.

We consider also the case of $\forall x\varphi (x)$:

where a is fresh, hence by Substitution Lemma we have a proof of the same height of:

$Eb, \varGamma \Rightarrow \varDelta , \forall x\varphi (x)^k, \varphi (b) \mid \varLambda \Rightarrow \varTheta$

Now we perform three cross-cuts of lesser height:

Two mixes on Eb and $\varphi (b)$ respectively, both of lesser complexity, lead to the required sequent after some contractions. Note that in case $\varphi (b)$ is modal we must apply (MMix) and some applications of transitional rules may be also required.    $\square$

Let us conclude with a brief comparison of BSC1 and BSC2. The former is more flexible as far as we want to use it for actual proof search. It is also strongly complete (even without cut) whereas BSC2 without cut is only weakly complete. However, in BSC2 we can keep better control over the structure of proofs and it allows for obtaining a constructive proof of cut elimination which is always seen as an advantage over calculi which can be only semantically shown to be cut-free. In particular, we have made use of it in this section. We restrict our investigation here to the problem of cut elimination but further features and applications of both versions seem to be worth exploring.