Inference Rules

Inference Rules

We have already seen an example of a logical argument 1 expressed as formulas of the sentential calculus. The proof that Q follows from P and PQ 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:

Modus Ponens

$$ \begin{array}{l} \Phi \rightarrow \Psi \\ \Phi \\ \hline \\ \Psi \end{array} $$

Modus Tollens

$$ \begin{array}{l} \Phi \rightarrow \Psi \\ \neg \Psi \\ \hline \\ \neg \Phi \end{array} $$

Modus Tollendo Ponens

$$ \begin{array}{l} \Phi \vee \Psi \\ \neg \Phi \\ \hline \\ \Psi \end{array} $$

Modus Ponendo Tollens

$$ \begin{array}{l} \neg (\Phi \wedge \Psi) \\ \Phi \\ \hline \\ \neg \Psi \end{array} $$

Further Reading

There are many more such inference rules with traditional names. See InferenceRules 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 inference 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.