This is what we mean. We've already seen that we can eliminate a universal quantifier by replacing the variable (x or y or z) with some definite name. This would never be a problem since the statement (x)Ax means Aa and Ab and Ac and so on. However, when we have (Ex)Ax it means Aa or Ab or Ac or somebody, on throughout the whole domain that we have in mind. We can never legitimately replace the variable with a name already in use, since there is never a guarantee that this individual is the same individual we have in mind when we say "someone," as in "someone is ambitious." Still, we want to be able to show how a characteristic would apply to at least one person without using the existential quantifier.
What we do is replace the variable with a new name--one that in no way is in the premises (or in the intended conclusion) or has not been previously introduced.
(Ex)Ax |- Aa EI (new
name:
a)
we are instantiating (hypothetically, that is) with the name "a"
Please note that
different textbooks have different ways of approaching what we call
existential instantiation. Many (such as the Hurley text) allow
the continued use of the variable letters "x" or "y" or "z." In
this course I ask that you use any other letter, as long as it has not
appeared either in the argument form itself or in a previous step in a
derivation. Accordingly, "Fx" would not be a WFF in our system.
We need a parallel rule to bring a universal quantifer back into play. Although there will be a major exception to this later (when we begin discussing conditional proofs), for the present we will have the rule that we can only introduce a universal quantifer when the name in question was the result of a previous elimination of the universal quantifier. Do note that we do not need to use same variable.
Aa |- (x)Ax UG
we are generalizing on the name "a"
Let's see how these rules will be applied in actual proofs.
Everybody
who is
ambitious will work
hard.
Some students are ambitious. Therefore, some students will work
hard.
(x)(Ax -> Wx), (Ex)(Sx & Ax) |- Ex(Sx
&
Wx)
1.
(x)(Ax
-> Wx)
2. (Ex)(Sx & Ax)
/ (Ex)
(Sx & Wx)
3. Sa &
Aa
2, EI note that
we have to do this step first in order to have a new name
4. Aa ->
Wa
1, UI
5.
Aa
3, Simp
6
Wa
4,5, MP
7.
Sa
3, Simp
8. Sa &
Wa
6,7, Conj
9. (Ex)(Sx & Wx)
8, EG
(x)Bx & (y)Cy |- (z)(Bz & Cz)
1.
(x)Bx
& (y)Cy
/(z)(Bz & Cz)
2.
(x)Bx
1, Simp note that since the main connective
is
&
we must eliminate this before we go ahead
3.
Ba
2, UI
4.
(y)Cy
1, Simp
5.
Ca
4, UI
6. Ba &
Ca
3,5, Conj
7. (z)(Bz &
Cz)
6, UG
We also have one very important equivalence rule (one that can be applied inside an expression as well as to the main operator). This is the idea of quantifier negation or quantifier exchange, and it is named CQ in your text:
~(Ex)Fx
:: (x)~Fx CQ
~(x)Fx ::
(Ex)~Fx CQ
note we are allowing DN to be built
into the application of the rule
Applying CQ with longer quantified expressions can involve a number of additional steps that include the use of several equivalence rules. In order to reduce the number of steps, we are allowing the following patterns as specific applications of CQ.
~(Ex)(Fx
& Gx) :: (x)Fx -> ~Gx) CQ
~(x)(Fx -> Gx) ::
(Ex)(Fx & ~Gx) CQ
this is sometimes referred to as
driving through the curl
This rule
often comes into play when we need to eliminate a quantifier, as in the
following example.
(x)Fx
v Gb, ~Fb |-
~(x)~Gx
1.
(x)Fx v Gb
2.
~Fb
/ ~(x)~Gx
3.
(Ex)~Fx 2, EG
4.
~(x)Fx
3, CQ
5.
Gb
1,4, DS
6.
(Ex)Gx
5, EG
7.
~(x)~Gx 6, CQ