2 Complete sets of sequent calculus rules

We recall some terminology: A literal is an atomic or a negated atomic formula. A disjunction of literals is also called a clause and is often often written simply as a set. Thus, the disjunction $\lnot A_1 \lor A_2$ may also be written as $\{\lnot A_1, A_2\}$ . Satisfaction conditions for clauses under a valuation ${\mathfrak {v}}$ are just those of the corresponding disjunction, i.e., if $C = \{L_1, \dots , L_n\}$ is a clause, ${\mathfrak {v}} \vDash C$ iff ${\mathfrak {v}} \vDash L_i$ for at least one $L_i$ . A set of clauses is satisfied in ${\mathfrak {v}}$ iff each clause in it is. Thus, a set of clauses corresponds to a conjunctive normal form, i.e., a conjunction of disjunctions of literals.

Now consider a truth-functional connective $\circledast $ . To say that $\circledast $ is truth-functional is to say that its semantics is given by a truth function $\tilde \circledast \colon \{\top , \bot \}^n \to \{\top , \bot \}$ , and that the truth conditions for a formula $A \equiv \circledast (A_1, \dots , A_n)$ are given by:

$$ \begin{align*} {\mathfrak{v}} \models \circledast(A_1, \dots, A_n) \text{ iff } \tilde\circledast(v_1, \dots, v_n) = \top, \end{align*} $$

where $v_i = \top $ if ${\mathfrak {v}} \models A_i$ and $= \bot $ otherwise.

As is well known, every truth-functional connective $\circledast (A_1, \dots , A_n)$ can be expressed by a conjunctive normal form in the $A_i$ , i.e., a conjunction of clauses in the $A_i$ , and the same is true for its negation. In other words, for every truth function $\tilde \circledast $ , there is a set of clauses ${\mathcal {C}}(\circledast )^+$ which is satisfied in ${\mathfrak {v}}$ iff $\circledast (A_1, \dots , A_n)$ is, and a set of clauses ${\mathcal {C}}(\circledast )^-$ which is not satisfied iff $\circledast (A_1, \dots , A_n)$ is not. ${\mathcal {C}}(\circledast )^+$ and ${\mathcal {C}}(\circledast )^-$ are of course not unique.

The Kowalski notation for a clause $C = \{\lnot A_1, \dots \lnot A_k, B_1, \dots , B_l\}$ ( $A_i$ , $B_j$ atomic) is an expression of the form $A_1, \dots , A_k {\vdash } B_1, \dots , B_l$ . We can now establish a correspondence between truth-functional connectives $\circledast $ , their associated clause sets ${\mathcal {C}}(\circledast )^+$ and ${\mathcal {C}}(\circledast )^-$ , and sequent calculus rules for them. If ${\mathcal {C}}$ is a clause set, then the corresponding set of premises is the set of sequents obtained from the Kowalski notations of the clauses in ${\mathcal {C}}$ by adding schematic variables for formula sequences $\Gamma $ , $\Delta $ in the antecedent and succedent. By a slight abuse of notation, we use the same meta-variables $A_i$ for the schematic formulas in the sequent on the one hand, and the atomic formulas in the clause set on the other. Each premise has the form $\Pi , \Gamma {\vdash } \Delta , \Lambda $ where the formulas in $\Pi $ are the $A_i$ occurring negatively in the respective clause, and those in $\Lambda $ are the $A_i$ occurring positively. The ${\circledast } {\mathrm{\scriptstyle L}}$ rule is the rule with the premise set corresponding to ${\mathcal {C}}(\circledast )^-$ and the conclusion $\circledast (A_1, \dots , A_n), \Gamma {\vdash } \Delta $ . The ${\circledast }{\mathrm{\scriptstyle R}}$ rule has a premise set corresponding to ${\mathcal {C}}(\circledast )^+$ and conclusion is $\Gamma {\vdash } \Delta , \circledast (A_1, \dots , A_n)$ . Rules have the general forms

where the formulas in $\Pi _i$ and $\Lambda _i$ in $\circledast{\mathrm{\scriptstyle R}}$ correspond to ${\mathcal {C}}(\circledast )^+$ and those in $\circledast{\mathrm{\scriptstyle L}}$ to ${\mathcal {C}}(\circledast )^-$ . We call the occurrence of $\circledast (\vec A)$ in the conclusion of such a rule the principal formula, the formulas in $\Pi _i$ and $\Lambda _i$ (or $\Pi _i'$ and $\Lambda _i'$ ) the auxiliary formulas, and those in $\Gamma $ and $\Delta $ the side formulas.

Suppose we have a set X of connectives $\circledast $ with associated $\circledast{\mathrm{\scriptstyle L}}$ and $\circledast{\mathrm{\scriptstyle R}}$ rules. The calculus consisting of these rules, the usual structural rules (weakening, contraction, exchange, cut), and initial sequents $A\,{\vdash }\,A$ is the classical sequent calculus ${\mathbf {LX}}$ for those connectives and rules.

When comparing the systems ${\mathbf {LX}}$ with natural deduction systems, it will be useful to start from a slight variant of ${\mathbf {LX}}$ in which the side formulas are not required to be identical in the premises. We replace an ${\mathbf {LX}}$ rule

by

to obtain the sequent calculus with independent contexts ${\mathbf {L^c X}}$ .

3 Splitting rules

The sequent calculi usually considered differ from the calculi ${\mathbf {LX}}$ as constructed above in that some of the rules are “split.” This is the case in particular for the $\mathord {\lor }{\mathrm{\scriptstyle R}}$ rule in ${\mathbf {LK}}$ . In this case, we replace the single rule with premise clause $ {\vdash } A, B$ by two rules, each with a single premise $ {\vdash } A$ or $ {\vdash } B$ . The availability of split rules is crucial if one wants to consider a variant of the sequent calculus with one side restricted to at most one formula, and when considering natural deduction systems, where the conclusion is also likewise restricted to a single formula. In such systems, we need rules where the premises satisfy the restriction as well.

Suppose we have a rule for $\circledast $ with premise set corresponding to a set of clauses ${\mathcal {C}}$ , and let $C \in {\mathcal {C}}$ be the clause corresponding to a single premise of the rule. We can partition the clause C into two parts: $C = C_1 \cup C_2$ , where $C_2 = \{L_1, \dots , L_k\}$ and consider the clause sets ${\mathcal {C}}_i = ({\mathcal {C}}\setminus \{C\}) \cup \{C_1 \cup \{ L_i\}\}$ . We can then consider the variant calculus ${\mathbf {LX}}^*$ with the rule corresponding to ${\mathcal {C}}$ replaced by the rules corresponding to all the ${\mathcal {C}}_i$ .

For instance, in the case of $\mathord {\lor }{\mathrm{\scriptstyle R}}$ , the constructed rule with premise clause $C = {} {\vdash } A, B$ can be replaced with the two $\mathord {\lor }{\mathrm{\scriptstyle R}}$ rules with premises $ {\vdash } A$ and $ {\vdash } B$ (here $C_1 = \emptyset $ and $C_2 = \{A, B\}$ ). An inference using $\mathord {\lor }{\mathrm{\scriptstyle R}}_1$ with premise $\Gamma {\vdash } \Delta , A$ can be replaced by

An inference using $\mathord {\lor }{\mathrm{\scriptstyle R}}$ can be replaced by a proof segment using $\mathord {\lor }{\mathrm{\scriptstyle R}}_1$ and $\mathord {\lor }{\mathrm{\scriptstyle R}}_2$ :

We thus have:

Note that this result does not establish that the calculus obtained from ${\mathbf {LX}}^*$ by restricting all sequents to at most one formula on the right proves the same (restricted) sequents as ${\mathbf {LX}}$ . It only shows that for every ${\mathbf {LX}}$ there is at least a candidate calculus ${\mathbf {LX}}^*$ where such a restriction would be possible as far as the logical rules are concerned. The resulting calculus may have different provable sequents. The example of ${\mathbf {LK}}$ and ${\mathbf {LJ}}$ illustrates this.

The set of rules obtained by splitting a rule of ${\mathbf {LX}}$ more than once may result in redundant rules, e.g., those where a premise contains an auxiliary formula A on the left and another premise contains it on the right. For instance, consider the $\mathord {\oplus }{\mathrm{\scriptstyle R}}$ rule from Table 2. Fully splitting the rule would result in four rules:

The two bottom rules are superfluous: the un-split rule can be simulated using the other two (and contractions):

Table 1. Clause sets and rules for the usual connectives

Table 2. Clause sets and rules for some unusual connectives

Table 3. Split rules for some unusual connectives

Table 4. Multi-conclusion natural deduction rules for some unusual connectives

Table 5. Some specialized and split elimination rules for some unusual connectives

Table 6. Single conclusion sequent rules for some unusual connectives

Table 7. Single-conclusion natural deduction rules for some unusual connectives

${\mathbf {LX}}^{**}$ is a calculus with “fully split” rules. In this case, each premise of a rule corresponds to a single literal (positive if the auxiliary formula appears on the right, negative if on the left). A rule then corresponds to a conjunction of literals, and a set of $\circledast{\mathrm{\scriptstyle R}}$ rules to a dnf of $\circledast (A_1, \dots , A_n)$ in the atomic formulas $A_i$ . Starting from a single $\circledast{\mathrm{\scriptstyle R}}$ rule corresponding to a cnf, the fully split set of rules corresponds to converting the cnf to a dnf by distributing $\land $ over $\lor $ . The fully split rules have the interesting property that when applied to initial sequents they derive the sequent $\Gamma {\vdash } \Delta , \circledast (A_1, \dots , A_n)$ where $\Gamma $ contains $A_i$ iff $A_i$ appears as an auxiliary formula on the right, and $\Delta $ contains $A_i$ iff $A_i$ appears as an auxiliary formula on the left. If $\lnot $ is present, we even get a derivation, using only $\lnot {\mathrm{\scriptstyle L}}$ and $\circledast{\mathrm{\scriptstyle R}}$ , of $\Pi {\vdash } \circledast (\vec A)$ (which moreover does not contain more than one formula on the right), where $\Pi = \Gamma , \lnot \Delta $ . The set of all $\Pi $ so obtained exactly describes the truth value assignments under which $\circledast (\vec A)$ is true.

Suppose now we have a sequent calculus with the usual structural rules but only right rules for a connective $\circledast $ . We can determine sound and complete left rules for $\circledast $ by reverse engineering the rules given. Each $\circledast{\mathrm{\scriptstyle R}}$ rule determines a set of clauses, which is equivalent to a conjunctive normal form for $\circledast (A_1, \dots , A_n)$ in the arguments $A_i$ , …, $A_n$ . If we have more than one $\circledast{\mathrm{\scriptstyle R}}$ rule, consider the disjunction of the corresponding cnfs. Its negation also has a cnf, which yields an $\circledast{\mathrm{\scriptstyle L}}$ rule which together with the $\circledast{\mathrm{\scriptstyle R}}$ rules is sound and complete, as is the calculus resulting from the given $\circledast{\mathrm{\scriptstyle R}}$ rules together with any rules obtained from $\circledast{\mathrm{\scriptstyle L}}$ by splitting.

4 Multi-conclusion natural deduction rules

A sequent calculus ${\mathbf {LX}}$ is straightforwardly and systematically related to a sequence-conclusion “sequent-style” natural deduction calculus ${\mathbf {N}_{m}^{s}\mathbf {X}}$ as follows. In ${\mathbf {N}_{m}^{s}\mathbf {X}}$ , the antecedent of a sequent $\Gamma {\vdash } \Delta $ is a multiset, not a sequence as in ${\mathbf {LX}}$ . The axioms of ${\mathbf {N}_{m}^{s}\mathbf {X}}$ are initial sequents $A {\vdash } A$ . Every $\circledast{\mathrm{\scriptstyle R}}$ rule is also a rule in ${\mathbf {N}_{m}^{s}\mathbf {X}}$ , an introduction rule for $\circledast $ . Every $\circledast {\mathrm{\scriptstyle L}}$ rule corresponds to a general elimination rule with the same premises as $\circledast{\mathrm{\scriptstyle L}}$ (the minor premises), an additional premise $\Gamma {\vdash } \Delta , \circledast (A_1, \ldots , A_n)$ (the major premise) and the conclusion $\Gamma {\vdash } \Delta $ , where $\Gamma $ and $\Delta $ are the same schematic context formulas as in the premises. As an example, consider the conditional, $\rightarrow $ . cnfs for $A \rightarrow B$ and $\lnot (A \rightarrow B)$ are

$$ \begin{align*} A \rightarrow B & \text{ iff } \lnot A \lor B\\ \lnot(A \rightarrow B) & \text{ iff } A \land \lnot B \end{align*} $$

These correspond to the introduction and elimination rules

The formulas in the antecedent of a sequent in an ${\mathbf {N}_{m}^{s}\mathbf {X}}$ derivation are called open assumptions. If a schematic variable A occurs in the antecedent of a premise in an elimination rule, it does not occur in the antecedent of the conclusion: the open assumption A is then said to be discharged by the rule.

Any proof in ${\mathbf {LX}}$ can be translated into a proof in ${\mathbf {N}_{m}^{s}\mathbf {X}}$ . A ${\circledast }{\mathrm{\scriptstyle L}}$ inference translates into a ${\circledast }{\mathrm{\scriptstyle E}}$ inference with major premise $\circledast (A_1, \dots , A_n), \Gamma {\vdash } \Delta , \circledast (A_1, \dots , A_n)$ . This premise itself can be derived from $\circledast (A_1, \dots , A_n) {\vdash } \circledast (A_1, \dots , A_n)$ by weakening and exchanges alone. Conversely, any proof in ${\mathbf {N}_{m}^{s}\mathbf {X}}$ can be translated into an ${\mathbf {LX}}$ proof. An ${\circledast }{\mathrm{\scriptstyle E}}$ inference is translated into a ${\circledast }{\mathrm{\scriptstyle L}}$ inference (with the minor premises as premises of the rule), followed by a cut with the proof ending in the major premise.

The sequent-style natural deduction calculus ${\mathbf {N}_{m}^{s}\mathbf {X}}$ corresponds to a natural deduction system in which proofs are trees of sequences of formulas.Footnote ¹ Whenever there is a derivation of $\Delta $ from undischarged assumptions $\Gamma $ there is a derivation of $\Gamma {\vdash } \Delta $ in ${\mathbf {N}_{m}^{s}\mathbf {X}}$ . Conversely, if ${\mathbf {N}_{m}^{s}\mathbf {X}}$ proves $\Gamma {\vdash } \Delta $ then there is a derivation in ${\mathbf {N}_m \mathbf {X}}$ of $\Gamma ' {\vdash } \Delta $ with $\Gamma ' \subseteq \Gamma $ . (Note that in natural deduction there is no equivalent to the left weakening rule, hence in general we can only get $\Gamma ' \subseteq \Gamma $ .)

In the context of natural deductions (especially when considering the Curry–Howard isomorphism) it is often necessary and helpful to consider a version of natural deduction in which one has more control over which elimination inferences discharge which assumptions, and to have book-keeping information for this in the derivations themselves. A corresponding sequent-style natural deduction calculus then will have labels on the formulas occurring in the antecedent (the assumptions), and the antecedent is now considered a set, not a multi-set, of labelled formulas. The antecedent of a sequent is also often called the context. The ${\mathrm{\scriptstyle WL}}$ and ${\mathrm{\scriptstyle CL}}$ rules are removed. Since the contexts are sets, contraction on the left is implicit. For simplicity we will also consider the consequent to be a multi-set of formulas (i.e., exchanges are implicit and the ${\mathrm{\scriptstyle XR}}$ rule is removed). In order to make the comparison with type systems easier, we will use variables x as these labels, and write a labelled assumption formula as $x \colon A$ . An initial sequent then is a sequent of the form

$$ \begin{align*} x \colon A \,{\vdash}\, A \end{align*} $$

We replace the introduction and elimination rules by rules in which the side formulas are not required to be shared. In other words, we replace a rule

Since the ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle L}}$ rule is removed, we must allow vacuous discharge of assumptions: a rule application is correct even if the discharged assumptions do not all appear in the premises. In other words, an application of a logical rule

may discharge any number of assumptions mentioned in the schematic form of the rule, including zero. The labels of assumptions discharged in an application are listed with the rule. Formulas instantiating the same schematic variable must have the same label. For instance, the $\mathord {\rightarrow }{\mathrm{\scriptstyle E}}$ rule now becomes:

A correct derivation is a tree of sequents starting in initial sequents in which every inference is correct according to the new definition. We denote the new system ${\mathbf {N}_{m}^{l}\mathbf {X}}$ .

Proof. In a first pass, we assign sets of labels to the formulas in the contexts in $\delta $ inductively:

If $A {\vdash } A$ is an initial sequent, replace it with $\{x\} \colon A {\vdash } A$ for some label x.

If A is the weakened formula in a ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle L}}$ inference, assign $\emptyset $ to it.

If label sets $l_1$ , and $l_2$ , both $\neq \emptyset $ , have been assigned to the auxiliary formulas $A, A$ in a ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle L}}$ inference, replace every label set $l_1$ and $l_2$ in the derivation ending in the premise by the set $l_1 \cup l_2$ and assign $l_1 \cup l_2$ to A in the conclusion.

In all other inferences, first uniformly replace labels throughout the derivations ending in the premises to ensure that the label sets appearing in any two derivations are disjoint. Then assign the same label sets to the formulas in the conclusion as the corresponding formulas in the premises.

If l, $l'$ are two different label sets in the result, $l \cap l' = \emptyset $ . We may assume that the labels $x_i$ are linearly ordered; let $\min (l)$ be the least label in l in this ordering.

We define the translation by induction on the height of the labelled derivation $\delta $ . The translation has the following property: if the labelled $\delta $ ends in $\Gamma {\vdash } \Delta $ and its translation $\delta '$ ends in $\Gamma ' {\vdash } \Delta '$ , then (a) if $l \colon A \in \Gamma $ with $l \neq \emptyset $ , then $\min (l) \colon A \in \Gamma '$ , and (b) if $x \colon A \in \Gamma '$ then for some l, $l \colon A \in \Gamma $ with $x = \min (l)$ , and (c) $\Gamma '$ contains each $x \colon A$ at most once. In each step below, it is easily verified that (a), (b), and (c) hold.

If $\delta $ is just an initial sequent $l \colon A {\vdash } A$ , $\delta '$ is $\min (l) \colon A {\vdash } A$ .

If $\delta $ ends in a ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ , ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle R}}$ , or ${{\mathrm{\scriptstyle CUT}}}$ inference, apply ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ , ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle R}}$ , or ${{\mathrm{\scriptstyle CUT}}}$ , respectively, to the translation of the premise.

If $\delta $ ends in ${{\mathrm{\scriptstyle X}}}{\mathrm{\scriptstyle R}}$ , or in a ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle L}}$ or ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle L}}$ inference with principal or weakened formula $l \colon A$ , $\delta '$ is the translation of its premise (i.e., we remove left weakenings and contractions). In the case of ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle L}}$ , by induction hypothesis, the antecedent of the translation of the premise already contains $\min (l) \colon A$ at most once.

Suppose $\delta $ ends in a logical inference,

Let $\delta _i'$ be the translations of the derivations ending in the premises. Each $\delta ^{\prime }_i$ proves $\Pi _i', \Gamma _i' {\vdash } \Delta _i, \Lambda _i$ where $\Pi _i'$ is a set of labelled formulas. For each $l \colon A \in \Pi _i$ , $\min (l) \colon A \in \Pi _i'$ iff $l \neq \emptyset $ , and if $x \colon A \in \Pi _i'$ then $x = \min (l)$ . If different labelled formulas $l \colon A$ and $l' \colon A$ appear in $\Pi _i$ and $\Pi _j$ but instantiate the same schematic formula of the rule, then $\min (l) \colon A$ and $\min (l') \colon A$ appear in $\Pi _i'$ and $\Pi _j'$ . Replace $\min (l') \colon A$ in the entire derivation $\delta _j'$ ending in the second premise by $\min (l) \colon A$ everywhere it occurs. In this way we obtain $\delta _i''$ in which labelled formulas $x \colon A$ which instantiate the same schematic variable have the same label. Adding ${\circledast }{\mathrm{\scriptstyle E}}$ to the resulting $\delta _i''$ results in a correct inference, if we label the inference with the list of labels appearing in the $\Pi _i$ . Note that when ${\circledast }{\mathrm{\scriptstyle E}}$ discharges a formula A which is obtained by weakening, it was originally labelled by $\emptyset $ . It either still was labelled with $\emptyset $ at the end, or its label set was combined with that of another occurrence of A with which it was later contracted. In the first case it no longer appears in the premise of the translated derivation, the corresponding inference thus vacuously discharges A.

The case of $\circledast{\mathrm{\scriptstyle I}}$ is treated the same way. □

5 Specialized elimination rules

In order to get the familiar elimination rules for natural deduction, the general elimination rules obtained from the ${\circledast }{\mathrm{\scriptstyle L}}$ rule must be simplified. For instance, the general elimination rule for $\rightarrow $ based on $\mathord {\rightarrow }{\mathrm{\scriptstyle L}}$ is

We can obtain a specialized rule by removing a premise which only discharges a single assumption, and instead add the discharged assumption to the conclusion. In the case of $\rightarrow $ , for instance, we observe that if $B \in \Delta $ , the right minor premise $B, \Gamma {\vdash } \Delta $ contains the initial sequent $B {\vdash } B$ as a subsequent and is thus always derivable. The additional formula B is then of course also part of $\Delta $ in the conclusion. The simplified rule ${\rightarrow }{\mathrm{\scriptstyle E}}'$ is the familiar modus ponens rule:

In general, a premise of ${\circledast }{\mathrm{\scriptstyle E}}$ of the form $A_i, \Gamma {\vdash } \Delta $ can be removed while $A_i$ is added to the right side of the conclusion to obtain a simplified rule ${\circledast }{\mathrm{\scriptstyle E}}'$ . For if $\Pi , \Gamma {\vdash } \Delta , \Lambda $ is derivable (the general form of any of the premises), so is $\Pi , \Gamma {\vdash } \Delta , A_i, \Lambda $ by ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ and ${{\mathrm{\scriptstyle X}}}{\mathrm{\scriptstyle R}}$ . The sequent corresponding to the removed premise is $A_i, \Gamma {\vdash } \Delta , A_i$ which is derivable from the initial sequent $A_i {\vdash } A_i$ by weakenings and exchanges alone. E.g.,

turns into

Thus, any inference using the specialized rule ${\circledast }{\mathrm{\scriptstyle E}}'$ can be replaced by the original rule ${\circledast }{\mathrm{\scriptstyle E}}$ . Conversely, if the premises of the original rule are derivable, the specialized rule applied to the premises still present in the specialized rule proves $\Gamma {\vdash } \Delta , A_i$ . The removed premise of the original rule is $A_i, \Gamma {\vdash } \Delta $ . Using ${{\mathrm{\scriptstyle CUT}}}$ and contraction, we obtain a derivation of $\Gamma {\vdash } \Delta $ . E.g.,

turns into

Since we allow multiple formulas in the succedent, this generalizes to multiple premises that only discharge single assumptions. For instance, we can simplify $\mathord {\lor }{\mathrm{\scriptstyle E}}$

to get

Note that the simulation of the original general rule by the specialized elimination rule requires a cut. It should thus not surprise that general elimination rules are proof-theoretically better behaved than the specialized rules.

It is also possible using the same idea to specialize rules by removing premises which only contain a single formula in the succedent. In that case, the corresponding formula must be added to the antecedent of the conclusion. Here is an example. The general $\mathord {\mid }{\mathrm{\scriptstyle E}}$ rule

specializes to the two rules

and further to the single rule

Sequent-style natural deduction is closely connected to standard natural deduction, in which assumptions are not collected in the antecedent of a sequent but are simply formulas at the top of a proof tree, possibly marked as discharged. In the standard formalism, such a specialized rule is difficult to accommodate, since it would amount to a rule that allows one to add undischarged assumptions to the proof tree which don’t already occur in the tree.

The restriction to a single formula in the antecedent of the specialized premise is essential. We cannot specialize a rule by removing a premise which discharges two assumptions by putting both assumptions into the succedent of the conclusion. The reason is that from the conclusion $\Gamma {\vdash } \Delta , A_i, A_j$ we cannot recover $\Gamma {\vdash } \Delta $ by cuts together with the removed premise $A_i, A_j, \Gamma {\vdash } \Delta $ . We can, however, replace the rule by a set of specialized rules, one for each assumption formula discharged in the specialized premise. This corresponds exactly to first splitting the ${\circledast }{\mathrm{\scriptstyle L}}$ rule, considering the generalized ${\circledast }{\mathrm{\scriptstyle E}}$ rules based on these split rules, and then specializing the resulting rules as before. Consider for example the rules for $\land $ . The standard $\mathord {\land }{\mathrm{\scriptstyle L}}$ rule has the single premise $A, B, \Gamma {\vdash } \Delta $ . It corresponds to the general elimination rule

The rule $\mathord {\land }{\mathrm{\scriptstyle L}}$ can be split into two $\mathord {\land }{\mathrm{\scriptstyle L}}$ rules with premises $A, \Gamma {\vdash } \Delta $ and $B, \Gamma {\vdash } \Delta $ , respectively. The corresponding general $\mathord {\land }{\mathrm{\scriptstyle E}}$ rules are

which can be specialized to the familiar two $\land $ elimination rules:

It is possible to generate a general elimination rule from a specialized one by reverse-engineering the specialization process. Suppose we have a specialized rule ${\circledast }{\mathrm{\scriptstyle E}}'$ :

Then the corresponding general elimination rule has the same premises as ${\circledast }{\mathrm{\scriptstyle E}}'$ plus an additional premise $A_i, \Gamma \vdash \Delta $ , and the conclusion leaves out the $A_i$ :

Since ${\circledast }{\mathrm{\scriptstyle E}}'$ is the result of ${\circledast }{\mathrm{\scriptstyle E}}$ specialized in the premise $A_i, \Gamma {\vdash } \Delta $ , the two rules are equivalent.

6 Cut elimination and substitution

Gentzen’s cut elimination method proceeds by permuting inference rules with the cut rule until there is a topmost cut where the cut formula is introduced in both premises of the cut by a right and a left inference, respectively. Such topmost cuts can then be reduced to cuts with cut formulas of a lower degree. We’ll now show that the fact that this is possible is no accident; in fact it holds whenever we have a calculus obtained by our procedure. The key fact here is that the original clause sets ${\mathcal {C}}(\circledast )^+$ and ${\mathcal {C}}(\circledast )^-$ are not jointly satisfiable. As an unsatisfiable clause set it has a resolution refutation, which can be immediately translated into a derivation of the empty sequent from the sequents corresponding to the clauses in ${\mathcal {C}}(\circledast )^+ \cup {\mathcal {C}}(\circledast )^-$ .

The same is true for clause sets corresponding to split rules, since each clause in them is a subset of a clause in ${\mathcal {C}}(\circledast )^+ \cup {\mathcal {C}}(\circledast )^-$ .

Proof. For a detailed proof, see Theorem 4.1 of Baaz et al. (Reference Baaz, Fermüller and Zach1994). We give a sketch only. As in Gentzen (Reference Gentzen1934), we observe that the cut rule is equivalent to the mix rule,

where $\Delta ^*$ and $\Theta ^*$ are $\Delta $ and $\Xi $ , respectively, with every occurrence of the mix formula A removed. We show that a proof with a single mix inference as its last inference can be transformed into one without mix. The result then follows by induction on the number of applications of mix in the proof.

We introduce two measures on proofs ending in a single mix: The degree is the degree of the mix formula A. The left rank is the maximum number of consecutive sequents on a branch ending in the left premise that contains the mix formula A on the right, counting from the left premise; and similarly for the right rank. The rank of the mix is the sum of the left and right rank. The proof then proceeds by double induction on the rank and degree. We distinguish cases according to the inferences ending in the premises of the mix inference and show how, in every case, either that the degree of the mix can be reduced, or else that there is a proof using a mix of the same degree but of lower rank.

The first case occurs when the mix formula A appears only once in $\Delta $ and $\Theta $ and as the principal formula of a $\circledast{\mathrm{\scriptstyle R}}$ inference that ends in the left premise $\Gamma {\vdash } \Delta $ and of a ${\circledast }{\mathrm{\scriptstyle L}}$ inference that ends in the right premise $\Theta {\vdash } \Xi $ . In all other cases, the mix inference is switched with the last inference on the left or right side, thus reducing the rank.

In the critical first case, the proof ends in

Remove the side formulas $\Gamma $ , $\Delta $ , $\Theta $ , $\Xi $ from the premises and consider the set of sequents $\Pi _i {\vdash } \Lambda _i$ and $\Pi _i' {\vdash } \Lambda _i'$ . These are just the clauses ${\mathcal {C}}(\circledast )^+$ and ${\mathcal {C}}(\circledast )^-$ , which together form an unsatisfiable set of Kowalski clauses. A resolution refutation of this clause set yields a derivation of the empty sequent from these sequents using only mix inferences on the $A_i$ . This derivation in turn, by adding the side formulas $\Gamma $ , $\Delta $ , $\Theta $ , $\Xi $ appropriately, and adding some exchanges and contractions at the end, yields a derivation of the sequent $\Gamma , \Theta {\vdash } \Delta , \Xi $ . The remaining mix inferences are all of lower degree, and so the induction hypothesis applies.

In the other cases we show that the end-sequent has a cut-free derivation by appealing to the second clause of the induction hypothesis, namely, that proofs ending in mix inferences of lower rank can be transformed into mix-free proofs. For instance, suppose the right premise ends in ${\circledast }{\mathrm{\scriptstyle L}}$ but its principal formula $\circledast (\vec A)$ is not the only occurrence of the mix formula in the antecedent of the right premise:

We may assume that the mix formula $\circledast (\vec A)$ does not occur in $\Gamma $ , since otherwise we can obtain a mix-free proof of the end-sequent from the right premise of the mix using only weakening and exchanges.

If we now apply mix to the left premise and to each of the premises of the ${\circledast }{\mathrm{\scriptstyle L}}$ inference directly we have:

Since the subproof leading to the premise on the right no longer contains the ${\circledast }{\mathrm{\scriptstyle L}}$ inference, the right rank is reduced by $1$ , and so the induction hypothesis applies. Each of these derivations can be transformed into a mix-free derivation. We can apply ${\circledast }{\mathrm{\scriptstyle L}}$ and mix again:

The right rank of this mix is $1$ since $\circledast (\vec A)$ does not occur in $\Pi _i', \Gamma , \Theta ^*$ , so the rank is lower than that of the original mix and the induction hypothesis again applies: $\Gamma , \Gamma , \Theta ^* {\vdash } \Delta ^*, \Delta ^*, \Xi $ has a proof without mix. We can obtain the original end-sequent $\Gamma , \Theta ^* {\vdash } \Delta ^*, \Xi $ from $\Gamma , \Gamma , \Theta ^* {\vdash } \Delta ^*, \Delta ^*, \Xi $ by exchanges and contractions. □

To illustrate the use of resolution refutations in the first case, consider a proof that ends in

The corresponding set of Kowalski clauses is

$$ \begin{align*} {\vdash} A, \qquad {\vdash} B, \qquad A, B {\vdash} \end{align*} $$

(i.e., $\{A\}$ , $\{B\}$ , $\{\lnot A, \lnot B\}$ ). A resolution refutation is

to which we add the side formulas appropriately, and exchanges and contraction inferences at the end, to obtain:

In the natural deduction system ${\mathbf {N}_{m}^{s}\mathbf {X}}$ , the cut rule can also be eliminated. In this case, however, the proof is much simpler than for ${\mathbf {LX}}$ . In fact, in ${\mathbf {N}_{m}^{s}\mathbf {X}}$ the cut rule simply corresponds to substituting derivations for assumptions. Since ${\mathbf {N}_{m}^{s}\mathbf {X}}$ has no rules which introduce a formula in the antecedent of a sequent in a derivation, every formula in the antecedent is either weakened, or it stems from an initial sequent. Whenever it is weakened, we can derive the conclusion of the cut inference from the premise of the weakening inference already. If it stems from an initial sequent, we can replace the initial sequent by the derivation ending in the left premise, and adding the context formulas $\Gamma $ and $\Delta $ to the antecedent and succedent of every inference below it, adjusting any inferences with weakenings as necessary.

Suppose $\delta $ is a derivation of $\Gamma {\vdash } \Delta , A$ and $\delta '$ is a derivation of $A, \Pi {\vdash } \Lambda $ , and suppose that neither $\delta $ nor $\delta '$ contains a cut. We can define the substitution $\delta '[\delta / A]$ with end sequent $\Pi , \Gamma {\vdash } \Delta , \Lambda $ recursively as follows. We distinguish cases according to the last inference of $\delta '$ :

1. 1. $\delta '$ is an initial sequent $A {\vdash } A$ . Then $\Pi = \emptyset $ , $\Lambda = A$ , and $\delta '[\delta /A]$ is $\delta $ .

2. 2. $\delta '$ is an initial sequent $B {\vdash } B$ , but $B \neq A$ . Then $\delta '[\delta /A]$ is

   

3. 3. $\delta '$ ends in a ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle L}}$ . The weakening formula is A, and the deduction ending in the premise is $\delta '' \colon \Pi {\vdash } \Lambda $ . Let $\delta '[\delta /A]$ be

   

4. 4. $\delta '$ ends in any other rule: Then $\delta '[\delta /A]$ is obtained by substituting $\delta $ for A in each of the premises, and then applying the same rule. It is straightforward to verify that the result is a correct derivation of $\Pi , \Gamma {\vdash } \Delta , \Lambda $ . Note in particular that in none of the remaining rules of ${\mathbf {N}_{m}^{s}\mathbf {X}}$ can A be a principal formula in the antecedent.

Proof. By induction on the number of cut inferences in a derivation $\delta $ . If there are no cuts in $\delta $ , there is nothing to prove. Suppose $\delta $ contains a cut inference; pick an uppermost one. Replace the subderivation

□

Substitutions can similarly be defined for ${\mathbf {N}_{m}^{l}\mathbf {X}}$ , the variant of ${\mathbf {N}_{m}^{s}\mathbf {X}}$ without left weakening and contraction in which antecedent formulas are labelled. Suppose $\delta $ and $\delta '$ are ${\mathbf {N}_{m}^{l}\mathbf {X}}$ derivations without labels in common, without ${{\mathrm{\scriptstyle CUT}}}$ , and $\delta $ ends in $\Gamma {\vdash } \Delta , A$ and $\delta '$ ends in $x \colon A, \Pi {\vdash } \Lambda $ . We define a substituted translation $\delta '[\delta /x \colon A]$ of $\Gamma ', \Pi {\vdash } \Delta , \Lambda $ with $\Gamma ' \subseteq \Gamma $ .

1. 1. $\delta '$ is an initial sequent $x \colon A {\vdash } A$ . Then $\Lambda = \{A\}$ . Let $\delta '[\delta /x \colon A]$ be $\delta $ plus ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ to obtain a derivation of $\Gamma {\vdash } \Delta , A$ .

2. 2. $\delta '$ is an initial sequent $y \colon B {\vdash } B$ , but $B \neq A$ or $x \neq y$ . Then $\delta '[\delta /A]$ is $\delta '$ plus ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ to obtain a derivation of $\Pi {\vdash } \Delta , B$ .

3. 3. $\delta '$ ends in any other rule: Then $\delta '[\delta /x \colon A]$ is obtained by substituting $\delta $ for $x \colon A$ in each of the premises, and then applying the same rule. If the rule discharged an assumption $x \colon A$ no longer present in the antecedent of the respective substituted premise, in the resulting inference the corresponding discharge is vacuous and the label y removed from the list of discharged labels.

It is straightforward to verify that the result is a correct derivation of $\Gamma ', \Pi {\vdash } \Delta , \Lambda $ .

7 Normalization for multi-conclusion natural deduction

The cut elimination theorem in ${\mathbf {N}_{m}^{s}\mathbf {X}}$ and ${\mathbf {N}_{m}^{l}\mathbf {X}}$ is, as we have seen, simply the result that derivations of a conclusion involving a formula A may be substituted for assumptions of that formula. In the context of natural deduction, the more interesting result is that every derivation reduces, via a sequence of local reduction steps, to a normal form. A derivation is in normal form if it involves no “detours,” i.e., no introductions of a formula by $\circledast{\mathrm{\scriptstyle I}}$ followed by eliminations of the same formula by ${\circledast }{\mathrm{\scriptstyle E}}$ .

We prove the normalization result for ${\mathbf {N}_{m}^{l}\mathbf {X}}$ without cut. Since conclusions are now multi-sets of formulas, the situation vis-à-vis detours in derivations is more complicated than in the single-conclusion case. Specifically, in a single-conclusion derivation any sequence of consecutive sequents beginning with an $\circledast{\mathrm{\scriptstyle I}}$ and ending in an ${\circledast }{\mathrm{\scriptstyle E}}$ inference is a “detour,” i.e., a maximum segment. No two such segments can overlap, and the beginning and end of any segment is uniquely determined. In the multi-conclusion case, segments can overlap, i.e., it is possible to have sequences of sequents in which a formula $\circledast (\vec A)$ is introduced, then another $\odot (\vec B)$ is introduced, then $\circledast (\vec A)$ is eliminated, and finally $\odot (\vec B)$ is eliminated. The presence of the ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle R}}$ rule adds further complications: a single ${\circledast }{\mathrm{\scriptstyle E}}$ inference can count as the end-point of more than one maximum segment.Footnote ² In order to deal with these complications, we must track the specific formula occurrences introduced and later eliminated in the definition of maximal segments.

The formula $\circledast (\vec A)$ is the maximal formula of the segment. The degree of the segment is the degree of $\circledast (\vec A)$ , i.e., the number of logical operators in $\circledast (\vec A)$ . The length of the segment is k.

Note that although the principal formula of a ${\circledast }{\mathrm{\scriptstyle E}}$ inference may be the last formula occurrence of more than one maximal segment (if it passes through a ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle R}}$ inference), any principal formula occurrence of $\circledast{\mathrm{\scriptstyle I}}$ is the first formula of at most one maximal segment. Since we are dealing with multisets of formulas, which formula occurrence in the conclusion of a rule corresponds to which formula occurrence in which premise is underdetermined. We could make this precise by introducing labels or moving to a calculus of sequences in which it is determined; for simplicity we assume that we have picked a way to associate corresponding formula occurrences in the derivation we start from and keep this association the same throughout the transformation.

Proof. Let $m(\delta )$ be the maximal degree of segments in $\delta $ , and let $i(\delta )$ be the number of segments of maximal degree $m(\delta )$ . We proceed by induction on $(m(\delta ), i(\delta ))$ .

We first ensure that at least one suitable segment of maximal degree is of length $1$ . There must be a segment $S_1$ , …, $S_k$ with maximal formula $\circledast (A_1, \dots , A_n)$ of degree $m(\delta )$ with the following properties. (a) No premise of the $\circledast{\mathrm{\scriptstyle I}}$ or ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ rule with $S_1$ as conclusion lies on or below a segment of degree $m(\delta )$ . (b) No minor premise of the ${\circledast }{\mathrm{\scriptstyle E}}$ rule of which $S_k$ is the major premise lies on or below a segment of degree $m(\delta )$ . If the length $k=1$ we are done. Otherwise, we decrease the length of this maximal segment.

We consider cases according to the rule of which $S_k$ is the conclusion. Since the segment is of length $>1$ , the formula occurrence $B_k = \circledast (\vec A)$ is not the principal formula of an $\circledast{\mathrm{\scriptstyle I}}$ or ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ inference. In each remaining case, this last inference and the following ${\circledast }{\mathrm{\scriptstyle E}}$ inference can be permuted and the length of the segment considered reduced.

1. 1. The rule is ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ , but $B_k$ is not the weakened formula. Then replace the inference

   
   The length of any segment which ends with the ${\circledast }{\mathrm{\scriptstyle E}}$ inference, and any segment which begins with the ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ inference have decreased, and others are unchanged. No new maximal segments are added.

2. 2. The rule is ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle R}}$ with the principal formula not $B_k = \circledast (\vec A)$ . Then replace the inferences

   

3. 3. The rule is ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle R}}$ and the principal formula is $B_k = \circledast (\vec A)$ . The segment ends in:

   
   where only one of the occurrences of $\circledast (\vec A)$ in the premise of ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle R}}$ is the maximal formula occurrence $B_{k-1}$ of the segment. (The other occurrence of $\circledast (\vec A)$ possibly belongs to another maximal segment ending in the ${\circledast }{\mathrm{\scriptstyle E}}$ inference, say, it is $B^{\prime }_{k'-1}$ in some segment consisting of $B^{\prime }_1$ , …, $B^{\prime }_{k'}$ .) Replace these inferences by
   
   This changes maximal segments as follows: The segment under consideration now ends at $B_{k-1}$ , and has therefore decreased in length. Any segment ending in the original ${\circledast }{\mathrm{\scriptstyle E}}$ inference which contained the other contracted formula occurrence $B^{\prime }_{k'-1}$ now ends at the lower ${\circledast }{\mathrm{\scriptstyle E}}$ inference, and is of the same length ( $k'$ ) as before. Because of property (b) of the topmost segment under consideration, there are no segments of maximal degree passing through or lying above the minor premises of the ${\circledast }{\mathrm{\scriptstyle E}}$ rule, and so the duplication of the subproofs ending in these minor premises has no effect on the number of segments of maximal degree.

4. 4. The rule is a $\mathord {\odot }{\mathrm{\scriptstyle I}}$ rule, with a principal formula $\odot (\vec C)$ , but the principal formula $\odot (\vec C)$ is not $B_{k-1} = \circledast (\vec A)$ . Exactly one of the premises must belong to the segment being considered, without loss of generality assume the first is. Then that premise is of the form $\Pi ^{\prime }_1, \Gamma ^{\prime }_1 {\vdash } \Delta _1', B_{k-1} = \circledast (\vec A), \Lambda _1$ . Suppose the other premises of the $\mathord {\odot }{\mathrm{\scriptstyle I}}$ inference are the sequents $\Pi _j', \Gamma _j' {\vdash } \Delta _j', \Lambda _j'$ (the formulas in $\Pi _i'$ and $\Lambda _i'$ are the auxiliary formulas). The conclusion of the inference is $\Gamma _1', \dots , \Gamma _n' {\vdash } \Delta _1', \dots , \Delta _n', B_k = \circledast (\vec A), \odot (\vec C)$ .

   Let $\Pi _i, \Gamma _i {\vdash } \Delta _i,\Lambda _i$ be the minor premises of the ${\circledast }{\mathrm{\scriptstyle E}}$ rule. If we let

   $$ \begin{align*} \Gamma & = \Gamma_1, \dots, \Gamma_n \\ \Gamma' & = \Gamma_1', \dots, \Gamma_m'\\ \Delta & = \Delta_1, \dots, \Delta_n \\ \Delta' & = \Delta_1', \dots, \Delta_m' \end{align*} $$
   the last inference in the segment has the following form:
   
   where $\dots \Pi _j', \Gamma _j' {\vdash } \Delta _j', \Lambda _j' \dots $ are the premises of the $\mathord {\odot }{\mathrm{\scriptstyle I}}$ inference other than the first. Replace the inferences with
   

5. 5. The last inference is $\odot {\mathrm{\scriptstyle E}}$ . This is treated as the previous one, except that we now have to distinguish cases according to whether the segment runs through the major premise or one of the minor premises. Again, since $\circledast (\vec A)$ must occur in the context of one of the premises, the ${\circledast }{\mathrm{\scriptstyle E}}$ rule can first be applied to that premise, and the $\odot {\mathrm{\scriptstyle E}}$ rule then to its original premises, with the one premise belonging to the segment replaced with the conclusion of the ${\circledast }{\mathrm{\scriptstyle E}}$ rule.

Now consider a topmost maximal segment of length $1$ . We have that $S_1 = S_k$ is both the conclusion of a $\circledast{\mathrm{\scriptstyle I}}$ or ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ rule and the major premise of a ${\circledast }{\mathrm{\scriptstyle E}}$ rule with $B_1=B_k$ the principal formula. In the second case, the segment in question has the form

This segment can be replaced by the premise of the ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ rule followed by ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ to add the $\Delta _i$ on the right:

Any inferences below which discharge assumptions in $\Gamma _1$ , …, $\Gamma _n$ are now vacuous.

The first case is the crucial one. The segment is of the form

As in the cut elimination theorem, the premises $\Pi _i {\vdash } \Lambda _i$ of the $\circledast{\mathrm{\scriptstyle I}}$ rule together with the minor premises $\Pi _i ' {\vdash } \Lambda _i'$ of the ${\circledast }{\mathrm{\scriptstyle E}}$ rule (with the context formulas $\Gamma _i$ , $\Gamma _i'$ , $\Delta _i$ , $\Delta _i'$ removed) form an unsatisfiable set of Kowalski clauses. A resolution refutation of these clauses results in a derivation of the empty sequent $ {\vdash }$ . If any literal is removed from such a derivation, the resolution refutation can be pruned to yield a possible shorter refutation. For any assumption $x \colon A$ not discharged by the ${\circledast }{\mathrm{\scriptstyle E}}$ and $\circledast{\mathrm{\scriptstyle I}}$ rules, remove the corresponding negative literal from the initial set of clauses and prune the refutation. (These cases correspond to what are usually called simplification conversions.)

Now add the context formulas $\Gamma _i$ , $\Gamma _j'$ , $\Delta _i$ , $\Delta _j'$ , to get a derivation of $\dots \Gamma _i,\Gamma _i'\dots {\vdash } \dots \Delta _i,\Delta _j\dots $ from the premises of the $\circledast{\mathrm{\scriptstyle I}}$ and the minor premises of the ${\circledast }{\mathrm{\scriptstyle E}}$ rule using cuts and structural rules only. We replace the maximal segment with this derivation and eliminate the cuts.

Because the maximal segment beginning with $\circledast{\mathrm{\scriptstyle I}}$ is topmost, and the derivations ending in the minor premises of ${\circledast }{\mathrm{\scriptstyle E}}$ contain no segments of maximal degree, the resulting derivation does not contain any new segments of maximal degree. We have removed one segment of maximal degree. If the segment in question was the only maximal segment of degree $m(\delta )$ , the maximal degree of segments in the resulting derivation is $< m(\delta )$ . Otherwise, we have removed at least one maximal segment, and thus reduced the number of the segments of maximal degree by $1$ . Thus, either the maximal degree of the resulting derivation is $< m(\delta )$ (if the segment was the only segment of degree $m(\delta )$ ), or the number of segments of maximal degree in the resulting derivation is $< i(\delta )$ .□

To illustrate the differences to the case of normalization for single-conclusion systems, consider the derivation fragment

This derivation fragment contains three overlapping segments, the formulas labelled a, b, and c respectively. Assuming that $A \lor B$ and $C \land D$ are of the same degree, all three are segments of maximal degree. The segment labelled c with maximum formula $C \land D$ is not topmost, since condition (a) is violated. We must pick one of the other segments, say the one labelled a. (We assume that no segments of maximal degree run through the minor premises of $\mathord {\lor }{\mathrm{\scriptstyle E}}$ and $\mathord {\land }{\mathrm{\scriptstyle E}}$ .) We first permute the $\mathord {\lor }{\mathrm{\scriptstyle E}}$ rule across the $\mathord {\land }{\mathrm{\scriptstyle E}}$ rule to obtain:

Now the $\mathord {\lor }{\mathrm{\scriptstyle E}}$ follows a contraction; we replace it with two $\lor E$ rules, the first of which ends the segment a.

Note that only one premise of the $\mathord {\lor }{\mathrm{\scriptstyle I}}$ rule contains the maximal formula of the segment labelled a—the left one. We obtain:

The segment labelled a is now of length $1$ and can be removed. The segment labelled b is the new topmost segment of maximal degree; the segment labelled c is considered when that one is removed.

The reader familiar with the normalization proof of Prawitz (Reference Prawitz1965) will of course realize that the structure of the preceding proof mirrors that of Prawitz’s proof very closely. By generalizing the proof, however, we see that its success does not at all depend on the specific logical inference rules used. The crucial steps are eliminating segments of length 1, and permuting elimination rules upward across any inference in which the formula eliminated by $\circledast{\mathrm{\scriptstyle E}}$ is not the principal formula of an $\circledast{\mathrm{\scriptstyle I}}$ rule eliminated by the ${\circledast }{\mathrm{\scriptstyle E}}$ rule. The first step always works if the premises of any $\circledast{\mathrm{\scriptstyle I}}$ and ${\circledast }{\mathrm{\scriptstyle E}}$ inference are jointly unsatisfiable clauses, as is the case with the introduction and general elimination rules constructed by our general method. The second step also always works, as long as the calculus has the general form of ${\mathbf {N}_{m}^{s}\mathbf {X}} $ , although not all of its features are essential. For instance, we can modify the proof to work on a calculus with sequences instead of multisets of formulas but with exchange rules, simply by not counting exchange inferences in the length of segments. However, we run into problems if left contraction is explicitly present. In conversion reductions, contractions are used to simulate resolution inferences by cuts. These cannot in general be avoided, even if the resolution proof is Horn. For instance, consider

Although such a cut can be replaced by two cuts, it multiplies the context formulas:

To obtain the original conclusion, we would need contraction again. One might consider replacing the cut rule with a multi-cut or “mix” rule that allows the removal of any number of occurrences of the cut formula to avoid the difficulty. Such a rule, however, allows us to simulate contraction (by applying mix to a suitable initial sequent), and so nothing is gained. In natural deduction where assumptions are labelled, these problems are avoided since the work of contractions on the left is done by having assumptions in different initial sequents sharing a label.

8 Single-conclusion sequent calculi

From the multiple conclusion sequent calculus ${\mathbf {LK}}$ we obtain a single-conclusion system ${\mathbf {LJ}}$ by restricting the succedent in every rule and every sequent in a proof to contain at most one formula. The calculus ${\mathbf {LJ}}$ is sound and complete for intuitionistic logic. This idea can be applied to any calculus ${\mathbf {LX}}$ , of course, and results in an “intuitionistic” variant of the calculus.

We begin by considering the sequent calculus ${\mathbf {LJX}}$ resulting from ${\mathbf {LX}}$ by restricting the rules in such a way that the succedent is guaranteed to contain at most one formula. This requires first of all that the premises of each rule have at most one auxiliary formula in the succedent. This can always be achieved by replacing a rule that does not satisfy this condition by split rules that do (see Corollary 5). We will assume that the logical rules of ${\mathbf {LX}}$ do satisfy this condition.

The restriction in ${\mathbf {LJX}}$ requires that in any application of a rule, the succedent of the premises and conclusion contains at most one formula. This means that in every right rule, $\Delta $ is empty. Furthermore, if a premise of a left rule has an auxiliary formula $\Lambda _i$ in the succedent, $\Delta $ must also be empty in that premise (i.e., there is no side formula). If all premises of a left rule have an auxiliary formula on the right, then no premise allows a side formula $\Delta $ , and the succedent of the conclusion of the rule is empty. We’ll call rules of this form restricted.

The ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ and ${{\mathrm{\scriptstyle CUT}}}$ rules now take the form:

where $\Lambda $ may contain at most one formula.

The intuitionistic sequent calculus ${\mathbf {LJ}}$ is the single-conclusion sequent calculus corresponding to the multi-conclusion classical sequent calculus ${\mathbf {LK}}$ obtained in this way.

Not every set of restricted rules will result in a reasonable single-conclusion sequent calculus. For instance, consider the restricted rules for $\nrightarrow $ , the negated conditional (aka “exclusion”) in which the left and right rules for $\rightarrow $ are reversed:

Note that the succedent is required to be empty in the right premise of $\mathord {\nrightarrow }{\mathrm{\scriptstyle R}}$ and in the conclusion of $\mathord {\nrightarrow }{\mathrm{\scriptstyle L}}$ . Because of this, $A \nrightarrow B {\vdash } A \nrightarrow B$ cannot be derived from $A {\vdash } A$ and $B {\vdash } B$ . In the regular sequent calculus for $\nrightarrow $ we would have:

These are not correct derivations in the restricted calculus.Footnote ³ To obtain a set of rules in which it is possible to give such a derivation, we must split the $\mathord {\nrightarrow }{\mathrm{\scriptstyle L}}$ rule further to guarantee that no premise has auxiliary formulas on both the left and the right side:

Now the derivation can be carried out:

(This corresponds to the right of the two derivations above; a version corresponding to the left one, where we first apply $\mathord {\nrightarrow }{\mathrm{\scriptstyle R}}$ and then $\mathord {\nrightarrow }{\mathrm{\scriptstyle L}}$ is not possible since the right premise of the restricted $\mathord {\nrightarrow }{\mathrm{\scriptstyle R}}$ must have empty succedent.)

Perhaps surprisingly, insufficient intuitionistic calculi can also result from splitting rules too much. Consider the restricted rules for nand, i.e., the Sheffer stroke:

These can derive $A \mid B {\vdash } A \mid B$ from atomic sequents:

However, this is not possible when the $\mathord {\mid }{\mathrm{\scriptstyle R}}$ rule is split into

In the unrestricted calculus, the last inference of the above proof can be replaced by

The application of $\mathord {\mid }{\mathrm{\scriptstyle R}}_2$ is not allowed in the restricted calculus, since there the right side of the premise is restricted to be empty.

The question of when suitable restricted calculi ${\mathbf {LJX}}$ are sound and complete for (something like) an intuitionistic semantics will be the topic of a future paper (but see Baaz & Fermüller, Reference Baaz and Fermüller1996, and Geuvers & Hurkens, Reference Geuvers, Hurkens, Ghosh and Prasad2017, for results in this direction). However, any calculus the rules of which satisfy the restriction, also has cut elimination.

Proof. The rules for ${\mathbf {LJX}}$ are obtained, if necessary, by first splitting rules to guarantee that the premises of of the rule contain at most one auxiliary formula on the right. In this case, the clauses corresponding to the premises of a rule for a connective are Horn, i.e., they contain at most one positive literal. Resolution on Horn clauses only produces Horn clauses. Since the set of clauses corresponding to the premises of a pair of ${\circledast }{\mathrm{\scriptstyle L}}$ and $\circledast{\mathrm{\scriptstyle R}}$ rules is unsatisfiable (even when these are split rules), it has a resolution refutation consisting only of Horn clauses. As before, we can add the side formulas of the actual premises to this resolution refutation to obtain a derivation of the conclusion of the mix from the premises of the ${\circledast }{\mathrm{\scriptstyle L}}$ and $\circledast{\mathrm{\scriptstyle R}}$ rules. Since each premise has at most one formula in the succedent, mix inferences cannot result in more than one formula on the right in the resulting proof segment. Thus the mix on $\circledast (\vec A)$ can be replaced with a sequence of mixes with the subformulas $A_i$ as mix formulas in ${\mathbf {LJX}}$ .

When permuting mix inferences with rules to reduce the rank, we have to verify that the resulting inferences obey the restrictions of the rules of ${\mathbf {LJX}}$ . First of all, observe that if the inference ending in the left premise of the mix is $\circledast{\mathrm{\scriptstyle R}}$ , the mix formula must be $\circledast (\vec A)$ and thus the left rank is $1$ . Thus we never have to permute a mix with an $\circledast{\mathrm{\scriptstyle R}}$ rule on the left side of a mix.

If the last inference on the right side of the mix is $\circledast{\mathrm{\scriptstyle L}}$ introducing the mix formula, we start from a derivation that has the form

where $\Xi _i$ is empty if $\Lambda _i'$ is not, and is $\Xi $ otherwise. $\Xi $ itself is empty if no $\Lambda _i'$ is empty. This guarantees that $\Xi $ and $\Xi _i, \Lambda ^{\prime }_i$ all contain at most one formula. This is converted to

Since by induction hypothesis, this mix can be removed, we get mix-free derivations of $\Pi _i', \Gamma , \Theta ^* {\vdash } \Xi _i, \Lambda _i'$ (by applying suitable ${\mathrm{\scriptstyle X}}{\mathrm{\scriptstyle L}}$ inferences). These are exactly the premises of a correct ${\circledast }{\mathrm{\scriptstyle L}}$ inference, as required. Now consider

As $\circledast (\vec A)$ does not occur in $\Pi _i', \Gamma , \Theta ^*$ , the right rank is now $1$ , and by induction hypothesis the mix can be eliminated.

The other interesting cases where the right premise is the conclusion of ${\circledast }{\mathrm{\scriptstyle L}}$ not introducing the mix formula or of $\circledast{\mathrm{\scriptstyle R}}$ are similar. □

As an example of reducing the degree of a mix on a formula introduced by restricted left and right rules other than the usual ones in ${\mathbf {LJ}}$ , consider the calculus for the Sheffer stroke from before. A mix of rank $2$ on $A \mid B$ ,

is reduced to mix inferences on A and B:

This corresponds to the resolution refutation:

9 Classical single-conclusion sequent calculi

It is possible to turn an intuitionistic, single-conclusion sequent calculus into a classical one without allowing multiple formulas in the succedent. The simplest way to do this is to introduce additional initial sequents, e.g., $ {\vdash } A \lor \lnot A$ or $\lnot \lnot A {\vdash } A$ . In natural deduction, a classical system can also be obtained from ${\mathbf {NJ}}$ by adding axioms, but it is more, well, natural to add a rule instead. Prawitz (Reference Prawitz1965) proposed the classical absurdity rule

For the sequent calculus, the corresponding rule would replace $\bot $ in the conclusion with an empty succedent:

Equivalent rules are double negation elimination and rule of excluded middle:

These rules, however, do not have the subformula property in at least the extended sense that $\bot _C$ does, where every formula in the premise is a subformula of a formula in the conclusion or the negation of one.

Suppose now that something like the negation connective is present in X and that ${\mathbf {LJX}}$ has the usual $\mathord {\lnot }{\mathrm{\scriptstyle L}}$ and $\mathord {\lnot }{\mathrm{\scriptstyle R}}$ rules. It suffices in fact that a connective that behaves like $\lnot $ can be expressed with the connectives of X in such a way that the $\mathord {\lnot }{\mathrm{\scriptstyle L}}$ and $\mathord {\lnot }{\mathrm{\scriptstyle R}}$ rules can be simulated. E.g., if the Sheffer stroke is present, the corresponding version of the $\bot _C$ rule would be

Proof. We define a translation of proofs in ${\mathbf {LX}}$ to proofs in ${\mathbf {LJX}} + \bot _C$ by induction on the height of a proof in ${\mathbf {LX}}$ . The end-sequent of a translation of a proof of $\Gamma {\vdash } \Delta , D$ is $\Gamma , \Delta ^\lnot {\vdash } D$ , where $\Delta ^\lnot $ is $\lnot A_n, \dots , \lnot A_1$ if $\Delta $ is $A_1, \dots , A_n$ . The translation of a proof of $\Gamma {\vdash } {}$ also ends in $\Gamma {\vdash } {}$ .

The translation of an initial sequent $A {\vdash } A$ is just $A {\vdash } A$ .

If the proof ends in ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ , either add ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ if the succedent of the premise is empty, or ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle L}}$ on the negation of the weakening formula plus ${\mathrm{\scriptstyle X}}{\mathrm{\scriptstyle L}}$ .

If the proof ends in ${{\mathrm{\scriptstyle X}}}{\mathrm{\scriptstyle R}}$ where the exchanged formulas do not include the rightmost formula, add suitable ${\mathrm{\scriptstyle X}}{\mathrm{\scriptstyle L}}$ inferences to the translation of the proof of the premise.

A proof ending in ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle R}}$ is translated as follows:

A proof ending in ${{\mathrm{\scriptstyle X}}}{\mathrm{\scriptstyle R}}$ in which the rightmost formula is active is translated as follows:

If the proof ends in a cut, in a weakening or contraction on the left, or in a logical inference, add the corresponding inferences to the translations of the proofs ending in the premise(s). □

The converse of course also holds, since every application of a rule of ${\mathbf {LJX}}$ is also a correct application of a rule of ${\mathbf {LX}}$ , and $\bot _C$ can be derived in ${\mathbf {LX}}$ by

In order to obtain cut elimination results for ${\mathbf {LJX}}$ , it is convenient to replace the $\bot _C$ rule with a classical version of the cut rule:

( $\Lambda $ contains at most one formula.)

The ${{\mathrm{\scriptstyle KUT}}}$ rule can simulate the $\bot _C$ rule over ${\mathbf {LJX}}$ :

In the reverse direction, $\bot _C$ together with cut can simulate kut:

(Again, $\Lambda $ contains at most one formula.)

Consequently, the previous result establishing structure-preserving translations of ${\mathbf {LX}}$ proofs into ${\mathbf {LJX}} + \bot _C$ proofs also transfers to ${\mathbf {LJX}} + {{\mathrm{\scriptstyle KUT}}}$ proofs. As an example, consider the derivation of excluded middle in ${\mathbf {LJ}} + {{\mathrm{\scriptstyle KUT}}}$ given by

The ${{\mathrm{\scriptstyle GEM}}}$ rule is also derivable using ${{\mathrm{\scriptstyle KUT}}}$ :

The restricted system ${\mathbf {LJX}}$ enjoys cut elimination in precisely the same way ${\mathbf {LJ}}$ does. However, for the corresponding classical systems ${\mathbf {LJX}} + \bot _C$ and ${\mathbf {LJX}} + {{\mathrm{\scriptstyle KUT}}}$ the situation is more complicated. Clearly, $\bot _C$ and ${{\mathrm{\scriptstyle KUT}}}$ , considered as variant cut rules, cannot be eliminated from proofs in ${\mathbf {LJX}}$ . We might hope, however, that ${{\mathrm{\scriptstyle CUT}}}$ can be eliminated from proofs in ${\mathbf {LJX}} + \bot _C$ and ${\mathbf {LJX}} + {{\mathrm{\scriptstyle KUT}}}$ , and that we can “control” the applications of $\bot _C$ and ${{\mathrm{\scriptstyle KUT}}}$ , e.g., to atomic A. This was shown by Negri & von Plato (Reference Negri and Plato2001) to hold for their related system $\mathbf {G3ip} + {{\mathrm{\scriptstyle GEM}}}$ , via the Schütte–Tait method of cut elimination.

Like ${{\mathrm{\scriptstyle CUT}}}$ , neither $\bot _C$ nor ${{\mathrm{\scriptstyle KUT}}}$ permute across ${{\mathrm{\scriptstyle C}}}{\mathrm{\scriptstyle R}}$ . In order to study Gentzen’s cut-elimination procedure for ${\mathbf {LJX}}$ we should thus consider their analogs to Gentzen’s ${{\mathrm{\scriptstyle MIX}}}$ rule which allows the removal of any number of occurrences of the cut formula A, not just the outermost ones. Let us call these rules $\bot _C^*$ and ${{\mathrm{\scriptstyle KIX}}}$ .

It is, however, possible to obtain restricted cut elimination results for ${{\mathrm{\scriptstyle KUT}}}$ .

Proof. We give the derivations for cases where the rules are also applications of ${{\mathrm{\scriptstyle KUT}}}$ and ${{\mathrm{\scriptstyle CUT}}}$ for simplicity.

Note that if C is $\lnot A$ in the second case, the starting derivation is impossible, since the conclusion of the mix then does not contain C on the left. □

By contrast, $\bot _C^*$ (and thus also $\bot _C$ ) does not permute with ${{\mathrm{\scriptstyle MIX}}}$ . Consider the following case:

Since the cut formula A does not appear in the succedent of the premise of the $\bot _C^*$ rule, we cannot apply the ${{\mathrm{\scriptstyle MIX}}}$ rule to it. If we first use ${\mathrm{\scriptstyle W}}{\mathrm{\scriptstyle R}}$ to introduce the cut formula A in the succedent, the conclusion sequent still contains $\lnot A$ on the left, but application of $\bot _C^*$ is blocked by the presence of C in the succedent. It would be possible to derive from $A, \Pi {\vdash } C$ the sequent $\lnot C, \Pi {\vdash } \lnot A$ (using $\mathord {\lnot }{\mathrm{\scriptstyle L}}$ and $\mathord {\lnot }{\mathrm{\scriptstyle R}}$ ) and then apply a mix on $\lnot A$ , but this would increase the degree of the mix formula and (because of the additional inferences required) would not be guaranteed to decrease the rank of the mix.

One last strategy to avoid this difficulty would be to show that we can transform the proof of the premise of $\bot _C^*$ into one of its conclusion that avoids the $\bot _C^*$ inference and does not increase the height of that subproof. Then the application of ${{\mathrm{\scriptstyle MIX}}}$ would apply to two subproofs of lower height than the original (since the $\bot _C^*$ rule would be removed) and so the induction hypothesis would apply. However, the conclusion $\bot _C^*$ rule is in general not provable without $\bot _C^*$ at all. Consider the case $\lnot (A \lor \lnot A) {\vdash } {}$ , which is derivable without $\bot _C$ . However, the corresponding conclusion of $\bot _C$ , $ {\vdash } A \lor \lnot A$ , is not so derivable.

Proof. If $\lnot A$ is principal, it was introduced by a $\mathord {\lnot }{\mathrm{\scriptstyle L}}$ rule. Then we can replace

□

10 Single-conclusion natural deduction

We have seen that the multi-conclusion “sequent style” natural deduction systems ${\mathbf {N}_{m}^{l}\mathbf {X}}$ always normalize. If we restrict the succedent of sequents in derivations to at most one formula, we obtain a single-conclusion “sequent style” natural deduction system ${\mathbf {N}^l\mathbf {X}}$ . This will be an “intuitionistic” version of ${\mathbf {N}_{m}^{l}\mathbf {X}}$ . For the standard set of logical operators, this system is the standard intuitionistic natural deduction system in sequent style, with one slight difference. In the standard systems, the succedent of sequents always contains exactly one formula; an empty succedent is represented by the contradiction symbol $\bot $ . So, if we are content to add the contradiction constant $\bot $ to the language, we can obtain the standard systems simply by marking every empty succedent in the rules of ${\mathbf {N}^l\mathbf {X}}$ with $\bot $ .

An example rule of an intuitionistic sequent-style natural deduction rule would be

Like in the case of the sequent calculus, where we obtained a single-conclusion system equivalent to ${\mathbf {LX}}$ by adding the $\bot _C$ rule to ${\mathbf {LJX}}$ , it is possible to obtain a classical single-conclusion sequent-style natural deduction system. In order to be able to translate derivations in ${\mathbf {LJX}} + \bot _C$ to a single-conclusion natural deduction derivations, we have to add the natural-deduction version of $\bot _C$ (or equivalent rules) to ${\mathbf {N}^l\mathbf {X}}$ , such as:

With ${{\mathrm{\scriptstyle LEM}}}$ we can derive ${{\mathrm{\scriptstyle KUT}}}$ , with ${{\mathrm{\scriptstyle KUT}}}$ we can derive $\bot _C$ , and with $\bot _C + {{\mathrm{\scriptstyle CUT}}}$ we can derive ${{\mathrm{\scriptstyle LEM}}}$ .

The proof of normalization for classical single-conclusion natural deduction including the rule $\bot _C$ is more complicated than both the pure intuitionist case and the multi-conclusion case. This is due to the fact that the notion of maximal segment must be extended to include sequences of formulas beginning with the conclusion of $\bot _C$ and ending with a major premise of an elimination rule. Such segments are harder to remove. Although Prawitz (Reference Prawitz1965) already showed normalization for the fragment excluding $\lor $ , normalization of the full system was not established until Stålmarck (Reference Stålmarck1991).

11 Proof terms and formulas-as-types

Under the Curry–Howard isomorphism, proofs in ${\mathbf {N}^{l}\mathbf {X}}$ can be assigned proof terms, just like they can in the standard intuitionistic cases. Under this isomorphism, conversions of inference segments used to reduce or permute inferences correspond to operations on proof terms. The general case considered here suggests that it might be fruitful to separate the proof operation of substitution, which corresponds to the cut rule, from the conversions themselves.

For each connective $\circledast $ , we may introduce two function symbols, one that applies to premises of an introduction rule (a proof constructor), and one to the premises of an elimination rule (a proof destructor). The types of these functions are given by the corresponding auxiliary formulas; and their conversion clauses by the corresponding derivation simplifications obtained from resolution refutations. Labels of discharged assumptions are abstracted similar to $\lambda $ -abstraction. We begin by considering some familiar examples.

Conjunction can be given a single introduction rule in Horn form,

The constructor corresponding to $\mathord {\land }{\mathrm{\scriptstyle I}}$ is the pairing function, $c^\land $ . It takes two arguments, one for each premise. If the premises end in derivations labelled by s and t, respectively, we label the derivation ending in the conclusion by $c^\land (s, t)$ . We may include this in the statement of the rule itself, by adding a type annotation on the right:

Split general elimination rules are

They correspond to the two destructors $d_1^\land $ , $d_2^\land $ , and the rules may be written:

Such a destructor may be seen as a generalized $\lambda $ abstraction operator; the x in the second argument is bound.

A cut inference is treated using a substitution operator,

It too binds the label of the discharged assumption $x \colon A$ .

An $\mathord {\land }{\mathrm{\scriptstyle I}}$ inference followed by an $\mathord {\land }{\mathrm{\scriptstyle E}}_1$ inference may be reduced from

to

and similarly for an $\mathord {\land }{\mathrm{\scriptstyle I}}$ followed by a $\mathord {\land }{\mathrm{\scriptstyle E}}_2$ inference.

The corresponding reductions for proof terms then are:

$$ \begin{align*} d^\land_1(c^\land(s, t), [x]u) & \rightarrow {{\mathrm{\scriptstyle SUBST}}}(s, x, [x]u) \\ d^\land_2(c^\land(s, t), [x]u) & \rightarrow {{\mathrm{\scriptstyle SUBST}}}(t, x, [x]u) \\ \end{align*} $$

A single general elimination rule for $\land $ is given by

The destructor corresponding to it is $d^\land $ , it takes two arguments, the proof terms for the major and minor premise. The labels of the discharged assumptions are abstracted. The rule with proof terms is as follows:

The proof simplification corresponding to a $\mathord {\land }{\mathrm{\scriptstyle I}}$ followed by $\mathord {\land }{\mathrm{\scriptstyle E}}$ is:

to

Correspondingly, the $\beta $ -conversion rule for $c^\land /d^\land $ is

$$ \begin{align*} d^\land(c^\land(s, t), [x,y]u) \rightarrow {{\mathrm{\scriptstyle SUBST}}}(t, y, {{\mathrm{\scriptstyle SUBST}}}(s, x, [x,y]u)) \end{align*} $$

For the conditional, the introduction and general elimination rules are

Here $c^\rightarrow ([x]s)$ is just a complex way of writing $\lambda x.s$ . $d^\rightarrow (s, t, [x]u)$ is the generalized application operator of Joachimski & Matthes (Reference Joachimski and Matthes2003). The corresponding proof simplification obtained from a resolution refutation of the premises is

to

The $\beta $ -reduction rule for the $c^\rightarrow /d^\rightarrow $ pair is then:

$$ \begin{align*} d^\rightarrow(c^\rightarrow([x]s), t, [x]u) \to {{\mathrm{\scriptstyle SUBST}}}({{\mathrm{\scriptstyle SUBST}}}(t, x, [x]s), x, [x]u) \end{align*} $$

or, if we prefer standard notation

$$ \begin{align*} \mathrm{app}(\lambda x.s, t, [x]u) \to u[s[t/x]/x] \end{align*} $$

In general, we have the following situation: For a connective with introduction rules $\circledast{\mathrm{\scriptstyle I}}_k$ and elimination rules ${\circledast }{\mathrm{\scriptstyle E}}_l$ we introduce function symbols: constructors $c_k^\circledast $ and destructors $d^\circledast _l$ . Each such function symbol has the same arity as the corresponding rule has premises. In an application of the rule, the succedent of the conclusion is labelled by the term

$$ \begin{align*} c^\circledast_k([\vec x_1^k]s_1^k, \dots, [\vec x_n^k]s_n^k) \text{ or } d^\circledast_l(s_0, [\vec x_1^l]s_1^l, \dots, [\vec x_m^l]s_m^l), \end{align*} $$

where the $s_i$ are the terms labelling the succedents of the premise sequents and $\vec x_i$ are the labels of the assumptions discharged in the ith premise.

The $\beta $ -reduction rule for a redex of the form

$$ \begin{align*} d^\circledast_l(c^\circledast_k([\vec x_1^k]s_1^k, \dots, [\vec x_n^k]s_n^k), [\vec x_1^l]s_1^l, \dots, [\vec x_m^l]s_m^l) \end{align*} $$

is provided by the corresponding simplification conversion on proofs, which in turn is given by a derivation segment consisting only of cut rules, i.e., a resolution refutation of the premises of the $\circledast{\mathrm{\scriptstyle I}}_i$ and ${\circledast }{\mathrm{\scriptstyle E}}_j$ rules. This simplification conversion produces a term built from the arguments $s_i^k$ and $s_j^l$ using only ${{\mathrm{\scriptstyle SUBST}}}$ operations. There are corresponding general $\alpha $ conversions: replace any subterm of the form $[x]s$ by $[y]s'$ where $s'$ is the result of substituting y for every free occurrence of x in s, provided y is free for x in s. $\eta $ -conversion corresponds to converting between $[x]s$ and s, provided x is not free in s. Finally, we define substitution redexes ${{\mathrm{\scriptstyle SUBST}}}(t, y, [\vec x]s)$ which convert to $[\vec z]s'$ , where $s'$ is s with every free occurrence of y in s replaced by t, provided t is free for y in s and y occurs in $\vec x$ , and $\vec z$ is $\vec x$ without y. If $y \notin \vec x$ , then ${{\mathrm{\scriptstyle SUBST}}}(t, y, [\vec x]s)$ converts to $[\vec x]s$ .

12 Free deduction

Parigot (Reference Parigot and Voronkov1992a) has introduced a calculus he called free deduction ${\mathbf {FD}}$ . It has pairs of rules for each connective called left and right elimination rules. The right elimination rules are just the general elimination rules of sequent-style natural deduction. Left elimination rules are what Milne (Reference Milne and Wansing2015) has called “general introduction rules.” Rather than adding the complex formula containing a connective as a conclusion, they allow assumptions containing the complex formula to be discharged. They are thus perfectly symmetric with the general elimination rule. The major premise contains the principal formula not on the right (as a conclusion) but on the left (as a discharged assumption).

For instance, the ${\mathbf {FD}}$ rules for $\rightarrow $ are:

and

This is a multi-conclusion version of Milne’s natural deduction system with general elimination (right elimination) and general introduction (left elimination) rules. Here the $\mathord {\rightarrow }{\mathrm{\scriptstyle LE}}$ rule is split; an equivalent version has a single rule,

Parigot presents this (and nonsplit rules for $\land $ , $\lor $ ) as a variant system ${\mathbf {FD}}'$ .

Free deduction rules (and hence Milne’s “general introduction rules”) can be formulated for arbitrary connectives $\circledast $ along the same lines as for sequent calculus and natural deduction. Given an introduction rule for $\circledast $ with premises $\Pi _i, \Gamma {\vdash } \Delta , \Lambda _i$ , the corresponding $\circledast{\mathrm{\scriptstyle LE}}$ rule is

Free deduction embeds both sequent calculus and natural deduction. The left and right sequent calculus rules can be simulated by taking the major premise in the corresponding free deduction right or left elimination rule to be an initial sequent. The introduction rule of natural deduction is obtained the same way as the right rule of the sequent calculus from the ${\mathrm{\scriptstyle LE}}{}$ rule, e.g.,

Cuts in this system are just like segments in natural deduction, except that here the formula $\circledast (\vec A)$ which appears in the major premise of an ${\circledast }{\mathrm{\scriptstyle E}}$ rule at the end of the segment is—not the conclusion of an $\circledast{\mathrm{\scriptstyle I}}$ rule as in natural deduction, but—discharged by an application of $\circledast{\mathrm{\scriptstyle LE}}$ at the beginning of a segment. A segment of length 1 then is of the form,

The cut-elimination mechanism of ${\mathbf {FD}}$ can be straightforwardly adapted to the generalized case. In this situation, we have to introduce labels not just for assumptions (formulas occurring on the left of a sequent) but also for those on the right. A maximal segment can be replaced by a sequence of cuts. As in he case of natural deduction, cuts correspond to proof substitutions. In ${\mathbf {FD}}$ , however, not only can we substitute derivations of $\Gamma {\vdash } A$ for assumptions in derivations of $x \colon A, \Pi {\vdash } \Lambda $ , but also conversely substitute a derivation of $A, \Pi {\vdash } \Lambda $ in a derivation of $\Gamma {\vdash } \Lambda , x \colon A$ . This of course results in a nondeterministic reduction procedure, as a cut inference may be replaced either by a substitution of the conclusion of the left premise in corresponding assumptions in the proof ending in the right premise, or the other way around.

13 Quantifiers

The basic principle underlying the generation of sequent calculus and natural deduction rules with the usual proof-theoretic properties can be extended to quantifiers as well. The important additional aspect of quantifier rules is that they (sometimes) require eigenvariable conditions, as in the case of $\mathord {\forall }{\mathrm{\scriptstyle R}}$ . Eigenvariable conditions are necessary for soundness, but they also guarantee that terms can be substituted in a proof for a variable appearing in an auxiliary formula, which is crucial for the cut-elimination and normalization properties.

The correspondence between a sequent calculus rule and a set of clauses also holds for quantifiers. The most general case of a quantifier for which this model could be considered has a fixed finite number of bound variables and a fixed finite number of schematic subformulas which may contain these variables:

$$ \begin{align*} {\mathsf{Q}} x_1 \dots x_m(A_1(x_1, \dots, x_m), \dots, A_n(x_1, \dots, x_m)). \end{align*} $$

The truth conditions of such a quantifier ${\mathsf {Q}}$ may be given by a set ${\mathcal {C}}$ of clauses, i.e., a conjunction of disjunctions of literals, where each atom is of the form $A_i(t_1, \dots , t_m)$ , and where $t_j$ is either a variable $x_j$ or a Skolem term $f(x_1, \dots , x_k)$ with $k < j$ . Under this interpretation, ${\mathsf {Q}} \vec x(A_1(\vec x), \dots , A_n(\vec x))$ is true iff $\exists \vec f\forall \vec x {\mathcal {C}}$ . Similarly, falsity conditions may be given for ${\mathsf {Q}}$ as well.

Such a set of clauses ${\mathcal {C}}$ corresponds to a sequent calculus rule for ${\mathsf {Q}}{\mathrm{\scriptstyle R}}$ , by interpreting a variable $x_j$ as an eigenvariable $a_j$ and a Skolem term $f(x_1, \dots , x_k)$ as schematic variable for a term which may contain the eigenvariables $a_1$ , …, $a_k$ . If the truth and falsity conditions for ${\mathsf {Q}}$ underlying the ${\mathsf {Q}}{\mathrm{\scriptstyle L}}$ and ${\mathsf {Q}}{\mathrm{\scriptstyle R}}$ rules are mutually exclusive (i.e., in each interpretation at most one of the two is satisfied), the resulting sequent calculus rules are sound. However, they will be complete only if it is not the case that the left and right rules each contain both term and eigenvariables.

Let us consider some examples. The syllogistic quantifiers, e.g., “All As are Bs” and “Some As are Bs,” fit this scheme:

$$ \begin{align*} \textsf{A} x(A(x), B(x)) & \text{ iff } \forall x(\lnot A(x) \lor B(x)) \\ \lnot \textsf{A} x(A(x), A(x)) & \text{ iff } \exists f(A(f) \land \lnot B(f)) \\ \textsf{S} x(A(x), B(x)) & \text{ iff } \exists f(A(f) \land B(f)) \\ \lnot \textsf{S} x(A(x), B(x)) & \text{ iff } \forall x(\lnot A(x) \lor \lnot B(x)) \end{align*} $$

We obtain the rules

and

Schönfinkel’s generalized Sheffer stroke $A(x) \mid ^x B(x)$ is the dual of $\textsf {S}$ :

$$ \begin{align*} \textsf{U} x(A(x), B(x)) & \text{ iff } \forall x(\lnot A(x) \lor \lnot B(x)) \\ \lnot \textsf{U} x(A(x), B(x)) & \text{ iff } \exists f(A(f) \land B(f)) \end{align*} $$

and has the rules

We can also consider nonmonadic quantifiers, e.g., the totality quantifier $\textsf {T}xy\,A(x, y)$ , expressed by

$$ \begin{align*} \textsf{T} xy\,A(x, y) & \text{ iff } \exists f\forall x\,A(x, f(x)) \\ \lnot \textsf{T} xy\,A(x, y) & \text{ iff } \exists g\forall x\,\lnot A(g, x) \end{align*} $$

with the rules

In ${\textsf {T}}{\mathrm{\scriptstyle L}}$ , the eigenvariable a may not appear in the conclusion, but also not in t, while in ${\textsf {T}}{\mathrm{\scriptstyle R}}$ the eigenvariable a may not appear in the conclusion, but is allowed to appear in $t(a)$ . These rules are sound, but not complete. For instance, there is no derivation of $\textsf {T}xy\, A(x, y) {\vdash } \textsf {T}xy\, A(x,y)$ from instances of $A(x, y) {\vdash } A(x, y)$ , since the eigenvariable condition is violated if ${\textsf {T}}{\mathrm{\scriptstyle L}}$ or ${\textsf {T}}{\mathrm{\scriptstyle R}}$ is applied to such an initial sequent.

Of course, not all natural quantifiers can even be provided with rules using this framework. For instance, the Henkin quantifier $\left \{{\forall x\exists y}\atop {\forall u\exists v}\right \} A(x, y, u, v)$ has truth conditions given by

$$ \begin{align*} \exists f\exists g\forall x\forall u\,A(x,f(x),u,g(u)) \end{align*} $$

but its falsity conditions cannot be stated in this form.

Whether or not the rules obtained this way are complete, they always enjoy cut-elimination. Since the clause sets ${\mathcal {C}}$ and ${\mathcal {C}}'$ corresponding to the ${\mathsf {Q}}{\mathrm{\scriptstyle L}}$ a ${\mathsf {Q}}{\mathrm{\scriptstyle R}}$ rules are mutually exclusive, ${\mathcal {C}} \cup {\mathcal {C}}'$ is an unsatisfiable set of clauses. Thus a mix inference in which the left premise is the conclusion of ${\mathsf {Q}}{\mathrm{\scriptstyle R}}$ and the right premise the conclusion of ${\mathsf {Q}}{\mathrm{\scriptstyle L}}$ can be reduced to mix inferences operating on the premises of the ${\mathsf {Q}}{\mathrm{\scriptstyle L}}$ and ${\mathsf {Q}}{\mathrm{\scriptstyle R}}$ rules, or on sequents obtained from them by substituting terms for eigenvariables. For instance, consider

The clause set $\{\{\lnot A(g, x)\}, \{A(y, f(y))\}\}$ is refutable by a single resolution inference, with most general unifier $\{g \mapsto y, f(g) \mapsto x\}$ . This means the eigenvariable a corresponding to y will be substituted by the term s corresponding to g, and the eigenvariable b corresponding to x will be substituted by the term corresponding to $f(g)$ , i.e., $t(s)$ . The restriction that b must not occur in s guarantees that this latter substitution performed in the proof ending in the premise of $\textsf {T}R$ can be carried out. We can then replace the cut by

We obtain natural deduction rules just as in the propositional case; normalization holds here as well for the same reason: the clause sets corresponding to the premises of a ${\mathsf {Q}}{\mathrm{\scriptstyle I}}$ rule together with the minor premises of a ${\mathsf {Q}}{\mathrm{\scriptstyle E}}$ rule are jointly unsatisfiable, hence refutable by resolution. The resolution refutation translates into a sequence of cut inferences applied to derivations ending in these premises, possibly with eigenvariables replaced by terms. The substitution for each cut inference is provided by the unifier in the corresponding resolution inference; eigenvariable conditions guarantee that the corresponding substitution of terms for eigenvariables can be applied to the entire derivation. (This is the idea behind the “cut elimination by resolution” method of Baaz & Leitsch (Reference Baaz and Leitsch2000).)