Theorem Proving in Propositional Logic

People use logic every day of their lives. At the moment of writing it is not raining but it looks very much as though it will be within the hour and I deduce that if this is the case (I have to go out shortly) then I will get cold and wet. Propositional logic is a formal system for performing and studying this kind of reasoning. Part of the system is the language of well formed formulae (Wffs). Being a formal language, this has a precisely defined grammar.

<Wff>         ::= <Wff> -> <Disjunction> | <Disjunction>

<Disjunction> ::= <Disjunction> or <Conjunction> |
                  <Conjunction>

<Conjunction> ::= <Conjunction> and <Literal> | <Literal>

<Literal>     ::= not <Literal> | <Variable> | ( <Wff> )

NB. often also allow  ‘&’, ‘.’, or ‘∧’ for ‘and’,  ‘~’ or ‘¬’ for ‘not’,  and ‘+’ or ‘∨’ for ‘or’.

Grammar for Well Formed Formulae (Wff).

The propositional variables, and their negations (~, ¬, not), allow basic propositions or facts to be stated about the world or a world. For example:

raining, not raining, cold, wet

The remainder of the grammar allows a form of expression to be written including the logical operators implies (->), `and' (&) and `or'. This enables rules about the world to be written down, for example:

raining -> cold & wet

The operators can be interpreted in a way to model what humans do when reasoning informally but logically. For example, we know that if the proposition p holds, and if the rule `p implies q' holds, then q holds. We say that q logically follows from p and from p implies q. This example of reasoning is known as modus ponens. An application is that `cold and wet' logically follows from raining and from raining implies cold and wet.

Propositional logic does not "know" if it is raining or not, whether `raining' is true or false. Truth must be given by us, from outside the system. When truth or falsity is assigned to propositional variables the truth of a Wff can be evaluated. Truth tables can be used to define the meaning of the operators on truth values.

p         not p
false      true
 true     false

p         q         p and q
false     false     false
false      true     false
 true     false     false
 true      true      true

p         q         p or q
false     false     false
false      true      true
 true     false      true
 true      true      true

p         q         p -> q   (sometimes written p=>q)
false     false      true
false      true      true
 true     false     false
 true      true      true

Operator Truth Tables.

Note that the table for p->q is the same as that for ~p or q. In other words p->q has the same meaning as ~p or q.

Propositional logic is used in Computer Science in circuit design. It is a subset of a more powerful system, predicate logic, which is used in program verification and in artificial intelligence. Predicate logic has given rise to the field of logic programming and to the programming language Prolog. A study of propositional logic is basic to a study of these fields.

This chapter shows how the manipulation of Wffs and how reasoning in propositional logic can be formalised and carried out by computer programs. It forms a case study on some uses of trees, tree traversals and recursion. It is also a good place to note that logical deduction, this particular form of calculation in a formal system, models a very small part of what makes human beings intelligent.

Parsing

A recursive-descent parser for well-formed formulae can be based on the formal grammar. The grammar and the resulting parser are very similar to those for arithmetic expressions.

Wff: p and (p->q) -> q

              ->
             .  .
            .    .
           .      .
          &       q
         . .
        .   .
       .     .
      p      ->
            .  .
           .    .
          p      q

An Example Parse Tree.

Proof   (Gentzen)

We say that a Wff v logically follows from a Wff w, `w=>v', if and only if (iff) v is true whenever w is true. Think of w as being the antecedant(s) or condition(s) for v. Note that v may be true if w is false. We say that w is a tautology, or is always true, iff it has no conditions: `=>w'. We say that w is a contradiction, or is always false, if ~w is a tautology `=>~w', also `w=>'. If w is neither a tautology nor a contradiction then it is said to be satisfiable. As examples, p or ~p is a tautology, p&~p is a contradiction and p or q is satisfiable.

Logically-following is a property of some pairs of Wffs. Proof is a process. It is obviously a desirable property of a formal system that logically-following can be proven to hold, whenever it does hold, and this is the case for propositional logic.

For some simple Wffs the relationship `logically follows' is obvious:

p, q, r, ..., x, y, z, ... are propositional variables.

(a) p=>p            p logically follows from p

(b) p&q => p        strengthen LHS

(c) p => p or q     weaken RHS

(d) p&q&r&... => x or y or z or ...
    iff the LHS and the RHS have a
    common propositional variable.

Logically Follows, Base Cases.

In general we wish to know if an arbitrary Wff R logically follows from an arbitrary Wff L: `?L=>R?'. Arbitrary Wffs can contain the operators ~, &, or, ->. First, consider p or q on the LHS. R logically follows from p or q iff R is true whenever p or q is true. Now, p or q is true whenever p is true and whenever q is true. So R logically follows from p or q iff R is true whenever p is true and whenever q is true. (Note that p, q can be arbitrary Wffs.) This gives rule 1 which removes `or's from the LHS.

Special case:
   p or q => R
   iff (i) p=>R and (ii) q=>R

General case:
   (p or q)&rest => R
   iff  (i) p&rest => R
   and (ii) q&rest => R

Rule 1.

If the LHS contains an implications, p->q, this can be replaced by ~p or q and dealt with by rules 1 and 3:

Special case:
   p->q => R
   iff ~p or q -> R

General case:
   (p->q)&rest => R
   iff (~p or q)&rest => R    see rules 1 and 3

Rule 2.

Negation (~, not) behaves much like arithmetic minus and there is even a kind of cancellation rule. R logically follows from ~p iff R is true whenever ~p is true, ie. whenever p is false. This is equivalent to demanding that p or R be a tautology:

Special case:
   ~p => R
   iff => p or R

General case:
   ~p&rest => R
   iff rest => p or R

Rule 3.

The previous rules apply to the LHS; similar rules apply to the RHS. p&q logically follows from L iff p&q is true whenever L is true, ie. iff p is true whenever L is true and q is true whenever L is true:

Special case:
   L => p & q
   iff  (i) L => p
   and (ii) L => q

General case:
   L => (p & q) or rest
   iff  (i) L => p or rest
   and (ii) L => q or rest

Rule 4.

An implication p->q on the RHS can be replaced by ~p or q and dealt with by rule 6:

Special case:
   L => p->q
   iff L => ~p or q

General case:
   L => (p->q) or rest
   iff L => ~p or q or rest   see rule 6

Rule 5.

A negation, ~p, logically follows from L iff ~p is true, ie. iff p is false, whenever L is true. This is the case iff L&p is a contradiction:

Special case:
   L => ~p
   iff  L&p =>

General case:
   L => ~p or rest
   iff  L&p => rest

Rule 6.

Finally, repeated application of rules one to six makes the Wffs on the LHS and RHS simpler and simpler. Eventually only the base case remains:

L => R,   L conjunction of variables
          R disjunction of variables
iff L intersection R ~= {}

Rule 7.

The rules given above were first discovered by Gentzen.

A Proof Program

The rules given in the previous section are easily implemented by a routine `Prove' that manipulates the parse trees of Wffs.

An auxiliary routine `FindOpr' is needed to locate a top-most, "troublesome" operator in a tree of a Wff: {or, ->, ~} on the LHS and {&, ->, ~} on the RHS of a proof. There must be no other troublesome operator on the path from the root to the operator although there may be other troublesome operators in other parts of the tree. This routine performs a depth-first search of the parse-tree of a Wff for such an operator. If successful it returns pointers to the subtree having the operator as root and a tree for the "rest" of the Wff.

The proof routine proper, applies the rules previously defined. Rules one to six require one or two recursive calls to prove simpler problems. Rule seven, the base case, requires traversals of two parse trees, now in simple form, to see if they share any propositional variable.

The routine also contains statements to print out the steps of the proof and examples are given below.

A Wff w is a tautology if it follows from nothing, =>w. W is a contradiction if ~w is a tautology. Failing both of these, w is satisfiable. The simplest satisfiable Wff is a single variable:

Expression is: p
1:  => p fail          % not a tautology, try ~p

1:  =>  not p
1.1: p =>  fail        % not a contradiction so ...

Expression is satisfiable

Expression is: (p or  not p)

1:  => (p or  not p)
1.1: p => p succeed         % LHS and RHS intersect

Expression is a tautology

Expression is: (p and  not p)

1:  => (p and  not p)
1.1:  => p fail
1.2:  =>  not p
1.2.1: p =>  fail           % not a tautology ...
                            % ... try not(p and not p)

1:  =>  not (p and  not p)
1.1: (p and  not p) =>
1.1.1: p => p succeed

Expression is a contradiction

Modus-ponens is a basic law of logic. q logically follows from (i) p and (ii)p->q:

Expression is: ((p and (p->q))->q)

1:  => ((p and (p->q))->q)
1.1:  => ( not (p and (p->q)) or q)
1.1.1: (p and (p->q)) => q
1.1.1.1: (( not p or q) and p) => q  % proof branches now
1.1.1.1.1: ( not p and p) => q
1.1.1.1.1.1: p => (p or q) succeed   % LHS & RHS intersect
1.1.1.1.2: (q and p) => q succeed    % ditto

Expression is a tautology

Notes

• Gerhard Gentzen originated this type of formal system for logic; see (p140) of M. Wand, Induction, Recursion and Programming, North-Holland 1980.
• See the [Prolog interpreter] and Prolog notes for the mechanisation of Predicate Logic (as opposed to propositional logic).

Exercises

1. For each Wff below, determine if it is a tautology, is a contradiction or is satisfiable:
   • (p->q)->(q->p)
   • (p->q)->(~q->~p)
   • (p->q)&(q->r)->(p->r)
2. Project: Write a program to print the truth-table of a Wff: Collect the distinct variables into a list. Write a routine to make all possible assignments of truth values to the variables. Write a routine to evaluate the Wff given such an assignment.
3. Project: Implement a program to convert an arbitrary Wff into "two-level" Conjunctive-Normal-Form (CNF): a disjunction of conjunctions of literals where a literal is a variable or the negation of a variable.
   • eg. p&(p->q)->q
   • = ~(p&(~p or q))or q
   • = ~p or ~(~p or q)or q
   • = ~p or (p & ~q) or q
   Use the rules:
   • p->q = ~p or q
   • p&(q or r) = p&q or p&r
   • ~(p&q) = ~p or ~q
   • ~(p or q) = ~p & ~q