November 20, 2000 November 20, 2000

As (9.17) is an axiom we can introduce it at any point.
 |-  (\$x |R:P) º Ø("x|R: ØP) .
We prove
 |- (\$x|:Ax Þ Bx) º ("x|:Ax) Þ (\$x|:Bx) .
This is a standard type test question.
 ("x|:Ax) Þ (\$x|:Bx)
 =

 (3.59)

 Ø("x|:Ax) Ú(\$x |:Bx)
 =

 (9.18)(c) which is an easy consequence of (9.17)

 (\$x|:ØAx) Ú(\$x |:Bx)
 =

 (8.15)

 (\$x |:ØAx ÚBx)
 =

 ((3.59)

 (\$x|:Ax Þ Bx)
It is a useful exercise to determine for each step which particular Leibniz rule or rules are being used.

(9.7) is
 Provided x d.n.o.f. in P, |- Ø("x|:ØR) Þ (("x |R:P ÙQ) º P Ù(" x|R:Q)) .
Note that if R is true then we have |- Ø("x|:ØR) (proof is a simple exercise) so that by Modus Ponens,
 |- ("x |:P ÙQ) º P Ù("x|:Q) .
By taking R to be false and P to be false check ("x |R:P ÙQ) º P Ù(" x|R:Q) for validity to see that it is not a theorem. For the proof of (9.7) use the Deduction Theorem.
Assume Ø("x|:ØR).
 ("x|R:P ÙQ)
 =

 (8.15)

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

 (3.30)

 ("x|R:P Úfalse )Ù("x|R:Q )
 =

 (9.5)

 P Ú("x|R:false )Ù("x|R:Q )
 =

 (9.2)

 P Ú("x|:RÞ false )Ù("x|R:Q )
 =

 (3.74)

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

 Assumption

 P Úfalse Ù("x|R:Q )
 =

 (3.30)

 P Ù("x|R:Q )
(9.8) is |- ("x|R:true) º true.
 ("x|R:true)
 =

 (3.29)

 ("x|R:trueÚtrue)
 =

 x d.n.o.f. in true

 trueÚ("x|R:true)
 =

 (3.29)

 true
(9.10) follows easily from (8.18) and (3.76)(b).
Here is a proof of (9.11),
 |- ("x|R:P ÙQ) Þ ("x|R:P) .

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

 (3.60)

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

 (8.15)

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

 (3.38)

 ("x|R:P ÙQ )    º   ("x|R:P ÙQ)

File translated from TEX by TTH, version 2.60.
On 20 Nov 2000, 16:32.