| Exercise 3.7 |
Prove the following sequents, using the primitive rules from
chapter 3 and any of the primitive or derived rules from chapter 1.
|
| S130* | ~@xPx -||- $x~Px Quantifier Exchange |
| S131 | ~$xPx -||- @x~Px QE |
| S132 | ~@x~Px -||- $xPx QE |
| S133 | ~$x~Px -||- @xPx QE |
| S134 | @x(Px & Qx) -||- @xPx & @xQx Confinement |
| S135* | @x(Px -> Q) -||- $xPx -> Q Conf |
| S136* | @xPx v @xQx |- @x(Px v Qx) Conf |
| S137* | $xy(Px & Qy) -||- $xPx & $xQx Conf |
| S138 | $x(Px v Qx) -||- $xPx v $xQx Conf |
| S139 | $x(Px -> Q) -||- @xPx -> Q Conf |
| S140* | P -> $xQx -||- $x(P -> Qx) Conf |
| S141 | P -> @xQx -||- @x(P -> Qx) Conf |
| QE (derived rule) |
The important quantifier-exchange rules establish that an initial tilde can always be
moved to the right of an adjacent quantifier, changing the quantifier from a universal
to an existential (or vice versa). Also, a tilde that immediately follows an initial
quantifier can be moved to the front of the sentence provided, again, that the
quantifier is changed as just described. Although the above versions of the rules
(S130-S133) involve quantifications of a simple formula, it is easily recognizable
that the proof s of these sequents do not depend on the sim-plicity of the quantified
formula. QUANTIFIER EXCHANGE (QE) may thus be used as a derived rule of proof as below.
Example. 1 (1) $x~(Fx & Gx) A 2 (2) $xGx -> @x(Fx & Gx) A 1 (3) ~@x(Fx & Gx) 1 QE 1,2 (4) ~$xGx 2,3 MTT 1,2 (5) @x~Gx 4 QE |
| Exercise 3.8 | Prove the following sequents, using any of the primitive or derived rules established so far. |
| T40* | |- @x(Fx -> Gx) -> (@xFx -> @xGx) |
| T41 | |- @x(Fx -> Gx) -> ($xFx -> $xGx) |
| T42 | |- $x(Fx v Gx) <-> $xFx v $xGx |
| T43 | |- @x(Fx & Gx) <-> @xFx & @xGx |
| T44 | |- $x(Fx & Gx) -> $xFx & $xGx |
| T45 | |- @xFx v @xGx -> @x(Fx v Gx) |
| T46 | |- ($xFx -> $xGx) -> $x(Fx -> Gx) |
| T47 | |- (@xFx -> @xGx) -> $x(Fx -> Gx) |
| T48 | |- ~@x(Fx <-> Gx) v (@xFx <-> @xGx) |
| T49 | |- ~@x(Fx <-> Gx) v ($xFx <-> $xGx) |
| T50 | |- ~@x(P & Fx) <-> (P -> ~@xFx) |
| T51 | |- ~$x(P & Fx) <-> (P -> ~$xFx) |
| T52 | |- @x(P v Fx) <-> (~P -> @xFx) |
| T53 | |- $x(P v Fx) <-> (~P -> $xFx) |
| T54 | |- @x(Fx -> P) <-> ($xFx -> P) |
| T55 | |- ~$x(Fx -> P) <-> ~(@xFx -> P) |
| T56 | |- @x(Fx <-> P) -> (@xFx <-> P) |
| T57 | |- @x(Fx <-> P) -> ($xFx <-> P) |
| T58 | |- ($xFx <-> P) -> $x(Fx <-> P) |
| T59 | |- (@xFx <-> P) -> $x(Fx <-> P) |
| prenex form |
Comment. The quantifier-exchange rules and the confinement rules (S134-
S141) indicate that any sentence may be converted into an equivalent sentence in which no connective i
s outside the scope of any quantifier in the formula. Such a sentence, called a PRENEX sentenc
e, has all its quantifiers in a row at the beginning of the sentence.
|
| Exercise 3.9 | For each of the following, find a prenex equivalent and prove the equivalence. |
| 1* | @x(Px -> @zRxz) |
| 2* | $y(Fy&@z(Hyz & Jz)) |
| 3* | $xFxa -> @yGyaa |
| 4* | ~@xFx -> $xHx |
| 5* | ~$x($yFyx -> ~@zGzx) |
| Find prenex equivalents for the other non-prenex sentences in this chapter and the next. |