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.
The propositional variables, and their negations (~, ¬, not), allow basic propositions or facts to be stated about the world or a world. For example:
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:
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.
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 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. ParsingA recursivedescent parser for wellformed formulae can be based on the formal grammar. The grammar and the resulting parser are very similar to those for arithmetic expressions.
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. Logicallyfollowing is a property of some pairs of Wffs. Proof is a process. It is obviously a desirable property of a formal system that logicallyfollowing 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:
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.
If the LHS contains an implications, p>q, this can be replaced by ~p or q and dealt with by rules 1 and 3:
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:
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:
An implication p>q on the RHS can be replaced by ~p or q and dealt with by rule 6:
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:
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:
The rules given above were first discovered by Gentzen. A Proof ProgramThe 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 topmost, "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 depthfirst search of the parsetree 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:
Modusponens is a basic law of logic. q logically follows from (i) p and (ii)p>q:
Notes
Exercises


