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 |-(RÙP)[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|:RÙP)Þ Q
 =

 (8.22)

 (\$z|:(RÙP)[x: = z])Þ Q
 =

 (3.59), (.18)(c)

 ("z|:Ø(RÙP)[x: = z])ÚQ
 =

 (9.5)

 ("z|:Ø(RÙP)[x: = z] ÚQ)
 =

 (3.59)

 ("z|:(RÙP)[x: = z] Þ Q)
By (9.16), the last line is a theorem if and only if |- (RÙP)[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.