Kirk Rader
1.0SNAPSHOT

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 follows from and 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:
There are many more such inference rules with traditional names. See https://en.wikipedia.org/wiki/Category:Rules_of_inference 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].