A Cut-Like Inference in a Framework of Explicit Composition for Various Calculi of Natural Deduction

Abstract

An explicit concatenation rule (EC) is proposed, obtained by generalizations and formalization of one of the most intuitive principle of abstract reasoning, which governs the composition of abstract derivations from the left and from the right at the same time, via the mediation of control clauses that occur in the position of the major premise. The sets of control clauses necessary to express various different calculi of natural deduction—standard natural deduction, natural deduction with general elimination rules, “bioriented” natural deduction and their variants—are considered, with a specific focus on a control clause for co-identity, a cut-like inference expressing the principle of linear substitution and on the effect of its addition to these calculi.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

1.1 A Fundamental Principle of Abstract Reasoning

According to Paul Hertz, reasoning is concerned with relationships between (sets of) elements and a (single) element. More [conventionally], we shall here deal with symmetric relationships between formulae¹: an abstract derivation from any number of assumptions $\Gamma$ to any number of assertions $\Delta$ will be represented by the notation $\Gamma \triangleright \Delta$ (which is suited to refer both to a derivation in natural deduction as well as to sequents²). An act of reasoning is, then, to obtain a previously unavailable (unknown) relationship of this kind by drawing on one (or several) of such that are already available (known).

One of the most fundamental principles of abstract reasoning is represented by the possibility of connecting different objects of reasoning by means of intermediary elements:

This step amounts to the realization that A mediates between the relationships expressed by the abstract derivations $\Gamma \triangleright \Delta,A$ and $A,\Theta \triangleright \Lambda$, used as premises, and that by way of some generalized notion of transitivity, the relation expressed by the inferred abstract derivation $\Gamma,\Theta \triangleright \Delta,\Lambda$ may be obtained. Another way to put it is if some formula A occurs both as an assertion in an abstract derivation and also as an assumption in another abstract derivation, a new abstract derivation is obtained by joining the assumptions and the assertions of the premises and removing either references to A.

Whereas this principle is included in the sequent calculus as a proper rule—the cut rule—the calculus of natural deduction does not contain a formal inference rule that has this effect. Instead, the following (implicit) principle of substitution—indispensable for the meta-theory of natural deduction—is commonly employed as a notational convenience for the composition of derivations:

Actually, only a single occurrence of A is considered in the antecedent and succedent of the premises of cut, whereas this notation of substitution conventionally relates a single derivation of a formula A to multiple assumptions of that formula, so cut should rather be likened to a principle of linear substitution, that is, the composition of two abstract derivations on a single occurrence of a formula in the succedent of one and the antecedent of the other.

The cut rule and the substitution principle have been compared very often. They bear striking similarities, but also some significant differences. Firstly, substitution in natural deduction affects the composition of the two derivations by means of fusing the two occurrences of A into a single occurrence, which is retained in the resulting derivation, even though it no longer has the status of either assumption or assertion. Secondly, in no way can the principle of substitution can be stated as a proper rule of natural deduction, because it composes arbitrary derivations, whereas proper inference rules of the systems always add a single formula as new conclusion. However, when considering abstract derivations, implicit composition of derivations and cut become indistinguishable: thus, we shall consider cut as fundamental principle of reasoning corresponding to the joining of abstract derivations on complementary occurrences of the same formula.³

1.2 From Cut to Bidirectional Multicut

We shall now formulate a rule multicut that expresses the effect of subsequent applications of cut addressed to different elements of the antecedent in turn:

The abstract derivations on the left are the minor premises of multicut, and the abstract derivation on the right is its major premise. The particular notation serves to emphasize how the minor premises are related to the cut formulae in the antecedent of the major premise.⁴ The major premise acts as an accumulator for all of the minor premises by means of these cut formulae. Technically, it is a rule that has k + 1 premises, that is, it is schematic in that instances depend on the number of minor premises.

Moreover, in addition to the possibility to choose multiple cut formulae from the antecedent of the major premise, the possibility is open to choose multiple cut formulae also from the succedent of an abstract derivation. These generalizations are merged in a single rule called bidirectional multicut:

This rule singles out an intermediary derivation that acts as major premise in both directions, that is, several elements of both the antecedent and the succedent can be used as cut elements. Correspondingly, there are two groups of minor premises, left minor premises and right minor premises. As in the case of the unidirectional multicut, the conclusion of bidirectional multicut can be obtained by k + l applications of the symmetric cut rule. The rule’s unique feature lies in its ability to have a single abstract derivation mediate between two sets of abstract derivations by accumulating them from the left and from the right by means of cuts.

1.3 From Bidirectional Multicut to Explicit Composition

Bidirectional multicut expresses the mere idea of composing multiple derivations into a single one and is an absolutely generic rule; otherwise, its action depends exclusively on the choice of what is to be used as a main premise. For this reason, we shall use it as a foundation for a rule that will be called explicit composition.

Principles like that, governing abstract reasoning, are often employed in order to talk about consequence relations, and cut is usually just one of many means by which new pairs can be obtained. Instead, we shall take bidirectional multicut as the only reasoning principle that is to be employed on the level of abstract derivations so—since we wish to model reasoning steps by inference steps—explicit composition will be the only inference rule of the framework that we shall build.⁵ As a consequence, whatever has to do with logical constants will have to enter in the manner of (instances of) very simple abstract derivations that address only logical constants and the constituents they are used with, insomuch as their configuration of formulae specifies the properties of the constants themselves. These simple abstract derivations are to play the role of major premises, which will accordingly exercise control over the manner in which the minor premises are to be composed.

The ultimate formulation of the explicit composition principle in the general case consists of a modification of bidirectional multicut, in which the major premise is required to be a clause, that we shall call the control clause, which expresses a relationships of formulae, whereas the minor premises are arbitrary abstract derivations. Specifically, it expresses a local relationship, in the sense that it is free of contextual formulae: only those formulae that are immediately relevant for the rule occur in the control clause, whereas all the contextual formulae reside in the abstract derivations that are composed by means of it. In its most general—though, as we shall see, very naive still—form, it is schematically given as

We shall divide the minor premises into those that are composed from the left and those that are composed from the right. A minor premise belonging to the former is called an antecessor, whereas one belonging to the latter is called a successor. In view of this terminology, the major premise can also be called the intercessor.

It is allowed that k, l, $\vert \Theta \vert$ or $\vert \Lambda \vert$ (and combinations thereof) are 0, the former two resulting in an empty antecessor or, respectively, an empty successor. Since this inference rule is the only rule of this framework for composing abstract derivations, we will usually omit the label (EC).

2 The Rule of Explicit Composition

Explicit composition, as it is given above, is powerful enough to express some of the rules of both natural deduction and the sequent calculus by means of control clauses. But still, in order to accurately give account of all the effects that occur in the various rules of the calculi we are considering, additional features have to be available for the control clauses. We shall restrict ourselves to mentioning the limits of the formulation proposed so far and define the generalizations that will make up for them, together with some example for natural deduction. We refer to Arndt and Tesconi (2014) for details and examples for the sequent calculus.

2.1 Effective and Ineffective Formulae

Observe that natural deduction rules always compose abstract derivations from the left by means of their assertions: for this reason, for example, the control clause for natural deduction rule ( ⊃ E)

uses A and A ⊃ B as substitution formulae, whereas a substitution on B should be explicitly forbidden.

The given example stresses the necessity to distinguish which formulae of a control clause are available for composition and which are not. For this purpose, we shall employ the following notation⁶:

$$\displaystyle{\left.\begin{array}{c} A_{1}\\ \\ \\ \vdots\\ \\ \\ A_{k}\\ \\ \\ \end{array} \right \}\Theta \blacktriangleright \Lambda \left \{\begin{array}{c} C_{1}\\ \vdots \\ C_{l}\\ \end{array} \right.}$$

The position of $\Theta$ and $\Lambda$ on the inside of the clause indicates that the formulae they contain are protected against composition, whereas formulae A ₁, …, A _k are cut formulae for compositions of abstract derivations from the left, and formulae C ₁, …, C _l are cut formulae for compositions of abstract derivations from the right. We call the formulae in $\Theta$ and $\Lambda$ ineffective and the A _i and C _j effective in as far as their purpose to compose abstract derivations is concerned. The ineffective formulae are carried over into the conclusion of (EC), whereas the effective formulae will usually not reoccur in the conclusion, unless there are multiple occurrences thereof in the minor premises.

2.2 Near and Far Effects

It is now possible to express by means of control clauses all the inference rules that do not affect the assumptions of the derivations that are composed. However, there are inference rules that affect the antecedent of their premise in addition to its succedent. For example, in defining a control clause for rule ($\rightarrow$ I),

one wants to express the fact that the assertion $A \rightarrow B$ is obtained and the assumption A is contextually discharged. In order to fulfill this requirement, a conceptual extension of (EC) is needed in as far as it must also allow for the cancellation of assumptions in abstract derivations. Specifically, it must allow for a control clause to cut a formula occurring in the succedent of an antecessor, the near side of some abstract derivation, and simultaneously remove another formula that occurs on the far side of the very same abstract derivation. A combination of such a far effect on a formula A in the antecedent of an antecessor and a near effect on a formula B in its succedent is expressed by the effective pair $\langle A\vert B\rangle$. Moreover, even though the standard calculi feature nothing like cancellation of assertions, we allow for the dual combination of near and far effects on the right-hand side of a control clause.⁷

The notation for control clauses is extended correspondingly:

$$\displaystyle{\left.\begin{array}{c} \langle A_{1}\vert B_{1}\rangle \\ \\ \\ \vdots\\ \\ \\ \langle A_{k}\vert B_{k}\rangle \\ \\ \\ \end{array} \right \}\Theta \blacktriangleright \Lambda \left \{\begin{array}{c} \langle C_{1}\vert D_{1}\rangle \\ \vdots \\ \langle C_{l}\vert D_{l}\rangle \\ \end{array} \right.}$$

Any of the A _i and any of the D _i can be vacuous, and the default cases that there should be no far effect are expressed by leaving the corresponding part of the combined effect empty, as in $\langle \cdot \vert B\rangle$ and $\langle C\vert \cdot \rangle$.

2.3 Iterated and Compound Effects

The additional features introduced above are not yet enough to define a correct control clause for the rule ( → I). Whereas control clause $\langle A\vert B\rangle \Big\} \blacktriangleright A \rightarrow B$ appears to embody all the desired features, $\langle A\vert B\rangle$ expresses the removal of a single formula on each side of the abstract derivation it affects, whereas the cancellation expressed by the rule ( → I) is seen as merely allowing the removal of selected occurrences. This is accommodated by allowing effects to be marked by a Kleene star that indicates their iteration. The combined effect $\langle A^{{\ast}}\vert B\rangle$ on the left-hand side of a control clause can compose an abstract derivation $\Gamma \triangleright \Delta,B$ from the left by means of a near effect on B, that is, a cut with cut formula B, but at the same time any number of occurrences of A (even none at all) may be removed⁸ from $\Gamma$. Using this generalized far effect, the natural deduction rule of ( ⊃ I) may be finally expressed by the control clause $\{\langle A^{{\ast}}\vert B\rangle \} \blacktriangleright A \supset B$ which allows any instance (for n ≥ 0) of the following inference:

In a dual way, the combined effect $\langle C\vert D^{{\ast}}\rangle$ on the right-hand side of a control clause can compose an abstract derivation $C,\Gamma \triangleright \Delta$ from the right by means of a near effect on C, but at the same time, any number of occurrences of D (even none at all) may be removed from $\Delta$. With a simple generalization, combinations of iterated near and far effects become available as well, as in $\langle A^{{\ast}}\vert B^{{\ast}}\rangle$, though they are not required for the present purpose.

A specialization of the general notion of iterated effects is that of compound effects. Instead of using the Kleene star, we use superscript letters to specify some exact multiplicity of formula occurrences. Thus, $\langle A^{n}\vert B^{m}\rangle$ expresses a compound effect resulting in the removal of n occurrences of the formula A from the antecedent of some abstract derivation and m occurrences of the formula B from its succedent. Analogously, $\langle C^{n}\vert D^{m}\rangle$ expresses a compound effect resulting in the removal of n occurrences of the formula C from the antecedent of some abstract derivation and m occurrences of the formula D from its succedent. Whereas the superscript n of far effects is ≥ ​ 0—the case of n = 0 will yield the same result as an empty effect—the superscript m of near effects must be > ​ 0. A compound effect can be considered as a mixing-style cut (in the case of a near effect) or as a multiple cancellation (in the case of a far effect). It corresponds to the simultaneous consideration in a single inference step of several occurrences of a formula, or even two or more different formulae: for example, the control clause

$$\displaystyle{\begin{array}{r} \langle \cdot \vert A \wedge B\rangle \\ \\ \\ \langle A^{{\ast} }, B^{{\ast} } \vert C\rangle \end{array} \Bigg\} \blacktriangleright C}$$

yields the general elimination rule ($\wedge$ E), in which an arbitrary number of occurrences of assumptions A and B are simultaneously cancelled from one of the two minor premises. Thus, compound effects are not only limited to purely structural issues but also to a particular structural issue that is covered implicitly in certain logical rules.

2.4 Explicit Composition, Revisited Formulation

The various generalizations that were introduced so far can be summarized in the following formulation of explicit composition:

All the multisets occurring in the abstract derivations—the $\Gamma _{i}$, $\Delta _{i}$, $\Xi _{i}$ and $\Pi _{i}$ as well as the $\Sigma _{i}^{\circ }$, $\Phi _{i}^{\circ }$, $\Psi _{i}^{\circ }$ and $\Omega _{i}^{\circ }$—are multisets of formulae, as are the ineffective formulae of $\Theta$ and $\Lambda$ of the control clause, whereas multisets $\Sigma _{i}^{\bullet }$, $\Phi _{i}^{\bullet }$, $\Psi _{i}^{\bullet }$ and $\Omega _{i}^{\bullet }$ may also contain superscripted formulae. The relationship between ∘-ed and •-ed multisets is given as follows:

• 1. Each occurrence of a formula A in $\Sigma _{i}^{\bullet }$ relates to exactly one occurrence of A in $\Sigma _{i}^{\circ }$.

• 2. Each occurrence of a superscripted formula A ⁿ in $\Sigma _{i}^{\bullet }$ relates to exactly n occurrences of $A$ in $\Sigma _{i}^{\circ }$.

• 3. Each occurrence of an asterisked formula A ^∗ in $\Sigma _{i}^{\bullet }$ relates to an arbitrary number of occurrences of A in $\Sigma _{i}^{\circ }$ that is not otherwise accounted for.

That is to say, every ∘-ed multiset is a specific instance of a •-ed multiset that may contain superscript specifications.

A control clause

$$\displaystyle{\left.\begin{array}{c} \langle \Sigma _{1}^{\bullet }\vert \Phi _{1}^{\bullet }\rangle \\ \\ \\ \vdots\\ \\ \\ \langle \Sigma _{k}^{\bullet }\vert \Phi _{k}^{\bullet }\rangle \\ \\ \\ \end{array} \right \}\Theta \blacktriangleright \Lambda \left \{\begin{array}{c} \langle \Psi _{1}^{\bullet }\vert \Omega _{1}^{\bullet }\rangle \\ \vdots \\ \langle \Psi _{l}^{\bullet }\vert \Omega _{l}^{\bullet }\rangle \\ \end{array} \right.}$$

will be called bidirectional when k, l ≥ 1, that is, when it allows composition both from the left- and the right-hand side; analogously, it will be called bioriented when $\vert \Theta \vert,\vert \Lambda \vert > 1$, and if $\vert \Theta \vert = \vert \Lambda \vert$ and $k = l = 0$, then $\Theta \not =\Lambda$, that is, when it allows the addition of formulae both in the antecedent and the succedent of the conclusion of explicit composition, except for the trivial case of the same multiset of formulae. It will be called left (right) directed when k ≥ 1, l = 0 (l ≥ 1, k = 0), that is, when it allows composition only from the left (right)-hand side; analogously, it will be called left (right) oriented when $\vert \Theta \vert \not =0,\vert \Lambda \vert = 0$ ($\vert \Theta \vert = 0,\Lambda \not =0$), that is, when it allows addition of formulae only in the antecedent (succedent) of the conclusion of explicit composition. A set of control clauses is bidirectional (bioriented), when some of its control clauses are bidirectional (bioriented) or when some of its control clauses are left directed (left oriented) and some of its control clauses are right directed (right oriented).

Whereas the final formulation of (EC) no longer bears a close semblance to the original simple reasoning principle, we obtained it through successive generalizations, not only in the sense of simply allowing for multiple and bidirectional compositions, each focussing on a single formula, but instead allowing a much wider range of cut-like effects in each of the compositions that contribute to the conclusion of the rule. All of these effects were obtained from a close inspection of the rules of natural deduction and the sequent calculus.

With anything that specifically affects the premises or the conclusion being specified in the control clauses, the rule (EC) is much more general than, say, a logical or structural inference rule. Instead, it should be seen as a purely combinatorial operation that takes some number of abstract derivations and produces the composition thereof—with some minor but significant modifications that are determined by the control clause through its effective and ineffective formulae.

3 Control Bases

By allowing the wide spectrum of effects described in the previous section, control clauses can mimic, emulate, produce, generate, obtain? all the rules of the calculus of natural deduction (and all the structural and logical rules of the sequent calculus, using the multiplicative formulation of its rules, but this would lead us too far from the purposes of the present work) in the sense that (EC) has the premises of those rules as minor premises and their conclusions as its conclusion. The set of control clauses that correspond to the rules of a given system shall be called the control base for that system.

In this section, the control bases for standard natural deduction, natural deduction with general elimination rules and “bioriented” natural deduction⁹ shall be defined in Figs. 9.1–9.3, respectively. The inherent properties of the calculi are reflected in the specific features of the corresponding control base, and this enables a direct comparison between the calculi that is based on the simple direct comparison of the control bases, rather than a comparison effected by some translation function. The advantages provided by this aspect of the framework will be fully appreciated once the control base for sequent calculus is defined as well (see Arndt and Tesconi 2014). In particular, the compared analysis of these control bases will emphasize that only the control base for the sequent calculus is bidirectional and bioriented, whereas an essential feature of control bases for the most conventional versions of natural deduction seems to be the left directionality—but modified versions will be defined already in the present work that show different properties.

Fig. 9.1

Control base $\mathbb{B}_{\text{ND}}$ for standard natural deduction

Fig. 9.2

Control base $\mathbb{B}_{\text{GND}}$ for natural deduction with general elimination rules

Fig. 9.3

Control base $\mathbb{B}_{\text{BND}}$ for “bioriented” natural deduction

3.1 Some Properties of Control Clauses

We shall now give an overview of some general features of control clauses that concern the relationship between near and far effects and the bidirectionality that is intrinsically expressed in the explicit composition rule.

The first observation is that the combined effect $\langle A\vert B\rangle$ is directionally neutral in the sense that an abstract derivation $A,\Gamma \triangleright \Delta,B$ can either be composed from the left to a control clause via a combined effect $\langle A\vert B\rangle$ on its left-hand side or from the right via $\langle A\vert B\rangle$ on its right-hand side:

and

It is to be noted that “directional neutrality” holds with respect to the relation of premises and conclusion, but, as regarding abstract derivations, the two control clauses refer to two different compositions.

The second observation requires the condition that succedents of abstract derivations never be empty—this is trivial when dealing with all of the control bases given so far. Then, when a combined effect $\langle A^{{\ast}}\vert B\rangle$ and an ineffective formula B both occur in the right side of a control clause, the same conclusion could be rendered by a control clause that does not employ combined effects.¹⁰ In the derivation,

the far effect of the control clause removes B from the antecedent of the abstract derivation, but at the same time, the ineffective formula B is retained in the conclusion. The same effect is obtained by a control clause that leaves the conclusion B intact:

These observations imply that a combined effect $\langle A^{{\ast}}\vert B\rangle$ on the left side of a control clause (in $\mathbb{B}_{\text{ND}}$, $\mathbb{B}_{\text{GND}}$ or $\mathbb{B}_{\text{BND}}$) that also has an ineffective formula B on its right side amounts to a near effect $\langle A^{{\ast}}\vert \cdot \rangle$ on the right side of the control clause:

and

However, these control clauses are not at all equivalent to each other, as they exercise different controls over the premises that are to be composed by (EC). In fact, regardless of the fact that they obtain the same abstract derivation as a conclusion, they express different rules with different directionality.

3.2 Modified Control Bases

We shall now exploit these properties in order to “invert” the directionality of control clauses for elimination rules of $\mathbb{B}_{\text{GND}}$ and $\mathbb{B}_{\text{BGND}}$ —except for the case of disjunction that we shall not consider here because it would require a limitation of (EC), in order to prevent that more than one formula appear in the succedent of a conclusion (further details will be included in an already mentioned following work). The “modified” control bases $\mathbb{B}_{\text{MGND}}$ and $\mathbb{B}_{\text{MBND}}$ are shown in Figs. 9.4 and 9.5, respectively, and, opposite to the original control bases, are both bidirectional.

Fig. 9.4

Control base $\mathbb{B}_{\text{MGND}}$ for modified natural deduction with general elimination rules

Fig. 9.5

Control base $\mathbb{B}_{\text{MBND}}$ for modified “bioriented” natural deduction

4 Co-Identity and Its Effects on Control Bases for Natural Deduction Systems

4.1 The Control Clause for Co-Identity

All of the control bases defined so far share the control clause for identity

$$\displaystyle{A \blacktriangleright A,}$$

which trivially introduces the formula A both in the antecedent and the succedent of the conclusion. This corresponds to the initial sequent A ⇒ A, in the sequent calculus, or the derivation of A by its assumption in natural deduction.

Its “dual”, the control clause for co-identity

$$\displaystyle{\langle \cdot \vert A\rangle \Big\} \blacktriangleright \Big\{\langle A\vert \cdot \rangle }$$

instead has the effect of restoring the restriction performed by ineffective formulae on the character of bidirectionality.

This clause forces (EC) to simply connect the antecessor to the successor, which in this case are just two abstract derivations:

thus expressing in the setting of abstract derivations the principle of linear substitution: in fact, in the context of the sequent calculus this control clause renders the cut rule. However, it is not included in the control bases for any of the versions of natural deduction considered.

Co-identity recovers the possibility of composition on formulae that were introduced by means of ineffective formulae in previous inference steps. Compare how the following two derivations yield the same conclusion from the premises $\Gamma \triangleright \Delta,A$ and $C,\Xi \triangleright \Pi$:

and

In the first derivation, the upper application of (EC) employs the schematic control clause $A \blacktriangleright \{\langle C\vert \cdot \rangle \}$ to compose $C,\Xi \triangleright \Pi$ on formula C, which—by means of the ineffective formula A—introduces A into the antecedent of its conclusion. The subsequent composition that uses co-identity has the effect of a simple cut with cut formula A. In contrast to this, the second derivation first composes $\Gamma \triangleright \Delta,A$ on A through a schematic control clause $\{\langle \cdot \vert A\rangle \} \blacktriangleright C$, thereby introducing C, and the second composition, employing co-identity, then acts as cut on the formula C.

4.2 The Addition of Co-identity to Given Control Bases

Although the observations up to this point might seem to suggest a substantial correlation between co-identity and bidirectionality, there are other aspects to consider. It is indeed true that co-identity confers an explicit feature of bidirectionality to a given control base it is added to, but—as a first thing, and trivially enough—there are bidirectional control bases that do not contain co-identity among their control clauses: consider, for instance, the control base $\mathbb{B}_{\text{MGND}}$ which contains the bidirectional control clauses for conjunction elimination and implication elimination. Then, on the one hand, we shall see that the addition of co-identity to a unidirectional control base does not necessarily imply that the resulting system has more compositional possibilities than the original one—this is the case, for example, of control bases $\mathbb{B}_{\text{ND}}$, $\mathbb{B}_{\text{GND}}$ and $\mathbb{B}_{\text{MGND}}$, as we shall demonstrate shortly. On the other hand, the addition of co-identity to a control base that already enjoys bidirectionality may imply that the resulting system has more compositional possibilities than the original one. This is the case for control bases $\mathbb{B}_{\text{BND}}$ and $\mathbb{B}_{\text{MBND}}$.

Control bases $\mathbb{B}_{\text{ND}}$ and $\mathbb{B}_{\text{GND}}$ are strictly unidirectional and right oriented. That is, control clauses in $\mathbb{B}_{\text{ND}}$ and $\mathbb{B}_{\text{GND}}$ always compose abstract derivations from the left and all of the ineffective formulae occur in their right-hand sides. In these systems, all formulae might be considered “joining knots” of different derivation fragments, so the addition of co-identity to the corresponding control bases will not actually add the possibility of the join itself but rather the possibility of giving information about which formula we want to be considered as “joining knot”. In the framework of explicit composition for the mentioned control bases, co-identity may perform a cut on the same formula, in different points of the derivation or even on different formulae, without altering neither the conclusion nor the order of the other inferences. We shall now show that, in the framework of explicit composition for $\mathbb{B}_{\text{ND}}$, adding the possibility of using co-identity does not add the possibility of new combinations of derivation fragments. In other words, any two derivation fragments on which co-identity could be applied could be combined, with the same result, without resorting to co-identity, via the control clauses of $\mathbb{B}_{\text{ND}}$ alone. In fact, consider a derivation that ends with

Inferences leading to $B,\Delta \triangleright C$ may as well be performed, one by one, starting from $\Gamma \triangleright B$ instead of $B \triangleright B$—which results from identity—without any application of co-identity. This is proved by a trivial induction on the length of derivation $\mathcal{D}_{2}$, and we will only provide some representative examples of the cases. In particular, only for the most trivial case described below, we will give the example of a derivation that does not end with co-identity, in order to show how the procedure affects—or better: does not affect—the subsequent applications of explicit compositions.

If the co-identity is performed on a derivation of minimal length, as in

then it can be simply eliminated:

This case corresponds to composing on an assumption:

Here the notation^∗ B ^∗ emphasizes that the composition takes place on the derivation ending with B, that is, B itself.

If the co-identity is performed on a derivation of non-minimal length, as in

then it can be permuted over the last inference of its successor in order to be able to apply the induction hypothesis:

This case corresponds to composing on an assumption of a derivation:

Here the notation^∗ D ^∗ and $^{{\ast}}E \vee F^{{\ast}}$ emphasizes that the compositions take place on the fragments of derivation ending with D and $E \vee F$, respectively. We have thus proved that any derivation of $\mathbb{B}_{\text{ND}}$ plus co-identity can be transformed into a derivation of $\mathbb{B}_{\text{ND}}$ of the same conclusion where the order of the other inferences is not altered.¹¹

The case of $\mathbb{B}_{\text{GND}}$ is completely analogous and we shall only demonstrate a single example:

first becomes

and eventually becomes

This case corresponds to

first being considered as

which may be transformed in to (???)

Here the notation^∗ C ^∗ and $^{{\ast}}E \rightarrow F^{{\ast}}$ emphasizes that the compositions take place on the fragments of derivation ending with C and $E \rightarrow F$, respectively.

The modified control base $\mathbb{B}_{\text{MGND}}$ is still right oriented, but it is bidirectional already in the absence of co-identity. As for its conventional version, the addition of this control clause has no other real effect than providing information about the exact point in a derivation where a composition takes place. Consider, for example, the derivation

Because of bidirectionality, co-identity can always be permuted over the last inference of its successor, as in the procedure exploited before, or its antecessor, provided that the control clause of its last inference admits a successor, as in the following derivation:

Both possibilities decrease the length of premises of co-identity; the latter is obviously never available for $\mathbb{B}_{\text{ND}}$, $\mathbb{B}_{\text{GND}}$ and $\mathbb{B}_{\text{BND}}$ because their control clauses do not admit any successors.

Control base $\mathbb{B}_{\text{BND}}$, instead, is unidirectional, and it is bioriented as well. That is, control clauses in $\mathbb{B}_{\text{BND}}$ always compose abstract derivations from the left, but ineffective formulae occur in both sides. In this case, adding the possibility of using co-identity truly adds the possibility of new combinations of fragments of derivation. In other words, it is not the case that any two fragments of derivation on which co-identity could be applied could be combined together, with the same result, already without resorting to co-identity, via the control clauses of $\mathbb{B}_{\text{BND}}$. Specifically, the addition of co-identity allows composition on ineffective formulae on the left-hand side of control clauses for elimination rules, something that would not be possible otherwise.

In fact, observe that a derivation $A,\Delta \triangleright \Gamma$ cannot be a successor of any other control clause than co-identity, since they all have ineffective formulae on their right side; this is true for control bases $\mathbb{B}_{\text{ND}}$ and $\mathbb{B}_{\text{GND}}$ as well, but whereas in the this latter case co-identity can be permuted without altering the order of other inferences until it reaches the point where it is performed on an abstract derivation obtained from the identity, it is not always the case for control base $\mathbb{B}_{\text{BND}}$, where some control clauses have ineffective formulae on the left-hand side that introduce elements in to the antecedent of the conclusion. The following derivation will serve as a counterexample:

The same obstacle arises for the modified control base $\mathbb{B}_{\text{MBND}}$ which is both bidirectional and bioriented. That is, when the last inference of co-identity’s successor is left oriented, it is not possible to permute co-identity over it. As it happens for the modified control bases $\mathbb{B}_{\text{MGND}}$, because of the gained feature of bidirectionality, in some cases co-identity can be permuted over the last inference of its antecessor (namely, when the last inference of its control clause admits a successor) instead, but not always, as the following example shows:

4.3 Conclusions

The examples proposed suggest that the addition of co-identity to a single-oriented control base, regardless of its directionality, does not open more possibilities of combination of abstract derivations, whereas its addition to a bioriented control base does. In this latter case, in fact, when a formula is introduced among the assumptions by means of a certain rule, it appears as a leaf in the derivation tree, but it is not available before the application of the rule itself. Thus, it is not always possible that it is (???), at the same time and in that very same point of the derivation, introduced as a conclusion by some other inference. Another way to put it is that in bioriented systems not all formulae of a derivation can be considered “joining knots” of different fragments of derivations.

As a conclusion, explicit composition turns out to provide a framework that proves to be very suited to compare the effects of a cut-like inference, embodied by co-identity, on various calculi of natural deduction. In particular, it becomes evident that the absence of such inferences in single-oriented systems, like natural deduction or natural deduction with general elimination rules, does not entail an absence of “detours”, whereas it does for bioriented systems—indeed, absence of co-identity in bioriented systems entails the very impossibility of even expressing “detours” (in the same way as the impossibility of expressing “detours” is entailed by the absence of cut in the sequent calculus). This observation provides evidence against a quite hasty account of the cut rule, according to which it can be matched either to a redundancy or to composition of derivations, indiscriminately (thus, sometimes, erroneously establishing a link between the two notions). Instead, the cut rule should be rather read as a principle of reasoning, whose potential depends very much on the formal context within which it is employed and whose correspondence to the idea of redundancy is only a—very interesting indeed—particular case of a much broader range of effects.