November 24, 2000 November 24, 2000

I was asked how to prove ("x|:false) false. Start with (9.13).
("x|:false) false
=

(3.57)

("x|:false) false false
=

(3.30)

("x|:false) false
Note that if x d.n.o.f. in P, we have P ("x|:P), so that by (9.13) and Mutual Implication P ("x|:P).
P ("x |:P)
=

(3.57)

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

(3.26)

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

(9.5), x d.n.o.f. in P

P ("x |:P) P ("x |:P)
We now consider the Theorems on Existential Quantification. (9.17), the Axiom which we considered earlier, provides the means to exploit theorems about universal quantification to prove ones about existential quantification.

Recall (9.17),
|- ($x |R:P) ("x|R:P) .

The various parts of (9.18) are easy to prove from (9.17), in particular,
|- ($x|R:P) ("x|R:P)
and
|- ("x|R:P) ($x|R:P)
so that from the point of view of manipulation, to negate a quantification, change it to the other kind (existential to universal or vice versa) and negate the body. This is semantically just DeMorgan in the case of R holding on a finite set.
(9.19), Trading, is
|- ($|R:P) ($x|:RP) .
We have
($x |R:P)
=

(9.17)

("x|R:P)
=

(9.2)

("x|:R P)
=

(9.18)(c)

($x |: (R P))
=

(3.59)

($x |: (R P))
=

(3.47)(b)

($x |: R P)
As an application, we prove |- ($x|:x = 1 x = 2 ) false.
($x|:x = 1 x = 2)
=

(9.19)

($x|x = 1 :x = 2)
=

(8.14)

1 = 2
=

Arithmetic

false
(9.20),
|- ($x | Q R:P) ($x |:Q:RP)
is an easy consequence of (9.19).
(9.21),
|- Provided x d.n.o.f. in P,      P ($x|R:Q) ($x|R:P Q) .
This is the analogue of (9.5).
($x|R:PQ)
=

(9.18), (3.12)

("x|R:(PQ))
=

(3.47)(a)

("x|R:PQ))
=

(9.5), as x d.n.o.f. in P, x d.n.o.f. in P

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

(3.47)(b), (3.12)

P ("x|R: Q)
=

(9.18)(b), (3.12)

P ($x|R: Q)
=

(3.12)

P ($x|R: Q)
(9.22),
Provided x d.n.o.f. in P,      ($x |R:P) P ($x|:R),
is an easy exercise using (9.19) and (9.21).


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