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|QÚR: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.