Formal Logic/Sentential Logic/Subderivations and Discharge Rules

← Constructing a Simple Derivation

↑ Sentential Logic

Constructing a Complex Derivation →

Subderivations and Discharge Rules

As already seen, we need three more inference rules, Conditional Introduction (CI), Negation Introduction (NI), and Negation Elimination (NE). These require subderivations.

Deriving conditionals

Example derivation

We begin with an example derivation which illustrates Conditional Introduction, then follow with an explanation. A derivation for the argument

$\mathrm {Q} \land \mathrm {R} \!$   ∴   $\mathrm {P} \rightarrow \mathrm {Q}$

is as follows:

1.   $\mathrm {Q} \land \mathrm {R} \,\!$   Premise   2.     $\mathrm {P} \,\!$   Assumption 3.     $\mathrm {Q} \,\!$   1 KE   4.   $\mathrm {P} \rightarrow \mathrm {Q} \,\!$   2–3 CI

Lines 2 and 3 constitute a subderivation. It starts by assuming desired formula's antecedent and ends by deriving the desired formula's consequent. There are two vertical fences between the line numbers and the formulae to set it off from the rest of the derivation and to indicate its subordinate status. Line 2 has a horizontal fence under it to separate the assumption from the rest of the subderivation. Line 4 is the application of Conditional Introduction. It follows not from one or two individual lines but from the entire subderivation (lines 2–3) as a whole.

Conditional Introduction is a discharge rule. It discharges (makes inactive) that assumption and indeed makes the entire subderivation inactive. Once we apply a discharge rule, no line from the subderivation (here, lines 2 and 3) can be further used in the derivation.

The Conditional Introduction rule

To derive a formula $(\varphi \rightarrow \psi )\,\!$, the rule of Conditional Introduction (CI) is applied by first assuming in a subderivation that the antecedent $\varphi$ is true, then deriving $\psi$ as the conclusion of the subderivation. Symbolically, CI is written as

${\underline {{\text{Assume }}\varphi {\text{, derive }}\psi }}$

$(\varphi \rightarrow \psi )\,\!$

Here, the consequent line is not inferred from one or more antecedent lines, but from a subderivation as a whole. The annotation is the range of lines occupied by the subderivation and the abbreviation CI. Unlike previously introduced inference rules, Conditional Introduction cannot be justified by a truth table. Rather it is justified by the Deduction Principle introduced at Properties of Sentential Connectives. The intuition behind why we assume $\varphi$ in order to derive $(\varphi \rightarrow \psi )\,\!$, however, is that $(\varphi \rightarrow \psi )\,\!$ is true by definition if $\varphi$ is false. Thus, if we show $\psi$ is true whenever $\varphi$ happens to be true, then $(\varphi \rightarrow \psi )\,\!$ must be true.

Note that the antecedent subderivation can consist of a single line serving both as the assumed $\varphi \,\!$ and the derived $\psi \,\!$, as in the following derivation of

∴   $\mathrm {P} \rightarrow \mathrm {P} ,$

1.     $\mathrm {P} \,\!$   Assumption   2.   $\mathrm {P} \rightarrow \mathrm {P} \,\!$   1 CI

Negations

Example derivation

To illustrate Negation Introduction, we will provide a derivation for the argument

$\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {R} ,\ \mathrm {P} \land \lnot \mathrm {Q} \!$   ∴   $\mathrm {Q} \lor \mathrm {R} \,\!$

1.   $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\rightarrow \mathrm {R} \,\!$   Premise 2.   $\mathrm {P} \land \lnot \mathrm {Q} \,\!$   Premise   3.     $\mathrm {P} \rightarrow \mathrm {Q} \,\!$   Assumption 4.     $\mathrm {P} \,\!$   2 KE 5.     $\mathrm {Q} \,\!$   3, 4 CE 6.     $\lnot \mathrm {Q} \,\!$   2 KE   7.   $\lnot (\mathrm {P} \rightarrow \mathrm {Q} )\,\!$   3–6 NI 8.   $\mathrm {R} \,\!$   1, 7 CE 9.   $\mathrm {Q} \lor \mathrm {R} \,\!$   8 DI

Lines 3 through 6 constitute a subderivation. It starts by assuming the desired formula's opposite and ends by assuming a contradiction (a formula and its negation). As before, there are two vertical fences between the line numbers and the formulae to set it off from the rest of the derivation and to indicate its subordinate status. And the horizontal fence under line 3 again separates the assumption from the rest of the subderivation. Line 7, which follows from the entire subderivation, is the application of Negation Introduction.

At line 9, note that the annotation '5 DI' would be incorrect. Although inferring $\mathrm {Q} \lor \mathrm {R} \,\!$ from $\mathrm {Q} \,\!$ is valid by DI, line 5 is no longer active when we get to line 9. Thus we are not allowed to derive anything from line 5 at that point.

The Negation Introduction rule

Negation Introduction (NI)

${\underline {{\text{Assume }}\varphi {\text{, derive }}\psi {\text{ and }}\lnot \psi }}$

$\lnot \varphi \,\!$

The consequent line is inferred from the whole subderivation. The annotation is the range of lines occupied by the subderivation and the abbreviation is NI. Negation Introduction sometimes goes by the Latin name Reductio ad Absurdum or sometimes by Proof by Contradiction.

Like Conditional Introduction, Negation Introduction cannot be justified by a truth table. Rather it is justified by the Reductio Principle introduced at Properties of Sentential Connectives.

Another example derivation

To illustrate Negation Elimination, we will provide a derivation for the argument

$\lnot (\lnot \mathrm {P} \lor \lnot \mathrm {Q} )\land \mathrm {R} \!$   ∴   $\mathrm {P} \,\!$

1.   $\lnot (\lnot \mathrm {P} \lor \lnot \mathrm {Q} )\land \mathrm {R} \,\!$   Premise   2.     $\lnot \mathrm {P} \,\!$   Assumption 3.     $\lnot \mathrm {P} \lor \lnot \mathrm {Q} \,\!$   2 DI 4.     $\lnot (\lnot \mathrm {P} \lor \lnot \mathrm {Q} )\,\!$   1 KE   5.   $\mathrm {P} \,\!$   2–4 NE

Lines 2 through 4 constitute a subderivation. As in the previous example, it starts by assuming the desired formula's opposite and ends by assuming a contradiction (a formula and its negation). Line 5, which follows from the entire subderivation, is the application of Negation Elimination.

The Negation Elimination rule

Negation Elimination (NE)

${\underline {{\text{Assume }}\lnot \varphi {\text{, derive }}\psi {\text{ and }}\lnot \psi }}$

$\varphi \,\!$

The consequent line is inferred from the whole subderivation. The annotation is the range of lines occupied by the subderivation and the abbreviation is NE. Like Negation Introduction, Negation Elimination sometimes goes by the Latin name Reductio ad Absurdum or sometimes by Proof by Contradiction.

Like Negation Introduction, Negation Elimination is justified by the Reductio Principle introduced at Properties of Sentential Connectives. This rule's place in the Introduction/Elimination naming convention is somewhat more awkward than for the other rules. Unlike the other elimination rules, the negation that gets eliminated by this rule does not occur in an already derived line. Rather the eliminated negation occurs in the assumption of the subderivation.

Terminology

The inference rules introduced in this module, Conditional Introduction and Negation Introduction, are discharge rules. For lack of a better term, we can call the inference rules introduced in Inference Rules 'standard rules'. A standard rule is an inference rule whose antecedent is a set of lines. A discharge rule is an inference rule whose antecedent is a subderivation.

The depth of a line in a derivation is the number of fences standing between the line number and the formula. All lines of a derivation have a depth of at least one. Each temporary assumption increases the depth by one. Each discharge rule decreases the depth by one.

An active line is a line that is available for use as an antecedent line for a standard inference rule. In particular, it is a line whose depth is less than or equal to the depth of the current line. An inactive line is a line that is not active.

A discharge rule is said to discharge an assumption. It makes all lines in its antecedent subderivation inactive.