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.