1.
(Ex)Fx v (Ex)Gx
\(Ex)(Fx v Gx)
| 2. ~(Ex)(Fx v Gx)
AIP we
are going to use an indirect derivation
| 3. (x)~(Fx v
Gx) 2, CQ
| 4.
(x)(~Fx & ~Gx) 3, DM
| 5.
~Fa & ~Ga 4, UI
| 6.
~Fa
5, Simp
| 7.
(x)~Fx
6, UG note what we
need
to do in order to move ahead
|
8.
~(Ex)Fx
7, CQ
| 9.
(Ex)Gx
1,8, DS
| 10.
~Ga
5, Simp
| 11.
(x)~Gx
10, UG
| 12.
~(Ex)Gx
11,
CQ again we need to
get
the opposite of Ex(Gx)
| 13.
(Ex)Gx
& ~(Ex)Gx 9,12 Conj
14. (Ex)(Fx v
Gx)
2-13 IP
(Ex)Fx -> (Ey)Gy |- (x)(Ey)(Fx -> Gy)
1.
(Ex)Fx ->
(Ey)Gy
/ (x)(Ey)(Fx -> Gy)
| 2.
Fa
ACP we are going to use a
conditional
derivation
| 3. (Ex)Fx
2, EG
| 4.
(Ey)Gy
1,3, MP
| 5.
Gb
4, EI (y=b)
6. Fa ->
Gb
2-5, CP
7. (Ey)(Fa ->
Gy) 6,
EG
8. (x)(Ey)(Fx ->
Gy) 7, UG remember
this is a legitimate step even though Fa
was assumed; the truth value of the conditional is not affected even if
there were no one who had the characteristic "F"
(x)(Ey)(Fx -> Gy) |- (Ex)Fx -> (Ey)Gy
1.
(x)(Ey)(Fx ->
Gy) (Ex)Fx ->
(Ey)Gy
| 2.
(Ex)Fx
ACP
|
3.
Fa
2, EI (x=a)
| 4.
(Ey)(Fa -> Gy)
1, UI
| 5. Fa ->
Gb
4, EI (y=b)
| 6.
Gb
3,5, MP
| 7.
(Ey)Gy
6, EG
8. (Ex)Fx -> (Ey)Gy
2-7 CP