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.
|
Demonstration
There is a demonstration of the manipulation of propositional expressions [here...]. |
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.
| © L . A l l i s o n |
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.
Clearly, p logically follows from p. If the left hand side is strengthened to p&q then p still logically follows from it. If the right hand side is weakened to p or q then it still logically follows from p. If the LHS is strengthened to p&q and the RHS is weakened to p or x then the RHS still logically follows from the LHS. If the LHS is a conjunction of variables and the RHS is a disjunction of variables, the RHS logically follows from the LHS if they share a common variable. If not, it is possible to make all the variables in the LHS true and all the variable in the RHS false demonstrating that the RHS does not logically follow from the LHS.
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.
This rule seems odd in that an `or' seems to be replaced by an `and' but it is doing the right thing: The word `and' can be used in two distinct ways - as an operator in a Wff and also to group two sub-steps to carry out; rule 1 is doing the latter. Note that two problems must now be solved but they are simpler than the original problem.
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
- 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)
- 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.
- 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
- p->q = ~p or q
- p&(q or r) = p&q or p&r
- ~(p&q) = ~p or ~q
- ~(p or q) = ~p & ~q