Derivations
Let's look at our last example and the sequence of inferences we made:
| 1. | P ⊃ (Q & R) | premise |
| 2. | P | premise |
| 3. | (Q & R) | mp 1, 2 |
| 4. | Q | simp, 3 |
We have a numbered sequence of wffs. Every wff is either a premise or is inferred from an earlier line by a rule of inference. We call such a sequence of wffs a derivation. Every line of a derivation has a line number, a wff, and a justification. We construct derivations by applying rules of inference to given wffs, or premises. A derivation can be as short as one line, in which case it would simply be a premise, or any finite length.
Here's another derivation:
| 1. | (A ⊃ (~B v E)) & (~C ⊃ ~D) | premise |
| 2. | (A & ~C) | premise |
| 3. | (A ⊃ (~B v E)) | simp, 1 |
| 4. | A | simp 2 |
| 5. | (~B v E) | mp 3, 4 |
| 6. | (~C ⊃ ~D) | simp 1 |
| 7. | ~C | simp 2 |
| 8. | ~D | mp 6, 7 |
In this derivation, we begin with two premises. They are both conjunctions. Simplification is the rule of inference we have for conjunctions, so we apply it. Notice that at line 3 we've applied it by inferring the left conjunct, which is itself a complex wff. To apply the rules of inference correctly, we must play attention to the main operator.
