Reasoning with Propositional Logic

We can use propositional logic to reason formally about (or construct proofs of) propositions.

A deductive argument takes as given a set of premises (or hypotheses) which are known to be true and attempts to prove a conclusion valid by a sequence of steps, termed inferences.

Each inference follows from the premises or a previous inference by the application of an inference rule.

Given premises (or inferences) P1..Pn, we can infer expression E if P1 AND P2 AND .. Pn -> E is a tautology.

• Whenever E is a tautology, P1 AND P2 AND .. Pn -> E is a tautology.

• Given two premises P1 and P2, we can infer P1 AND P2.

• If P1 and (P1 -> P2) are given or inferred, then we can infer P2 by the rule of modus ponens (p AND (p->q) -> q).

• If NOT P2 and (P1 -> P2) are given or inferred, then we can infer NOT P1 by the rule of modens tollens.

• If P1 and (P1==P2) are given or inferred, we can infer P2.

Proving Tautologies Using Inferences

Prove (p -> q) AND (NOT p -> q) == q:

   1. (p -> q) AND (NOT p -> q)
   Given
  
   2. (NOT p OR q) AND (NOT NOT p OR q)
   Rewriting -> in terms of NOT and OR
  
   3. (NOT p OR q) AND (p OR q)
   Elimination of double negation
  
   4. ((NOT p OR q) AND p) OR ((NOT p OR q) AND q)
   Distribute AND over OR
  
   5. ( NOT p AND p OR q AND p) OR (NOT p AND q OR q)
   Distribute AND over OR
  
   6. (q AND p) OR (NOT p AND q OR q)
   Eliminate p AND NOT p
  
   7. (q AND p) OR q
   Subsumption
  
   8. q
   Subsumption
  
   QED
  

Deductive Proof

If the weather is warm and the sky is clear, then either we go swimming or we go boating. It is not the case that if the sky is clear then we go swimming. Therefore, if we do not go boating, then the weather is not warm.

We can rewrite this argument formally, using the following variables to correspond to each of the propositions in the argument:

      w = weather is warm   c = sky is clear
      s = we go swimming    b = we go boating
  

If the weather is warm and the sky is clear, then either we go swimming or we go boating:

      (w AND c) -> (s OR b)
  

It is not the case that if the sky is clear then we go swimming.

      NOT (c -> s)
  

Therefore, if we do not go boating, then the weather is not warm.

      NOT b -> NOT w
  

To prove the conclusion given the premises, we need to be able to infer the conclusion from the premises.

   1. (w AND c) -> (s OR b)        Premise 1
   2. NOT (c -> s)                 Premise 2
   3. NOT (w AND c) OR (s OR b)    L1, rewriting -> 
   4. (NOT w OR NOT c) OR (s OR b) L3, DeMorgan's law
   5. NOT (NOT c OR s)             L2, rewriting ->
   6. c AND NOT s                  L5, DeMorgan's law
   7. c                            L6
   8. NOT s                        L6
   9. (NOT w OR b) OR (NOT c OR s) L4, assoc/comm OR
  10. (NOT w OR b) OR s            L7,L9, (F OR p == p)
  11. NOT w OR b                   L8,L10, (p OR F == p)
  12. w -> b                       L11, rewriting ->
  13. NOT b -> NOT w   QED         L12, contrapos. law
  

Finding Proofs

The previous examples of proofs show how to start with a set of premises and prove a conclusion (or infer an equivalence).

In proving an equivalence using inferences, we repeatedly simplify a complex logical expression until the result is the simplified expression for which equivalence is desired.

In proving a conclusion from a set of premises, we repeatedly establish inferences from the premises until we are able to infer the conclusion.

In each case, the process is somewhat ad hoc, with no guarantee that the simplifications we choose will lead to the desired conclusion (or equivalence) quickly.

Since the best known algorithm for the tautology problem is exponential, there is no optimal algorithm for finding a proof that doesn't explore all possible simplications (in the worst case).

However, there are techniques that help direct our search for a proof in the right direction. Resolution is one such technique.