3.

GROUNDWORK -  PROPOSITIONAL SEQUENT-LOGIC

Introduction

TO this point, the object of our study has been a family of logics called propositional calculi; in particular, we have studied systems known as the intuitionist and the classical propositional calculi, IC and PC respectively. We now expand our study to include systems that in a sense are metatheoretical, that tell us things about our propositional logics, but which we shall study as object systems just as we did the calculi of the preceding sections.

In our study of propositional calculi, we have proved a number of important metatheorems, and in doing so, we have begun to put forward a 'theory of deduction'. This theory of deduction is informal, for it is stated in the unformalized language of mathematical English (this is in contrast to the objects of study, the propositional calculi themselves, which are indeed formalized, and formalized within the metalanguage of mathematical English). We may think of what we are about to do as a formalization of a part of our developing theory of deduction. We shall therefore define new systems, systems which will contain the notation of the propositional calculus and more besides, systems which may be thought of as formalizing part of the process of deducing propositional calculus statements from other propositional calculus statements. The principal way in which we shall use these systems is to provide decision procedures both for the propositional calculi we have been examining and for many of the modal systems we shall study; other points of metatheory may also be conveniently handled by them, however. Systems of the kind studied here were first developed in detail in Gentzen 1934; the rules we use are generally in the form of Ketonen 1944; our notation and terminology generally follows Kleene 1952.

Formulas, sequences, and sequents

As we have remarked, the systems of the present chapter will include all the symbols of the propositional calculus and the rules of formation for those symbols; a set of symbols will be called a wff here iff it is a wff in the standard propositional calculi. In addition to the symbols and rules of the propositional calculus, the present systems will have as part of their formal body of signs two additional symbols, the comma ',', and the arrow '®'. The comma will be used to form formal objects called 'sequences'; the sequence may be defined as follows (note that we use upper case Greek letters as metalinguistic signs for sequences, just as we use lower case Greek for formulas)

(1) An individual wff constitutes a sequence; 

(2) Where G and D are sequences, so too is 

G, D.

For purposes of clause (1), we include among the wffs a very special one, the 'null' formula, the blank space. Thus a sequence is a string of zero or more formulas, separated (when there are more than one) by commas.

The arrow will be used to form formal objects from sequences; these objects will be called 'sequents'. Thus we refer to the systems of the present chapter as 'sequent logics'. The definition of a sequent is simple:

Where G and Q are sequences,

G ® Q

is a sequent.

The sequent G ® Q may be read 'G yields Q'. Where Q is a single formula and g_l, . .  , g_n are the formulas constituting G, this sequent might be interpreted as a formalization of the metalinguistic statement

g_l, . .  , g_n q

where q is the one member of Q. Clearly, then, the simple ® Q might be interpreted as the statement 'Q is a theorem'. The notation of the sequent-logics is a bit broader at this point, however, than is that of the metalanguage we have been using, for we have attached no sense, till now, to a metalinguistic expression like a, b, which would have more formulas than one to the right of its sign of deducibility. In sequent-logic we must supply an interpretation for this situation. It is clear that when we write G ® Q, we mean to assert that Q follows from the conjunction of all the formulas of G, of all the formulas to the left of the arrow; we may say that the sequence to the left of the arrow is interpreted conjunctively, and this agrees with our intuitive grasp of the set of formulas which may appear to the left of the metalinguistic sign F. Τo maintain certain structural parallels between the left side of the arrow and the right, however, the sequence to the right will not be interpreted conjunctively, but rather disjunctively. G ® Q will be meant to assert that the disjunction of all the formulas of Q follows from the conjunction of all those of G. For convenience, from now on we shall refer to the sequence to the left of the arrow as the 'antecedent' and that to the right as the 'succedent' of the sequent.

There is another point of interpretation needed here which does not arise in the ordinary metalanguage of the PC. We have remarked that ® a could be read 'a is a theorem'; it states, in short, that a is deducible from the empty set of hypotheses. But in sequent-logic, the sequence Q in the sequent G ® Q may be empty; how is the sequent Ρ, to be interpreted? Just as the maintenance of structural parallels requires that a non-null sequence right of the arrow be interpreted differently, in general, from one left of it, so too will the null sequence right differ from the null sequence left. Where ® Q means that the disjunction of Q's formulas is a theorem, G ® may be taken to mean that the conjunction of Gs formulas is contradictory. G ® may then be interpreted as the negation of the conjunction of the formulas of Γ. Another way of looking at it is to say that the empty sequence as antecedent is interpreted as a constant true proposition, and as succedent as a constant false proposition, the arrow always being a kind of implication.

We shall, in fact, have occasion to refer in a very specific manner to interpretations of sequents in ordinary propositional logic. For these purposes, the 'interpretation of the sequent G ® Q in the ordinary propositional calculus' will be the formula Cgq, where

(1) If G contains more formulas than one, g will be the conjunction of those formulas;

(2) If Q contains more formulas than one, q will be the disjunction of those formulas;

(3) If G or Q contains exactly one formula, g  or q respectively will be that formula;

(4) If G is empty, g will be a constant true formula; 

(5) If Q is empty, q will be a constant false formula.

The sequent is interpreted as showing a relationship of deducibility between its succedent and its antecedent; this is the deducibility which is formalized by the sequent logic. But there is a notion of deducibility which applies to the sequent logic itself, the notion of the deducibility of one sequent from another, or from a preceding set of sequents.

Sequent generation

To express this notion of deducibility, we must move into the (unformalized) metalanguage in which we talk about sequent logics; in short, we shall state a number of rules of inference which will permit us to generate new sequents from old; the old sequents are the premises and the new are the conclusions. We shall express the rules of inference by writing the premiss or premises above and the conclusion below a horizontal line. Most of the rules we use are one-premiss rules, but a few of them employ two premises. Proofs in the system will be constructed as strings of instances of the rules; each step except the last will provide in its conclusion a premiss for further steps, and premises will be separated from their conclusions by horizontal lines. Since there are two-premiss rules, branchings will occur in many proofs, and indeed, the proof will fall into a tree form, with the final conclusion at the very bottom -- this final conclusion may be referred to as the 'end sequent'. Α continuous line of proof from the tip of one of the branches to the end sequent will be called a 'proof string'. The tips of the branches are our starting-points, and the top sequent in every branch will be an axiom of the system; the axioms are all defined by one axiom schema; where a is a wff, not including the null formula,

a ® a

is an axiom of the sequent logics we are discussing.

The rules of inference fall into two general classes. The function of one of these classes of rules is to introduce new symbols into sequents, specifically to introduce instances of the connectives of the propositional calculus; these rules are called the 'logical' rules of inference. The rules of the other set do not deal with specific logical symbols, but rather with 'housekeeping chores', in general, with manipulating of certain formulas within the sequents; these rules are called the 'structural' rules of inference. Four of the structural rules 'pair off', defining two 'structural functions' with one member of each functional pair affecting the antecedent and the other the succedent of the sequent. We display these rules in the following table.

The weakening rules permit the addition of an arbitrary wff to either the antecedent or the succedent of a sequent; the contraction rules permit the dropping of duplicated formulas. An additional functional pair of rules is often stated in addition to weakening and contraction; these rules, commonly called 'interchange' or some similar name, permit the rearrangement of formulas in the antecedent and succedent. Rather than stating this pair of rules specifically, we shall simply consider a sequent standing in a proof to represent a11 sequents formable by simply permuting- the formulas in the antecedent and in the succedent of the original sequent; thus, the location of a formula in a given antecedent or succedent will not affect the way it enters into the application of rules of the system. In addition to the rules in the table above, there is one more rule classified as structural, a rule about which we shall be hearing a considerable amount; it is called 'cut':

Cut differs from the other structural rules, of course, in that it has two premisses. It also differs from them and from all the other rules in that a formula appearing in a premiss (a) fails to occur itself or as a subformula of another formula in the conclusion.

We now move to the logical rules. As with the structural rules, the logical rules fall into functional pairs, one pair for each of the operators of the propositional calculus. One member of each pair governs the introduction of an operator into the antecedent of a sequent, and the other governs its introduction into the succedent.

These rules will be called 'the rule for C (or other connective involved) in antecedent (in succedent)' or the rule 'C-left (C-right)' etc. They will most commonly be designated in even briefer form by writing an arrow with the appropriate connective letter to its left or right as the rule being named happens to be, respectively, an antecedent or a succedent rule. The above rules, then, are C® , ®C, Κ® , ®Κ, Α® , ®Α, Ν®, ®N. Notation due to Kleene 1952. It will be noticed that certain formulas in the premisses of the rules (both logical and structural) will pass through the application of the rule unchanged; these may be referred to as parametric formulas. The formulas explicitly shown in the premises of the rules (a and b) will be called 'side formulas', while those specifically shown in the conclusions (those introduced) will be called 'main formulas' or 'principal formulas'.

Sequent-logic and propositional calculus

Though we have listed above only one set of rules, it is evident that we have defined two separate systems of sequent logic. The specifications on the rules of weakening in the succedent, C®, ®Α, and ®N are such that any proof employing only the intuitionistic versions of these rules will be a proof in the intuitionistic sequent-logic, which we shall call LIC. Α proof employing the classical versions of these rules is a proof in the classical sequent-logic, called LPC. Our first task will be to show that LIC and LPC are equivalent, respectively, to IC and PC.

We cannot, of course, have equivalence here in the sense that every theorem of the one system will be a theorem of the other and vice versa, for IC and PC have as their theorems wffs, while the theorems of LIC and LPC are sequents. Α notion of equivalence can, however, be formulated in a manner convenient for our purpose. We shall say that a sequent-logic and an ordinary logic are equivalent iff the formula a is a thesis of the latter when and only when the sequent ® a a theorem of the former. We state part of the required equivalence in the following:

We start out by proving that when a is an axiom of  IC, ® a is provable in LIC (and so in LPC) and furthermore, that axiom C3, CCCpqpp, is provable in LPC. We first prove axiom C2:

The end sequent of this proof corresponds to axiom C2 of IC. Actually, it should be evident that this end sequent also corresponds to all substitution instances of axiom C2. This will be the case with each sequent which we prove corresponding to an axiom; any substitution instance of the axiom may be proved in a manner exactly similar to the proof of the axiom. This will mean, of course, that we have in these systems the equivalent of the rule of substitution for variables. Note, by the way, that in the above proof we have placed the name of the rule employed at each step at an end of the horizontal line associated with that step. This will be our common way of justifying steps in these proofs. We turn to axiom C1 of IC:

The final sequent in this proof corresponds to axiom Cl, Frege; again, all substitution instances of Frege are clearly derivable in parallel proofs. The reader should have no trouble constructing proofs for sequents corresponding to the rest of the axioms of IC; we shall here offer proofs for a couple more of them, however, as further examples of the use of the rules of inference.

Two more applications of the rule ®C will give an end sequent corresponding to axiom Α3 (and, again, all its substitution instances). We present one more example of a proof in LIC of an IC axiom:

The end sequent of this proof corresponds to reductio ad absurdum, axiom Ν1. Proof of sequents corresponding to the remaining IC axioms is left to the reader. We may take it as shown, then, that if a is an axiom of IC, then ® a is a theorem of LIC; indeed, considering our arguments accompanying the above proofs, we may say that if a is any substitution instance of an axiom of IC, then ® a is provable in LIC.

Let us now assume that the sequents  ® a and  ® Cab are both provable in LIC; we have then (using for the first time the rule of cut)

Using cut, then, we are able to move from the assertion of ® a and  ® Cab to the assertion of ® b. The system LIC then contains an analogue of the rule of detachment as a derived rule of inference. Since all substitution instances of sequents corresponding to axioms of IC are provable, this means that substitution for variables is also a derived rule of inference, and so we have shown that *3.1, as it applies to IC and LIC, holds; that is, that if a is a theorem of IC, then ® a will be a theorem of LIC.

We now turn to the systems PC and LPC. The reader may easily satisfy himself that if a sequent is provable by the LIC versions of our rules, then it will be provable by the LPC versions. In addition, we will have certain proofs which are characteristic of LPC.

This last end sequent corresponds to Peirce, axiom C3. It is clear, then, that the broadening of the rules of LIC to those of LPC permits the proof in LPC of sequents corresponding to all theses of PC, and so if a is a PC thesis, ® a is a theorem of LPC, and *3.1 holds for PC and LPC.

There are other ways to obtain the above result; we show two of them to illustrate the use of the classical versions of the rules.

This last sequent corresponds to strong double negation, which if added to IC yields PC; note that only the rule ®N is used here in its classical version.

This last end sequent again corresponds to a formula which if added to IC extends it to PC; here only weakening and ®A in their classical forms are used. We thus see that there is a certain amount of redundancy in the rules we have offered for classical sequent-logic.

We now quickly state and prove a metatheorem which expresses the basic difference between the classical and the intuitionist sequent-logics:

We note that the succedent of an LIC axiom has always one member; further, the only rules that increase the number of formulas in a succedent are weakening and ®N. But in LIC these rules can be used only to increase that number from zero to one. By induction on number of steps needed to prove a sequent in LIC, then, *3.2 follows.

We now turn to the converse of *3.1, which is:

We prove *3.3 by first proving a lemma which is actually more general than *3.3:

First of all, an axiom of one of our sequent logics is always of form 

a ® a

The interpretation of this sequent as earlier defined is the formula Caa, which is a thesis of both IC and PC. Now let S be a sequent of LIC or LPC; we shall then call i(S) the formula of IC or PC which is the interpretation of S. Consider any of the one-premiss rules of LIC (LPC), letting S₁ be the premiss and S₂ the conclusion of that rule. We shall see that in the case of each of these rules, the statement 'If i(S₁) then i(S₂)' is a derived rule of inference in IC (PC). Similarly for the two-premiss rules; taking S₁ and S₂ as the premisses and S₃ as the conclusion of any of these rules, we shall find that the statement 'If i(S₁)  and i(S₂) then i(S₃)' i is a derived rule of inference of IC (PC). The presence of these rules of inference in IC (PC) coupled with the fact that all sequent-logic axioms have their interpretations as theses of IC and PC will be sufficient to prove *3.4. We turn now to proof of these rules of inference in IC (PC).

The general form of i(S) where S is the premiss of the rule of weakening in the antecedent is Cgq for non-empty and C 1q (with 1 as a constant true proposition) for empty antecedent. CKagg and CKal (both IC (PC) theses) along with syl justify the movement in IC (PC) respectively to CKagq  and Cgq , the forms of the interpretation of the conclusion of weakening in the antecedent in the nonempty and the empty antecedent cases. Thus there is in IC (PC) a rule of inference paralleling this sequent logic rule. Similarly for weakening in the succedent; the relevant i(S) forms here for S as premiss are  Cgq  and  CgÆ  (Æ = constant false proposition) for the non-empty and the empty succedent cases. By. the theses CqAqa  and CÆa  we move to the proper conclusion forms, CgAqaa and Cga.

Analogues of the rules of contraction in the antecedent and in the succedent are present in IC (PC) by virtue of SBC and the theses ΕpΚpp and ΕpΑpp. The permission to consider all permutations of a sequence as equivalent to that sequence must also be considered here; this permission is justified by SBC and the theses EKpqKqp and EApqAqp.

The last structural rule is cut; for the system LIC, where S₁ and S₂ are the left and the right premisses of cut, by *3.2 the sequence Q must be empty, and so i(S₁) and i(S₂) are Cga and CΚadl (or Cal for empty D). By SSI we move immediately from these formulas to CΚgdl (or Cgl) as required for the interpretation of S₃, where S₃ is the conclusion of cut. In LPC, we must consider the case where Q is non-empty; here  i(S₁) is CgAqa, i(S₂) as before. In the classical PC, thisi(S₁) is equivalent to CgCNqa and so to CKgNqa; this last formula with i(S₂) and SSI yields CKKgNqdl; classically, this easily transforms to CKgdAql, the interpretation of the conclusion of cut with non-empty G, D, Q, and L. The proof must be varied somewhat as different combinations of these sequences occur empty; details are left to the reader. We see, then, that the rule cut has an analogue in IC and PC.

Turning to the rule C®, we note that the interpretations i(S₁) and i(S₂) of the left and the right premises (in LIC) are Cga and CKbgq, for non-empty G. In IC, modus ponens, CpCCpqq, and i(S₁) give CgCCabb, which comms and imports to CKCabgb. This with i(S₂) and SSI yields CKKCabggq; the iterated g in this formula is dropped, ultimately, by ΕpKpp, leaving us with the interpretation of the conclusion of this rule. Proof for the case in which G is empty is similar and is left to the reader, as is the proof for the rule in LPC.

Left to the reader too will be the proofs for the rest of the logical rules; we shall supply here, however, the key theorems of IC and PC employed in the proofs for each of these rules -- working out the details of the proofs will then be simple. For ®C, use 2.45, CCKpqrCpCqr; for K®, the interpretations of the premiss and the conclusion will be the same, as they will for the classical ®A (for intuitionist ®A, use axioms Α1 and Α2, CpApq and CqApq); for -®K, use 2.37, CCpqCCprCpKqr; for A®, use axiom Α3, CCprCCqrCApqr; for N®, use the equivalence ENpCpÆ and importation (a bit more detail is required in all these for the full classical cases); for the intuitionist ®N, use exportation and ENpCpÆ; for the classical ®N, use exportation and the 'definitional' equivalence ECpqANpq. We may now consider lemma *3.4 proved.

The proof of *3.3 follows immediately. If ®a is provable in LIC (LPC), then (with 1 as constant true) its interpretation C1a is an IC (PC) thesis by *3.4. But 1 is an IC (PC) thesis itself, and so by detachment we have a as an IC (PC) thesis.

From *3.1 and *3.3 comes the statement of equivalence of the ordinary propositional calculi and the sequent logics of this chapter:

The 'normal form' theorem

We now come to the metatheorem which is the heart and centre of the theory of sequent-logics. Gentzen 1934 refers to it as his Hauptsatz, his principal assertion; Curry 1963 calls it the 'elimination theorem'; we shall follow Kleene 1952 in referring to it as the 'normal form theorem'.

This metatheorem is called the normal form theorem not because it has anything to do with a formula or sequent in some normal form, but because it states that any proof in our sequent-logics may be put into a certain standard form. The normal form theorem will show, essentially, that any sequent provable in LIC or LPC will be derivable in a proof in which each succeeding step in a proof string will be no shorter than the step which precedes it. (An exception here is shortening of a sequent by contraction; we shall see later, however, that contraction as well as cut is redundant as a rule of inference.) As it turns out, every formula occurring in a sequent of a given proof string will occur as a subformula in every sequent below the sequent in which it initially occurred; this property of certain proofs in sequent-logics may be called the 'subformula property'. The specific proofs always having the subformula property are those in which no application of the rule cut occurs; before going on to the normal form theorem, we state a metatheorem about the subformula property:

Proof is immediate; it may be verified by examination of the rules other than cut.

We now begin to move toward the statement and proof of the normal form theorem, which in the presence of *3.6 will permit us to assert that all theorems of LIC (LPC) are provable in proofs having the subformula property. It will be simplest to do so by slightly altering our systems; what we shall do is to replace the rule cut by a very similar rule which simplifies the requisite proofs but is exactly equivalent to cut in so far as the present matter is concerned. The new rule is called 'mix' and is as follows:

m is a formula having one or more occurrences in each of D and Q, and is called the 'mix formula'. The sequences D_m and Q_m are like D and Q except for having all occurrences of m deleted. The system formed by replacing cut by mix in LIC (LPC) is called LIC' (LPC'). Now suppose that the rule cut is applied somewhere in an LIC (LPC) proof (using the notation of the original presentation of cut). If this cut is replaced by a mix with a -- the formula eliminated by the cut -- as mix formula, the conclusion will be G, D_a ® Q_a, L (with D_a and Q_a free of the formula a) rather than  G, D ® Q, L. But if D or Q originally contained occurrences of a, these occurrences may now be restored in D_a and Q_a, by appropriate applications of weakening, attaining the same result as did the cut. On the other hand, if a mix occurs in an LIC' (LPC') proof, the occurrences of the mix formula in D and Q in the premises may be reduced to one in each of those sequences by proper applications of contraction, transforming the premises to G ® Q_m, m and m, D_m ® L; an application of cut to these preτnisses yields the conclusion of mix as indicated above. On the basis of this argument, we may state:

This last sentence follows from the fact that the systems are identical except for the cut-mix distinction. We shall now state the normal form theorem for LIC and LPC; *3.7 then permits us to prove it by showing that the rule mix is redundant in LIC' and LPC'.

The proof of *3.8 involves a triple induction; the main induction is on the number of applications of mix occurring in an LIC' (LPC') proof. For this induction, we note that if a proof contains any applications at all of mix, then it contains one which is the 'highest' application of mix in the proof, that is, one which has above it no applications of mix. If we are able to eliminate applications of mix above which there are no applications of mix, then we can successively eliminate all applications of mix in a proof, working from the top of the proof tree to the bottom. This first induction, then, reduces the proof of *3.8 to a question of showing that a proof containing a single mix may be replaced by a proof with the same end sequent and containing no mixes.

It will be sufficient, then, to consider an LIC' (LPC') proof whose last step is an application of mix, and in which there is no other application of mix. We have already done one of our three inductions; the present case is then a double induction, first of all on a property of the mix in question called grade, and -- within the induction on grade -- on a property of the mix called rank. The grade of a mix is dependent on the mix formula μ of that mix; specifically, it is equal to the number of occurrences of connectives -- C, Κ, Α, Ν -- in the mix formula. We turn now to rank; to determine the left rank of a mix, examine each proof string which terminates in the left premiss of that mix, counting upwards from the left premiss (inclusive) the number of consecutive sequents in that proof string that contain the mix formula m in their succedents. After checking each such proof string, the highest such number is the left rank of the mix. The right rank is determined similarly, counting upwards from the right premiss the presence of m in antecedents. The rank itself is the sum of the left and the right ranks.

We shall first set up the subordinate induction, that on rank; there are some preliminaries. Our mix will be of form

Suppose that m is in G (m is in L ). Here we may begin with the right preτniss (or, in the m in L case, the left premiss) alone, as follows:

In either case, then, the conclusion is derivable by weakening and contraction and so the mix may be eliminated.

In the cases we consider, we assume that this preliminary case is not in question. We turn now to the induction step of the induction on rank. Let us assume that whenever the rank of a mix with no mixes above it is £ j (with j ³ 2, for each of the left and the right ranks must be at least = 1) that mix is redundant. Consider now the cases in which the mix is of rank j + 1. Since  j ³ 2, at least one of the left or right ranks will be³ 2; if a side has a rank ³ 2 the premiss (of mix) on that side cannot be an axiom, but must be the conclusion of a rule application, structural or logical. Look first at the case in which the left rank ³ 2, the left premiss of the mix is the conclusion of a single-premiss rule, and the mix formula is parametric (neither a principal nor a side formula) in that rule. Here the bottom of the proof is of form:

We replace this deduction by the following:

The original rule, whatever it is, may now be applied to the conclusion of this mix to yield the sequent G, D_m ® Q_m, L. But the mix in this latter deduction is of rank j, and so falls into the scope of the induction hypothesis and may be eliminated. This applies both to the classical and the intuitionist systems, of course; note that the restrictions on the intuitionist rules of ®N  and weakening in the succedent cause us no problem, for neither of these rules can be involved here-else m would have to be the principal formula of the rule, which is excluded for this case.

If the right rank is ³ 2 and the right premiss of the mix is again the conclusion of a single premiss rule with m parametric, the treatment is just as above; here, of course, form the new deduction by first mixing the premiss of the rule involved with the left premiss of the original mix, and apply the rule to the conclusion of the mix. If the rule involved here is the intuitionist ®N  or weakening in the succedent, we point out that by the restrictions on those rules, S (succedent of the rule involved) is empty and Q (succedent of the left premiss of the original mix) is simply m, by *3.2. The end of the proof in question for these two rules is then:

This is replaced by:

This achieves the required results within the necessary restrictions.

Now let us consider the cases in which the left rank is ³ 2, the rule from which the left premiss results is a single-premiss rule, and the mix formula is the principal formula of that rule. In this case, the rule must be a succedent rule, and the general form of the end of the original proof will be:

This may be replaced by:

The end sequent of this proof is easily converted by contraction to that of the original proof. The upper mix in the new proof is of rank j and so is able to be eliminated by the induction hypothesis. The lower mix may then be considered to have no mixes above it; we note that the left rank of this mix is precisely 1, while its right rank is the same as that of the original proof. Its total rank, then, is equal to or less than j, for the left rank of the original proof was ³ 2. The lower mix then also falls into the scope of the induction hypothesis, and so is eliminable. Note that if the rule involved is contraction, execution of the upper mix alone will give us the desired result. Again, we have no trouble with the rules ®N and weakening on the right in their intuitionist forms; since the premisses of these rules must have empty succedents, the left rank of mixes whose left premisses are derived by these rules cannot be greater than one, while here it must be at least two. These rules are then excluded from consideration here.

The cases in which the right rank is ³ 2, the rule involved is a single-premiss rule, and the mix formula is the principal formula of that rule, are treated in similar fashion to the cases above; here, of course, the rules involved are antecedent rules, and the replacing proof will start out by mixing the premiss of the rule involved with the left premiss of the original mix, applying the rule, and mining the result of the application again with the left premiss of the original mix; contraction again will be given the briefer treatment indicated in the above paragraph.

We now turn to cases in which the left rank is ³ 2, the rule involved is a single-premiss rule, and the mix formula is the same as a side formula of the relevant rule; here only the logical rules are involved. The general form of deduction here is:

Replace this deduction by: