As illustrated by the derivation given at the end of Chapter 4, using the deduction theorem under the form of an admissible inference rule may be quite useful. In this chapter, we introduce several other rules, and we show that they are admissible. We start with the three following structural rules:

Rule "identity" is not quite a rule. It just expresses a fact that corresponds to the first clause of Definition 10. When seen as a rule, "identity" corresponds to a degenerated rule in the sense that it does not have any premise. Consequently, it may be used as a leave in a derivation tree.

Rule "cut" is just a shortcut for the following piece of derivation:

Finally, Rule "weakening" corresponds to the quite intuitive fact that a derivable formula remains derivable when extending the set of hypotheses. This may be established by a straightforward induction on the definition of a formula provable under a set of hypotheses (Definition 10).

We now give a first collection of systematic rules. This collection is organized into introduction and elimination rules, and there are such rules for each connective. Intuitively, an introduction rule for a given connective stipulates how to prove a formula whose main connective is the given connective. By contrast, an elimination rule for a given connective allows one to take advantage of a hypothesis whose main connective is the given connective.

There is no introduction rule for ⊥. This corresponds to the fact that there should be no valid way of proving absusrdity. Similarly, there is no eliminartion rule for ⊤.

Rule ($¬¬$) corresponds to reductio ad absurdum, i.e., the reasoning that consists in proving that a statement is true by showing that if it were not true one could derive something impossible. This rule can be seen as a stronger version of ($\text'⊥'$-elim).

It remains to show that all the rules of Definition 11 hold.

It is possible to show that the set of rules of Definition 11 is complete in the sense that every formula that is provable according to the axiomatic system of Chapter 3 can be derived using the rules of Definition 11 together with Rule (identity). For instance, we can prove that that $(α ∧ β)→(β ∧ α)$ is derivable as follows:

The introduction rules of Defintion 11 are also called right-introduction rules because the formula they "introduce" in their conclusion occurs in the right-hand of the deduction symbol ($⊢$). By analogy, one may define a left-introduction rule to be a rule whose introduced formula occurs in the left-hand side of the deduction symbol.

The second collection of systematic rules that we give is organized into left- and right-introduction rules. The right-introduction rules are just identical to the introduction rules of Defintion 11. As for the left-introduction rules, the logical part they play is similar to the one played by the elimination rules.

We now establish the admissibility of the rules of Definition 12.

The set of rules of Definition 12, together with Rule ($¬¬$) is also complete in the sense that it allows every provable formula to be derived. Rule ($¬¬$), which is typical of classical logic, played an important role. It reflects the Aristotelian principle according to which a proposition is either true or false. Without Rule ($¬¬$), we would obtain a weaker logic, known as intuitionistic logic. We end this chapter by giving a derivation of $((α → β) → α) → α$. This formula, which is known as Peirce's law, does not hold in intuitionistic logic. Accordingly, it could not be derived with the rules of Definition 12 only. Using Rule ($¬¬$) is mandatory.