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
- Assuming the antecedent: Based on the Deduction
- 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.