Mathematics 470 Spring 2005

Exam #2 Wednesday, April 6

 

 

 

I. (30 points)   In each of problems 1 through 3,  use resolution  to determine whether or not the given proposition is valid.

 

1.      (P -> Q) -> ( ¬Q -> ¬P)

 The negation of the formula in CNF is:

(ØP  v Q)  ^ ( ØQ ) ^ (P)

Resolving on P gives (Q) and then on Q gives the empty clause, showing that the original formula is valid.

If we use the Davis-Putnam Procedure, first eliminating P to get {Q}  and {ØQ} and then Q to get the empty clause, we also see that the original formula is valid.

2.     ((Q -> P) ^ ØQ) -> P

The negation of the formula in CNF is:

(ØQ v P)  ^ (Ø Q) ^ ( ØP)

Resolution on P leads to (ØQ).

There are no further clauses to be obtained from these by resolution.

If we use the Davis-Putnam Procedure, first eliminating P to get {ØQ} and then Q to get no clauses, we also see that the original formula is not valid.

 

3.     (P -> Q)  ->  ( (P -> R ) -> (Q -> R))

The negation of the formula in CNF is:

(ØP  v Q)  ^ (ØP v R) ^ (Q) ^ (ØR).

Resolving on R gives (ØP)

There are no further clauses to be obtained from these by resolution.

If we use the Davis-Putnam Procedure, first eliminating P to get {Q} ^ {ØR)  and then Q to get  {ØR} and finally on R to get no clauses, we also see that the original formula is not valid.

 

 

II. ( 50 points)   Let  L be a language with one binary predicate symbol R.  Construct a tableau to  attempt to determine whether each of the sentences of L in questions 4 through 6  is

a)     valid

b)    unsatisfiable

c)     neither valid nor unsatisfiable

In case a) and c)  give an interpretation in which it is true.  In case c) also give an interpretation in which it is false

 

4.     "x$y R(x,y)   -> $y"x R(x, y)   c) neither valid nor unsatisfaiable,

The following tableau shows that the formula  is satisfiable:

T "x$y R(x,y)   -> $y"x R(x, y)

                                          /                       \

                                F"x$y R(x,y)       T $y"x R(x, y)

                                      F$yR(c,y)                T "xR(x, d)

                                 F R(c,c)                      T R(d,d)

                                        FR(c, d)                     T R(c,d)

There are no further relevant extensions to the tableau and neither path is contradictory.

      The following tableau shows that the negation of the formula is satisfiable:

F "x$y R(x,y)   -> $y"x R(x, y)

                                                T "x$y R(x,y)  

                                                 F $y"x R(x, y)

                                           T$yR(c,y)

                                                  T R(c,d)

                                            T $y R(d,y)

                                                  T  R(d, e)

                                            T $y R(e, y)

                                                   …

 

                                            F "xR(c, x)

                                                  F  R( c, c’)

                                            F "x R( d, x)

                                                  F R(d, d’)

                                              …

        This tableau continues infinitely without producing a contradiction.

 

An interpretation in which the original formula is true is A is N and R is <=.

An interpretation in which it is false is A is N and R is N and  R is <.

 

5.     $y"x R(x,y)   -> "x$y R(x,y)  a) valid

The following tableau shows that the negation of the formula is  not satisfiable:

F $x"y R(x,y)   -> "x$yR(x, y)

            T $y"x R(x, y)

            F "x$y R(x,y)  

                                           T "x R(x,c)

                                                  F $y R(d, y)

                                          T "x R(x,c)

                                            T R(d,c)

                                                 F $y R(d, y)

                                                  F R(d, c)

                                               X

An interpretation in which the original formula is true is A is N and R is <=.

There is no interpretation in which it is false.

                            6. "x"y R(x,y) ^ $xØR(x, x)      b) unsatisfiable

The following tableau shows that the formula is unsatisfiable:

                                   T"x"y R(x,y) ^ $xØR(x, x)

                                          T "x"y R(x,y)

                                           T $xØR(x, x)

                                       T ØR(c,c)

                                              F R(c,c)

                                     T"x"y R(x,y)

                                             T "y R(c, y)

                                        T R(c,c )

                                                   X

 

III, (20 points)

 

7.         a) State the compactness theorem for predicate logic.

Let S be a set of sentences of predicate logic. S is satisfiable iff every finite subset of S is satisfiable.  Equivalently, if S is unsatisfiable then some finite subset of S is unsatisfiable.

 

 b) Assuming the soundness and completeness of an axiomatic system for predicate logic, prove the compactness theorem.

              Let  H be a sound and complete axiomatic system for predicate logic.   Then for S any set of sentences  and a any sentence of predicate logic, a is a consequence of S iff there is a proof  in H of a from S.

    Suppose that S is unsatisfiable; then P ^ ØP is a consequence of S.  By the completeness of H, there is a proof in H of P ^ ØP from S.  Since proofs in an axiomatic system are finite, the proof uses only a finite number of sentences from S.  Thus we have a proof in H of P ^ ØP from a finite subset S’  of S.   By the soundness of H, it follows that P ^ ØP is a consequence of S’ and hence that S’ is unsatisfiable.