Proofs
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 Q follows from the premises that P is true and that P implies Q. Here is a proof using the techniques described in Kalish and Montague’s Logic: Techniques of Formal Reasoning.
Note that the set of symbols and formal syntax used here is a mixture of Kalish & Montague’s and Whitehead & Russell’s. This is simply due to the limitations of the standard LaTeX and HTML fonts. The use of symbols like ∀, ¬ etc. in place of the corresponding symbols used by K&M has no effect on the meaning of expressions of the sentential calculus nor on the techniques demonstrated here.
We begin by asserting the conclusion that we wish to show is true, given its premises:
$$ \begin{array}{llll} 1. & \textit{Show} & Q & \end{array} $$
Since this is not a tautology we have some premises that we can now simply assert to be true:
$$ \begin{array}{llll} 1. & \textit{Show} & Q & \\ 2. & & P \rightarrow Q & \text{premise} \\ 3. & & P & \text{premise} \end{array} $$
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 Q from lines 2 and 3 using modus ponens[]:
$$ \begin{array}{llll} 1. & \textit{Show} & Q & \\ 2. & & P \rightarrow Q & \text{premise} \\ 3. & & P & \text{premise} \\ 4. & & Q & 2, 3, \text{modus ponens} \end{array} $$
At this point, we have directly proven our current goal, Q, 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
$$ \begin{array}{llll} 1. & \sout{Show} & Q & 4, \text{direct proof} \\ \end{array} $$
$$ \begin{array}{llll} \hline \\ 2. & & P \rightarrow Q & \text{premise} \\ 3. & & P & \text{premise} \\ 4. & & Q & 2, 3, \text{modus ponens} \\ \hline \end{array} $$
Each such inference rule – and there are many more – has a name that must be cited when it is applied in the course of a proof along with the line numbers to which it is applied.
If the Q 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.
A proof 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.
Complete Example
As a more elaborate example, here is a complete proof of a basic tautaology asserting the equivalence of the conditional connective and a particular disjunction:
The preceding proves a biconditional directly by proving the two conditionals formed by using its operands as the antecedent and consequent in both directions. The proofs of each of those conditionals take different approaches. One is proven using an “indirect” proof or reductio ad absurdum argument. I.e. assuming the negation of the assertion and then deriving a constradiction. The other is a direct proof that assuming the consequent is sufficient to prove the consequent in the context of the assumptions made at that point in the overall proof.