November 27, 2000 November 27, 2000


We prove (9.23), provided x d.n.o.f. in P.
|- ($x|:R) (($x|R:P Q) P ($x|R:Q))
This corresponds to (9.7). Review the proof with this in mind.
($x|:R) (($x|R:P Q) P ($x|R:Q))
=

(9.17)

("x|:R) (("x|R:(P Q)) P ("x|R:Q))
=

(3.47)(b)

("x|:R) (("x|R:P Q)) P ("x|R:Q)
=

(3.11)

("x|:R) ( ("x|R:P Q)) (P ("x|R:Q))
=

(3.47)(b)

("x|:R) ( ("x|R:P Q) (P ("x|R:Q))
We now prove (9.24),
|- ($x|R:false) false .

($x|R:false)
=

(9.17), (3.13)

("x |R:true)
=

(9.8)

true
=

(3.8)

false
(9.26),
|- ($x|R:P) ($x|QR:P)
and (9.27),
|- ($x |R:P) ($x|R:P Q)
are both easy exercises using (3.76).
(9.27).
|- ("x|R:Q P)    (($x|R:Q) ($x|R:P))
can be proved starting with (9.12).
Exercise: Find an interpretation which shows that ($x|R:Q P)    (($x|R:Q) ($x|R:P)) cannot be a theorem. Use {0,1} as universe of discourse.
("x|R: P Q)    ((" x|:P) ("x|R:Q))
=

(3.61)

("x|R: Q P)    ((" x|R:Q) (" x|:P))
=

(9.17)

("x|R:Q P)    (($x|R:Q) ($x|R:P))
$-Introduction, (9.28), corresponds to Instantiation, (9.13). As in (9.13) there is no restriction on the expression e which appears in it.
We prove
|- P [x: = e] ($x|:P) .

("x|:P) P[x: = e]
=

(3.61), (3.12)

P[x: = e] ("x|:P)
=

(9.17)

P [x: = e] ($x|:P)
Some examples:
22 = 4 ($x|:x2 = 4)
3 = 3 ($x|:x = 3)
x = 3 ($x|:x = 3)
y = 3 ($x|:x = 3)


File translated from TEX by TTH, version 2.60.
On 26 Nov 2000, 10:43.