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|:RÙP) .
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:RÙP)
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:PÙQ)
=
(9.18), (3.12)
Ø("x|R:Ø(PÙQ))
=
(3.47)(a)
Ø("x|R:ØPÚØQ))
=
(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
T_{E}X
by
T_{T}H,
version 2.60. On 26 Nov 2000, 10:45.