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.