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:truetrue)
=

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.