20130211

Propositional Logic - Final Thoughts

Conjunctive Normal Form (CNF)

We say that a proposition or formula PHI (the words "proposition" and "formula" are interchangeable at this point) is valid if it is a tautology.  (As an aside, "valid" is a severely overworked term.)  Determining if some formula PHI is a tautology is a practical problem: if PHI describes something that we think should be true when a program or method completes, it would be nice to be able to prove that PHI is true under all circumstances, which is just another way of saying that |= PHI is a tautology.

Unfortunately, computing the truth table for PHI may be very time-consuming if the number of atoms is large.  As an alternative, we can try to convert PHI into an equivalent formula for which validity checking is easy.

One popular method is to convert PHI to conjunctive normal form.  Informally, a formula is in CNF if it consists of a set of clauses connected by "AND", such that each clause contains only atoms and their negations, connected by "OR".

For example, (p V q V !r) ^ (!p V s) ^ (q V !r V !q)   is in CNF

The formal definition of CNF depends on a grammar which defines three types of object: Literals (L), Disjunctions (D) and Conjunctions (C)

L ::= p | !p               - this means "a Literal is either an atom or the negation of an atom"
D ::= L | L V D        - this means "a Disjunction is either a Literal, or a Literal connected to a Disjunction with an "V"  "
C ::= D | D ^ C        - this means "a Conjunction is either a Disjunction, or a Disjunction connected to a Conjunction with an "^"   "


The nice thing about a formula in CNF is that it is extremely easy to check for validity.  The formula can only be valid if all of its disjunctions are valid (if any of them can be false, then the whole expression can be false).  A disjunction is only valid if it contains a pair of literals that negate each other (for example, "p" and "!p") - this is pretty easy to see: if a disjunction does not contain such a pair, we can always make it false by choosing values for the literals it contains.  However, if a disjunction does contain such a pair, either p or !p will be true under any assignment of truth values to the literals, so the disjunction will always evaluate to True.

Creating a CNF Formula From a Truth Table

Suppose we are given a truth table for a formula PHI, but we are not given the actual formula.  We can create PHI in CNF using the following method.

Recall that a CNF formula consists of a conjunction of disjunctions.  In order for the formula to evaluate to True, all of its disjunctions must evaluate to True simultaneously.  Our task is simplified by the binary nature of Propositional Logic:  if we can create a formula which is True in exactly the right situations, it must also be false in exactly the right situations (and vice versa).

We apply this insight by focusing on the lines of the truth table where PHI is false.  We want to construct a formula that evaluates to True if the combination of literal values (i.e. true/false for the atomic propositions) does not place us on any of these lines.  Luckily, the literals themselves tell us how to do this.  Each line of the truth table corresponds to a specific set of literal values.  If any one of those literal values is changed, then we would no longer be on that line of the truth table.  By linking together disjunctive clauses, each of which corresponds to the idea "not on line i of the truth table" we create a formula which is true if and only if we are one of the lines of the truth table where PHI is true.

Example:

p   q   r   PHI

T   T   T   T
T   T   F   F
T   F   T   T
T   F   F   T
F   T   T   F
F   T   F   T
F   F   T   F
F   F   F   T

We will create a formula which says, in effect, "not on line 2" AND "not on line 5" AND "not on line 7"

On line 2, p is true, q is true, and r is false.  If any of these conditions do not hold, then we are not on line 2.  Thus "!p V !q V r" is a formula for "not on line 2" and lo and behold, it is a disjunction.  Analysing lines 5 and 7 the same way, we get two more disjunctions, and when we link them together, we get

                    (!p V !q V r) ^ (p V !q V !r) ^ (p V q V !r)

For your own satisfaction, you may wish to verify that this CNF formula has exactly the desired truth table.

Note that the correctness of this method has an immediate implication.  We started with an entirely arbitrary unknown formula PHI, and derived an equivalent CNF formula.    This means that if we had started with a known formula, we could follow exactly the same steps: construct the truth table, identify the lines where the formula is False, and build a CNF formula based on those lines.  The conclusion is that for every formula in propositional logic, there is an equivalent CNF formula.

This is very useful knowledge because it means that if we can prove things about CNF formulas, or create algorithms that apply only to CNF formulas, we are able to apply these results to all formulas.

Unfortunately, this method of translating a given formula into CNF format is very inefficient if there are a lot of atomic propositions involved (the truth table grows exponentially).  If we are given the truth table up front (and no other information about PHI) then this is the method we use.  However, if we are actually given the formula PHI, there is another method for creating a CNF equivalent ... and we will look at that in our next class.

Validity versus Satisfiability

A proposition PHI is satisfiable if there is some model of its atoms that makes PHI evaluate to True.   (Compare this to validity, which requires that every model of PHI's atoms makes PHI evaluate to True.)

There is a very interesting and useful result linking validity and satisfiability:

Theorem:   PHI is satisfiable iff !PHI is not valid (ie not a tautology).

This can be seen to be true by considering the truth table for PHI.  If PHI is satisfiable there must be a T somewhere in its column of the TT.  If we add a column for !PHI, it would have an F in this row - which means !PHI is not valid.

This theorem can be reworded in a number of different ways.  For example "PHI is valid iff  !PHI is not satisfiable", or "PHI is not valid iff !PHI is satisfiable" etc.

Satisfiability is a very important practical problem.  As computer scientists, when we create a complex piece of code, we need to know whether certain situations can ever arise.  For example, we may be dealing with three variables x, y and z, with the need to perform specific actions for different combinations of values of these variables.  However, if we can prove that (for example) it is not possible for "(x < 0) ^ (y < 0) ^ (z > 0)" to be true, then this reduces the number of cases we need to cover.


Unfortunately, there is no known efficient algorithm to test an arbitrarily chosen proposition for satisfiability.  There is an obvious algorithm: generate the truth table - but this is extremely inefficient, and for any realistic application this method is not feasible.  In fact, satisfiability (or SAT, as it is usually called) is one of the fundamental unsolved problems in computer science.  In 1971, Steve Cook proved that if SAT can be solved in polynomial time, then so can a vast (in fact, infinitely large) collection of other problems.  Over 40 years have elapsed, and nobody has yet found an efficient algorithm to solve SAT.  It seems that most computer scientists believe that no efficient algorithm for solving SAT exists.




Predicate Calculus

Suppose we wish to state the proposition "All dogs eat cheese".  Putting this into propositional logic is challenging.  If we had a list of all dogs, we could do something like "Fido eats cheese" ^ "Spot eats cheese" ^ "Clifford eats cheese" ^ ... which might be feasible if there are only a few dogs, but is more likely to be exhausting.  Further, if there are an infinite number of dogs (as there may well be, if we include dogs on other planets, in parallel universes, etc.) then we just can't list them all.

It gets worse.  Suppose we think of "being a dog" and "eating cheese" as properties that objects might have.  Then "All dogs eat cheese" can be written as
"If a thing is a dog, then that thing eats cheese".  To assert that this implication is true, we have to consider every possible thing in the entire universe (including all non-physical things such as numbers).  If anything that turns out to be a dog doesn't eat cheese, then we would have to reject the statement. 

Predicate calculus is designed to give us a way to make sound logical arguments about elements of (possibly infinitely large) sets.  It is based, as you might suspect, on the concept of a predicate.

A predicate is a statement which is either true or false about an object or combination of objects.  If the predicate takes a single argument, as in the example IsADog(x) or more simply Dog(x), we can think of it as a property of the object, or equivalently as membership in a set.  If the predicate takes more than one argument, as in the examples SumIsLessThanTen(x,y) or WereInTheSameRes(x,y,z) we can think of it as a relationship between the objects.  Note that when we define a predicate, we must specify how many arguments it takes.  The common notation uses "." for each argument, so we might use "Father(.,.)" to indicate that Father is a predicate that takes two arguments.  With a predicate like this, we need to be explicit whether we mean that the first object is the father of the second or vice versa.

Note that by convention, predicate names always start with capital letters.

Implicit in all of the above is the idea of a variable.  When we construct arguments in predicate logic, we sometimes define a universe of discourse or domain of discourse which means that all of our variables represent values from a particular set.  Without a specified universe, variables are assumed to represent any possible object.

Predicate calculus also includes functions.  A function is similar to a predicate except that instead of returning True or False, it returns an object.  Some examples with fairly obvious meanings are sumOf(x,y), motherOf(x), nearestCityTo(x).  Functions need not have any arguments.  An example would be squareRootOfTwo().  We call such functions constants for the obvious reason that they always return the same value.  We also call them nullary functions, in an extention of the more familiar unary and binary designations.  In general, the arity of a function or predicate is the number of arguments it requires.

By convention, function names always begin with lower case letters.

The other major new concept in predicate calculus is the quantifier.  We use two: "for all" which I will abbreviate as FA, and "there exists", which I will abbreviate as TE.  The meaning of FA x P(x) is pretty self-explanatory.  TE x P(x) means there is at least one object x for which P(x) is true.

As we explore the formal definition of predicate calculus, we will use the concept of a term.  Basically, a term is any part of an expression that represents an object in the universe of discourse.

Terms:

1.  All variables are terms.
2.  If f() is a nullary function, then f() is a term.
3.  If t1, ..., tn are terms and f(., ..., .) is a function of arity n, then f(t1, ..., tn) is a term.
4.  Nothing else is a term.

Formulas:

1.  If P is a predicate of arity n and t1, ... tn are terms, then P(t1, ..., tn) is a formula.
2.  If PHI is a formula, then (!PHI) is a formula
3.  If PHI and PSI are formulas, then (PHI ^ PSI), (PHI V PSI) and (PHI -> PSI) are formulas.
4.  If PHI is a formula, FAx PHI  and  TEx PHI  are formulas.
5.  Nothing else is a formula.

In practice we dispense with most of the parentheses by applying the same binding order that we used in propositional logic.  The quantifiers bind with the same precedence as ! (ie. first).  This means that if we want a quantifier to apply to anything more than the formula immediately after it, we need to make that explicit with parentheses.

For example, in "FAx P(x) -> Q(x)" the quantifier applies only to P(x).  If we want it to apply to the whole formula, we must write "FAx (P(x) -> Q(x))"

We discussed the structure of parse trees for predicate formulas.

We introduced the idea of a model for a formula PHI, which is a specific assignment of meaning to the predicates and functions that appear in PHI.  We observed that some formulas are true under some models and false under others, while other formulas are true under all models.  An example of the latter is "P(x) V !P(x)" which is true no matter what the definition of P(.).

Determining whether a formula is always true, or true under some conditions, or never true is one of the main goals of predicate calculus.  Before we get to that, we need to think about variables.  Variables as we have said are just place holders.  We need to establish the conditions under which we can substitute other things (values, other variables, and terms of any form) for variables.

We call a variable bound if when we walk up the parse tree from the leaf containing the variable, we encounter a quantifier for that variable.  We call a variable free if it is not bound.

We cannot replace bound variables under any circumstances.  It is easy to see why - we run the risk of changing the meaning of the formula.  For example, if we substitute y for the x in TEx P(x)  we would get TEx P(y).  It is entirely possible that the first might be true and the second might be false - in fact, if y represents a constant such that P(y) is false, the second formula is necessarily false.

Substituting for free variables is always legal.  We write "PHI[t/x]" to mean "replace all free instances of x in PHI with t".  Note that if  PHI does not contain any free instances of x, then the substitution has no effect.

Even though it is legal, substituting for free variables is not always safe.  Suppose that in PHI, a free instance of x occurs within the scope of a quantified variable y.  If we replace x with a term that includes the variable y, then this variable is now bound by the quantifier.  It is easy to see that by giving up this freedom we run the risk of changing the circumstances in which the formula is true.