
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.
