Grounding informal proof techniques in logic

One of the objects of our rigorous approach to proof is to explain how informal proof methods are grounded in logic. In Chapter 4 of A Logical Approach to Discrete Math, we explain how each informal technique has a solid foundation underneath it, in the form of a theorem or metatheorem. Here is a list of informal techniques together with the theorems on which they are based.

• Assuming the antecedent: Based on the Deduction Metatheorem.
• Case analysis: (p \/ q) /\ (p => r) /\ (q => r) => r.
• Partial evaluation (if P[z:= true] and E[z:= false] are theorems, then so is P):

      P[z:= p]  ==  (p /\ E[z:= true]) /\ (~p /\ E[z:= false])

• Mutual implication: (p == q) == (p => q) /\ (q => p).
• Proof by contradiction: p => false == p.
• Proof by contrapositive: p => q == ~q => ~p.