24. Appendix: Natural Deduction Rules

Implication:

Conjunction:

Negation:

Disjunction:

Truth and falsity:

Bi-implication:

Reductio ad absurdum (proof by contradiction):

The universal quantifier:

In the introduction rule, $x$ should not be free in any uncanceled hypothesis. In the elimination rule, $t$ can be any term that does not clash with any of the bound variables in $A$.

The existential quantifier:

In the introduction rule, $t$ can be any term that does not clash with any of the bound variables in $A$. In the elimination rule, $y$ should not be free in $B$ or any uncanceled hypothesis.

Equality:

Strictly speaking, only $\mathrm{refl}$ and the second substitution rule are necessary. The others can be derived from them.