Grounding informal proof techniques in logic

 
Teaching OO using Java
Calculational
logic
festive occasions
ABC book
CS Faculty over the years
CS@Cornell
The Triple-I Administration
How Bush Operated

 

 

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.