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(Fx → Gx)

 

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)