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 = x,y: z r P ) )
=

(9.4)(a)

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

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

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

(9.2) for multiple quantification

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

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

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

(9.18) for multiple quantification

("| z r: ($x,y  | : z = x,y)    P )
=

(3.59)

("| z r: ($x,y  | : z = x,y)    P )
=

(9.4)(a)

("| (z r)     ($x,y  | : z = x,y):P )
=

14 R

("| 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.