Kirk Rader  1.0-SNAPSHOT
Inference Rules

Axioms of symbolic logic expressed as formula transformations.

We have already seen an example of a logical argument expressed as formulas of the sentential calculus. The proof that $Q$ follows from $P$ and $P \rightarrow Q$ relies on the inference rule* traditionally known as modus ponens. Modus ponens is one of a number of such rules that owe their names to the history of syllogisms and similar attempts to turn informal critical reasoning into a more rigorous discipline.

Like truth tables, such inference rules correspond to axioms and theorems of symbolic logic. Here are a few examples:

\[ \begin{aligned} & \textit{modus ponens} \\ & \phi \rightarrow \psi \\ & \phi \\ \hline \\ \therefore & \psi \end{aligned} \]

\[ \begin{aligned} & \textit{modus tollens} \\ & \phi \rightarrow \psi \\ & \lognot \psi \\ \hline \\ \therefore & \lognot \phi \end{aligned} \]

\[ \begin{aligned} & \textit{modus tollendo ponens} \\ & \phi \vee \psi \\ & \lognot \phi \\ \hline \\ \therefore & \psi \end{aligned} \]

\[ \begin{aligned} & \textit{modus ponendo tollens} \\ & \lognot (\phi \wedge \psi) \\ & \phi \\ \hline \\ \therefore & \lognot \psi \end{aligned} \]

There are many more such inference rules with traditional names. See for more examples.

Just as the simple truth tables for individual connectives can be combined to form truth tables for arbitrarily complex formulas, applications of these rules can be combined to prove arbitrarily complex logical arguments. Kalish & Montague refined work done by Jaskowski and others, devising what have become standard techniques for carrying out such proofs in their classic text, Logic: Techniques of Formal Reasoning [1].