A Formal Framework for Hypersequent Calculi and Their Fibring

Abstract

Hypersequents are a natural generalization of ordinary sequents which turn out to be a very suitable tool for presenting cut-free Gentzent-type formulations for diverse logics. In this paper, an alternative way of formulating hypersequent calculi (by introducing meta-variables for formulas, sequents and hypersequents in the object language) is presented. A suitable category of hypersequent calculi with their morphisms is defined and both types of fibring (constrained and unconstrained) are introduced. The introduced morphisms induce a novel notion of translation between logics which preserves metaproperties in a strong sense. Finally, some preservation features are explored.

This paper constitutes a revised, extended and improved version from the preprint [9]. That preliminary version is described with full details in [10].

1 Introduction

In recent years, the development of methods for combining logics has gained attention, and motivations came from different areas such as Philosophy and Computer Science (see, for instance, [4] and [5]). Logics presented in different ways require ad hoc combination techniques. In [11], the well-known method of fibring for combining modal logics was introduced. Categorical (a.k.a. algebraic) fibring, introduced in [16], is a wide and extremely useful tool for combining logics, allowing to combine a vast class of logic systems of different nature (consult [5]). In general, it is possible to define two different kinds of fibring: unconstrained fibring, in which there is no sharing of logic constructors from the combined logics (and so the resulting logic is a coproduct of the given logics), and constrained fibring, in which some constructors are shared. In categorical terms, the latter is obtained from the former by taking an appropriate quotient.

In [8], a novel category of formal sequent calculi was introduced, and both types of categorical fibring (called meta-fibring) were obtained. Two kinds of sequents were considered: commutative sequents, formed by pairs of sets of formulas (thus taking for granted structural rules such as permutation and contraction) and non-commutative sequents, formed by pairs of sequences of formulas. The former are called general assertions, while the latter are called general sequents. A remarkable feature of the presentation of this approach is the use in the object language of variables for sets and sequences of formulas, respectively, besides the standard use of scheme variables for formulas. This peculiarity permits considering sequent rules with full generality, allowing to combine by fibring two calculi in a satisfactory way. Another novelty of the approach is the notion of morphism between sequent calculi proposed therein (called meta-translations), being stronger than the usual one in the sense that more meta-properties (in rough terms, sequent rules) of the consequence relation of the source logic are preserved. This is a key feature which allows the reconstruction of a given logic by means of the fibring of its fragments. An interesting possibility of generalization of the results obtained in [8] lies in the use of hypersequents instead of sequents, because of their subtleties.

Hypersequents (see [2, 15] among others) constitute a natural generalization of ordinary sequents and turn out to be a very suitable tool for presenting cut-free Gentzen-type formulations for several non-classical logics. In particular, hypersequents are well-suited for describing disjunctive properties by analytic means. The proof of cut-elimination in a (hyper)sequent calculus for a given logic is desirable, because of its important consequences, such as the consistency of the logic and interpolation properties.

This paper proposes a generalization of the work done in [8] to the richer framework of hypersequents. Thus, departing from a formal presentation of hypersequent in which meta-variables for contexts (i.e. sequents) are introduced in the object language, the fibring of such systems is defined within a suitable category of hypersequents. Besides, it is shown that fibring does not preserve, in general, rule-elimination properties such as the cut-elimination property. Finally, a brief conceptual discussion about the relevance of this approach concerning the theory of translations between logics is carried out.

2 The Category of Formal Hypersequent Calculi

This section presents the category of hypersequent calculi, generalizing the notion of assertion calculi introduced in [8]. An independent similar approach was developed in [7].

In what follows, we shall consider a denumerable set $\varXi=\{\xi_{i} : i \in\mathbb{N} \}$ of symbols called variables of level 1 (or scheme variables); a denumerable set $\mathcal{X} = \{X_{i} : i \in\mathbb{N} \}$ whose elements are called variables of level 2 (or context variables); and, finally, a denumerable set ${\mathfrak{H}}=\{ H_{i} : i \in\mathbb{N} \}$ whose elements are called variables of level 3 (or sequent variables) where these sets are pairwise disjoint.

A propositional signature is a denumerable family $C=\{C_{n}\}_{n \in\mathbb{N}}$ of pairwise disjoint denumerable sets; additionally, every C _n is disjoint with $\mathcal{H} \cup \mathcal{X} \cup\varXi$. Elements in C _n are called n-ary connectives (or constructors). The set of constructors of C is $|C|=\bigcup_{n \in\mathbb{N}}C_{n}$. The algebra of type C freely generated by Ξ is denoted by L(C). Elements of L(C) are called formulas. From now on, and for the sake of simplicity, in the examples we will refer to a signature C as the set |C|.

Generalizing to multisets the definition from [8] of general assertion, a sequent over a signature C is an expression of the form (A;Γ≻Δ;B) where Γ and Δ are multisets of formulas in L(C) and A,B are finite multisets of context variables such that Γ∪Δ∪A∪B≠∅. The set of sequents over C is denoted by Seq(C).

It should be noted that a sequent (in our sense) is nothing more than an ordinary commutative sequent, enriched with both variables of type 2 for sets of formulas (describing the context of the sequent) and variables of type 1 for formulas. This formalism allows defining in a precise way sequent calculi and their fibring (cf. [8]). Now we shall introduce the notion of commutative hypersequent by using sequent variables, that is, variables of type 3.

Definition 2.1

A commutative hypersequent h over C is a pair $h= \langle\mathcal{H}; \mathcal{S} \rangle$ where $\mathcal{H}$ is a finite multiset of sequent variables and $\mathcal{S}$ is a finite multiset of sequents. The set of commutative hypersequents over C will be denoted by HSeq(C).

Following the usual notation, a commutative hypersequent

$$h = \bigl\langle \{G_1, \dots, G_n\} ;\bigl\{ (A_1; \varGamma_1 \succ\Delta_1; B_1), \dots, (A_m; \varGamma_m \succ \Delta_m; B_m) \bigr\} \bigr\rangle $$

will be written, from now on, as

$$h = G_1 | \cdots| G_n | A_1; \varGamma_1 \succ\Delta_1; B_1 | \cdots|A_m; \varGamma_m \succ\Delta_m; B_m. $$

An empty component of a sequent will be simply omitted from the notation and so we will write, for instance, (A;Γ≻Δ) and (≻Δ;B) instead of (A;Γ≻Δ;∅) and (∅;∅≻Δ;B), respectively. As usual, Γ,Γ′ and Γ,φ will stand for Γ∪Γ′ and Γ∪{φ}, respectively. Besides, we shall write X and X,Y instead of {X} and {X,Y}, respectively, for any variables X and Y. The same notation applies to sequent variables. Moreover, given a finite multisubset $\mathcal{H}$ of $\mathfrak{H}$, the hypersequent $\langle\mathcal{H}; \emptyset\rangle$ will be simply denoted by $\mathcal{H}$. Analogously, given a finite multisubset $\mathcal{S}$ of Seq(C) the hypersequent $\langle\emptyset; \mathcal{S} \rangle$ will be simply denoted by $\mathcal{S}$.

Definition 2.2

Let C be a signature. A (n-ary) rule of inference of commutative hypersequents over C is a pair r=〈{h ₁,…,h _n },h〉 such that h _i ,h∈HSeq(C). If n=0 then r is called an axiom. A commutative hypersequent calculus (chc) is a pair $\mathcal{A}=\langle C, R\rangle$ where C is a signature and R is a finite set of rules of inference of commutative hypersequents over C.

For simplicity, we shall denote pairs 〈{h ₁,…,h _n },h〉 and 〈∅,h〉 by

$$\frac{ h_1 \quad \dots\quad h_n}{h}\quad \mbox{and}\quad \frac{\phantom{e}}{h}. $$

Example 2.3

The logical hypersequent rule r _¬≻ for negation which is usually represented by

$$r_{\neg \succ}=\displaystyle\frac{G|\, \varGamma\vdash \Delta, \alpha}{G|\, \neg\alpha, \varGamma\vdash\Delta} $$

is here represented by

$$\displaystyle\frac{ \langle\{G\}; \{(\{X\}; \emptyset\succ\{ \xi\} ; \{Y\}) \} \rangle}{ \langle\{G\}; \{(\{X\}; \{\neg\xi\} \succ\emptyset; \{Y\}) \} \rangle}, $$

or simply by

$$\displaystyle\frac{ G | X \succ\xi; Y }{ G | X; \neg\xi\succ Y} $$

(see Remark 2.5 below).

From now on, we will denote by $\mathcal{MP}_{\mathrm{fin}}(X)$ the set of all finite multisubsets of a set X.

Recall that a substitution over a signature C is a map σ:Ξ→L(C). We denote by $\hat{\sigma}:L(C) \to L(C)$ the unique homomorphic extension of σ to L(C). Adapting [8], an instantiation over C is a map $\varrho: \mathcal{X} \to\mathcal{MP}_{\mathrm{fin}}(L(C) \cup\mathcal{X})$. If ϱ is an instantiation over C and $A \in\mathcal{MP}_{\mathrm{fin}}(\mathcal {X})$ is a finite multiset of variables of type 2, we define the following finite multisets:

$$\begin{aligned} A_{\mathcal{X}}^{\varrho} &= \bigl\{ Y \in\mathcal{X}: Y \in\varrho (X) \mbox{ for some } X\in A\bigr\} = \biggl(\bigcup _{X \in A} \varrho(X)\biggr) \cap \mathcal{X} ; \\ A_{L(C)}^{\varrho} &= \bigl\{ \varphi\in L(C): \varphi\in\varrho (X) \mbox{ for some } X\in A\bigr\} = \biggl(\bigcup_{X \in A} \varrho(X)\biggr) \cap L(C). \end{aligned}$$

Thus, given a substitution σ and an instantiation ϱ over C, respectively, the map (σ,ϱ):Seq(C)→Seq(C) is defined in the following way: given a sequent (A;Γ≻Δ;B), then

$$(\sigma, \varrho) (A; \varGamma\succ \Delta; B) = \bigl(A_{\mathcal{X}}^{\varrho} ;\hat{\sigma}( \varGamma) \cup A_{L(C)}^{\varrho} \,\succ\, \hat{ \sigma}( \Delta) \cup B_{L(C)}^{\varrho}; B_{\mathcal{X}}^{\varrho} \bigr). $$

In order to deal with hypersequents, we shall introduce a notion of substitution for variables of level 3.

Definition 2.4

We shall say that λ is a sequent instantiation over C if λ is a mapping from $\mathfrak{H}$ to the set $\mathcal {MP}_{\mathrm{fin}}({\mathfrak{H}} \cup \mathit{Seq}(C))$ of all finite multisubsets of ${\mathfrak{H}} \cup \mathit{Seq}(C)$.

Let λ be a sequent instantiation and $h=\langle\mathcal{H}; \mathcal{S} \rangle$ a hypersequent over C. Consider the following multisets:

$$\begin{aligned} \mathcal{H}_{\mathfrak{H}}^{\lambda} &= \bigl\{ G \in\mathfrak{H}: G \in \lambda(H) \mbox{ for some } H\in \mathcal{H}\bigr\} = \biggl(\bigcup _{H \in\mathcal{H}} \lambda(H)\biggr) \cap\mathfrak{H}; \\ \mathcal{H}_{\mathit{Seq}(C)}^{\lambda} &= \bigl\{ s \in \mathit{Seq}(C): s \in\lambda(H) \mbox { for some } H\in \mathcal{H}\bigr\} =\biggl(\bigcup _{H \in\mathcal{H}} \lambda(H)\biggr) \cap \mathit{Seq}(C). \end{aligned}$$

Then, given a substitution σ, an instantiation ϱ and a sequent instantiation λ over C, respectively, the map (σ,ϱ,λ):HSeq(C)→HSeq(C) is defined as follows:

$$(\sigma, \varrho, \lambda) (h)= \bigl\langle \mathcal{H}_{\mathfrak{H}}^{\lambda} ; (\sigma, \varrho) (\mathcal{S}) \cup\mathcal {H}_{\mathit{Seq}(C)}^{\lambda} \bigr\rangle . $$

Remark 2.5

(Extensional rules vs. Intensional rules)

Recall the Example 2.3 above. Despite the apparent similarities between the traditional notation for hypersequent rules and our notation, there are deep differences between r _¬≻ and our representation. In the former, G denotes an arbitrary multiset of concrete sequents; in their turn, Γ and Δ denote arbitrary multisets of formulas; finally, α denotes an arbitrary concrete formula. That is, r _¬≻ consists of infinite concrete rules obtained by instantiation of their metavariables, that is, variables in the metalanguage: it is an extensional approach to inference rules. On the other hand, our notation is extremely precise: G, X, Y and ξ are concrete variables of the formal language of hypersequents, and so the rule is represented by a single linguistic object instead of infinite ones represented by variables in the metalanguage, as done in the traditional approach to (hyper)sequents. In other words, we propose an intensional approach to inference rules. Despite the obvious advantages of this fact, there is a much more important advantage of our formal approach to (hyper)sequents. Since we are interested in combining different (hyper)sequent calculi, the use of formal variables instead of metavariables (that is, informal variables) is crucial. In fact, in the intensional approach, rules are prepared to be combined, since they are open to accept new connectives: ξ can be replaced by any formula, while X and Y can be replaced by any multisets of formulas, as well as G is open to be substituted by any multiset of sequents, and this holds for any language. That is, if we add new connectives to the language (as a consequence of a combination process), the meaning of the rule will be the same. On the other hand, in the traditional extensional approach to (hyper)sequent rules, this possibility is no longer allowed, and the rule must be extended in order to cope with the new language. This is the main novelty of the intensional approach to combination of hypersequents, first introduced in [8] in the setting of sequent calculi.

Now we are in conditions to define the notion of derivation in a commutative hypersequent calculus.

Definition 2.6

Let $\mathcal{A} = \langle C, R \rangle$ be a commutative hypersequent calculus and let ϒ∪{h}⊆HSeq(C) be a set of hypersequents. We shall say that h is derivable in $\mathcal{A}$ from ϒ, and write $\varUpsilon \vdash_{\mathcal{A}} h$, if there exists a finite sequence h ₁…h _n of elements of HSeq(C) such that h _n =h and, for all 1≤i≤n, either h _i ∈ϒ, or there exist an hypersequent rule $r =\langle\{h'_{1}, \dots, h'_{k}\}, h'\rangle$ in R, a substitution σ, an instantiation ϱ and a sequent instantiation λ over C such that $(\sigma, \varrho, \lambda) (h'_{j}) \in\{ h_{1}, \dots, h_{i-1}\}$ (for 1≤j≤k) and (σ,ϱ,λ)(h′)=h _i . If ϒ=∅ we shall just say that h is provable in $\mathcal{A}$.

Remark 2.7

The expressive power of hypersequents, allied to the possibility of using variables either of type 1, 2 or 3, allows defining structural rules in many different ways. For instance, the contraction rule, as pointed out by A. Avron, admits two versions: an internal (inside a sequent) and an external (inside the context of the hypersequent). Thus, the internal version of contraction (using variables of type 1) and the external version (using variables of type 2) are as follows:

$$\frac{ G| X; \xi, \xi\succ Y }{ G| X; \xi\succ Y }, \qquad \frac{ G | X \succ\xi, \xi; Y }{ G | X \succ\xi; Y }, $$

$$\frac{ G | X \succ Y | X \succ Y }{ G | X \succ Y }. $$

We can add one more possibility by using variables of level 3:

$$\displaystyle\frac{ G|G|H }{ G|H }. $$

Clearly, the level 3 version can simulate the level 2 version, meanwhile each concrete application of the level 3 contraction is recovered by successive applications of the level 2 contraction. On the other hand, the internal contraction can be alternatively defined by using variables of level 2:

$$\displaystyle\frac{ G| X, X, Y \succ Z }{ G| X,Y \succ Z }, \qquad \frac{ G | X \succ Y, Y, Z }{ G | X \succ Y, Z } . $$

In an analogous way to the remark above, the internal contractions of level 2 and level 1 are equivalent.

Now we are going to define the category of formal commutative hypersequent calculi. Recall that in [8] the following category of signatures was used:

Definition 2.8

The category Sig of signatures is the category whose objects are propositional signatures. A morphism f:C→C′ in Sig is a function f:|C|→L(C′) such that f(c) is a formula which depends at most on schema variables ξ ₁,…,ξ _n whenever $c \in C'_{n}$ (in particular, $f(c) \in L(C'_{0})$ if c∈C ₀). If f ₁:C→C′ and f ₂:C′→C″ are two morphisms in Sig, the composite morphism f ₂∘f ₁:C→C″ in Sig is the composite map $\hat{f_{2}} \circ f_{1} :|C| \to L(C'')$, where the function $\hat{f_{2}}:L(C') \to L(C'')$ is defined as follows:

$$\begin{aligned} \begin{aligned} &\hat{f_2}(\xi)=\xi,\quad \mbox{for}\ \xi \in\varXi ; \qquad \hat {f_2}(c)=f_2(c),\quad \mbox{for}\ c \in C'_0; \\ &\hat{f_2}\bigl(c(\varphi_1, \dots, \varphi_n)\bigr)= f_2(c) \bigl(\hat{f_2}( \varphi_1), \dots, \hat{f_2}(\varphi_n)\bigr) \quad \mbox{for}\ c \in C'_n , n \geq1. \end{aligned} \end{aligned}$$

The identity morphism id _C :C→C for the signature C is the function id _C :|C|→L(C) such that id _C (c)=c(ξ ₁,…,ξ _n ) if c∈C _n . In particular, id _C (c)=c, if c∈C ₀.

Recall from [8] that if (A;Γ≻Δ;B) is a sequent over C and f:C→C′ is a signature morphism, then $\hat{f}(A;\varGamma\succ\Delta; B)$ is, by definition, the sequent $(A;\hat{f}(\varGamma) \succ\hat{f}(\Delta); B)$ over C′. This can be naturally extended to hypersequents:

$$\hat{f}\bigl(\langle\mathcal{H}; \mathcal{S} \rangle\bigr)=\bigl\langle \mathcal{H}; \hat{f}(\mathcal{S}) \bigr\rangle . $$

It is clear that $\hat{f}(h)$ is a hypersequent over C′ provided that h is a hypersequent over C.

The category of commutative hypersequent calculi is defined as follows.

Definition 2.9

The category CHC of commutative hypersequent calculi is the category whose objects are commutative hypersequent calculi of the form $\mathcal{A}=\langle C, R \rangle$. A morphism f:〈C,R〉→〈C′,R′〉 in CHC is a morphism f:C→C′ in Sig such that, for every r=〈{h ₁,…,h _n },h〉 in R, it is verified that $\hat{f}(h)$ is derivable in 〈C′,R′〉 from $\{\hat{f}(h_{1}), \dots, \hat{f}(h_{n})\}$. The composition of morphisms and the identity morphism in CHC is defined as in Sig.

3 Unconstrained Fibring of Hypersequent Calculi

Taking advantage of the formal framework for defining hypersequent calculi described in the previous section, we are now ready to combine these proof systems. The combination method proposed here is known in the literature as (categorical) fibring (see [11, 16]). Basically, categorical fibring can be performed in two (related) ways: the simpler one, called unconstrained fibring, consists in joining up the inference rules of the two systems being combined, were the rules must be rewritten in the language generated by the free combination of the symbols of both systems. In formal terms, it is the coproduct of both systems, in the category in which they are represented. In Sect. 6, we shall study the second (and more general) way of categorical fibring, called unconstrained fibring, in which some connectives of the systems to be combined are shared in the resulting system.

Prior to the definition of unconstrained fibring, it is necessary to introduce some results and concepts.

Definition 3.1

Given substitutions σ,σ′ and instantiations ϱ,ϱ′ over C, the product (σ,ϱ)⋅(σ′,ϱ′) is given by

$$(\sigma, \varrho)\cdot\bigl(\sigma', \varrho'\bigr)= \bigl(\sigma\cdot\sigma', \bigl(\varrho\cdot \varrho' \bigr)_\sigma\bigr) $$

where σ⋅σ′ is the substitution over C given by $\sigma\cdot\sigma'(\xi)= \hat{\sigma} (\sigma'(\xi))$ and (ϱ⋅ϱ′) _σ is the instantiation over C given by

$$\bigl(\varrho\cdot\varrho'\bigr)_{\sigma}(X) = \bigl(\{X \}_{\mathcal{X}}^{\varrho '}\bigr)_{\mathcal{X}}^{\varrho} \cup\bigl(\{X \}_{\mathcal{X}}^{\varrho'}\bigr)_{L(C)}^{\varrho} \cup \hat{ \sigma}\bigl( \{X\}_{L(C)}^{\varrho'}\bigr). $$

The proof of the following useful result is straightforward:

Proposition 3.2

Let σ,σ′ be substitutions over C and let ϱ,ϱ′ be instantiations over C. Then, for every s∈Seq(C),

$$\bigl[(\sigma, \varrho)\cdot\bigl(\sigma', \varrho' \bigr)\bigr] (s) = (\sigma, \varrho ) \bigl(\bigl(\sigma', \varrho'\bigr) (s)\bigr). $$

In order to consider variables of level 3, we introduce the following definition.

Definition 3.3

Given substitutions σ,σ′, instantiations ϱ,ϱ′ and sequent instantiations λ,λ′ over C, the product (σ,ϱ,λ)⋅(σ′,ϱ′,λ′) is given by

$$(\sigma, \varrho, \lambda)\cdot\bigl(\sigma', \varrho', \lambda'\bigr)=\bigl(\sigma\cdot\sigma', \bigl(\varrho \cdot \varrho'\bigr)_\sigma, \bigl(\lambda\cdot \lambda'\bigr)_{\sigma\varrho}\bigr) $$

where σ⋅σ′ and (ϱ⋅ϱ′) _σ are as in Definition 3.1; and (λ⋅λ′) _σϱ is the sequent instantiation given by

$$\bigl(\lambda\cdot\lambda'\bigr)_{\sigma\varrho}(H) = \bigl(\{H \}_{\mathfrak {H}}^{\lambda'}\bigr)_{\mathfrak{H}}^{\lambda} \cup\bigl(\{H \}_{\mathfrak {H}}^{\lambda'}\bigr)_{\mathit{Seq}(C)}^{\lambda} \cup(\sigma, \varrho) \bigl( \{H\} _{\mathit{Seq}(C)}^{\lambda'}\bigr). $$

Using Proposition 3.2, it is easy to prove the following result.

Proposition 3.4

Let σ,σ′ be substitutions over C, let ϱ,ϱ′ be instantiations over C and let λ,λ′ be sequent instantiations over C. Then, for every h∈HSeq(C),

$$\bigl[(\sigma, \varrho, \lambda)\cdot\bigl(\sigma', \varrho', \lambda'\bigr)\bigr] (h) = (\sigma, \varrho, \lambda) \bigl(\bigl(\sigma', \varrho', \lambda'\bigr) (h)\bigr). $$

The next proposition will be useful.

Proposition 3.5

Let h ₁…h _n be a derivation of h in $\mathcal{A}$ from ϒ. Then, for every (σ,ϱ,λ), the sequence (σ,ϱ,λ)(h ₁)…(σ,ϱ,λ)(h _n ) is a derivation of (σ,ϱ,λ)(h) in $\mathcal{A}$ from (σ,ϱ,λ)(ϒ).

Proof

By induction on n, taking into account Definition 2.6 and Proposition 3.4. □

Given an hypersequent h, we denote by Var(h) the set of all the scheme variables occurring in formulas in h. If ϒ is a set of hypersequents, then Var(ϒ) denotes the subset ⋃ _h∈ϒ Var(h) of Ξ.

Corollary 3.6

Let $\mathcal{A}=\langle C, R\rangle$ be a chc, and ϒ∪{h}⊆HSeq(C) such that $\varUpsilon\vdash _{\mathcal{A}} h$. Then, there exists a derivation h ₁…h _n of h in $\mathcal{A}$ from ϒ such that Var(h _i )⊆Var(ϒ)∪Var(h), for every 1≤i≤n.

Proof

Consider a derivation h ₁…h _n of h in $\mathcal {A}$ from ϒ. Let σ be a substitution over C such that σ(ξ)∈Var(ϒ)∪Var(h) whenever ξ∉Var(ϒ)∪Var(h), and σ(ξ)=ξ otherwise. Let ϱ and λ be the identity instantiation and the identity sequent instantiation over C, respectively. By Proposition 3.5, the sequence (σ,ϱ,λ)(h ₁)…(σ,ϱ,λ)(h _n ) is a derivation of h in $\mathcal{A}$ from ϒ such that, for every 1≤i≤n, Var((σ,ϱ,λ)(h _i ))⊆Var(ϒ)∪Var(h). □

The proof of the next result is routine. In particular, item (i) is an immediate consequence of Proposition 3.5.

Theorem 3.7

• (i) If $\varUpsilon\vdash_{\mathcal{A}} h$, then $(\sigma, \varrho, \lambda)(\varUpsilon) \vdash_{\mathcal{A}} (\sigma, \varrho, \lambda)(h)$, for every triple (σ,ϱ,λ).

• (ii) If $\varUpsilon\vdash_{\mathcal{A}_{1}} h$, then $\hat{f}(\varUpsilon) \vdash_{\mathcal{A}_{2}} \hat{f}(h)$, for every morphism $f:\mathcal{A}_{1} \to\mathcal{A}_{2}$ in  CHC.

Recall from [8] the following result:

Proposition 3.8

The category Sig has finite coproducts.

The coproduct of the signatures C and C′ will be denoted by C⊕C′, with the canonical injections i:C→C⊕C′ and i′:C′→C⊕C′.

The (unconstrained) fibring of hypersequent calculi is defined as expected:

Definition 3.9

Let $\mathcal{A} = \langle C, R\rangle$ and $\mathcal{A}' = \langle C', R'\rangle$ be two chcs. The (unconstrained) fibring of $\mathcal{A}$ and $\mathcal{A}'$ is the commutative hypersequent calculus $\mathcal{A} \oplus\mathcal{A}' =\langle C, R \rangle$ where:

• C=C⊕C′,

• $R=\{ \hat{i}(r): r \in R\} \cup\{ \hat{i'}(r): r \in R\}$.

Here i and i′ are the canonical injections from C and C′ to C⊕C′, respectively.

The characterization of unconstrained fibring as a coproduct can be proved by generalizing the corresponding proof for sequent calculi found in [8]:

Proposition 3.10

Let $\mathcal{A} = \langle C, R\rangle$ and $\mathcal{A}' = \langle C', R'\rangle$ be two chcs. Then, $\mathcal{A} \oplus\mathcal {A}'$ is the coproduct in CHC of $\mathcal{A}$ and $\mathcal{A}'$ with canonical injections induced by the injections i and i′ in Sig.

4 Admissible and Derivable Rules and the Rule Elimination Property

Recall that a rule of inference is admissible in a formal system if the set of theorems of the system is closed under the rule. In our context, we arrive to the following definition:

Definition 4.1

Let $\mathcal{A} = \langle C, R\rangle$, and let r=〈{h ₁,…,h _n },h〉 be an inference rule over C (r can belong or not to R). We say that r is an admissible inference rule of $\mathcal{A}$ if, for every substitution σ, instantiation ϱ and sequent instantiation λ over C, it is verified that

$$\mbox{if}\ \vdash_\mathcal{A} (\sigma, \varrho,\lambda)(h_i)\quad \mbox{for all}\ i=1, \dots n,\quad \mbox{then}\ \vdash_\mathcal{A} (\sigma, \varrho,\lambda)(h). $$

That is to say, an admissible rule is one whose conclusion holds whenever the premises hold, and so that rule can be added to the system without changing theoremhood. It is easy to prove the following:

Proposition 4.2

Let $\mathcal{A} = \langle C, R\rangle$ and let r be an inference rule over C. Let $\mathcal{A}^{r}= \langle C, R\cup\{r\}\rangle$. Then r is admissible in $\mathcal{A}$ iff, for every hypersequent h over C, $\vdash_{\mathcal{A}^{r}} h$ implies $\vdash_{\mathcal{A}} h$.

Clearly, if r∈R then r is admissible in 〈C,R〉. A related notion is that of derived rule. A rule r is said to be derivable in a chc if its conclusion can be derived from its premises using the other rules of the system. Formally:

Definition 4.3

Let $\mathcal{A} = \langle C, R\rangle$, and let r=〈ϒ,h〉 be an inference rule over C such that r∉R. We say that r is a derived inference rule of $\mathcal{A}$ if $\varUpsilon\vdash_{\mathcal{A}} h$.

From now on, if $\mathcal{A} = \langle C, R\rangle$, we will denote by $\mathcal{A}_{r}$ the chc 〈C,R∖{r}〉.

Remark 4.4

• (i) If $f:\mathcal{A} \to\mathcal{A}'$ is a morphism in CHC and r∈R, then we have that $\hat{f}(r)$ is a derived inference rule of $\mathcal{A}'$.

• (ii) Every derived rule is admissible, but the converse does not hold.

Recall that the cut-elimination theorem (Hauptsatz) states that any sentence that possesses a proof in the sequent calculus (hypersequent calculus) that makes use of the cut rule also possesses a cut-free proof, that is, a proof that does not make use of the cut rule. It was originally proved by G. Gentzen (see [12]) for the systems LJ and LK formalizing intuitionistic and classical logic, respectively. It is well known that in a sequent calculus where cut elimination holds, the cut rule is admissible in the calculus obtained by removing the cut rule. Taking that into account we introduce the following definition:

Definition 4.5

(Rule elimination property)

Let $\mathcal{A}=\langle C, R \rangle$ be a chc, and let r be a rule in R. We shall say that $\mathcal{A}$ admits elimination of rule r (or simply that $\mathcal{A}$ has the r-elimination property) if every time that h∈HSeq(C) has a proof in $\mathcal{A}$, then there is a proof of h in $\mathcal{A}_{r}$.

Then, by Proposition 4.2, we have:

Corollary 4.6

Let $\mathcal{A}=\langle C, R \rangle$ be a chc, and let r be a rule in R. Then, the following conditions are equivalent:

• (i) r is admissible in $\mathcal{A}_{r}$;

• (ii) $\mathcal{A}$ has the r-elimination property.

Definition 4.5 can be generalized as follows:

Definition 4.7

Let $\mathcal{A}=\langle C, R \rangle$ be a chc, and let r be a rule in R. We shall say that $\mathcal{A}$ admits full elimination of the rule r (or simply that $\mathcal{A}$ has the full r-elimination property) if for every derivation of h from ϒ in $\mathcal{A}$, there is a derivation of h from ϒ in $\mathcal{A}_{r}$.

Clearly, if $\mathcal{A}$ admits full elimination of r then it admits the elimination of r: it is enough to take ϒ=∅. The converse does not hold.

The next result is the counterpart of Corollary 4.6 in terms of the notion of derivability.

Proposition 4.8

Let $\mathcal{A}=\langle C, R \rangle$ be a chc, and let r be a rule in R. Then, the following conditions are equivalent:

• (i) r is derivable in $\mathcal{A}_{r}$;

• (ii) $\mathcal{A}$ has the full r-elimination property.

5 Preservation Features and Translating Derivations

In this section, some preservation features are explored. In particular, it is noted that r-elimination property is not preserved by fibring of commutative hypersequent calculi, provided that one (or both) of the calculi enjoys this property. Additionally, by using the notion of goedelization proposed in [5], we shall be able to translate derivations from a given calculus into another.

Observe that, in general, the rule-elimination property is not preserved by fibring of commutative hypersequent calculi provided that just one of the calculi has the rule-elimination property: for instance, cut-elimination property is not preserved by fibring of commutative hypersequent calculi such that just one of them enjoys cut-elimination.

Example 5.1

A. Avron (in [1]) constructed a commutative hypersequent calculus called GLCW enjoying cut-elimination property such that, by adding the connective ∧ together with the usual rules, the resulting calculus GLC ^∗ does not have the cut-elimination property. In our framework, this means that the fibring of GLCW (with cut-elimination) and a calculus of conjunction plus cut (without cut-elimination), results in a calculus without cut-elimination.

This proves the following assertion:

Fact 5.2

In general, unrestricted fibring of commutative hypersequent calculi does not preserve the cut-elimination property, provided that just one of them has this metaproperty.

The more interesting case is when both fibred systems admit r-elimination. However, it is not hard to see that the obtained system need not to admit r-elimination. Indeed, take the sequent calculus for the multiplicative fragment of abelian logic and the additive fragment of linear logic (see [15]). Both calculi have cut-elimination, but the result of fibring does not.

Fact 5.3

In general, unrestricted fibring of commutative hypersequent calculi does not preserve the cut-elimination property, provided that both of them have this metaproperty.

Remark 5.4

Observe that connectives are not shared in the unrestricted fibring. However, the rule r is present in both calculi, collapsing into just one rule in the fibring. Then, r must be a rule without occurrences of connectives, that is, a structural rule like, for instance, Cut or Contraction.

On the other hand, things change when we consider full rule elimination. From Proposition 4.8 we have:

Fact 5.5

Let $\mathcal{A} =\langle C, R \rangle$ be a chc. If $\mathcal{A}$ has the full r-elimination property, then so does $\mathcal{A} \oplus\mathcal {A}'$, for any chc $\mathcal{A}'=\langle C', R' \rangle$.

The next two results are tools for translating derivations from a given calculus into an extension of it, and vice versa. This technique is based on the notion of goedelization introduced in [5].

Definition 5.6

Let C and C′ be two signatures. An embedding from C to C′ is a signature morphism l:C→C′ such that, for every n≥0 and c∈C _n , there exists a unique $c' \in C'_{n}$ such that l(c)=c′(ξ ₁,…,ξ _n ), if n>0, and l(c)=c′ if n=0. We write C≤ _l C′ to denote that l:C→C′ is an embedding.

Observe that if C≤ _l C′ then the underlying functions l:|C|→L(C′) and $\hat{l}: {L(C) \to L(C')}$ are injective. Additionally, $C_{j} \leq_{i_{j}} C_{1} \oplus C_{2}$ for j=1,2, for every signatures C ₁ and C ₂. That is, the canonical injections i ₁ and i ₂ of the coproduct C ₁⊕C ₂ are embeddings.

Definition 5.7

Let C and C′ be two signatures such that C≤ _l C′, and consider a recursive bijection (from now on called goedelization) $g:L(C') \to{\mathbb{N}}$. The translation τ _g :L(C′)→L(C) is the function inductively defined as follows:

• τ _g (ξ _i )=ξ _2i+1, for ξ _i ∈Ξ;

• τ _g (l(c))=c, for c∈C ₀;

• τ _g (c′)=ξ _2g(c′), for $c' \in C'_{0} \setminus l(C_{0})$;

• $\tau_{g}(l(c)(\gamma'_{1}, \dots, \gamma'_{k}))= c(\tau_{g}(\gamma '_{1}), \dots, \tau_{g}(\gamma'_{k}))$, for c∈C _k , k>0 and $\gamma'_{i} \in L(C')$;

• $\tau_{g}(c'(\gamma'_{1}, \dots, \gamma'_{k}))= \xi_{2g(c'(\gamma'_{1}, \dots, \gamma'_{k}))}$, if k>0, $c' \in C'_{k}$ is such that c′(ξ ₁,…,ξ _k )≠l(c) for every c∈C _k , and $\gamma'_{i} \in L(C')$.

The substitution $\tau^{-1}_{g}: \varXi\to L(C')$ is the function defined by

• $\tau^{-1}_{g}(\xi_{2i+1}) = \xi_{i}$ and

• $\tau^{-1}_{g}(\xi_{2i}) = g^{-1}(i)$, for all $i \in\mathbb{N}$.

We shall denote by $\tau^{-1}_{g}$ the only extension of $\tau^{-1}_{g}$ to L(C). It can be proved that τ _g and $\tau^{-1}_{g}$ are inverses of each other. The function defined by

$$\hat{\tau_{g}}(A; \varGamma\succ\Delta; B ) = \bigl(A; \tau_{g}(\varGamma) \succ\tau_{g}(\Delta) ; B\bigr) $$

induces the function $\hat{\tau_{g}}:\mathcal {MP}_{\mathrm{fin}}(\mathcal{X} \cup L(C')) \to\mathcal{MP}_{\mathrm{fin}}(\mathcal{X} \cup L(C))$ in a natural way; and if we define

$$\hat{\hat{\tau_{g}}} \bigl(\langle\mathcal{H}; \mathcal{S}\rangle \bigr) = \bigl\langle \mathcal{H}; \hat{\tau}_{g}(\mathcal{S})\bigr\rangle , $$

it induces a function $\hat{\hat{\tau_{g}}}:\mathcal {MP}_{\mathrm{fin}}({\mathfrak{H}} \cup \mathit{Seq}(C')) \to\mathcal {MP}_{\mathrm{fin}}({\mathfrak{H}} \cup \mathit{Seq}(C))$.

Analogously, we define $\hat{\tau_{g}}^{-1}:\mathcal{MP}_{\mathrm{fin}}(\mathcal {X} \cup L(C)) \to\mathcal{MP}_{\mathrm{fin}}(\mathcal{X} \cup L(C'))$ and $\hat{\hat{\tau_{g}}}^{-1}:\mathcal{MP}_{\mathrm{fin}}({\mathfrak{H}} \cup \mathit{Seq}(C')) \to\mathcal{MP}_{\mathrm{fin}}({\mathfrak{H}} \cup \mathit{Seq}(C))$.

Remark 5.8

It is easy to see that $\hat{\tau_{g}}$ and $\hat{\tau_{g}}^{-1}$; and $\hat{\hat{\tau_{g}}}$ and $\hat{\hat{\tau_{g}}}^{-1}$ are inverse to each other, respectively.

Lemma 5.9

Let C and C′ be two signatures such that C≤ _l C′, and let $g: L(C') \to\mathbb{N}$ be a goedelization.

• (i) If σ′:Ξ→L(C′) is a substitution over C′, then $\bar{\sigma}:\varXi\to L(C)$ given by $\bar{\sigma}(\xi)= \tau_{g}(\sigma' (\xi))$ is a substitution over C such that $\hat{\bar{\sigma}}(\varphi)= \tau_{g}(\hat{\sigma}' (\hat{l}(\varphi )))$ for all φ∈L(C).

• (ii) If $\varrho':\mathcal{X} \to \mathcal{MP}_{\mathrm{fin}}(\mathcal {X} \cup L(C'))$ is an instantiation over C′ and $\hat{\tau_{g}}:\mathcal{MP}_{\mathrm{fin}}(\mathcal{X} \cup L(C')) \to \mathcal{MP}_{\mathrm{fin}}(\mathcal{X} \cup L(C))$ is defined as above, then the composite map $\bar{\varrho} = \hat{\tau _{g}} \circ\varrho'$ is an instantiation over C.

• (iii) If $\lambda':{\mathfrak{H}} \to \mathcal {MP}_{\mathrm{fin}}({\mathfrak{H}} \cup \mathit{Seq}(C'))$ is a sequent instantiation over C′ and $\hat{\hat{\tau_{g}}}:\mathcal {MP}_{\mathrm{fin}}({\mathfrak{H}} \cup \mathit{Seq}(C')) \to \mathcal{MP}_{\mathrm{fin}}({\mathfrak{H}} \cup \mathit{Seq}(C))$ is defined as above, then the composite map $\bar{\lambda} = \hat{\hat{\tau_{g}}} \circ\lambda'$ is a sequent instantiation over C.

• (iv) With the notation used in the above items, if h∈HSeq(C) then

  $$\hat{\hat{\tau_{g}}}\bigl(\bigl(\sigma', \varrho', \lambda'\bigr) \bigl(\hat{l}(h)\bigr)\bigr)=( \bar {\sigma}, \bar{\varrho},\bar{\lambda}) (h). $$

Proof

Straightforward. □

Using the above results we are now able to translate derivations.

Proposition 5.10

Let $\mathcal{A}=\langle C, R\rangle$ and $\mathcal{A}'=\langle C', R'\rangle$ be two chcs such that C≤ _l C′ and $\hat{l}(R) \subseteq R'$, and let ϒ∪{h}⊆HSeq(C′) such that h ₁…h _n is a derivation of h in $\mathcal{A}'$ from ϒ using exclusively rules from $\hat{l}(R)$. Then, $\hat{\hat{\tau _{g}}}(\varUpsilon) \vdash_{\mathcal{A}} \hat{\hat{\tau_{g}}}(h)$, for any goedelization $g:L(C') \to\mathbb{N}$. Moreover, $\hat{\hat{\tau_{g}}}(h_{1}) \dots \hat{\hat{\tau_{g}}}(h_{n})$ is a derivation of $\hat{\hat{\tau_{g}}}(h)$ in $\mathcal{A}$ from $\hat{\hat{\tau_{g}}}(\varUpsilon)$.

Proof

We shall use induction over the length m of the derivation. If m=1, then we have two possible cases:

• Case 1. h ₁∈ϒ and h ₁=h. Then, $\hat{\hat{\tau_{g}}}(h_{1}) \in\hat{\hat{\tau_{g}}}(\varUpsilon) \subseteq \mathit{HSeq}(C)$ and $\hat{\hat{\tau_{g}}}(h)=\hat{\hat{\tau_{g}}}(h_{1})$. Hence, $\hat{\hat{\tau_{g}}}(\varUpsilon) \vdash_{\mathcal{A}} \hat{\hat{\tau_{g}}}(h)$.

• Case 2. h ₁ is the image of an axiom of R. That is to say, there are an r∈R, r=〈∅,h′〉, a substitution σ′ over C′, an instantiation ϱ′ over C′ and a sequent instantiation λ over C′ such that $h_{1}=(\sigma', \varrho', \lambda')(\hat{l}(h'))$. By Lemma 5.9(iv), $\hat{\hat{\tau_{g}}}(h_{1}) = \hat{\hat{\tau_{g}}}((\sigma', \varrho', \lambda')(\hat{l}(h')))= (\bar{\sigma}, \bar{\varrho},\bar{\lambda})(h')$, where $\bar{\sigma}$, $\bar{\varrho}$ and $\bar{\lambda}$ are a substitution, an instantiation, and a sequent instantiation, respectively, over C. This means that $\vdash_{\mathcal{A}} \hat{\hat{\tau_{g}}}(h)$, and therefore $\hat{\hat{\tau_{g}}}(\varUpsilon)\vdash_{\mathcal{A}} \hat {\hat{\tau_{g}}}(h)$.

Suppose now that the assertion stands for derivations of length ≤m and let us see that it also stands for length m+1.

Let

$$h_1 \dots h_m h_{m+1} $$

be a derivation of h in $\mathcal{A}'$ from ϒ. Then $\hat{\hat{\tau_{g}}}(h_{1}) \dots\hat{\hat{\tau_{g}}}(h_{m})$ is a derivation of $\hat{\hat{\tau_{g}}}(h_{m})$ in $\mathcal{A}$ from $\hat{\tau_{g}}(\varUpsilon)$.

If either h _m+1 is the image of an axiom of R or it belongs to ϒ, the treatment is as above.

On the other hand, suppose that there are an r∈R, r=〈{g ₁,…,g _k },g′〉, a substitution σ′, an instantiation ϱ′, and a sequent instantiation λ′ on C′ such that $(\sigma', \varrho', \lambda') (\hat{l}(g_{j})) \in\{h_{1}, \dots, h_{m}\}$, for 1≤j≤k, and $(\sigma,' \varrho', \lambda')(\hat {l}(g'))=h_{m+1}=h$. Then, $\hat{\hat{\tau_{g}}}((\sigma', \varrho', \lambda')(\hat{l}(g_{j})))= (\bar{\sigma}, \bar{\varrho},\bar{\lambda})(g_{j}) \in\{\hat{\hat{\tau _{g}}}(h_{1}), \dots, \hat{\hat{\tau_{g}}}(h_{m})\}$, for 1≤j≤k, and $\hat{\hat{\tau_{g}}}((\sigma', \varrho', \lambda')(\hat {l}(g')))=(\bar{\sigma}, \bar{\varrho},\bar{\lambda})(g')= \hat{\hat{\tau_{g}}}(h_{m+1})=\hat{\hat{\tau_{g}}}(h)$, by Lemma 5.9(iv). By induction hypothesis, we may assert that

$$\hat{\hat{\tau_{g}}}(h_1) \dots\hat{\hat{ \tau_{g}}}(h_m) \hat{\hat{\tau _{g}}}(h_{m+1}) $$

is a derivation of $\hat{\hat{\tau_{g}}}(h)$ in $\mathcal{A}$ from $\hat{\hat{\tau_{g}}}(\varUpsilon)$. □

And conversely:

Proposition 5.11

Let $\mathcal{A}=\langle C, R\rangle$ and $\mathcal{A}'=\langle C', R'\rangle$ be two chcs such that C≤ _l C′ and $\hat{l}(R) \subseteq R'$, and let ϒ∪{h}⊆HSeq(C) such that h ₁…h _n is a derivation of h in $\mathcal{A}$ from ϒ. Then, $\hat{\hat{\tau_{g}}}^{-1}(h_{1}) \dots\hat{\hat{\tau_{g}}}^{-1}(h_{n})$ is a derivation of $\hat{\hat{\tau_{g}}}^{-1}(h)$ in $\mathcal{A}'$ from $\hat{\hat{\tau_{g}}}^{-1}(\varUpsilon)$, for any goedelization $g:L(C') \to\mathbb{N}$.

Proof

It is similar to the previous one. □

6 Extension to Constrained Fibring

In Sect. 3, we introduced the notion of unconstrained fibring in CHC, that is, the combination of two chcs without sharing any connectives. However, it is frequently necessary to combine logics while sharing some connectives. Here is when the constrained fibring appears. In this section, we shall introduce the notion of constrained fibring in the category CHC, generalizing the results of the previous sections.

Let C be a signature and let ≡⊆|C|×|C| be an equivalence relation on |C|. We shall say that ≡ is a signature congruence over C if it verifies the following condition:

$$c_1 \equiv c_2\quad \mbox{implies } c_1, c_2 \in C_n,\ \mbox{for some } n \in\mathbb{N}. $$

It is clear that $C/{\equiv} \, = \, \{C_{n}/{\equiv}\}_{n\in\mathbb{N}}$ is a signature. The canonical map q:|C|→L(C/≡) is the function defined as follows:

• q(c)=[c], if c∈C ₀,

• q(c)=[c](ξ ₁,…,ξ _n ), if c∈C _n , for n≥1

where [c] denotes the equivalence class of c by ≡. Clearly, q is a morphism q:C→C/≡ in Sig.

Definition 6.1

Let $\mathcal{A}=\langle C, R \rangle$ be a chc and let ≡ be a signature congruence over C. The quotient commutative hypersequent calculus (or simply the quotient calculus) determined by ≡ is the chc $\mathcal{A}/{\equiv} \, = \, \langle C/{\equiv}, R' \rangle$ such that

$$R'=\bigl\{ \hat{q}(r): r \in R\bigr\} . $$

It is clear that $\mathcal{A}/{\equiv}$ is indeed a commutative hypersequential calculus and that q induces a morphism $q:\mathcal{A} \to\mathcal{A}/{\equiv}$ in CHC.

Proposition 6.2

If $\mathcal{A}$ has the full r-elimination property, then so does $\mathcal{A}/{\equiv}$ for any congruence ≡.

Proof

Straightforward. □

Let $\mathcal{A}=\langle C, R \rangle$ and $\mathcal{A}'=\langle C', R' \rangle$ be two chcs to be combined by sharing the connectives in the signature $C\cap C' = \{C_{n}\cap C'_{n}\}_{n\in\mathbb{N}}$. Let inc:C∩C′→C and inc′:C∩C′→C′ be the inclusion morphisms. Consider now the coproduct C⊕C′ and the canonical injections i:C→C⊕C′, i′:C′→C⊕C′. Then, the relation ≡ given by

$${\equiv} = \bigl\{ \bigl(\bigl\lfloor i\circ \mathit{inc}(c)\bigr\rfloor , \bigl\lfloor i'\circ \mathit{inc}'(c)\bigr\rfloor \bigr): c \in C\cap C' \bigr\} \cup\bigl\{ \bigl(c',c'\bigr): c' \in\bigl(C \cup C'\bigr) \setminus C\cap C' \bigr\} $$

where $C\cup C' = \{C_{n}\cup C'_{n}\}_{n\in\mathbb{N}}$ and ⌊c(ξ ₁,…,ξ _n )⌋=c for any connective c, is a congruence over C⊕C′.

The constrained fibring of $\mathcal{A}$ and $\mathcal{A}'$ by sharing the symbols in C∩C′ is the chc

$$\mathcal{A}\mathop{\oplus}\limits^{{\ C\cap C'}}\mathcal{A}' = \bigl(\mathcal {A} \oplus\mathcal{A}'\bigr)/{\equiv}. $$

Observe that if c′∈(C⊕C′) _n , we have the following cases:

• (I) [c′]={⌊i∘inc(c)⌋,⌊i′∘inc′(c)⌋}, for $c\in(C_{n}\cap C'_{n})$;

• (II) [c′]={⌊i(c)⌋} for a unique $c \in C_{n}\setminus C'_{n}$;

• (III) [c′]={⌊i′(c)⌋} for a unique $c \in C'_{n}\setminus C_{n}$.

Example 6.3

Let |C|={¬,→,∧,∨,□} and |C′|={¬,→,&,∘}. Then,

Then, the formula $\overline{\square}_{1} \overline{\neg}_{1}( \, \xi_{1} \, \overline{\rightarrow}_{1} \, (\xi_{2} \, \overline{\&}_{2} \, \xi_{3}))$ of L((C ¹⊕C ²)/≡) stands for identifying the following formulas of L(C ¹⊕C ²):

• □₁¬₁( ξ ₁ →₁ (ξ ₂ &₂ ξ ₃)),

• □₁¬₁( ξ ₁ →₂ (ξ ₂ &₂ ξ ₃)),

• □₁¬₂( ξ ₁ →₁ (ξ ₂ &₂ ξ ₃)), and

• □₁¬₂( ξ ₁ →₂ (ξ ₂ &₂ ξ ₃)).

From Fact 5.5 and Proposition 6.2, we can state the following:

Fact 6.4

Let $\mathcal{A}$ a chc. If $\mathcal{A}$ has the full r-elimination property then so does $\mathcal{A}{\buildrel{\ C\cap C'} \over\oplus}\mathcal {A}'$, for every chc $\mathcal{A}'$.

7 The Non-commutative Case

In the previous section, ‘concrete’ sequents were considered as formed by pairs of (finite) multisets of formulas, while ‘concrete’ hypersequents were defined as (finite) multisets of sequents. It is a natural question how to generalize the previous approach to general (non-commutative) sequents and hypersequents, where finite sequences are taken instead of multisets. It is worth noting that the case of general sequents was already addressed in [8]. The aim of this section is to generalize the previous definitions and results to general hypersequents, composed of general sequents.

Given a set X, we denote by X ^∗ the set of all finite sequences formed by elements of X, and by X ² the Cartesian product X×X. The empty sequence is denoted by ϵ. The concatenation of two finite sequences s,s′∈X ^∗ is the finite sequence denoted by s⋅s′. Note that s⋅ϵ=ϵ⋅s=s, for every s∈X ^∗.

Recall from Sect. 2 that Ξ, $\mathcal{X}$ and $\mathfrak {H}$ are the set of scheme variables, context variables and sequent variables, respectively.

Definition 7.1

Let C be a signature. A general sequent (over C) is a pair of finite sequences whose elements are either formulas over C or elements of $\mathcal{X}$. The set of all general sequents over C will be denoted by GSeq(C). That is,

$$ \mathit{GSeq}(C) = \bigl(\bigl(L(C) \cup\mathcal{X}\bigr)^*\bigr)^2. $$

A general sequent $\langle s_{1} \dots s_{n},s'_{1} \dots s'_{m}\rangle$ will be usually written as $s_{1} \dots s_{n} \succ s'_{1} \dots s'_{m}$. The sequent 〈ϵ,ϵ〉 is called the bottom sequent, and it is denoted by ⊥ _s .

Definition 7.2

Let C be a signature. A general hypersequent (over C) is a finite sequence whose elements are either general sequents over C or elements of ${\mathfrak{H}}$. The set of all general hypersequents over C will be denoted by GHSeq(C). That is,

$$ \mathit{GHSeq}(C) = \bigl(\mathit{GSeq}(C) \cup{\mathfrak{H}}\bigr)^*. $$

A general hypersequent s ₁…s _n will be usually written as s ₁|⋯|s _n . The hypersequent ϵ is called the bottom hypersequent, denoted by ⊥ _h .

Definition 7.3

Let C be a signature. A (n-ary) inference rule of general hypersequents over C is a pair r=〈{h ₁,…,h _n },h〉 such that h _i ,h∈GHSeq(C). If n=0 then r is called an axiom. A general hypersequent calculus (ghc) is a pair $\mathcal{A}=\langle C, R\rangle$ where C is a signature and R is a finite set of inference rules of general hypersequents over C.

As it was done for chcs, rules of the form 〈{h ₁,…,h _n },h〉 and 〈∅,h〉 will be simply denoted by

$$\frac{ h_1 \quad \dots\quad h_n}{h} \quad \mbox{and}\quad \frac{\phantom{A}}{h}. $$

Recall that a substitution over a signature C is a map σ:Ξ→L(C), and that its unique homomorphic extension to L(C) is denote by $\hat{\sigma}:L(C) \to L(C)$. Additionally, if σ and σ′ are substitutions over C then σ⋅σ′ is the substitution over C given by $\sigma\cdot\sigma'(\xi)= \hat{\sigma} (\sigma'(\xi))$ which satisfies the following:

$$\widehat{\sigma\cdot\sigma'}= \hat{\sigma} \circ\hat{ \sigma}'. $$

Adapting [8] and the previous definitions of instantiation ϱ, sequent instantiation λ as well as the mappings of the form (σ,ϱ,λ):HSeq(C)→HSeq(C), we introduce the following notions to deal with inference rules of general hypersequents.

Definition 7.4

(Context substitutions)

Let σ be a substitution over C and let $\varrho:\mathcal{X} \to(L(C) \cup\mathcal{X})^{*}$ be a mapping (called context instantiation over C). A pair 〈σ,ϱ〉 is called a context substitution over C.

A context substitution μ=〈σ,ϱ〉 generates naturally a function $\bar{\mu}: L(C) \cup\mathcal{X} \to (L(C) \cup\mathcal{X})^{*}$ as follows: $\bar{\mu}(s)=\hat{\sigma}(s)$, if s∈L(C), and $\bar{\mu}(s)=\varrho(s)$, if $s \in\mathcal{X}$ (note that this is well-defined, since it is assumed that $L(C) \cap \mathcal{X}=\emptyset$). It induces a unique function $\tilde{\mu }:(L(C) \cup\mathcal{X})^{*} \to(L(C) \cup\mathcal{X})^{*}$ as follows: $\tilde{\mu}(s_{1}\dots s_{n})=\bar{\mu}(s_{1}) \dots\bar{\mu}(s_{n})$, for n≥0. Note that $\tilde{\mu}(\epsilon)=\epsilon$. Finally, the last mapping induces a unique function $\hat{\mu}: \mathit{GSeq}(C) \to \mathit{GSeq}(C)$ as expected: $\hat{\mu}(\langle s_{1} \dots s_{n},s'_{1} \dots s'_{m} \rangle )=\langle\tilde{\mu}(s_{1}\dots s_{n}), \tilde{\mu}(s'_{1}\dots s'_{m}) \rangle$. Observe that $\hat{\mu}(\bot_{\mathbf{s}})=\bot_{\mathbf{s}}$.

The following notion comes from [8]. Let μ=〈σ,ϱ〉 and μ′=〈σ′,ϱ′〉 be context substitutions over C, and consider the context instantiation (ϱ⋅ϱ′) _σ over C defined as follows: if $s \in\mathcal{X}$ and ϱ′(s)=s ₁…s _n then $(\varrho\cdot \varrho')_{\sigma}(s) = f^{\sigma}_{\varrho}(s_{1}) \cdots f^{\sigma }_{\varrho}(s_{n})$, where, for every $s' \in L(C) \cup\mathcal{X}$,

$$ f^{\sigma}_\varrho\bigl(s'\bigr) = \left \{ \begin{array}{l@{\quad}l} \varrho(s') & \mbox{if}\ s' \in\mathcal{X},\\ \hat{\sigma}(s') & \mbox{if}\ s' \in L(C) . \end{array} \right . $$

It is easy to prove that the context substitution μ″=〈σ⋅σ′,(ϱ⋅ϱ′) _σ 〉 over C is such that $\hat{\mu}'' = \hat{\mu} \circ\hat{\mu}'$.

Definition 7.5

(Sequent substitutions)

Let σ be a substitution over C, ϱ a context instantiation over C and let $\lambda:{\mathfrak{H}} \to \mathit{GHSeq}(C)$ be a mapping (called general sequent instantiation over C). A triple 〈σ,ϱ,λ〉 is called a sequent substitution over C.

A sequent substitution κ=〈σ,ϱ,λ〉 generates a function $\bar{\kappa}: \mathit{GSeq}(C) \cup{\mathfrak{H}} \to \mathit{GHSeq}(C)$ as follows: $\bar{\kappa}(s)=\widehat{\langle\sigma, \varrho\rangle}(s)$, if s∈GSeq(C), and $\bar{\kappa}(s)=\lambda (s)$, if $s \in{\mathfrak{H}}$. From this, a unique function $\hat {\kappa}:\mathit{GHSeq}(C) \to \mathit{GHSeq}(C)$ is defined as follows: $\hat{\kappa }(s_{1}\ldots s_{n})=\bar{\kappa}(s_{1}) \cdots\bar{\kappa}(s_{n})$, for n≥0. Note that $\hat{\kappa}(\bot_{\mathbf{h}})=\bot_{\mathbf{h}}$.

Now, let κ=〈σ,ϱ,λ〉 and κ′=〈σ′,ϱ′,λ′〉 be sequent substitutions over C, and consider the general sequent instantiation (λ⋅λ′) _σϱ over C defined as follows: if λ′(s)=s ₁…s _n then $(\lambda\cdot\lambda')_{\sigma \varrho}(s) = \theta^{\sigma\varrho}_{\lambda}(s_{1})\cdots\theta^{\sigma \varrho}_{\lambda}(s_{n})$, where, for every $s' \in \mathit{GSeq}(C) \cup {\mathfrak{H}}$,

$$\theta^{\sigma\varrho}_\lambda\bigl(s'\bigr) = \left \{ \begin{array}{l@{\quad}l} \lambda(s') & \mbox{if}\ s' \in{\mathfrak{H}},\\ \widehat{\langle\sigma,\varrho\rangle}(s') & \mbox{if}\ s' \in \mathit{GSeq}(C) . \end{array} \right . $$

It is immediate that the sequent substitution κ″=〈σ⋅σ′,(ϱ⋅ϱ′) _σ ,(λ⋅λ′) _σϱ 〉 over C is such that $\hat{\kappa}'' = \hat {\kappa} \circ\hat{\kappa}'$.

Now, we can define the notion of derivation in ghcs:

Definition 7.6

Let $\mathcal{A}=\langle C,R\rangle$ be a general hypersequent calculus over C and let ϒ∪{s}⊆GHSeq(C). We say that h is derivable in $\mathcal{A}$ from ϒ, and write $\varUpsilon \vdash_{\mathcal{A}} h$, if there is a finite sequence h ₁…h _n of elements of GHSeq(C) such that h _n =h and for all 1≤i≤n, either h _i ∈ϒ, or there exist an inference rule $r =\langle\{h'_{1}, \dots, h'_{k}\}, h'\rangle$ in R, a substitution σ, a context instantiation ϱ and a general sequent instantiation λ over C such that $(\sigma, \varrho, \lambda) (h'_{j}) \in\{ h_{1}, \dots, h_{i-1}\}$ (for 1≤j≤k) and (σ,ϱ,λ)(h′)=h _i . If ϒ=∅ we shall just say that h is provable in $\mathcal{A}$.

The category of general hypersequent calculi can now be defined.

If $s_{1} \dots s_{n} \succ s'_{1} \dots s'_{m}$ is a general sequent over C and f:C→C′ is a signature morphism, then $\hat{f}(s_{1} \dots s_{n} \succ s'_{1} \dots s'_{m})$ is, by definition, the general sequent $\bar{s}_{1} \dots\bar{s}_{n} \succ\bar{s}'_{1} \dots\bar{s}'_{m}$ over C′ where, for every $s \in L(C) \cup\mathcal{X}$, $\bar{s}$ is $\hat{f}(s)$, if s∈L(C), and s otherwise. This can be naturally extended to hypersequents:

$$\hat{f}(s_1 \dots s_n)=\tilde{s}_1 \dots \tilde{s}_n $$

where, for every $s \in \mathit{GSeq}(C) \cup{\mathfrak{H}}$, $\tilde{s}$ is $\hat{f}(s)$, if s∈GSeq(C), and s otherwise. It is clear that $\hat{f}(h)$ is a general hypersequent over C′ provided that h is a general hypersequent over C.

Definition 7.7

The category GHC of general hypersequent calculi is the category whose objects are general hypersequent calculi. A morphism f:〈C,R〉→〈C′,R′〉 in GHC is a morphism f:C→C′ in Sig such that, for every r=〈{h ₁,…,h _n },h〉 in R, it is verified that $\hat{f}(h)$ is derivable in 〈C′,R′〉 from $\{\hat{f}(h_{1}), \dots, \hat{f}(h_{n})\}$. The composition of morphisms and the identity morphism in GHC is defined as in Sig.

It should be clear that all the previous definitions and results on (constrained and unconstrained) fibring of chcs, translation of derivations and preservation theorems can be reproduced in the framework of general hypersequent calculi. We left the details to the interested reader.

8 Hypersequent Calculi and Hypertranslations

In [8], the notion of meta-fibring based on meta-translations was proposed. Within this framework, designed to deal with sequent calculi, every morphism f (called meta-translation) in the category of sequent calculi has the following property: every (formal) sequent rule of the form

$$(r) \quad \frac{ s_1\quad \dots\quad s_n}{s} $$

is preserved by f. By interpreting a sequent rule as above as a meta-property of the logic associated to the given calculus, a morphism f can be, therefore, seen as a translation between logics which preserves all the meta-properties as above. This was the startpoint of [8], additionally developed in [6], where meta-translations were called contextual translations. In [3], the notion of meta-translation was also used to analyze the combination of the logics of (classical) conjunction and disjunction.

The main difference between meta-translations and usual translations is that the latter just preserve simple metaproperties of the logic of the form Γ⊢φ, while the former preserves logical combinations of them described by sequent rules as above. As argued in [6], contextual translations refine the usual concept of translation between logics, helping to analyze the complex question of how a logic should be translated into another one as well as the question of how a logic can be extended faithfully. As it was proved recently, the simpler notion of conservative translation was shown not to be informative enough, since any two reasonable deductive systems can be conservatively translated into each other (cf. [14]). This is not obviously the case for meta-translations: in order to be contextually translatable, the target logic must satisfy at least all the structural rules satisfied by the source logic (see [6]). This is why the inclusion morphism between the sequent calculi INT for intuitionistic propositional logic and CPL, the sequent calculus for classical propositional logic, is a meta-translation and so INT can be considered a “good” sublogic of CPL, since every meta-property of the former is enjoyed by the latter (cf. [6]).

But things are not so simple. As it is well-known, Gödel was the first to observe (cf. [13]) that, unlike to what happens in classical logic, intuitionistic propositional logic has the disjunction property, namely:

$$\mbox{(DP)}\quad \mbox{If}\ (\alpha\vee\beta)\ \mbox{is a theorem, then}\ \alpha\ \mbox{is a theorem or}\ \beta\ \mbox{is a theorem.} $$

It is easy to see that (DP) cannot be expressed as a metaproperty in the language of (formal) sequents introduced in [8]. In fact, the metaproperty (DP) has the form

$$\frac{\vdash\alpha\vee\beta}{\vdash\alpha\quad \mbox{or} \quad \vdash\beta} $$

which lies outside the scope of the language of sequent rules of the form (r). In this perspective, INT could not be considered such a good sublogic of CPL since the former satisfies the metaproperty (DP) which is not satisfied by the latter. This distinction can be made precise within the framework of hypersequents.

Recall the notion of morphism in the category CHC of chcs given in Definition 2.9, as well as the definition of morphism in the category GHC of ghcs given in Definition 7.7. In both cases, every (formal) hypersequent rule of the form

$$\bigl(r'\bigr)\quad \frac{ h_1 \quad \dots \quad h_n}{h} $$

is preserved by such a morphisms. As it was done with sequents, an hypersequent rule as (r′) could be seen as a meta-property of the logic associated to the given calculus, but written in a richer (meta)language which allows expressing metaproperties such as (DP). In fact, (DP) can be represented by the following hypersequent rule:

$$\bigl(\mbox{DP}'\bigr)\quad \frac{\succ\xi_1 \vee\xi_2 }{\ \succ \xi_1\quad {|}\quad \succ\xi_2}. $$

By Definition 2.9 or 7.7, a morphism f will force the target logic to satisfy the following metaproperty:

$$\bigl(\mbox{DP}'\bigr) \quad \frac{\succ\varphi(\xi_1, \xi_2) }{\succ\xi_1 \quad {|}\quad \succ\xi_2} $$

where φ(ξ ₁,ξ ₂) is the formula associated by f to the disjunction operator ∨, and so $\hat{f}(\xi_{1} \vee\xi _{2})=\varphi(\xi_{1}, \xi_{2})$. In particular, if f is the inclusion morphism, the rule (DP) will be satisfied by the target logic, since in this particular case we have that $\hat{f}(\xi_{1} \vee\xi_{2})=\xi_{1} \vee\xi_{2}$. In other words, if intuitionistic propositional logic (presented as an hypersequent calculus) is extended through an inclusion morphisms of hypersequent calculi, the target calculus must also satisfy the disjunction property. This justify to call the morphisms of hypersequent calculus as hypertranslations.

From the above discussion, we believe that the present framework of formal hypersequent calculi can throw some light on the subject of translations between logics and its significance.

9 Concluding Remarks

The present paper generalizes in a natural way the formal treatment of sequent calculi and their fibring introduced in [8]. Additionally, some preservation features were analyzed. Finally, the relevance of this approach concerning the theory of translations between logics was stressed.

As observed in Remark 2.5, we propose here an intensional approach to inference rules, in contrast with the traditional, extensional approach to inference rules. Being so, a single linguistic object represents infinite concrete rules which are obtained by instantiation of their metavariables, that is, variables in the metalanguage. The advantage of using formal variables instead of informal metavariables is crucial in the context of combining logic systems: in our framework, the rules are prepared to be combined, being ready to accept new connectives by means of substitutions over the language resulting from the combination procedure.

Several other questions remain open, and deserve future research. The use of hypersequents instead of sequents opens interesting possibilities to the study of how a logic can be constructed (or deconstructed) from (into) its fragments, along the lines of the studies initiated in [8]. The preservation by fibring of some meta-properties of hypersequent calculi (interpolation, for instance) should also be addressed.