Consequence Relations and Admissible Rules

In this paper our aim is to provide a framework in which to reason about the admissibility of rules of inference. In most papers on admissibility consequence relations are taken as the fundamental notion via which to represent logics or theories, and in this paper we provide arguments that support this choice. None of these arguments are very deep or completely new, but we feel it is worthwhile to present them in detail because in the literature they remain mostly implicit.

One of the incentives to spell out the details of what in most papers is discussed only briefly (and for good reasons) is the phenomenon, as pointed out in [9], that admissibility is defined in two ways in the literature, in what we will call the full and the strict way. Given a theory or logic L and a rule R:

(full) :

R is admissible in L if L extended by R has the same theorems as L.

(strict) :

R is admissible in L if under all substitutions, whenever all premisses of R become theorems of L, then so does the conclusion.

In talks and informal expositions on admissibility the first definition is often used, while the second one seems to be preferred in formal settings. Informally, it is quite easy to argue that the two definitions are equivalent, but if one wishes to make this precise, several issues appear that need to be addressed. For example, in the full definition of admissibility one has to describe what it means to extend a theory or logic by a rule. If the theory is given to us via a proof system, this might be quite straightforward, but if the theory is characterized in another way, say via a set of models or algebras, it is less clear what is meant. In this paper we describe what this means in detail, in a way that is applicable in many settings.

As is common in the literature on admissible rules, we choose consequence relations as our general framework. Since Tarski, consequence relations are traditionally used in the literature to capture the notion of consequence in a very general way, abstracting away from particular theories and particular syntax [15, 17]. We describe the notion of a rule scheme (a rule with a set of substitutions) that captures, we think, what is generally meant by a rule of inference in a mathematical or logical context. Then we define what it means to extend a consequence relation by a set of rule schemes, which is a slight generalization of a similar notion that occurs at many places in the literature. And we show in Proposition 3 (a reformulation of a theorem in [14]) that in this way, derivations in the extension indeed are derivations that consist of inferences that either belong to the original consequence relation or are instances of the rules added in the extension. Thus supporting the claim that this is the correct way to define what it means to extend a consequence relation by a rule (scheme). Substitutions, as required for the strict definition of admissibility, are described in Section 2.3.

Finally, we address another issue in this paper, namely the analogue of the above definitions for multi–conclusion consequence relations. Such relations are useful in the setting of admissibility because they allow one to express the disjunction property, which is the property that if A ∨ B is a theorem, then so is one of the disjuncts. This property, satisfied by many constructive theories including intuitionistic logic, can be expressed via admissibility, provided admissibility is defined in one of the following two ways.

(dp-full) :

R is admissible in L if L extended by R has the same theorems as L.

(dp-strict) :

R is admissible in L if under all substitutions, whenever all premisses of R become theorems of L, then so does at least one formula in the conclusion.

Because in this way, {A ∨ B}/{A, B} is admissible in a logic if and only if the logic has the disjunction property.

In this paper we consider the following generalizations of the above notions that, we think, are the genuine analogues, in a multi–conclusion setting, of the single–conclusion notions.

(full) :

R is admissible in L if L extended by R has the same multi–conclusion theorems as L.

(strict) :

R = Γ/Δ is admissible in L if under all substitutions Σ and for all finite sets Σ, whenever σ A, Σ is a multi–conclusion theorem of L for all A ∈ Γ, then so is σ Δ, Σ.

At first sight, one might guess that the strict view would be

R :

is admissible in L if under all substitutions, whenever all expressions in the premiss of R become theorems of L, then the conclusion becomes a multi–conclusion theorem of L.

But in Proposition 6 it is shown that the full and strict definition above are equivalent, and Remark 1 explains why the alternative is not. Thus explaining our choice of the strict view.

In many papers on admissibility, the dp-full or dp-strict view is taken as the definition of admissibility. In Section 5 we explain how this choice naturally fits into our framework. Whether there are other reasonable strict definitions of admissibility in a multi–conclusion setting is an issue that we leave open for speculation and further research.

Several observations in Section 3 also occur in one way or another in the book on multiple–conclusion logic by Shoesmith and Smiley [14]. But as our approach differs in some respects from the one in that book, we have included proofs also of the theorems covered there. Metcalfe in [9] studies similar problems as the ones addressed in this paper, but then in an algebraic context. He also distinguishes the strict and full view, though using different terminology, and proves that in an algebraic setting these notions do not always coincide for multi–conclusion rules.

When Tarski spoke in Paris at the International Congress of Scientific Philosophy in 1935 on logical consequence [15], he tried to characterize in all generality what it means for a sentence A to logically follow from a set of sentences Γ. He arrived at the definition that this is so if and only if every model of the sentences in Γ is a model of A. This led to the introduction and study of consequence relations, which are relations between sets of expressions and expressions, that satisfy reflexivity, transitivity and weakening. The Polish School has been particularly active in the area of consequence relations, which is no coincidence given Tarski’s Polish background. See [17] for an overview of its results.

Consequence relations play a central role in this paper, as we assume all the theories or logics that we consider to be given by a consequence relation. This is no great restriction as they cover almost all reasonable theories. As said in the introduction, in this paper we want to define in detail what it means that a rule of inference is admissible in a certain theory. As this has more to do with consequence relations in general and the way in which they can be extended by rules, results about particular logics will be only discussed as illustration of the general theory. For an overview of the area of admissible rules, the reader is referred to the literature, in particular to Rybakov’s monograph [12]. For a brief overview of the main results in this area on intermediate and modal logics, see [6].

We start by defining what a consequence relation is. To maintain a certain level of generality we assume that there is a language \(\mathcal {L}\), which is a set of symbols, and that there is a set of expressions \(\mathcal {F}_{\mathcal {L}}\) in this language. In this way consequence relations can be about regular formulas as well as other expressions, such as sequents or clauses. In a setting where expressions are usually called formulas, we will do so too.

In the case of propositional logic, the language, \(\mathcal {L}_{p}\), consists of infinitely many propositional variables p, q, r, … , parentheses (and ), the connectives ¬, →, ∧, ∨ and the constants ⊤ and ⊥. The set of expressions \(\mathcal {F}_{\mathcal {L}_{p}}\) is the set of propositional formulas in language \(\mathcal {L}_{p}\), defined as usual. The language, \(\mathcal {L}_{s}\), for sequents in propositional logic consists of \(\mathcal {L}_{p}\) extended with ⇒, the braces { and } and the comma. \(\mathcal {F}_{\mathcal {L}_{s}}\) consists of the sequents in \(\mathcal {L}_{p}\), that is, of all expressions Γ ⇒ Δ, where Γ and Δ are finite sets of formulas in \(\mathcal {L}_{p}\). The language, \(\mathcal {L}_{f}\), of predicate or first-order logic consists of predicates and functions, for every arity infinitely many, infinitely many variables, parentheses (and ), the connectives ¬, →, ∧, ∨ , constants ⊤ and ⊥ and quantifiers ∃, ∀. The set of expressions \(\mathcal {F}_{\mathcal {L}_{f}}\) is the set of first-order formulas in language \(\mathcal {L}_{f}\), defined as usual.

2.1 Multi–conclusion Consequence Relations

Multi–conclusion consequence relations are relations ⊢ between sets of expressions. We write Γ ⊢ Δ if the pair (Γ, Δ) belongs to the relation. We also write Γ/Δ for the pair (Γ, Δ), and A, Γ or Γ, A for {A} ∪ Γ, and Γ, π for Γ ∪ π. A finitary multi–conclusion consequence relation (mcr) is a relation ⊢ between finite sets of expressions that satisfies for all finite sets of expressions Γ, Γ′, Δ, Δ′ and expressions A:

reflexivity :

{A} ⊢ {A},

weakening :

if Γ ⊢ Δ, then Γ′, Γ ⊢ Δ, Δ′,

transitivity :

if Γ ⊢ Δ, A and Γ′, A ⊢ Δ′, then Γ′, Γ ⊢ Δ, Δ′.

For the first and third property we use Scott’s terminology from [13], where multi–conclusion consequence relations of this form are introduced for the first time. The second property is called monotonic in Scott’s paper. In Shoesmith and Smiley’s [14] the first two properties are called overlap and dilution, respectively. Transitivity, which clearly is not equal to what is usually called transitive in the setting of relations, is a form of the Cut rule, which is why we sometimes refer to it as such.

A finitary single–conclusion consequence relation (scr) is a relation between finite sets of expressions and expressions satisfying the single–conclusion variants of the three properties above, where Γ ⊢ {A} is replaced by Γ ⊢ A:

reflexivity :

{A} ⊢ A,

weakening :

if Γ ⊢ A, then Γ′, Γ ⊢ A,

transitivity :

if Γ ⊢ C and Γ′, C ⊢ A, then Γ′, Γ ⊢ A.

Although most logics we discuss can be represented via a single–conclusion consequence relation, the multi–conclusion analogue allows us to express certain properties more naturally, such as the disjunction property discussed below. We often omit the word “finitary” in what follows, and when we speak about “consequence relations” we refer to both multi–conclusion and single–conclusion ones. Given a mcr ⊢ , its single–conclusion fragment ⊢ _s is defined as

The minimal single–conclusion and multi–conclusion consequence relations ⊢ _m and ⊢ _{m m} are defined as follows.

A is a theorem if ∅ ⊢ A, which we write as ⊢ A. The set of all theorems of a consequence relation is denoted by Th( ⊢ ) (called the logical system of the consequence relation in [17], page 46). Δ is a multi–conclusion theorem if ⊢ Δ, which is short for ∅ ⊢ Δ. The set of all multi–conclusion theorems is denoted by Thm( ⊢ ).

In [3] the following observations about the multi–conclusion analogue of single–conclusion consequence relations can be found. In order to cover languages without conjunction or disjunction we use \(\bigwedge \) and \(\bigvee \), which are defined as follows, also in the case the language contains conjunction and disjunction.

In case the language contains conjunction we express the conjunction of a set of formulas Γ as \(\bigwedge _{A \in \varGamma }A\) to distinguish it from the use of \(\bigwedge \) above, and similarly for disjunction. A single–conclusion consequence relation ⊢ can have several multi–conclusion analogues, meaning multi–conclusion consequence relations that have ⊢ as their single–conclusion fragment. The minimal and maximal one are:

The following lemma is but a slight reformulation of Theorem 2 in Došen’s [3].

Lemma 1

⊢ _min and ⊢ _max are multi–conclusion consequence relations and for any mcr ⊢′ such that \({\vdash }_{s}^{\prime } = \vdash \) : ⊢ _min ⊆ ⊢′ ⊆ ⊢ _max .

Proof

For the first statement we only show that ⊢_max is transitive. Therefore suppose that Γ ⊢_max A, Δ and Γ′, A ⊢_max Δ′ and consider a finite set of formulas π and formula B such that \(\varPi \vdash _{\textsf {min}} \bigwedge (\varGamma \cup \varGamma ^{\prime })\) and \(\varPi ,\bigvee (\varDelta \cup \varDelta ^{\prime }) \vdash _{\textsf {min}} B\). We have to show that π ⊢_min B. Observe that for π′ being π ∪ {A} we have \(\varPi ^{\prime } \vdash _{\textsf {min}} \bigwedge (\varGamma ^{\prime } \cup \{A\})\) and \(\varPi ^{\prime },\bigvee \varDelta ^{\prime } \vdash _{\textsf {min}} B\). Thus from Γ′, A ⊢_max Δ′ follows π′ ⊢_min B, which implies \(\varPi ,\bigvee (\varDelta \cup \{A\}) \vdash _{\textsf {min}} B\). Combining this with \(\varPi \vdash _{\textsf {min}} \bigwedge \varGamma \) and Γ ⊢_max A, Δ gives π ⊢_min B.

For the second statement, we first prove ⊢_min ⊆ ⊢ ′ . If Γ ⊢_min Δ, then Γ ⊢ A for some A ∈ Δ. And as the single–conclusion fragments of ⊢ ′ and ⊢ are equal, this gives \(\varGamma \vdash ^{\prime }_{s} A\). Hence Γ ⊢ ′Δ by weakening.

To prove that ⊢ ′ ⊆ ⊢_max , assume that Γ ⊢ ′Δ for some Γ and Δ. To prove that Γ ⊢_max Δ, consider arbitrary π, B such that \(\varPi \vdash _{\textsf {min}} \bigwedge \varGamma \) and \(\varPi ,\bigvee \varDelta \vdash _{\textsf {min}} B\). We have to show that π ⊢_min B. From \(\varPi \vdash _{\textsf {min}} \bigwedge \varGamma \) it follows that π ⊢ ′Δ, which combined with \(\varPi ,\bigvee \varDelta \vdash ^{\prime } B\) gives π ⊢ ′B. Hence π ⊢_min B. □

2.2 The Consequence Relation of a Logic

The following straightforward examples illustrate the way in which logics can be presented via consequence relations, showing that certain representations are far more natural than others.

Example 1

Let L be a logic with set of theorems Th(L). Then

defines a single–conclusion consequence relation of which the set of theorems is Th(L). There are other consequence relations that have Th (L) as the set of their theorems, such as

This is a consequence relation under some mild conditions on the logic. The same holds for the following consequence relation.

Example 2

Many logics are given by a semantics such that

defines a consequence relation. Examples are the Kripke model semantics for modal and intermediate logics.

Example 3

There are two ways in which consequence relations can capture a (multi–conclusion) sequent calculus G. First, as the definition of a consequence relation ⊢^G on finite sets of formulas, given by

For standard sequent calculi, such as G3 for classical propositional logic [16], ⊢^G3 indeed is a multi–conclusion consequence relation. The transitivity of ⊢^G3 follows from the cut-elimination theorem for G3.

Second, as a consequence relation between finite sets of sequents and sequents, where for sequents S ₀, … , S _n the single–conclusion relation ⊢ _G is defined as

Note that transitivity, or cut, on the level of the consequence relation is different from the cut rule on the level of sequents: (\(\mathcal {S}\) and \(\mathcal {S}^{\prime }\) are finite sets of sequents)

Since ⊢_G is a consequence relation, it satisfies transitivity. But the following statement in general does not hold.

If G is G3, for example, the statement is equivalent to the derivability of the Cut rule, well-known to be admissible but not derivable. The admissibility of the Cut Rule in G3 is the statement that the consequence relations ⊢_G3 and ⊢_G3+Cut have the same theorems.

Suppose a logic L is given to us not as a consequence relation but in another way, for example by a class of models or algebras. What does it mean to say that a consequence relation represents the logic? That depends very much on the application one has in mind. But let us say that a (single- or multi–conclusion) consequence relation ⊢ covers a logic if Th( ⊢ ) equals the set of theorems of the logic, which we denote by Th(L).

Clearly, there are many consequence relations that cover a single logic L. The smallest such single–conclusion consequence relation ⊢ has already been discussed in the examples above:

What the greatest consequence relation is that covers L we shall see in Section 4 (Corollary 5).

For logics L being extensions of IPC or IQC (including extensions in a richer language, such as modal logics), we single out one particular single–conclusion consequence relation, denoted by ⊢_L, that covers L as follows (\(\bigwedge \emptyset \) equals ⊤):

Similarly, we define one particular multi–conclusion consequence relation, also denoted by ⊢_L, that covers L:

One could define these specific consequence relations for any logic containing implication, disjunction, and conjunction, but as we prefer to not address, in this note, the delicacies that arise in the setting of substructural logics, we define ⊢_L here only for the logics L mentioned above.

2.3 Substitutions

Since we will be mostly interested in rules closed under certain substitutions, we need to explain which substitutions we consider. If one would wish to present the matter as formal as possible one should introduce two languages, the meta-language \(\mathcal {L}_{m}\), also called the schematic language, and the object-language \(\mathcal {L}_{o}\), where all elements of the meta-language belong to the object language except possibly the meta-variables. We use the word meta to distinguish the variables from the regular variables that may occur in the object language. Substitutions are then maps from formulas in the meta-language to formulas in the object-language that commute with all non-meta-variable symbols and are the identity on constants, if any are present. In this way every logic comes with a notion of meta-language and object-language and corresponding set of substitutions Sub.

In the case of pure propositional or predicate logic the two languages are often mixed and considered as one. For example, substitutions in propositional logic are often considered to be maps on formulas commuting with the connectives. In this paper we will do so too where possible. So when talking about propositional or predicate logic, \(\mathcal {L}_{m} = \mathcal {L}_{o}\) and the atoms, respectively the atomic formulas, have a double role in that they are treated as meta-variables (in the meta-language) as well as atoms (in the object-language).

In predicate logic, there is a subtlety concerning regular variables, as illustrated by the rule for the introduction of the universal quantifier:

Here A(x) is a meta-variable and we have to indicate what formulas may be substituted for it. Clearly, there have to be some restrictions. For example, if B(x) is substituted for A(x), then B(y) should be substituted for A(y), and so on. However, for this exposition the actual choice is not relevant, and therefore will not be discussed any further.

In order to be able to express side condition such as “y is not free in A(x)” we introduce a generalization of rules, called rule schemes, in Section 3.1.

A consequence relation is structural (uniform in [1] and closed under substitution in [14]) if it satisfies

structurality :

if Γ ⊢ Δ, then σ Γ ⊢ σ Δ for all σ ∈ Sub.

Typically, schematic systems are structural consequence relations, such as Gentzen calculi, Hilbert systems or natural deduction.

3.1 Rules and Schemes

A multi–conclusion rule is an ordered pair of finite sets of expressions, written Γ/Δ or

for finite sets of expressions Γ and Δ. It is sharp if |Δ| ≤ 1. If no confusion is possible we write A/B for {A}/{B}. A single–conclusion rule is an ordered pair consisting of a finite set of expressions and an expression, written Γ/A or

Γ is the assumption(s) or premiss of rule Γ/Δ and Δ is its conclusion. For R = Γ/Δ, σ R is short for σ Γ/σ Δ, and similarly for sets of rules.

Given a multi–conclusion consequence relation ⊢ , rules Γ/Δ such that Γ ⊢ Δ are the rules of the consequence relation and Ru_⊢ denotes the set of rules of ⊢ . The rules of a single–conclusion consequence relation are defined in a similar way, replacing Δ by A.

Sometimes rules come with restrictions, such as the following atomic contraction rule and the universal quantifier rule in sequent calculi.

To capture these rules in our setting we use the notion of a rule scheme, which is a pair (R, S) consisting of a rule R and a set of substitutions S ⊆ S u b. Like rules and sets of rules, rule schemes and sets of rule schemes will be denoted by R and \(\mathcal {R}\) respectively, trusting that it will always be clear from the context whether the symbol refers to rules or schemes. Also, a rule R is sometimes considered as a rule scheme (R, {i d}), where id is the identity substitution.

The following definitions apply to single–conclusion as well as multi–conclusion rule schemes, where in the fist case one should read A for Δ. For σ ∈ S, a rule σ R is called an instance of the rule scheme (R, S), as well as an instance of the rule R. We define the set of rules that are instances of a rule scheme in \(\mathcal {R}\) as follows:

Given a set \(\mathcal {R}\) of rule schemes, the extension \(\vdash ^{\mathcal {R}}\) of a consequence relation ⊢ by these rule schemes is defined to be the smallest consequence relation extending ⊢ for which Γ ⊢ Δ holds for all Γ/Δ in \(\textsf {Ru}_{\mathcal {R}}\). When all rule schemes in \(\mathcal {R}\) have the same set of substitutions S we sometimes write \({\vdash }_{S}^{\mathcal {R}^{\prime }}\) for \(\vdash ^{\mathcal {R}}\), where \(\mathcal {R}^{\prime }\) is the set of rules that occur in the schemes in \(\mathcal {R}\). In case of a single rule scheme (R, S) we write \({\vdash }_{S}^{R}\) for ⊢^{{(R, S)}}.

Similar to the definition for consequence relations in Section 2.2, a set of rules \(\mathcal {R}\) is said to cover a logic L if the smallest consequence relation containing \(\mathcal {R}\) covers L, that is, if Th \(({\vdash }_{\!\!\!{m}}^{\mathcal {R}}) = \) Th(L), where ⊢ _m is defined in Section 2.1. Naturally, a consequence relation ⊢ covers a set of rules \(\mathcal {R}\) is then defined to mean that Th ( ⊢ ) = Th(\(\vdash _{\!\!\!{m}}^{\mathcal {R}}\)).

3.2 Derivations

Given a set \(\mathcal {R}\) of rules (schemes), a sequence of expressions A ₁, … , A _n is a single–conclusion derivation of Γ/A in \(\mathcal {R}\) if A _n = A and for all A _i ∉ Γ there are i ₁, … , i _m < i such that \(A_{i_{1}},\dots , A_{i_{m}}/A_{i}\) belongs to \(\textsf {Ru}_{\mathcal {R}}\). In this case we also say that rule Γ/A is derivable in \(\mathcal {R}\), that A follows from Γ or that Γ derives A in \(\mathcal {R}\). A single–conclusion derivation of Γ/Δ is a single–conclusion derivation of Γ/A, for some A ∈ Δ. (In [14] (p.25) the word deducible instead of derivable is used.) Observe that the definition applies to sets \(\mathcal {R}\) of single–conclusion as well as multi–conclusion rules. What is single–conclusion derivable from \(\mathcal {R}\) is determined by its “‘single–conclusion fragment”, which means by the rules in \(\mathcal {R}\) that have a single expression (or singleton set) as conclusion.

Most of Section 3.1 is dedicated to proving (Propositions 2 and 3) that extending a (singular) consequence relation by a set of (sharp) rule schemes is the same as allowing these rules in derivations: \(\varGamma \vdash ^{\mathcal {R}} \varDelta \) if and only if Γ/Δ has a derivation in \(\textsf {Ru}_{\vdash } \cup ~\textsf {Ru}_{\mathcal {R}}\).

For multi–conclusion rules that are not sharp, the analogue of a derivation uses trees [14]. Here a tree T is a labelled tree in the usual sense that contains at least two nodes and has a root. In order to have a closer resemblance to standard proofs, trees are considered upside down, so with the root (the assumptions) at the top, above all other nodes, and the conclusions at the bottom. Every node k has a label lb(k), which is a set that is empty or consists of a single expression, except the root, which has a set of expressions or the empty set as label. The leaves of T are the nodes with no successors, where k is a successor of l if k is below l. It is an immediate successor of l if it is immediately below l. k is predecessor of l if l is a successor of k. The set of leaves is denoted by lf(T), and lb(T) denotes the union of the labels at the leaves of T. For a node k, k ↑ denotes the set consisting of k and all its predecessors, and lb^↑(k) is the union of the labels at k and its predecessors.

Given a set \(\mathcal {R}\) of rule schemes, a tree T with root r is a multi–conclusion derivation of Γ/Δ in \(\mathcal {R}\) if T is finite, lb(r) ⊆ Γ, lb(T) ⊆ Δ and for every node k whose immediate successors are k ₁, … , k _n , there is a set Γ′ ⊆ lb^↑(k) such that Γ′/lb(k ₁) ∪ ⋯ ∪ lb(k _n ) belongs to \(\textsf {Ru}_{\mathcal {R}}\).

The definition of a multi–conclusion derivation is slightly awkward because of the different reading of assumption (conjunctive) and conclusion (disjunctive) of a rule. This problem would disappear once assumptions consisting of several sets are allowed, but this level of generality is not needed for our purposes.

As for single–conclusion rules, we show in Proposition 4 that extending a consequence relation by a set of multi–conclusion rules is the same as allowing these rules in derivations: \(\varGamma \vdash ^{\mathcal {R}} \varDelta \) if and only if Γ/Δ has a multi–conclusion derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\).

When we speak of derivations we mean single–conclusion derivations. Multi–conclusion derivations will always be indicated by their full name, so that no confusion can arise.

3.3 Example

Suppose that \(\mathcal {R}\) consists of the rule schemes

The second rule scheme is in fact a set of rule schemes, one for each implication (A → B) that holds in intuitionistic logic. The following is a derivation of the Scott rule (¬¬A → A) → A ∨ ¬A/{¬A,¬¬A} in \(\mathcal {R}\).

In agreement with what has been stated above, the above tree has its root at the top, and nodes are depicted by their labels. Thus in this picture the root has three successors, which each have one successor. In Section 4.1 (Example 5) the special role that \(\mathcal {R}\) plays in intuitionistic logic will be discussed.

The following example from [14] (Figure 3.4) is a multi–conclusion derivation of B from ¬¬B in a set of multi–conclusion rules that contains the rules {A,¬A}/∅ and ∅/{A, ¬A}.

In Proposition 4 below we need the following lemma, which proves the admissibility of cut for multi–conclusion derivations.

Lemma 2

If Γ/Δ, A and Γ′, A/Δ′ have multi–conclusion derivations in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\) , then Γ, Γ′/Δ,Δ′ has a multi–conclusion derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\).

Proof

Suppose that Γ/Δ, A and Γ′, A/Δ′ have respective multi–conclusion derivations T ₁ and T ₂ in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\). We have to show that Γ, Γ′/Δ, Δ′ has a multi–conclusion derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\). Let r _i be the root of T _i . If A is not an element of lb(T ₁), then T ₁ is a multi–conclusion derivation of Γ, Γ′/Δ, Δ′. And if A does not belong to lb(r ₂), then T ₂ is a multi–conclusion derivation of Γ, Γ′/Δ, Δ′. Therefore suppose that A ∈ lb(T ₁)∩lb(r ₂). Now let T be the tree obtained by glueing the root of T ₂ to all the leaves of T ₁ with label {A}, and let the label of this node remain {A}. All other labels remain as they were, except for the root, which receives label Γ ∪ Γ′ in T. It is not difficult to see that T is a multi–conclusion derivation of Γ, Γ′/Δ, Δ′ in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\). □

3.4 Derivations and Consequence Relations

We show that in case the underlying multi–conclusion consequence relation is singular ^{Footnote 1}, meaning that

for any set \(\mathcal {R}\) of single–conclusion rule schemes, the consequence relation \(\vdash ^{\mathcal {R}}\) captures precisely the idea of adding the rule schemes \(\mathcal {R}\) to the consequence relation: \(\varGamma \vdash ^{\mathcal {R}} \varDelta \) if and only if Γ/Δ has a single–conclusion derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\). That is, \(\varGamma \,\vdash ^{\mathcal {R}} \varDelta \) if and only if some A ∈ Δ can be derived from Γ using only inferences that are instances of the rule schemes in Ru _⊢ and \(\mathcal {R}\). We will see in Proposition 3 that a similar statement holds for single–conclusion consequence relations.

If Eq. 1 holds for empty Γ, ⊢ is said to be saturated. For a logic L that contains disjunction and a consequence relation ⊢ that covers it: if ⊢ Δ is equivalent to \(\vdash \bigvee \varDelta \), then ⊢ is saturated if and only if L has the disjunction property. Thus the multi–conclusion consequence relation ⊢_IPC as defined in Section 2.2 is saturated but not singular.

Given a relation X between finite sets of expressions, the weakening closure and cut closure of X are defined respectively as follows:

Proposition 1

\(\,\vdash ^{\mathcal {R}} = \text {cc}(\text {wc}(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}))\).

Proof

Denote \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\) by X. We prove the proposition by showing that cc(wc(X)) is a consequence relation. Since it clearly is contained in \(\,\vdash ^{\mathcal {R}}\), the minimality condition on \(\,\vdash ^{\mathcal {R}}\) implies that \(\,\vdash ^{\mathcal {R}}\) is actually equal to cc(wc(X)).

To show that cc(wc(X)) is a consequence relation, it suffices to show that it is closed under weakening and cut, that is, that cc(wc(cc(wc(X)))) = cc(wc(X)). Because of the definition of cut closure, it suffices to show that wc(cc(wc(X))) = cc(wc(X)). This follows if for all i, wc(cc _i (wc(X))) = cc _i (wc(X)), the proof of which is straightforward. □

Proposition 2

For any singular multi–conclusion consequence relation ⊢ and any set \(\mathcal {R}\) of sharp multi–conclusion rule schemes: \(\varGamma \,\vdash ^{\mathcal {R}} \varDelta \) if and only if Γ/Δ has a derivation in Ru _⊢ ∪ Ru \(_{\mathcal {R}}\).

Proof

For the direction from right to left it suffices to show that for any derivation A ₁, … , A _m of Γ/Δ in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\), for all i we have \(\varGamma \,\vdash ^{\mathcal {R}} A_{i}\), a proof that is left to the reader. For the other direction we use the equivalence from Proposition 1 stating that \(\vdash ^{\mathcal {R}}\) is equal to \(\text {cc}(\text {wc}(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}))\). The rules in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\) clearly have a derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\) because the rules in \(\mathcal {R}\) are sharp and ⊢ is saturated. Therefore it suffices to show that if all rules in X have a derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\), then so do all rules in wc(X) and cc _i (X) for all i.

We only show that if all rules in cc _i (X) have a derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\), then so do all rules in cc _i+1(X), and leave the rest of the proof to the reader. Consider rules Γ/Δ, A and Γ′, A/Δ′ in cc _i (X) with respective derivations A ₁, … , A _m and B ₁, … , B _n . We show that there exists a derivation of Γ, Γ′/Δ, Δ′ in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\). If A _m ≠ A, then A ₁, … , A _m is a derivation of Γ, Γ′/Δ, Δ′. And if for no i ≤ n, B _i equals A, then B ₁, … , B _n is a derivation of Γ, Γ′/Δ, Δ′.

Therefore suppose that A = A _m and that A occurs in B ₁, … , B _n−1. We show that A ₁, … , A _m , B ₁, … , B _n is a derivation of Γ, Γ′/Δ, Δ′ in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\). Consider a C ∉ Γ ∪ Γ′ in the derivation. If C is A _i , then it follows immediately that there are i ₁, … , i _k <i such that \(A_{i_{1}},\dots , A_{i_{k}}/C\) is in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\), as A ₁, … , A _m is a derivation. If C = B _i , then either C ≠ A or C = A. In the first case C ∉ Γ′ ∪ {A}, and as B ₁, … , B _n is a derivation, there are i ₁, … , i _k <i such that \(B_{i_{1}},\dots , B_{i_{k}}/C\) is in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\). In the second case, A _m /C is in Ru_⊢ because consequence relations are reflexive. □

The following theorem can be found in [14] (Theorem 1.13). The proof given there is different from the one below, but both proofs are quite straightforward.

Proposition 3

For any single–conclusion consequence relation ⊢ and any set \(\mathcal {R}\) of single–conclusion rule schemes: \(\varGamma \vdash ^{\mathcal {R}} A\) if and only if Γ/A has a derivation in Ru _⊢∪ Ru \(_{\mathcal {R}}\).

Proof

For ⊢ and \(\mathcal {R}\) as in the proposition, the consequence relation ⊢_min is a singular multi–conclusion consequence relation and \(\mathcal {R}_{\textsf {min}} =\{ \varGamma /\{A\} \mid \varGamma /A \in \mathcal {R} \}\) is a set of sharp multi–conclusion rules. Therefore by Proposition 2,

It is not hard to see that this implies what we have to show once we have established that

To prove (2) it suffices, by Lemma 1, to prove that

Note that \(\varGamma /A \in \textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\) if and only if \(\varGamma /\{A\} \in \textsf {Ru}_{\vdash _{\textsf {min}}} \cup \textsf {Ru}_{\mathcal {R}_{\textsf {min}}}\).

⇒: Since \(\text {cc}\left (\text {wc}\left (\textsf {Ru}_{\vdash _{\textsf {min}}} \cup \textsf {Ru}_{\mathcal {R}_{\textsf {min}}}\right )\right )\) is a consequence relation that contains \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\) and \(\vdash ^{\mathcal {R}}\) is by definition the smallest consequence relation containing Ru \(\cup \textsf {Ru}_{\mathcal {R}}\), this inclusion follows.

⇐: Consider \(R = \varGamma /\{A\} \in \text {cc}\left (\text {wc}\left (\textsf {Ru}_{\vdash _{\textsf {min}}} \cup \textsf {Ru}_{\mathcal {R}_{\textsf {min}}}\right )\right )\). We have to show that \(\varGamma \vdash ^{\mathcal {R}} A\). If \(R \in \textsf {Ru}_{\vdash _{\textsf {min}}} \cup \textsf {Ru}_{\mathcal {R}_{\textsf {min}}}\), then \(\varGamma \vdash ^{\mathcal {R}} A\) follows by definition. Suppose \(R \in \text {wc}\left (\textsf {Ru}_{\vdash _{\textsf {min}}} \cup \textsf {Ru}_{\mathcal {R}_{\textsf {min}}}\right )\) and let \(\varGamma ^{\prime }/\varDelta \in \textsf {Ru}_{\vdash _{\textsf {min}}} \cup \textsf {Ru}_{\mathcal {R}_{\textsf {min}}}\) be such that Γ′ ⊆ Γ and Δ ⊆ {A}. Since no rules in \(\text {cc}\left (\text {wc}\left (\textsf {Ru}_{\vdash _{\textsf {min}}} \cup \textsf {Ru}_{\mathcal {R}_{\textsf {min}}}\right )\right )\) have an empty conclusion, Δ = {A}. As just observed, \(\varGamma ^{\prime } \vdash ^{\mathcal {R}} A\). Therefore \(\varGamma \vdash ^{\mathcal {R}} A\) as well. If \(R \in \text {cc}\left (\text {wc}\left (\textsf {Ru}_{\vdash _{\textsf {min}}} \cup \textsf {Ru}_{\mathcal {R}_{\textsf {min}}}\right )\right )\), let Γ ₁/{B} and Γ ₂ ∪ {B}/{A} be elements of \(\text {wc}\left ({\textsf Ru}_{\vdash _{\textsf min}} \cup {\textsf Ru}_{\mathcal { R}_{\textsf {min}}}\right )\) such that Γ = (Γ ₁ ∪ Γ ₂). We just saw that then \(\varGamma _{1} \vdash ^{\mathcal {R}} B\) and \(\varGamma _{2},B \vdash ^{\mathcal {R}} A\). Hence \(\varGamma \vdash ^{\mathcal {R}} A\) also in this case. □

The following proposition is the analogue of Proposition 2 for multi–conclusion consequence relations that are not singular. It occurs as Theorem 3.5 in [14], but the proof here is different from the one provided there, due to the fact that consequence relations are there defined in an equivalent but different way than in this note.

Proposition 4

For any multi–conclusion consequence relation ⊢ and any set \(\mathcal {R}\) of multi–conclusion rule schemes: \(\varGamma \vdash ^{\mathcal {R}} \varDelta \) if and only if Γ/Δ has a multi–conclusion derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\).

Proof

⇐ First observe that any multi–conclusion derivation T in \({\textsf Ru}_{\vdash } \cup ~\textsf {Ru}_{\mathcal {R}}\) of Γ/Δ is a multi–conclusion derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\) of Γ/lb(T) as well. As \( \vdash ^{\mathcal {R}}\) is closed under weakening, it therefore suffices to show, for any multi–conclusion derivation T of Γ/lb(T) in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\) with root r, that \(\varGamma \vdash ^{\mathcal {R}} \text {lb}(T)\). We show this by proving for every node k in T of depth ≥1 that \(\varGamma ,\text {lb}^{\uparrow }(k) \vdash ^{\mathcal {R}} \text {lb}(T_{k})\), where T _k is the subtree of T generated by k, so with root k. This will prove the desired, as lb^↑(r) ⊆ Γ and T _r = T. We use induction to the depth of k, which is the maximal distance to any of its successors.

If k has depth 1, then T _k consists of root k and leaves k ₁, … , k _n , \(\text {lb}(T_{k}) = \bigcup _{i} \text {lb}(k_{i})\) and by definition Γ′ ⊆ lb^↑(k) exists such that \(\varGamma ^{\prime }/\bigcup _{i} \text {lb}(k_{i})\) belongs to \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\), which clearly implies \(\varGamma ,\text {lb}^{\uparrow }(k) \vdash ^{\mathcal {R}} \text {lb}(T_{k})\).

Suppose k has depth greater than 1 and immediate successors k ₁, … , k _m . Observe that \(\text {lb}(T_{k}) = \bigcup _{i=1}^{m} \text {lb}(T_{k_{i}})\) and k ↑ = k _i ↑∖{k _i } for all i. The induction hypothesis gives \(\varGamma ,\text {lb}^{\uparrow }(k_{i}) \vdash ^{\mathcal {R}} \text {lb}(T_{k_{i}})\). Because \(\varGamma ,\text {lb}^{\uparrow }(k) \vdash ^{\mathcal {R}} \text {lb}(k_{1})\cup \dots \cup \text {lb}(k_{m})\) by the definition of T, this implies \(\varGamma ,\text {lb}^{\uparrow }(k) \vdash ^{\mathcal {R}} \text {lb}(T_{k})\) by weakening in case all lb(k _i ) are empty. In case some lb(k _i ) are not empty, one can use the transitivity of consequence relations to obtain \(\varGamma ,\text {lb}^{\uparrow }(k) \vdash ^{\mathcal {R}} \bigcup _{i=1}^{m} \text {lb}(T_{k_{i}})\). Thus in both cases we have \(\varGamma ,\text {lb}^{\uparrow }(k) \vdash ^{\mathcal {R}} \text {lb}(T_{k})\), which is what had to be shown.

⇒ By Proposition 1 it suffices to show that any Γ/Δ in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\) has a multi–conclusion derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\), and if all rules in X have a multi–conclusion derivation in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\), then so do wc(X) and cc _i (X) for all i. We prove the first and the last statement.

For the first statement, suppose that Γ/Δ belongs to \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\), where Δ = {A ₁, … , A _n } is not empty. Then the following tree is a multi–conclusion derivation of it.

In case Δ = ∅, the multi–conclusion derivation looks as follows.

For the last statement it suffices to show that if Γ/Δ, A and Γ′, A/Δ′ have multi–conclusion derivations in \(\textsf {Ru}_{\vdash } \cup \textsf {Ru}_{\mathcal {R}}\), then so does Γ, Γ′/Δ, Δ′. This is exactly what is proven in Lemma 2. □

3.5 Hilbert Systems

In Section 2.2 we saw that for a consequence relation to cover a logic, the only requirement is that it has the same theorems as the logic. Sometimes a logic is given to us in such a way that one wonders whether a closer connection between a consequence relation and the logic exists. This is especially the case with Hilbert systems [16].

Hilbert systems are given as a set of axioms and rules, which in our terminology are rule schemes, where the set of substitutions for every rule is the maximal one, Sub. For example, a Hilbert system for the implication fragment of intuitionistic propositional logic is given by the set \(\mathcal {R}\) consisting of Modus Ponens and the Łukasiewicz axioms

where Sub is the substitution set of every rule. A proof of A from Γ is then thought of as a sequence of formulas in which every formula either is in Γ or follows via the rules in \(\mathcal {R}\) from formulas earlier in the sequence, which in our terminology (Section 3.2) amounts to: Γ/A has a derivation in \(\textsf {Ru}_{\mathcal {R}}\). For example, the following sequence is a proof of D → D from empty assumptions, where E abbreviates D → D.

We therefore say that a consequence relation ⊢ faithfully covers the Hilbert system given by \(\mathcal {R}\) if Γ ⊢ A holds exactly if Γ/A has a derivation in \(\textsf {Ru}_{\mathcal {R}}\). Recall that in Section 3.1 ⊢ is said to cover \(\mathcal {R}\) if \(\textsf {Th}\vdash =\textsf {Th}(\vdash ^{\mathcal {R}})\), where \({\vdash }_{\!\!\!m}^{\mathcal {R}}\) stands for the minimal single–conclusion consequence relation defined in Section 2.1. The following corollary of Proposition 3 shows that if a Hilbert system is given by \(\mathcal {R}\), then \({\vdash }_{\!\!\!m}^{\mathcal {R}}\) faithfully covers it. The discussion below the corollary shows that not all coverings are faithful.

Corollary 1

For any set \(\mathcal {R}\) of single–conclusion rule schemes: \(\varGamma {\vdash }_{\!\!\!{m}}^{\mathcal {R}} A\) if and only if Γ/A has a derivation in \(\textsf {Ru}_{\mathcal {R}}\).

Proof

Because of Proposition 3 it suffices to show that a derivation in \({\textsf Ru}_{\vdash _{\!\!m}} \cup \textsf {Ru}_{\mathcal {R}}\) is a derivation in \(\textsf {Ru}_{\mathcal {R}}\), a proof that we leave to the reader. □

In Section 2.2, for logics L being extensions of IPC or IQC (including extension in a richer language, such as modal logics), the consequence relation ⊢_L is defined as Γ ⊢_L A if and only if \((\bigwedge _{B \in \varGamma }B \rightarrow A)\in \) Th(L). Suppose that L is covered by the Hilbert system \(\mathcal {R}\), then in general ⊢_L does not need to be equal to \({\vdash }_{\!\!\!m}^{\mathcal {R}}\). For example, if \(\mathcal {R}\) consists only of the theorems of L, thus only of axioms, then \(\varGamma {\vdash }_{\!\!\!m}^{\mathcal {R}} A\) will only hold if A ∈ Γ or A ∈ Th(L), while Γ ⊢_L A will hold in many more cases, such as in A, B ⊢_L A∧B or A ⊢_L A ∨ B. The following proposition shows that, if \(\mathcal {R}\) contains Modus Ponens and a rule for conjunction, \(\vdash _{\textsf {L}} \subseteq {\vdash }_{\!\!\!m}^{\mathcal {R}}\) does in fact hold. Thus this holds in particular for Hilbert systems containing these two rules.

Proposition 5

For any logic L that is an extension of IPC or IQC that is covered by a set of rules \(\mathcal {R}\) that contains the rule schemes ((B,C/B∧C),Sub) and Modus Ponens ((B → C, B/C), Sub): \(\vdash _{\textsf {L}} \subseteq \vdash _{\!\!\!m}^{\mathcal {R}}\).

Proof

Suppose for some Γ and A that Γ ⊢_L A, which means that \((\bigwedge _{B \in \varGamma }B) \rightarrow A\) belongs to Th(L). Since L is covered by \(\mathcal {R}\), \((\bigwedge _{B \in \varGamma }B) \rightarrow A\) is an element of \(\textsf {Th}(\vdash _{\!\!\!m}^{\mathcal {R}})\). By the first condition on \(\mathcal {R}\), \(\varGamma {\vdash }_{\!\!\!m}^{\mathcal {R}} \bigwedge _{B \in \varGamma }B\). By the second condition and the transitivity of consequence relations, \(\varGamma {\vdash }_{\!\!\!m}^{\mathcal {R}} A\) follows. □

In this section we introduce the two notions, derivability and admissibility, that were the motivation for spelling out the details of consequence relations in the previous sections. Intuitively, derivable rules are the rules explicitly given by the consequence relation, while admissible rules can be used in proofs without changing the theorems that can be derived. Our definition of admissibility for multi–conclusion rules, according to the full view given in the introduction, is more general than the one found in the literature, which is usually the one based on the strict view.

Given a mcr ⊢ , a rule R = Γ/Δ is derivable if Γ ⊢ Δ. Note that by Proposition 4 this is equal to R having a multi–conclusion derivation in Ru_⊢, as defined in Section 3.1. The rule scheme (R, S) is derivable if for all σ ∈ S, σ R is derivable. (R, S) is admissible, written Γ ∣∼ _S Δ, if \(\textsf {Thm}(\vdash ) = \textsf {Thm}({\vdash }_{S}^{R})\). A rule R = Γ/Δ is admissible, written Γ ∣∼ Δ, if (R, S u b) is admissible, which means, if \(\textsf {Thm}(\vdash ) = \textsf {Thm}({\vdash }_{Sub}^{R})\). A set of rules (schemes) is admissible if all of its members are. Similarly for single–conclusion consequence relations. Thus we have defined:

Observe that for saturated consequence relations:

The analogues of the above definitions for single–conclusion consequence relations can be obtained by replacing the set of expressions Δ by a single expression A. Thus Eq. 3 holds also in case ⊢ is a scr.

It is clear that for structural consequence relations, derivable rules are admissible. The converse, however, is not always the case. In case it is, the consequence relation is called structurally complete: a single–conclusion consequence relation ⊢ is structurally complete [10] if all admissible single–conclusion rules (in the same language) are derivable. It is hereditarily structurally complete if all extensions in the same language are structurally complete. A multi–conclusion consequence relation ⊢ is universally complete [3] if all admissible multi–conclusion rules are derivable. Clearly, ⊢ is structurally complete if it coincides with ∣∼ . For single–conclusion consequence relations the converse holds as well, and moreover, structural completeness is in that case equivalent to having no proper extensions in the same language with the same theorems.

Structural completeness depends very much on the particular consequence relation one uses for a logic. That is, a logic can have two consequence relations that both cover it, where the one is structurally complete, and the other is not. For example, as is well–known, ⊢_CPC is structurally complete [10] and covers CPC. However, the minimal consequence relation covering CPC,

is certainly not structurally complete, as ¬¬A/A is admissible but nonderivable in it. More will be said about classical logic in Section 5.

In contrast to structural completeness, admissibility solely depends on the (multi–conclusion) theorems of a consequence relation, as can be seen from the definition as well as Proposition 6 below. Using the developed terminology, the full and strict view for single–conclusion consequence relations and single–conclusion rule schemes (R, S) becomes:

(full) :

(R, S) is admissible in ⊢ if \(\textsf {Th}(\vdash ) = \textsf {Th}({\vdash }_{S}^{R})\).

(strict) :

(R, S) is admissible in ⊢ if under all substitutions in S, whenever all expressions in the premiss of R become theorems of ⊢ , then so does the conclusion.

As mentioned in the introduction, the full definition of admissibility is the one most often given when the notion is described informally. The strict definition, however, is the one most used in technical settings. Corollary 2 states that they are the same. First we prove the following proposition for the multi–conclusion setting. Recall the definition of \(\bigwedge \) and \(\bigvee \) in Section 2.1.

Proposition 6

For every consequence relation ⊢ :

Proof

Let R = Γ/Δ.

⇒ Suppose Γ ∣∼ _S Δ, that is, Thm \((\vdash ) = \textsf {Thm}({\vdash }_{S}^{R})\). If ⊢ σ A, Σ for all A ∈ Γ and some σ ∈ S and some Σ, this means σ A, Σ belongs to Thm ( ⊢ ) for all A ∈ Γ. Hence σ Δ, Σ belongs to Thm \(({\vdash }_{S}^{R})\), and therefore σ Δ, Σ ∈ Thm ( ⊢ ), that is, ⊢ σ Δ, Σ.

⇐ Assuming the right side of the equivalence, we show that Thm ( ⊢ ) equals Thm \(({\vdash }_{S}^{R})\). Therefore assume \({\vdash }_{S}^{R} \varSigma \). By Proposition 4 there is a multi–conclusion derivation T of ∅/Σ in Ru_⊢ ∪ Ru_{{(R, S)}} = Ru_⊢ ∪ {σ R∣σ ∈ S}. Thus lb(T), the labels of the leaves of T, are contained in Σ and the label lb(r) at the root is empty.

For a node k, let lbs(k) be the union of the labels of the immediate successors of k. First we prove that for all nodes k and all finite sets π of expressions:

Note that because of the implicit universal quantifier at the left, the implcation above implies that ⊢ lbs(k) holds for all k for which lb^↑(k) is empty.

To prove Eq. 4, assume that \(\vdash \bigwedge \text {lb}^{\uparrow }(k),\varPi \). By the definition of trees there is a Γ′ ⊆ lb^↑(k) such that Γ′/lbs(k) belongs to Ru_⊢ ∪ Ru_{{(R, S)}}. If Γ′/lbs(k) belongs to Ru_⊢, then lb^↑(k) ⊢ lbs(k), and ⊢ lbs(k), π follows. If, on the other hand, Γ′/lbs(k) belongs to Ru_{{(R, S)}}, then Γ′=σ Γ and lbs(k) = σ Δ for some σ ∈ S. Hence \(\vdash \bigwedge \sigma \varGamma ,\varPi \), and thus ⊢ σ Δ, π, that is, ⊢ lbs(k), π.

Next we show with induction to the depth of a node that for all nodes k and all finite sets π of expressions:

As lb^↑(r) is empty, this will prove the desired. Assume \(\vdash \bigwedge \text {lb}^{\uparrow }(k),\varPi \). Thus ⊢ lbs(k), π by Eq. 4. If k has depth 1, lbs(k) ⊆ lb(T) ⊆ Σ and we are done.

If k has depth greater than 1, consider its immediate successors k ₁, … , k _n . Thus lbs(k) = lb(k ₁) ∪ ⋯ ∪ lb(k _n ) and lb^↑(k _i ) = lb(k _i ) ∪ lb^↑(k). Because ⊢ lbs(k), π and \(\vdash \bigwedge \text {lb}^{\uparrow }(k),\varPi \) we have \(\vdash \bigwedge \text {lb}^{\uparrow }(k_{1}),\varPi \cup \text {lb}(k_{2}) \cup \dots \cup \text {lb}(k_{n})\). The induction hypothesis for k ₁ gives ⊢ Σ ∪ lb(k ₂) ∪ ⋯ ∪ lb(k _n ) ∪ π. The induction hypothesis for k ₂ gives ⊢ Σ ∪ lb(k ₃) ∪ ⋯ ∪ lb(k _n ) ∪ π. And so on, proving that ⊢ Σ, π holds. □

Corollary 2

Every saturated consequence relation ⊢ satisfies

Every single–conclusion consequence relation ⊢ satisfies

The last proposition and corollary imply the following corollary, the proof of which is straightforward.

Corollary 3

Both in the single–conclusion and the multi–conclusion context, ∣∼ is a consequence relation. If the underlying consequence relation is structural, so is ∣∼ .

Corollary 4

For a saturated multi–conclusion consequence relation ⊢ , multi–conclusion ∣∼ is the greatest multi–conclusion consequence relation in the same language with the same multi–conclusion theorems as ⊢ . And the same when “multi” is replaced by “single” and the word “saturated” is omitted.

Proof

We show that for multi–conclusion consequence relations ⊢ , ∣∼ is the greatest consequence relation such that Thm( ⊢ ) = Thm( ∣∼ ). That Thm( ⊢ ) is contained in Thm( ∣∼ ) is clear. For the other direction, suppose ∣∼ Δ. By Proposition 6, ⊢ Δ follows, thus showing that Thm ( ⊢ ) ⊇ Thm( ∣∼ ). If Thm ( ⊢ ) = Thm( ⊢ ′) for some consequence relation ⊢ ′, then for all rule schemes (R, S) derivable in ⊢ ′, it follows that \(\textsf {Thm}(\vdash ) = \textsf {Thm}({\vdash }_{S}^{R}\), and thus that R is admissible. Thus proving that ⊢ ′ is contained in ∣∼ . □

Corollary 5

For any logic L and any single–conclusion consequence relation ⊢ that covers L, ∣∼ is the greatest single–conclusion consequence relation in the same language that covers L.

Remark 1

The full definition of admissibility for multi–conclusion rule schemes (R, S) as given informally in the introduction becomes in our terminology:

(full) :

(R, S) is admissible in ⊢ if \(\textsf {Thm}\vdash = \textsf {Thm}{{\vdash ^{R}_{S}}}\).

At first glance, the following might seem to be the correct analogue for the strict definition.

(R, S):

is admissible in ⊢ if under all substitutions in S, whenever the premiss of R becomes a multi–conclusion theorem of ⊢ , then so does the conclusion.

However, this is not equivalent to the full definition. Here is an actual counter example. Let R be {p}/{q} and S consist of the identity substitution, and let the multi–conclusion consequence relation ⊢ be the smallest one such that ⊢ {p, q} holds. Then it certainly holds that whenever the expressions in the premiss of R becomes a theorem of ⊢ , then so does the conclusion, as p is no theorem of ⊢ . On the other hand, Thm ( ⊢ ) is not equal to Thm \(({\vdash }_{S}^{R})\). Not even Th (⊢) is equal to Th \(({\vdash }_{S}^{R})\), as the former does not contain q, while the latter does.

It follows from Proposition 6 that the strict analogue is:

(strict) :

(Γ/Δ, S) is admissible in ⊢ if for all σ ∈ S and all finite Σ, whenever σ A, Σ ∈ Thm( ⊢ ) for all A ∈ Γ, then σ Δ, Σ ∈ Thm( ⊢ ).

Indeed, under this strict notion the above counter example ceases to be so, as for Σ = {q} and σ the identity, ⊢ σ p, Σ holds but ⊢ σ q, Σ does not.

4.1 Bases

Given consequence relations ⊢ ⊆ ⊢ ′, a set \(\mathcal {R}\) of rules is a basis for ⊢ ′over ⊢ if \(\vdash ^{\mathcal {R}} = \vdash ^{\prime }\). In particular, \(\mathcal {R}\) is a basis for \(\vdash ^{\mathcal {R}}\) over ⊢ . From the definition it follows that \(\mathcal {R}\) is a basis for the admissible rules of a given consequence relation ⊢ iff the rules in \(\mathcal {R}\) are admissible in ⊢ and all admissible rules of ⊢ are derivable in \(\vdash ^{\mathcal {R}}\):

This notion allows one to describe ∣∼ without having to include redundancies. For example, for intermediate or modal logics L, if the rule R = A/B is admissible, then so is A ∧ C/B ∧ C, but we do not have to add the latter to the basis as it is derivable in \({\vdash }_{\textsf {L}}^{R}\):

Here we use that A∧C ⊢_L A and B, C ⊢_L B∧C hold, which is the case for all logics L in which A∧C → A and B∧C → B∧C hold, by the definition of ⊢_L.

There always is a basis for the admissible rules of a consequence relation, namely the set of all its admissible rules. Naturally, one often looks for bases with better properties, such as finite ones or those consisting of the instances of one particular rule scheme. Many intermediate and modal logics and fragments thereof are known to have nonderivable admissible rules, and for several an explicit basis for the admissible rules is known. We refer the reader to (the references in) [6, 12].

Example 4

No doubt the most famous admissible rule (for intermediate logics) is the Kreisel–Putnam rule:

Prucnal [11] discovered the universal character of this rule, a result later strengthened by Minari and Wroński [8] who showed the admissibility, in any intermediate logic, of the stronger Harrop rule HR, which is the rule

That not every instance of KP is derivable follows from the underivability of the corresponding implication (¬A → B ∨ C) → (¬A → B) ∨ (¬A → C) in intuitionistic logic. As negations are Harrop formulas, the same holds for HR.

Example 5

Interestingly, in modal and intermediate logics certain rule schemes seem generic in that they cannot be admissible without being a basis. Intuitionistic logic as well as many transitive modal logics such as K4, S4 and GL, have such bases [5, 7]. What happens once such rules are not admissible is at present less clear. In [4] it is shown that for intuitionistic logic, the basis consists of generalizations of a rule that we have encountered before, in Section 3.1:

We will not provide the argument, but it is not hard to see that this rule is admissible in IPC. Hence so is the Scott rule (¬¬A → A) → A ∨ ¬A/{¬A,¬¬A} from Section 3.1.

In Section 2.2 we discussed a variety of ways in which a consequence relation can be associated with a logic. From Lemma 1 it follows that if one starts with a logic L covered by a single–conclusion consequence relation ⊢ , then the smallest multi–conclusion consequence relation having the same theorems as L is

Clearly, this consequence relation is singular. And by Corollary 2 the strict view on the corresponding notion of admissibility, ∣∼ ^min, is equal to the dp–strict view from the introduction:

This is the reason that in most papers on admissibility the above notions are taken as the definitions of derivability and admissibility outright. That is, given a single–conclusion consequence relation ⊢ , one defines:

We call this the dp–view because using these definitions one can express the disjunction property via admissibility: a logic has the disjunction property if and only if the rule {A ∨ B}/{A, B} is admissible.

In this paper we have chosen a more general approach because we wished to allow for multi–conclusion consequence relations that are not of the form ⊢_min. But it captures the usual approach once one agrees to consider ⊢_min as the natural multi–conclusion consequence relation associated with a logic.

We already encountered multi–conclusion consequence relations not of the form ⊢_min. For example, in Section 2.2 the multi–conclusion consequence relation ⊢_CPC is defined as

Clearly, if one starts with a single–conclusion consequence relation ⊢ that covers CPC, then {p ∨ q} ⊢_min{p, q} does not hold. But {p ∨ q} ⊢_CPC{p, q} does. In fact, ⊢_CPC is structurally complete. For suppose Γ ∣∼ _CPC Δ. By Proposition 6 this implies that for all substitutions that map atoms to ⊤ or ⊥, if Γ ⊆ Th ⊢_CPC, then Δ ∈ Thm ⊢_CPC. From this it follows that \((\bigwedge _{A \in \varGamma }A \rightarrow \bigvee _{B\in \varDelta }B)\) is a tautology. Therefore Γ/Δ is derivable in ⊢_CPC.

All this shows that there are certain design choices to be made when defining admissibility for multi–conclusion consequence relation. And, as often, what is best depends on the context in which one wishes to use them.