80-211                                                                                                             Spring 2003



Assignment #9

Due on Friday, March 21th



Problem 1 (4 pts):  Prove the following sequents, using the basic rules for the quantifiers (of course you can use any primitive or derived rule for propositional logic too).


            (a)        "x(~Ax→Kx), $y~Ky$w(Aw v ~Lwf)


            (b)        "x"y((Ry v Dx)~Ky), "x$y(Ax ~Ky),  $x(Ax v Rx) ├ $x ~Kx


            (c)        "x$y"zFxyz"x"z$yFxyz


            (d)        $x$y"zFxyz"z$y$xFxyz


Problem 2 (3 pts):  For the following proofs, you can use any previously proved sequents  from the predicate and propositional calculus.  You may find it useful to call any rule where the negation operator is moved past a quantifier a quantifier exchange (QE).  Some examples of this would include:

                        ~$x~Fx ┤├ "xFx

                        $xFx ┤├ ~"x~Fx

                        ~"xFx ┤├ $x~Fx

                        ~$xFx ┤ ├ "x~Fx



(a)    "z~Jz, ($y)(Hby v Ryy) → ($x)Jx"y~(Hby v Ryy)


(b)     ~($y)(Ty v ($x)~Hxy) ├ "x"yHxy & "x~Tx


      (c)  $xFx$xGx$x(FxGx)


Problem 3:  (3 pts) Show that each of the following sentences is not semantically true.  Make sure you give a quick explanation why (i.e., state briefly what your interpretation is intended to show).


      (a)  $xFx"xFx


(b)  "x(Fx→Gx) → "xGx


      (c)  ~($x)Gx"y(Fyy→Gy)