Kirk Rader
1.0SNAPSHOT

Proof procedures using inference rules.
All of the rest of this document so far lays the groundwork for the real work of symbolic logic: proving theorems. The truth tables described in other sections of this document are one way to visualize the validity of a given logical argument. Another way is by carrying out some sort of proof procedure that proceeds by successive applications of inference rules.
Let us return to that simplest of all arguments already referenced several times that follows from the premises that is true and that implies . Here is a proof using the techniques described in Kalish and Montague's Logic: Techniques of Formal Reasoning [1].
We begin by asserting the conclusion that we wish to show is true, given its premises:
Since this is not a tautology we have some premises that we can now simply assert to be true:
At this point, we can assume lines 2 and 3 are true, since they are not yet surrounded by a box and are not preceded by an uncanceled Show. The proof proceeds by making inferences from any such lines that we currently hold to be true, with the goal of showing that the closest preceding uncanceled Show follows from them.
In particular, we can infer from lines 2 and 3 using amodusponens
At this point, we have directly proven our current goal, , so we "box and cancel":
#. Draw a box around all of the lines that were used to draw the most recent conclusion
#. Strike out the word "show" for that conclusion, thus "canceling" the boxed lines that were used to prove that line's validity
If the in line 1 had been a lemma in a longer proof, we could then assume it to be true as long as it remained unboxed. However, from that point onward, we could no longer reference any of the lines 2  4 in any subsequent inferences after they have been boxed. This is because they were based on assumptions made only for the purposes of proving line 1.
As a more realistic example, consider a proof of one of the tautologies cited elsewhere:
Since this is a tautology, there are no premises to assume. However, it is always permissible to make certain assumptions based on the axioms and wellknown theorems of symbolic logic. For example, one can show that must be true if one can show that both and are true. This means that when the current goal is a biconditional, a valid approach is to show each of the corresponding conditionals, in turn. Once both conditionals are "boxed and canceled," one can then "box and cancel" the biconditional. This is called a "direct" proof using the "biconditional introduction" inference rule.
The same applies to other types of formulas and inference rules. For example, to show that it is sufficient to show that by assuming , must be true. Similarly, due to the very tautology that is the subject of the proof under discussion here, one can also "box and cancel" if one can derive by assuming .
If all else fails when trying to prove any formula , it is always valid to assume and then attempt to derive some contradiction. Once a contradiction is demonstrated, the assumption that and the lines that proceeded from it must be boxed and the Show beside canceled. This is known as an "indirect proof" or reductio ad absurdum ("reduced to an absurdity") argument.
Here is the complete proof of the preceding tautology using these sorts of techniques:
Each of the preceding proofs shows the final result of carrying out a manual procedure that begins by stating the formula being sought as the conclusion of a logical argument, labeled with the word Show to indicate that it is a supposition that has not yet been demonstrated to be true. Underneath that supposition, one then lists any premises – where there are no premises in the case of a tautology. None of these lines will as yet have a box drawn around them and the Show next to the initial supposition will not be "canceled" by drawing a line through it.
The proof continues by playing a kind of "game" according to very strict rules. At any given time, any line that is not yet boxed and which does not have an uncanceled Show label may be assumed to be true. One can then add more lines by applying inference rules and making certain assumptions in accordance with the axioms of symbolic logic. Once a set of unboxed lines produces a proof of an uncanceled supposition, the lines under the newlyproven supposition are surrounded by a box and the supposition's Show label is canceled, indicating that the boxed lines are no longer assumed to be true but the supposition has been demonstrated to be true so long as that canceled Show line, itself, remains unboxed. New suppositions can be made and more inference rules applied until the original (topmost) supposition has been canceled. At that point, the proof is complete.
Along the way, as lines are added and suppositions canceled each such "move" in the "game" must be annotated with the inference rule(s) that are being applied to which unboxed lines. This allows the reader to follow along with the reasoning explicitly and confirms its validity.