# Constructing a Simple Derivation

Our derivations consists two types of elements.
* Derived lines. A derived line has three parts:
   * Line number. This allows the line to be referred to later.
   * Formula. The purpose of a derivation is to derive formulae, and this is the formula that has been derived at this line.
   * Annotation. This specifies the justification for entering the formula into the derivation.
* Fencing. These include:
   * Vertical lines between the line number and the formula. These are used to set off subderivations which we will get to in the next module.
   * Horizontal lines separating premises and temporary assumptions from other lines. When we get to predicate logic, there are restrictions on using premises and temporary assumptions. Setting them off in an easy-to-recognize fashion aids in adhering to the restrictions.
We often speak informally of the formula as if it were the entire line, but the line also includes the line number and the annotation.

## Rules
### Premises

The annotation for a premise is 'Premise'. We require that all premises used in the derivation are in the first lines. No non-premise line is allowed to appear before a premise. In theory, an argument can have infinitely many premises. However, derivations have only finitely many lines, so only finitely many premises can be used in the derivation. We do not require that all premises appear before other lines. This would be impossible for arguments with infinitely many premises. But we do require that all premises to appear in the derivation appear before any other line.
The requirement that premises used in the derivation appear as its first lines is stricter than absolutely necessary. However, certain restrictions that will be needed when we get to predicate logic make the requirement at least a useful convention.

### Inference rules

We introduced all but two inference rules in the previous module, and will introduce the other two in the next module.

### Axioms

This derivation system does not have any axioms.

## An example derivation

We will construct a derivation for the following argument:
    $\mathrm {P} \land \mathrm {Q} ,\ \mathrm {P} \lor \mathrm {R} \rightarrow \mathrm {S} ,\ \mathrm {S} \land \mathrm {Q} \rightarrow \mathrm {T} \,\!$ ∴ $\mathrm {T} \,\!$
First, we enter the premises into the derivation:
| 1. | $\mathrm {P} \land \mathrm {Q} \,\!$ | Premise |
| 2. | $\mathrm {P} \lor \mathrm {R} \rightarrow \mathrm {S} \,\!$ | Premise |
| 3. | $\mathrm {S} \land \mathrm {Q} \rightarrow \mathrm {T} \,\!$ | Premise |
Note the vertical line between the line numbers and the formulae. That is part of the fencing that controls subderivations. We will get to subderivations in the next module. Until then, we simply put a single vertical line the length of the derivation. Note also the horizontal line under the premises. This is fencing that helps distinguish the premises from the other lines in the derivation.
Now we need to use the premises. Applying KE to the first premise twice. we add the following lines:
| 4. | $\mathrm {P} \,\!$ | 1 KE |
| 5. | $\mathrm {Q} \,\!$ | 1 KE |
Now we need to use the second premise by applying CE. Since CE has two antecedent lines, we first need to derive the other line that we will need. We thus add these lines:
| 6. | $\mathrm {P} \lor \mathrm {R} \,\!$ | 4 DI |
| 7. | $\mathrm {S} \,\!$ | 2, 6 CE |
Now we will use the third premise by applying CE. Again, we first need to derive the other line we will need. The new lines are:
| 8. | $\mathrm {S} \land \mathrm {Q} \,\!$ | 5, 7 KI |
| 9. | $\mathrm {T} \,\!$ | 3, 8 CE |
Line 9 is $\mathrm {T} \,\!$, the conclusion of our argument, so we are done. The conclusion does not always fall into our lap so nicely, but here it did. The complete derivation runs:
| 1. | $\mathrm {P} \land \mathrm {Q} \,\!$ | Premise |
| 2. | $\mathrm {P} \lor \mathrm {R} \rightarrow \mathrm {S} \,\!$ | Premise |
| 3. | $\mathrm {S} \land \mathrm {Q} \rightarrow \mathrm {T} \,\!$ | Premise |
| 4. | $\mathrm {P} \,\!$ | 1 KE |
| 5. | $\mathrm {Q} \,\!$ | 1 KE |
| 6. | $\mathrm {P} \lor \mathrm {R} \,\!$ | 4 DI |
| 7. | $\mathrm {S} \,\!$ | 2, 6 CE |
| 8. | $\mathrm {S} \land \mathrm {Q} \,\!$ | 5, 7 KI |
| 9. | $\mathrm {T} \,\!$ | 3, 8 CE |