December 1, 2000 December 1, 2000


(9.29) gives provided y d.n.o.f. in R and x d.n.o.f. in Q,
|- ($x|R:("y|Q:P))      ("y|Q:($ x|R:P)) .
Note that we have not . If R and Q are both true we have
($x|:("y|:P))      ("y|:($ x|:P)) .
Use that particular x to see why this is a valid formula.
For the converse,
("y|:($ x|:P))     ($x|:("y|:P))  .
try {0,1,-1} as UD with P the predicate x+y = 0 for an interpretation in which it does not hold.
What follows is a proof of this special case (i.e., R and Q are both true).
($x|:("y|:P)) ("y|:($x|:P))
=

(3.60)

($x|:("y|:P))("y|:($x|:P))      ($x|:("y|:P))
=

(9.21)

($x|:("y|:P)("y|:($x|:P)))      ($x|:("y|:P))
=

(8.15)

($x|:("y|:P($x|:P)))      ($x|:("y|:P))
=

(9.28), (3.60)

($x|:("y|:P))     ($x|:("y|:P))
Note: The general case is more complicated than the authors claim.
Metatheorem Witness (9.30) is provided z d.n.o.f. in P, Q,R
|- ($x|R:P) Q if and only if |-(RP)[x: = z] Q .
The condition on z is satisfied automatically if we choose z to be a fresh variable.
($x|R:P) Q
=

(9.19)

($x|:RP) Q
=

(8.22)

($z|:(RP)[x: = z]) Q
=

(3.59), (.18)(c)

("z|:(RP)[x: = z])Q
=

(9.5)

("z|:(RP)[x: = z] Q)
=

(3.59)

("z|:(RP)[x: = z] Q)
By (9.16), the last line is a theorem if and only if |- (RP)[x: = z] Q).
Here is a simple example of the use of (9.30).
We are given |-("z|:z2 0). We would like to prove
|- ($x|:x2 = y) (y 0) .
It suffices to prove |- (z2 = y) (y 0).
z2 = y
=

Metatheorem, (3.39)

(z2 = y) ("z|:z2 0)

(9.13), (4.3), Modus Ponens

(z2 = y) (z2 0)
=

(3.84)(a)

(z2 = y) (y 0)

(3.76)(b)

(y 0)
It follows from (8.19) that
|- ("x|:("y|:P)) ("y|:(" x|:P)) .
The following is a proof which uses Chapter 9 methods to prove this directly. It is a good illustration of the use of Mutual Implication.
Note that by the symmetry of the expression it is enough to prove
|- ("x|:("y|:P)) ("y|:(" x|:P)) .
as the other implication would have the identical proof (alternatively follows using (8.21).
("x|:("y|:P)) ("y|:(" x|:P))
=

(3.57)

("x|:("y|:P)) ("y|:(" x|:P))      ("y|:(" x|:P))
=

(9.5)

("y|:("x|:(" y|:P)("x|:P))      ("y|:(" x|:P))
We would be done provided
|- ("x|:("y|:P)) ("x|:P) .
But by (9.13),
|- ("y|:P) P .
By (9.16),
|- ("x|:("y|:P) P)) .
Apply (9.16) and Modus Ponens to obtain
|- ("x|:("y|:P)) ("x|:P) ,
the desired result.


File translated from TEX by TTH, version 2.60.
On 30 Nov 2000, 15:15.