Chapter 14 Fixes Chapter 14 Fixes

Definition 14 R: We say ``a set expression r is a relation expression'' if, with x, y having no free occurrences in r,
 |-  z Î r    Þ    (\$x,y | : z = á x,yñ ) .
By (3.60), an alternate formulation is
 |-  (z Î r)      º     (z Î r)   Ù  (\$x,y | :z = á x,yñ ) .

Theorem 14 RP: For r a relation expression and provided x, y, z d.n.o.f. in r, x, y d.n.o.f. in P,
 |-  ("z  | z Î r: P )     º     ("x,y | á x,yñ Î r: P [z : = áx,yñ] ) .
This result can be understood as change of dummy. The proof is suggested by the textbook's treatment of (8.22).
 ("x,y | á x,yñ Î r: P [z : = áx,yñ] )
 =

 (9.2) for multiple quantification

 ("x,y | : á x,yñ Î rÞ P [z : = áx,yñ] )
 =

 (8.14), z d.n.o.f. in á x,yñ

 ("x,y | : ("z | z = á x,yñ: z Î rÞ P ) )
 =

 (9.4)(a)

 ("x,y | : ("z | z Î r: z = á x,yñÞ P ) )
 =

 (8.19) for multiple quantification, x, y d.n.o.f. in z Î r

 ("z | z Î r: ("x,y  | : z = á x,yñÞ P ) )
 =

 (9.2) for multiple quantification

 ("z | z Î r: ("x,y  | z = á x,yñ: P ) )
 =

 (9.6) for multiple quantification, x, y d.n.o.f. in P

 ("z | z Î r: P  Ú  ("x,y  | : Ø (z = áx,yñ)) )
 =

 (9.18) for multiple quantification

 ("z | z Î r: Ø(\$x,y  | : z = áx,yñ)  Ú  P )
 =

 (3.59)

 ("z | z Î r: (\$x,y  | : z = áx,yñ)  Þ  P )
 =

 (9.4)(a)

 ("z | (z Î r)   Ù  (\$x,y  | : z = áx,yñ):P )
 =

 14 R

 ("z | z Î r: P )
Theorem 14 RE: For r, t relation expressions and provided x, y d.n.o.f. in r or t,
 |-  r = t       º       ("x,y|:áx,y ñ Î r   º áx,y ñ Î t) .
This is a straightforward proof by Mutual implication.
For necessity,
 r = t      Þ      ("x,y | :áx,y ñ Î r   º áx,y ñ Î t)
 =

 (3.84)(b)

 r = t      Þ      ("x,y | :áx,y ñ Î r   º áx,y ñ Î r)
 =

 (3.3)

 r = t      Þ      ("x,y | :true)
 =

 (9.8) for multiple quantification

 r = t      Þ      true
 =

 (3.72)

 true .
Sufficiency follows using the Deduction Theorem.
Assume
 ("x,y|:áx,y ñ Î r   º áx,y ñ Î t) .
Let z be a fresh variable. We prove
 z Î r     º     z Î t
from which
 r   =   t .

 z Î r
 =

 14 R

 (z Î r)   Ù  (\$x,y | :z = á x,yñ )
 =

 (9.21) for multiple quantification

 (\$x,y | :(z Î r)   Ù  z = á x,yñ )
 =

 (3.84)(a)

 (\$x,y | : á x,yñ Î r  Ù  z = á x,yñ )
 =

 Assumption

 (\$x,y | : á x,yñ Î t  Ù  z = á x,yñ )
 =

 (3.84)(a)

 (\$x,y | :(z Î t)   Ù  z = á x,yñ )
 =

 (9.21) for multiple quantification

 (z Î t)   Ù  (\$x,y | :z = á x,yñ )
 =

 14 R

 z Î t .

File translated from TEX by TTH, version 2.60.
On 16 Apr 2001, 13:05.