|
(b)
1 (1) @x(Fx -> Gx) A
1 (2) Fa -> Ga 1 @E
3 (3) @xFx A
3 (4) Fa 3 @E
1,3 (5) Ga 2,4 ->E
1,3 (6) @xGx 5 @I
Example of violation of the @I condition.
(c)
1 (1) @x(Fx -> Gx) A
2 (2) Fa A
1 (3) Fa -> Ga 1 @E
1,2 (4) Ga 2,3 ->E
| wrong! |
1,2 (5) @xGx 4 @I
|
|
Comment. Ordinarily we cannot conclude @xFx merely from Fa--the fact
that one thing is F doesn't guarantee that everything is F! The condition on
@I ensures that we do not make this mistake. If the sentence Fa is true, and
furthermore would still be true no matter what the name denotes, then
clearly every-thing is F, so we can conclude @xFx. When the condition on @I
is met, then we are in such a situation: if we prove Fa from assumptions
that do not contain the name a and hence say nothing in particular about
its referent, then we could just as well have used a different name, say b,
and proved Fb. In fact, when the condition on @I is met, any proof of Fa can
be turned into a proof of Fb just by replacing any involved occurrences of
the name a by the name b. This is sufficient to guarantee that everything is
F; hence, we can conclude @xFx.
|
| existential-intro |
Given a sentence (at line m) containing at least one occurrence
of a name, conclude an existentialization of that sentence with respect
to that name.
Condition: None.
Annotation: m $I
Assumption-set: same as line m.
Also known as: Existential Generalization.
Examples.
(a)
1 (1) Fa A
1 (2) $xFx 1 $I
(b)
1 (1) @x(Fx -> Gx) A
2 (2) Fa A
1 (3) Fa -> Ga 1 @E
1,2 (4) Ga 2,3 ->E
1,2 (5) $xGx 4 $I
(c)
1 (1) @xFax A
1 (2) $y@xFyx 1 $I
|
|
existential-elim |
Given a sentence (at line m) and an assumption (at line
i) that is an instance of some existentially quantified
sentence that is present (at line k), conclude the given
sentence again.
Condition: The instantial name at line i must not
appear in the sentence at line k or in the sentence at line
m. Also, it must not appear in any of the assumptions
belonging to the assumption set at line m, other than the
instance i itself.
Annotation: k,m $E (i)
Assumption set: all assumptions at line m other than i, and all a
ssumptions at line k.
Examples.
(a)
1 (1) $xFx A
2 (2) Fa A
2 (3) Fa v Ga 2 vI
2 (4) $x(Fx v Gx) 3 $I
1 (5) $x(Fx v Gx) 1,4 $E (2)
(b)
1 (1) $x(Fxx -> P) A
2 (2) Faa -> P A
3 (3) @xFxx A
3 (4) Faa 3 @E
2,3 (5) P 2,4 ->E
1,3 (6) P 1,5 $E (2)
Examples of violation of $E condition.
(a)
1 (1) $xFx A
2 (2) Fa A
3 (3) Ga A
2,3 (4) Fa & Ga 2,3 &I
2,3 (5) $x(Fx & Gx) 4 $I
|
| wrong! |
1,3 (6) $x(Fx & Gx) 1,5 $E (2) |
|
(b)
1 (1) $xFx A
2 (2) Fa A
|
| wrong! |
1 (3) Fa 1,2 $E (2)
|
|
(c)
1 (1) $xFax A
2 (2) Faa A
2 (3) $xFxx 2 $I
|
| wrong! |
1 (4) $xFxx 1,3 $E (2)
|
|
|
|
|
Comment. If all we know is that something is F, we are not entit
led to reason as if we know what it is that is F. As in the case of @I, a use of $E tha
t meets the conditions above and uses a certain instantial name can be turned into a proof of t
he same conclusion from the same assumptions but using any different instantial name. This sho
ws that the conclusion does not rest on any assumptions about the actual identity of the thing
that is said to exist. That is, if we apply $E to $xFx by discharging the assumed instance Fa,
the conditions ensure that we do not mistakenly use any information about the referent of `a'
in particular. After all, $xFx says only that some-thing is F--it doesn't tell us wh
ich individual is F.
|
| Exercise 3.6 |
Prove the following sequents, using the four quantifier rules and primi
tive or derived sentential rules.
|
| S77* | $x(Gx & ~Fx), @x(Gx -> Hx) |- $x(Hx & ~Fx) |
| S78 | $x(Gx & Fx), @x(Fx -> ~Hx) |- $x~Hx |
| S79 | @x(Gx -> ~Fx), @x(~Fx -> ~Hx) |- @x(Gx -> ~Hx) |
| S80 | @x(Gx -> $y(Fy & Hy)) |- @x~Fx -> ~$zGz |
| S81 | @x(Gx -> Hx & Jx), @x(Fx v ~Jx -> Gx)|- @x(Fx -> Hx) |
| S82 | @x(Gx & Kx <-> Hx), ~$x(Fx & Gx)|- @x~(Fx & Hx) |
| S83 | @x(Gx -> Hx), $x((Fx & Gx) & Mx)|- $x(Fx & (Hx & Mx)) |
| S84 | @x(~Gx v ~Hx), @x((Jx -> Fx) -> Hx)|- ~$x(Fx & Gx) |
| S85 | ~$x(~Gx & Hx), @x(Fx -> ~Hx)|- @x(Fx v ~Gx -> ~Hx) |
| S86 | @x~(Gx & Hx), $x(Fx & Gx) |- $x(Fx & ~Hx) |
| S87 | $x(Fx & ~Hx), ~$x(Fx & ~Gx) |- ~@x(Gx -> Hx) |
| S88 | @x(Hx -> Hx & Gx), $x(~Gx & Fx)|- $x(Fx & ~Hx) |
| S89 | @x(Hx -> ~Gx), ~$x(Fx & ~Gx) |- @x~(Fx & Hx) |
| S90 | @x(Fx <-> Gx) |- @xFx <-> @xGx |
| S91 | $xFx -> @y(Gy -> Hy), $xJx -> $xGx|- $x(Fx & Jx) -> $zHz |
| S92 | $xFx v $xGx, @x(Fx -> Gx) |- $xGx |
| S93 | @x(Fx -> ~Gx) |- ~$x(Fx & Gx) |
| S94 | @x(Fx v Hx -> Gx & Kx), ~@x(Kx & Gx) |- $x~Hx |
| S95 | @x(Fx & Gx -> Hx), Ga & @xFx |- Fa & Ha |
| S96 | @x(Fx <-> @yGy) |- @xFx v @x~Fx |
| S97 | @y(Fa -> ($xGx -> Gy)),@x(Gx -> Hx), @x(~Jx -> ~Hx) |- $x~Jx -> ~Fa v @x~Gx |
| S98 | @x(Dx -> Fx) |- @z(Dz -> (@y(Fy -> Gy) -> Gz)) |
| S99 | $xFx <-> @y(Fy v Gy -> Hy), $xHx, ~@z~Fz|- $x(Fx & Hx) |
| S100 | @xFx |- ~$xGx <-> ~($x(Fx & Gx) & @y(Gy -> Fy)) |
| S101 | @x($yFyx -> @zFxz) |- @yx(Fyx -> Fxy) |
| S102 | $x(Fx & @yGxy), @xy(Gxy -> Gyx)|- $x(Fx & @yGyx) |
| S103 | $x~@y(Gxy -> Gyx) |- $x$y(Gxy & ~Gyx) |
| S104 | @x(Gx -> @y(Fy -> Hxy)), $x(Fx & @z~Hxz)|- ~@xGx |
| S105 | @xy(Fxy -> Gxy) |- @x(Fxx -> $y(Gxy & Fyx)) |
|