by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]
[The following is summary. Boldface (except for metavariables) and bracketed commentary are my own. Please forgive my typos, as proofreading is incomplete. I highly recommend Agler’s excellent book. It is one of the best introductions to logic I have come across.]
Summary of
David W. Agler
Symbolic Logic: Syntax, Semantics, and Proof
Ch.8: Predicate Logic Derivations
8.1 Four Quantifier Rules
Brief summary:
For the language of predicate logic (RL), there are four proof derivation rules to add to those of propositional logic (PL), namely:
This new system of derivation is called RD. And corresponding to these are four additional strategic rules for making proofs in RL.
| Universal Elimination (∀E) From any universally quantified proposition ‘(∀x)P,’ we can derive a substitution instance ‘P(a/x)’ in which all bound variables are consistently replaced with any individual constant (name). | (∀x)P P(a/x) | ∀E |
| Existential Introduction (∃Ι) From any possible substitution instance ‘P(a/x),’ an existentially quantified proposition ‘(∃x)P’ can be derived by consistently replacing at least one individual constant (name) with an existentially quantified variable. | P(a/x) (∃x)P | ∃I |
| Universal Introduction (∀Ι) A universally quantified proposition ‘(∀x)P’ can be derived from a possible substitution instance ‘P(a/x)’ provided (1) ‘a’ does not occur as a premise or as an assumption in an open subproof, and (2) ‘a’ does not occur in ‘(∀x)P.’ | P(a/x) (∀x)P | ∀I |
| Existential Elimination (∃E) From an existentially quantified expression ‘(∃x)P,’ an expression ‘Q’ can be derived from the derivation of an assumed substitution instance ‘P(a/x)’ of ‘(∃x)P’ provided (1) the individuating constant ‘a’ does not occur in any premise or in an active proof (or subproof) prior to its arbitrary introduction in the assumption ‘P(a/x),’ and (2) the individuating constant ‘a’ does not occur in proposition ‘Q’ discharged from the subproof. | (∃x)P | P(a/x) | . | . | . | Q Q | ∃E |
SQ#1(∀E): When using (∀E), the choice of substitution instances ‘P(a/x)’ should be guided by the individual constants (names) already occurring in the proof and any individual constants (names) occurring in the conclusion.
(Agler 328)
SQ#2(∃I): When using (∃I), aim at deriving a substitution instance ‘P(a/x)’ such that a use of (∃I) will result in the desired conclusion. (In other words, if the ultimate goal is to derive ‘(∃x)Px,’ aim to derive a substitution instance of ‘(∃x)Px,’ like ‘Pa,’ ‘Pb,’ ‘Pr,’ so that a use of (∃I) will result in ‘(∃x)Px.’)
SQ#3(∀I): When the goal proposition is a universally quantified proposition ‘(∀x)P,’ derive a substitution instance ‘P(a/x)’ such that a use of (∀I) will result in the desired conclusion.
SQ#4(∃E) Generally, when deciding upon a substitution instance ‘P(a/x)’ to assume for a use of (∃E), choose one that is foreign to the proof.
Summary
Ch.8: Predicate Logic Derivations
We will now add new derivation rules for the language of predicate logic (RL) to the ones from the language of propositional logic (PL).
8.1 Four Quantifier Rules
The natural deduction system for RL that Agler will lay out is called RD, and it “consists of four quantifier derivation rules” (Agler 325). Two of the rules (‘∀E’ and ‘∃E’) are for eliminating quantifiers and two others (‘∀I’ and ‘∃I’) introduce them (Agler 325).
| Universal Elimination (∀E) From any universally quantified proposition ‘(∀x)P,’ we can derive a substitution instance ‘P(a/x)’ in which all bound variables are consistently replaced with any individual constant (name). | (∀x)P P(a/x) | ∀E |
(Agler 325)
Agler gives this simple example .
| 1 | (∀x)Px | P |
| 2 | Pa | 1∀E |
(Agler 325)
For this derivation, the substitution of constant 'a' for x is possible because the x is bound by the quantifier. And we can choose whichever constant we want from the domain.but we can derive any other constant we want instead or in addition, as seen below.
| 1 | (∀x)Px | P |
| 2 | Pa | 1∀E |
| 3 | Pb | 1∀E |
| 4 | Pc | 1∀E |
| 5 | Pd | 1∀E |
| 6 | Pe100 | 1∀E |
(Agler 326)
Note also that all bound variables of a universal quantifier must be substituted consistently.
| 1 | (∀x)Pxx | P |
| 2 | Paa | 1∀E |
| 3 | Pbb | 1∀E |
(Agler 326)
And thus we cannot do the following.
Agler first will show us an argument in English.
Formulated in RL, the above argument would look like the following.
Agler then gives another proof for.
The question still remains, how do we know which constants to choose when using universal elimination? Agler says this decision is guided by two considerations.
As we can see, by choosing the substitution 'b' in line 4, we have set ourselves up for the next line that will lead us to the conclusion. So this shows why in many cases we will want to pick a constant that is used previously in the proof.
The second consideration is to pick constants used in the conclusion. Agler has us look at the last part of the same proof from above.
We know that we need to eventually get Wt in the conclusion, so in line 6, we made a substitution of 't' so that we could eventually derive Wt (Agler 328).
On the basis of these considerations, Agler formulates strategic rule SQ#1(∀E).
[For the conclusion we will need to derive Paa, Pba, and Pma. So we can get those parts establish now.]
Now we can use conjunction elimination to get the different parts we need independently.]
8.1.2 Existential Introduction (∃I)
If we have an unquantified expression with a constant, we can substitute a variable for the constant and produce an existentially quantified expression.
Agler gives this simple example.
Agler then gives a proof for:
[We can see that we have the parts we need. First we will isolate the two predicates, then we will convert them to the existentially quantified expressions that we need, and finally we will combine them to get our goal proposition.]
Agler then clarifies two things when using existential introduction: if there are two or more of the same constants, we can substitute just one, many, or all of them with the variable under existential quantification, and if there are two or more different constants, we can only make the substitutions one constant or for one set of the same constants. To make this apparent, he illustrates with these examples instances.
Agler shows how existential introduction works with English sentences first with this simple example.
The next series shows how when there are two constants, we can replace either or both.
Now with the help of English sentences Agler will illustrate why constants need to be replaced consistently.
However, this situation can be correctly converted by using a second instance of existential introduction.
Agler then shows some more mistaken uses of existential introduction.
When we use existential introduction, the substitution applies to whole formulas. So this is why lines 4 and 5 are incorrect. [Suppose line 2 were Laa→Raa. Is one possible derivation: (∃x)Lax→Rax? And what about: (∃x)Lax→Rab? I am not exactly sure if when we are dealing with a formula like this, if we would need to substitute for all the same constants, even though for the example Laa above we did not need to.] We already know from before that 3 is incorrect because it does not consistently make its substitutions, as it substitutes for two difference constants rather than for just one.
Agler will now show more examples to help us use existential introduction strategically. We first consider:
[We know that we need (∃y)Wy. So we need a W+constant. We see that we have Wb as the consequent in line 2. So we just need Pa to derive it. We could derive Pa by first substituting the variables in line 1 and then using conjunction elimination. So let us do that.]
With this in mind, Agler formulates strategic rule SQ#2(∃I):
Agler says that we can think of this in terms of working backward in the proof. He has us consider this argument again from above.
Agler will show this working-backward method with another example.
[Obtaining the penultimate step is straightforward. We use universal elimination on lines 1 and 2 to obtain the parts for the penultimate step, then we combine them using conjunction introduction.]
Agler has us suppose that for line 4 we instead chose Zb. What would happen then? When we combine lines 3 and 4, we would get Pa∧Zb. Then, we use existential introduction on it, we would not get the conclusion we want. We instead would get (∃x)(Px∧Zb). (Agler 333)
Universal introduction allows us to go from an expression of the form Pa to one of the form (∀x)P. There are two restrictions. The constant being substituted cannot appear as a premise or as an assumption in an open subproof, and it cannot occur in the derived universally quantified formula.
As we can see, we stayed within our restrictions (336). [In the previous simpler proofs, it was immediately obvious why universal introduction was valid. For, it seemed to stay within our intuitions of what it means for a variable to be universally quantified. However, in this case, for some reason, it is less obvious. I am not exactly sure why. If we think of possible interpretations in English, we might have for the premises, "Either everyone loves Corinne or everyone runs quickly. But no one runs quickly." It would not seem to be counterintuitive to then infer, "Therefore, everyone loves Corinne."] But Agler observes it is not obvious why the universal introduction is valid in the above proof. So, he says, we might wonder, "Why is it deductively valid to infer ‘(∀x)P’ from ‘P(a/x)’?" (Agler 336).
To answer this question, Agler first will look at two cases were surely the use of universal introduction is invalid. Suppose we have the statement 'Johnny Walker is a criminal' which we will symbolize Cj. We of course cannot derive from this the statement 'everyone is a criminal' or (∀x)Cx. In the second case we begin with the statement 'someone is a criminal' or (∃x)Cx. From this we of course cannot derive 'everyone is a criminal' (Agler 336).
Agler says that these sorts of uses of universal introduction are often called "hasty generalizations".
Agler will continue through some more examples. In the first one, our domain is all living humans. We will prove the conclusion 'all men are mortal', symbolized as (∀x)(Mx→Rx). And our premises will be 'all organisms are mortal' or (∀x)(Ox→Rx) and 'all men are organisms' or (∀x)(Mx→Ox). [It seems we cannot just use universal elimination on all of them, giving them all the same constant, then use hypothetical syllogism to get Ma→Ra. And finally use universal introduction to get the conclusion we want. There must be a reason why we cannot do that, but I am missing it at the moment. Instead, Agler will do this proof by making the assumption Ma, then we derive within that subproof Ra. We make that eventual derivation by using universal elimination on the premises and then affirming their antecedents to finally get Ra. Then by using conditional introduction, we get Ma→Ra, from which we derive (∀x)(Mx→Rx) using universal introduction.]
Agler then explains why this conclusion does not violate our restrictions and is also not a hasty generalization.
For the next example, we will want to prove that no positive, even integer greater than 2 is prime. We know this already. 2 is a prime number. Every even number greater than 2 is divisible by 2. A prime number by definition is one that has no other divisor other than itself and 1. But even numbers greater than 2 are divisible by 1, by themselves, and by 2 (among potentially other numbers). So we know already that this conclusion is true. To prove this, we will first formulate the conclusion as 'no integer that is positive and even and greater than 2 is prime. [We will make 'I' mean 'is an integer', 'Q' mean 'is positive', 'E' mean 'is even', 'G' mean 'is greater than 2' and 'P' mean 'is prime'.] We would formulate this conclusion symbolically as:
[I am not following the next part. Let me quote it first.]
[It seems like Agler is saying that through a series of steps, which is guided by the definition of prime number, we can derive ¬Pa. In order to do that, I would think that somehow we would need already to have established that (∀x){[(Ix∧Qx)∧(Ex∧Gx)]→¬Px} or something that somehow functions to say that ¬Pa can be derived somehow from this formula or its parts. I am not sure why Agler leaves out the steps. Perhaps it is too obvious and/or also too lengthy. Or perhaps we are supposed to somehow derive ¬Pa from the definition somehow. But in that case, I do not understand the omitted lines. Or maybe the idea is that we do some sort of indefinite series of checks for each constant to determine semantically the truth value, and maybe furthermore this is some kind of inductive proof. No, probably not. At any rate, after having established this derivation, we can then use conditional introduction to obtain the conclusion structure but with all constants 'a' and then use universal introduction to get the goal proposition.]
[Agler then shows this general pattern now with a proof for the Pythagorean theorem. I again do not understand how things work in the omitted parts. But the idea seems to be the following. What we say about some randomly selected constant we can also say about all constants. I am probably missing the idea here, so let me quote.]
[Recall that the first restriction of universal introduction is that the constant being substituted not appear as a premise or as an assumption in an open subproof. In line 4, 'b' is substituted, but it appears in the premise. In line 5 'c' is substituted, but it also appears in line 1. Lines 6 and 7 similarly substitute for 'b' and 'd' respectively, which appear in the premise.] Lines 4 through 7 all break the restriction that we cannot substitute for a constant appearing in the premises or in an open subproof (Agler 340).
Agler then shows a violation of this restriction in terms of a
Here, the assumption is still open, as we have not discharged it yet. So we cannot substitute for 'a', which appears in that open assumption. But, if we do discharge the assumption, we can use universal introduction and substitute for the constant that appears in that discharged assumption. Agler shows that in this example.
[Recall that the second restriction was that the constant being substituted cannot appear in the final universally quantified formula.] Agler now gives some examples that break the second restriction on universal introduction and then in the final line shows an instance that does not break the second restriction.
Agler then gives us his strategic rule SQ#3(∀I)
Agler illustrates with a proof whose goal proposition is (∀x)(Rxx→Rxx).
[Recall the strategic rule for existential introduction: "SQ#2(∃I): When using (∃I), aim at deriving a substitution instance ‘P(a/x)’ such that a use of (∃I) will result in the desired conclusion".] Just like with the strategic rule for existential introduction, we for this rule also think backwards from the conclusion (Agler 342). He has us consider this proof.
[By working backward, we know that we will want to derive Raa→(Saa∨Raa) so that from it we can derive (∀x)[Rxx→(Sxx∨Rxx)] by means of universal introduction. As we have no premises, we will need to do this by means of assumptions in subproofs. Given it is a conditional, if we assume the antecedent and can derive the consequent, we can then derive this formula in the main proof. Suppose we assume Raa. How might we derive from it Saa∨Raa? We see that Raa, which we assumed is also in the disjunction. So by using disjunction introduction, we can disjoin to Raa any arbitrary formula. So we will disjoin to it Saa, which will allow us to eventually derive the goal proposition, as seen in these steps below.]
[For existential elimination, we begin with an existentially quantified expression. We then assume that predicate with some constant which has not appeared in the premises or in an active proof or subproof. We then derive some other proposition that does not contain this constant, and we derive that new proposition in the main proof.]
Agler provides this simple example.
Recall that existential elimination has two restrictions. We might ask:
Agler gives another example.
This example above shows a valid use of the rule.
Agler will now examine some incorrect uses of the existential elimination that are invalid because they violate one of the restrictions. The following example will break the first restriction.
Note that 'a' occurs in the first premise. There is nothing wrong with us assuming it in line 3. But there is something wrong in using existential elimination to extract (∀x)Px from the subproof, because (∀x)Px was made by substituting for the 'a' which occurred in the premise (Agler 344). Agler illustrates why this is invalid by using English sentences.
Agler now gives an example that does not violate this restriction.
But in the following case, restriction 1 is violated.
Again, the problem here is that the variable in line 5 is substituting for a constant in the subproof that appeared already in the second premise.
With this in mind, Agler formulates strategic rule SQ#4(∃E):
In line 4, we substituted x for the second constant 'b' in 'Wbb', leaving the first 'b' intact. This on its own is fine, but then we cannot make the derivation in line 5 using existential elimination, because we substituted x for 'b', but 'b' is found in the derived formula too (Agler 346). Agler further explains why this is invalid: "consider that line 1 only refers to there being at least one object z that is both ‘Wzz’ and ‘Mz.’ While we could validly infer ‘(∃x)(Wzz),’ we could never validly infer a specific object constant" (Agler 346). [I did not follow that explanation so well. Perhaps the idea is that we know that some constant holds for W, but we do not know which, so we cannot infer line 5.]
Note also that while the assumption in existential elimination is based on an existentially quantified formula, the formula that we eventually derive would be a universally quantified one, as in this example.
Agler, David. Symbolic Logic: Syntax, Semantics, and Proof. New York: Rowman &; Littlefield, 2013.
| 1 | (∀x)Pxx | P |
| 2 | Pab | 1∀E–NO! |
| 3 | Pba | 1∀E–NO! |
(Agler 326)
Agler first will show us an argument in English.
| 1 | Everyone is a person. | P |
| 2 | If Alfred is a person, then Bob is a zombie. | P |
| 3 | Alfred is a person. | 1∀E |
| 4 | Therefore, Bob is a zombie. | 2,3→E |
(Agler 326)
Formulated in RL, the above argument would look like the following.
(∀x)Px, Pa→Zb ⊢ Zb
| 1 | (∀x)Px | P |
| 2 | Pa→Zb | P |
| 3 | Pa | 1∀E |
| 4 | Zb | 2,3→E |
(∀x)[Px→(∀y)(Qx→Wy)],Pb∧Qb ⊢ WtLet us set it up.
| 1 | (∀x)[Px→(∀y)(Qx→Wy)] | P |
| 2 | Pb∧Qb | P |
[We see that if we could affirm the antecedent of the conditional in line 1, then we could derive the consequent formulation. We will be able to substitute what we want for the antecedent, so we should derive merely Pb from 2 for this purpose, then use universal elimination to make the antecedent be Pb, then use conditional elimination to derive the consequent.]
| 1 | (∀x)[Px→(∀y)(Qx→Wy)] | P |
| 2 | Pb∧Qb | P |
| 3 | Pb | 2∧E |
| 4 | Pb→(∀y)(Qb→Wy) | 1∀E |
| 5 | (∀y)(Qb→Wy) | 3,4→E |
[Agler will have us note how in line 4 when we used universal elimination that there were two bound instances of x that we substituted. He also has us note that in line 4, ∀y is not the main operator, which is why the rule did not apply to it in that instance.] [Now we know that we need to derive Wt eventually. We see that we could potentially obtain it by affirming Qb and using universal elimination to make the consequent Wt, in line 5. So let us get Qb, use it in this way, and derive our goal proposition.]
| 1 | (∀x)[Px→(∀y)(Qx→Wy)] | P |
| 2 | Pb∧Qb | P |
| 3 | Pb | 2∧E |
| 4 | Pb→(∀y)(Qb→Wy) | 1∀E |
| 5 | (∀y)(Qb→Wy) | 3,4→E |
| 6 | Qb→Wt | 5∀E |
| 7 | Qb | 2∧E |
| 8 | Wt | 6,7→E |
(Agler 327)
The question still remains, how do we know which constants to choose when using universal elimination? Agler says this decision is guided by two considerations.
(1) It is guided by individual constants already occurring in the proof.So let us look more at the first concern for the constants already there in the proof. Agler has us consider the example proof from above. [Let us first set it up.]
(2) It is guided by individual constants in the conclusion.
(Agler 328)
| 1 | (∀x)[Px→(∀y)(Qx→Wy)] | P |
| 2 | Pb∧Qb | P |
| 3 | Pb | 2∧E |
| 4 | Pb→(∀y)(Qb→Wy) | 1∀E |
| 5 | (∀y)(Qb→Wy) | 3,4→E |
(Agler 328)
As we can see, by choosing the substitution 'b' in line 4, we have set ourselves up for the next line that will lead us to the conclusion. So this shows why in many cases we will want to pick a constant that is used previously in the proof.
The second consideration is to pick constants used in the conclusion. Agler has us look at the last part of the same proof from above.
| 5 | (∀y)(Qb→Wy) | 3,4→E |
| 6 | Qb→Wt | 5∀E |
| 7 | Qb | 2∧E |
| 8 | Wt | 6,7→E |
(Agler 328)
We know that we need to eventually get Wt in the conclusion, so in line 6, we made a substitution of 't' so that we could eventually derive Wt (Agler 328).
On the basis of these considerations, Agler formulates strategic rule SQ#1(∀E).
SQ#1(∀E): When using (∀E), the choice of substitution instances ‘P(a/x)’ should be guided by the individual constants (names) already occurring in the proof and any individual constants (names) occurring in the conclusion.To illustrate, Agler has us consider the following proof.
(Agler 328)
(∀x)(Pxa∧Qxa) ⊢ (Paa∧Pba)∧Pma[Let us set it up.]
(Agler 328)
| 1 | (∀x)(Pxa∧Qxa) | P |
| 1 | (∀x)(Pxa∧Qxa) | P |
| 2 | Paa∧Qaa | 1∀E |
| 3 | Pba∧Qba | 1∀E |
| 4 | Pma∧Qma | 1∀E |
| 1 | (∀x)(Pxa∧Qxa) | P |
| 2 | Paa∧Qaa | 1∀E |
| 3 | Pba∧Qba | 1∀E |
| 4 | Pma∧Qma | 1∀E |
| 5 | Paa | 2∧E |
| 6 | Pba | 3∧E |
| 7 | Pma | 4∧E |
[And then with conjunction introduction we can build up the formula in the conclusion.]
| 1 | (∀x)(Pxa∧Qxa) | P |
| 2 | Paa∧Qaa | 1∀E |
| 3 | Pba∧Qba | 1∀E |
| 4 | Pma∧Qma | 1∀E |
| 5 | Paa | 2∧E |
| 6 | Pba | 3∧E |
| 7 | Pma | 4∧E |
| 8 | Paa∧Pba | 5,6∧I |
| 9 | (Paa∧Pba)∧Pma | 7,8∧I |
(Agler 328-329)
8.1.2 Existential Introduction (∃I)
| Existential Introduction (∃Ι) From any possible substitution instance ‘P(a/x),’ an existentially quantified proposition ‘(∃x)P’ can be derived by consistently replacing at least one individual constant (name) with an existentially quantified variable. | P(a/x) (∃x)P | ∃I |
(Agler 329)
Agler gives this simple example.
Zr ⊢ (∃x)Zx
| 1 | Zr | P |
| 2 | (∃x)Zx | 1∃I |
(Agler 329)
Agler then gives a proof for:
Pa→Qa, Pa ⊢ (∃y)Qy∧(∃x)Px[Let us set it up first.]
(Agler 329)
| 1 | Pa→Qa | P |
| 2 | Pa | P |
| 1 | Pa→Qa | P |
| 2 | Pa | P |
| 3 | Qa | 1,2→E |
| 4 | (∃x)Px | 2∃I |
| 5 | (∃y)Qy | 3∃I |
| 6 | (∃x)Px∧(∃y)Qy | 4,5∧I |
(Agler 329)
Agler then clarifies two things when using existential introduction: if there are two or more of the same constants, we can substitute just one, many, or all of them with the variable under existential quantification, and if there are two or more different constants, we can only make the substitutions one constant or for one set of the same constants. To make this apparent, he illustrates with these examples instances.
| 1 | Laab | P |
| 2 | (∃x)Lxab | 1∃I |
| 3 | (∃x)Laxb | 1∃I |
| 4 | (∃x)Lxxb | 1∃I |
| 5 | (∃x)Lxxx | 1∃I—NO! |
(Agler 330)
Excluding line 5, each of the above uses of (∃I) is valid. Notice that at lines 2 and 3, only one individual constant from line 1 is replaced by the use of (∃I). This is acceptable since (∃I) says that an existentially quantified proposition ‘(∃x)Px’ can be derived by replacing at least one individual constant with an existentially quantified variable. Also note that line 4 is correct since while more than one individual constant is being replaced, it is being replaced in a uniform manner. That is, more than one ‘a’ is being replaced by existentially quantified x’s. However, note that line 5 is not correct since the replacement of bound variables is not uniform. At line 5, not only is each ‘a’ being replaced by an x but so is every ‘b.’(Agler 330)
Agler shows how existential introduction works with English sentences first with this simple example.
| 1 | Rick is a zombie. | P |
| 2 | Therefore, someone is a zombie. | 1∃I |
(Agler 330)
| 1 | Alfred loves Alfred. | P |
| 2 | Someone loves Alfred. | 1∃I |
| 3 | Alfred loves someone. | 1∃I |
| 4 | Someone loves him- or herself. | 1∃I |
| 1 | Laa | P |
| 2 | (∃x)Lxa | 1∃I |
| 3 | (∃x)Lax | 1∃I |
| 4 | (∃x)Lxx | 1∃I |
(Agler 330)
Now with the help of English sentences Agler will illustrate why constants need to be replaced consistently.
| 1 | Alice loves Bob. | P |
| 2 | Someone loves themselves. | 1∃I—NO! |
| 1 | Lab | P |
| 2 | (∃x)Lxx | 1∃I—NO! |
(Agler 331)
However, this situation can be correctly converted by using a second instance of existential introduction.
| 1 | Lab | P/(∃x)(∃y)Lxy |
| 2 | (∃x)Lxx | 1∃I—NO! |
| 3 | (∃x)(∃y)Lxy | 2∃I |
(Agler 331)
Agler then shows some more mistaken uses of existential introduction.
| 1 | Lab | P |
| 2 | Lab→Rab | P |
| 3 | (∃x)Lxx | 1∃I—NO! |
| 4 | (∃x)Lax→Rab | 2∃I—NO! |
| 5 | (∃x)Lax→(∃x)Rax | 4∃I—NO! |
(Agler 331)
When we use existential introduction, the substitution applies to whole formulas. So this is why lines 4 and 5 are incorrect. [Suppose line 2 were Laa→Raa. Is one possible derivation: (∃x)Lax→Rax? And what about: (∃x)Lax→Rab? I am not exactly sure if when we are dealing with a formula like this, if we would need to substitute for all the same constants, even though for the example Laa above we did not need to.] We already know from before that 3 is incorrect because it does not consistently make its substitutions, as it substitutes for two difference constants rather than for just one.
Agler will now show more examples to help us use existential introduction strategically. We first consider:
(∀x)(Px∧Rx), Pa→Wb ⊢ (∃y)Wy[Let us first set it up.]
(Agler 331)
| 1 | (∀x)(Px∧Rx) | P |
| 2 | Pa→Wb | P/(∃y)Wy |
[We know that we need (∃y)Wy. So we need a W+constant. We see that we have Wb as the consequent in line 2. So we just need Pa to derive it. We could derive Pa by first substituting the variables in line 1 and then using conjunction elimination. So let us do that.]
| 1 | (∀x)(Px∧Rx) | P |
| 2 | Pa→Wb | P/(∃y)Wy |
| 3 | Pa∧Ra | 1∀E |
| 4 | Pa | 3∧E |
| 5 | Wb | 2,4→E |
| 6 | (∃y)Wy | 5∃I |
(Agler 332)
With this in mind, Agler formulates strategic rule SQ#2(∃I):
SQ#2(∃I): When using (∃I), aim at deriving a substitution instance ‘P(a/x)’ such that a use of (∃I) will result in the desired conclusion.
In other words, if the ultimate goal is to derive ‘(∃x)Px,’ aim to derive a substitution instance of ‘(∃x)Px,’ like ‘Pa,’ ‘Pb,’ ‘Pr,’ so that a use of (∃I) will result in ‘(∃x)Px.’
(Agler 332)
Agler says that we can think of this in terms of working backward in the proof. He has us consider this argument again from above.
(∀x)(Px∧Rx), Pa→Wb ⊢ (∃y)WyWe can imagine ourselves placing the conclusion at some indeterminate step at the very end. Then the step before it, we have the predicate with any possible constant that can be substituted for the variable in the conclusion.
(Agler 332)
| 1 | (∀x)(Px∧Rx) | P |
| 2 | Pa→Wb | P/(∃y)Wy |
| . | | |
| . | | |
| k | W(a, ..., v/x) | |
| k+1 | (∃y)Wy | k∃I |
(Agler 332)
Agler will show this working-backward method with another example.
(∀x)Px, (∀y)Zy⊢(∃x)(Px∧Zx)
(Agler 332)
| 1 | (∀x)Px | P |
| 2 | (∀y)Zy | P/(∃x)(Px∧Zx) |
| . | | |
| . | | |
| k | P(a/x)∧Z(a/x) | |
| k+1 | (∃x)(Px∧Zx) | k∃I |
(Agler 332)
[Obtaining the penultimate step is straightforward. We use universal elimination on lines 1 and 2 to obtain the parts for the penultimate step, then we combine them using conjunction introduction.]
| 1 | (∀x)Px | P |
| 2 | (∀y)Zy | P/(∃x)(Px∧Zx) |
| 3 | Pa | 1∀E |
| 4 | Za | 2∀E |
| 5 | P(a/x)∧Z(a/x) | 3,4∧I |
| 6 | (∃x)(Px∧Zx) | 5∃I |
(333)
Agler has us suppose that for line 4 we instead chose Zb. What would happen then? When we combine lines 3 and 4, we would get Pa∧Zb. Then, we use existential introduction on it, we would not get the conclusion we want. We instead would get (∃x)(Px∧Zb). (Agler 333)
8.1.3 Universal Introduction (∀I)
Universal introduction allows us to go from an expression of the form Pa to one of the form (∀x)P. There are two restrictions. The constant being substituted cannot appear as a premise or as an assumption in an open subproof, and it cannot occur in the derived universally quantified formula.
| Universal Introduction (∀Ι) A universally quantified proposition ‘(∀x)P’ can be derived from a possible substitution instance ‘P(a/x)’ provided (1) ‘a’ does not occur as a premise or as an assumption in an open subproof, and (2) ‘a’ does not occur in ‘(∀x)P.’ | P(a/x) (∀x)P | ∀I |
(Agler 335)
Agler gives the simple example of a proof for:
(∀x)Px ⊢ (∀y)Py(Agler 335)
| 1 | (∀x)Px | P |
| 2 | Pa | 1∀E |
| 3 | (∀y)Py | 2∀I |
(Agler 335)
Given the restrictions, we need always to check for these things when using universal introduction.
Agler offers another illustration.
We notice that 'b' does not occur in the premises or in an open assumption, and it is not in the final line where we perform the universal introduction. Thus we kept within the restrictions (Agler 336). Agler further explains:
Agler then provides a third example:
(1) Does the substitution instance ‘P(a/x)’ occur as a premise or as an open assumption?In this example, we should see why we are able to make the universal introduction derivation. [The reasoning seems to be that if we are able to derive Pa from (∀x)Px, then we are saying it holds for all constants. Thus we should also be able to say (∀y)Py, because it says the same thing, namely, that it holds for all constants.]
(2) Does the substitution instance ‘P(a/x)’ not occur in ‘(∀x)P?’
(Agler 335)
In this case, it should be somewhat obvious why it is valid to infer ‘(∀y)Py’ at line 3 from ‘Pa’ at line 2. This is because ‘(∀x)Px’ and ‘(∀y)Py’ are notational variants. That is, ‘(∀x) Px’ says that everything in the domain of discourse has the property ‘P,’ and ‘(∀y) Py’ says exactly the same thing. So, if ‘(∀x)Px’ is true, then ‘(∀y)Py’ cannot be false since ‘(∀y)Py’ and ‘(∀x)Px’ are logically equivalent.
(Agler 335)
Agler offers another illustration.
(∀x)(Px∧Rx) ⊢ (∀y)(Py)[This one is similar to one we did above, only this time we do not compose the conjunction but rather decompose it.]
(Agler 335d)
| 1 | (∀x)(Px∧Rx) | P |
| 2 | Pb∧Rb | 1∀E |
| 3 | Pb | 2∧E |
| 4 | (∀y)Py | 3∀I |
(Agler 336)
We notice that 'b' does not occur in the premises or in an open assumption, and it is not in the final line where we perform the universal introduction. Thus we kept within the restrictions (Agler 336). Agler further explains:
Here, ‘(∀x) (Px∧Rx)’ and ‘(∀y)Py’ are not notational variants, but it should be obvious that it is impossible for ‘(∀x)(Px∧Rx)’ to be true and ‘(∀y)Py’ false since ‘(∀x)(Px∧Rx)’ says that everything is both ‘P’ and R, while ‘(∀y)Py’ says that everything is ‘P.’
(Agler 336)
Agler then provides a third example:
(∀x)(Pxc∨Qx), (∀x)¬Qx ⊢ (∀x)(Pxc)[We will need Pxc. We see it in the first premise. Were we to use universal elimination on the first sentence, we would get a formula now with a constant in the first place of the predicate formula. If we also used universal elimination on the second premise, then we could use disjunctive syllogism to obtain the P with two constants. This would allow us to use universal introduction to get the desired conclusion.]
(Agler 336)
| 1 | (∀x)(Pxc∨Qx) | P |
| 2 | (∀x)￢Qx | P |
| 3 | Pac∨Qa | 1∀E |
| 4 | ￢Qa | 2∀E |
| 5 | Pac | 3,4DS |
| 6 | (∀x)Pxc | 5∀I |
(Agler 336)
As we can see, we stayed within our restrictions (336). [In the previous simpler proofs, it was immediately obvious why universal introduction was valid. For, it seemed to stay within our intuitions of what it means for a variable to be universally quantified. However, in this case, for some reason, it is less obvious. I am not exactly sure why. If we think of possible interpretations in English, we might have for the premises, "Either everyone loves Corinne or everyone runs quickly. But no one runs quickly." It would not seem to be counterintuitive to then infer, "Therefore, everyone loves Corinne."] But Agler observes it is not obvious why the universal introduction is valid in the above proof. So, he says, we might wonder, "Why is it deductively valid to infer ‘(∀x)P’ from ‘P(a/x)’?" (Agler 336).
To answer this question, Agler first will look at two cases were surely the use of universal introduction is invalid. Suppose we have the statement 'Johnny Walker is a criminal' which we will symbolize Cj. We of course cannot derive from this the statement 'everyone is a criminal' or (∀x)Cx. In the second case we begin with the statement 'someone is a criminal' or (∃x)Cx. From this we of course cannot derive 'everyone is a criminal' (Agler 336).
Agler says that these sorts of uses of universal introduction are often called "hasty generalizations".
That a single specific (or some nonspecific) object has a property does not entail that every object has that property. These two cases are what motivates the two restrictions placed on the use of (∀I). Namely, a use of (∀I) is not valid when it is used to generalize an instantiating constant that names either a single specific individual or some unknown individual. However, a use of (∀I) is valid when the instantiating constant it generalizes is an arbitrarily-selected individual, that is, an individual chosen at random from the domain of discourse.
(Agler 337)
Agler will continue through some more examples. In the first one, our domain is all living humans. We will prove the conclusion 'all men are mortal', symbolized as (∀x)(Mx→Rx). And our premises will be 'all organisms are mortal' or (∀x)(Ox→Rx) and 'all men are organisms' or (∀x)(Mx→Ox). [It seems we cannot just use universal elimination on all of them, giving them all the same constant, then use hypothetical syllogism to get Ma→Ra. And finally use universal introduction to get the conclusion we want. There must be a reason why we cannot do that, but I am missing it at the moment. Instead, Agler will do this proof by making the assumption Ma, then we derive within that subproof Ra. We make that eventual derivation by using universal elimination on the premises and then affirming their antecedents to finally get Ra. Then by using conditional introduction, we get Ma→Ra, from which we derive (∀x)(Mx→Rx) using universal introduction.]
| 1 | (∀x)(Ox→Rx) | P |
| 2 | (∀x)(Mx→Ox) | P |
| 3 | Ma | A |
| 4 | Oa→Ra | 1∀E |
| 5 | Ma→Oa | 2∀E |
| 6 | Oa | 3,5→E |
| 7 | Ra | 4,6→E |
| 8 | Ma→Ra | 3–7→I |
| 9 | (∀x)(Mx→Rx) | 8∀I |
(Agler 338)
Agler then explains why this conclusion does not violate our restrictions and is also not a hasty generalization.
Note two things. First, line 9 does not violate either of the two restrictions on the use of (∀I), and it is not a hasty generalization because it generalizes not from some specific man and not from some unknown man but from a randomly selected man. We have shown then that if we randomly select a man from the universe of discourse and show that the man has the property of being mortal, we can generalize that every man has that property. This is valid because the generalization depends not on any idiosyncratic property that belongs to a specific man but on a property of all men.
(Agler 338)
For the next example, we will want to prove that no positive, even integer greater than 2 is prime. We know this already. 2 is a prime number. Every even number greater than 2 is divisible by 2. A prime number by definition is one that has no other divisor other than itself and 1. But even numbers greater than 2 are divisible by 1, by themselves, and by 2 (among potentially other numbers). So we know already that this conclusion is true. To prove this, we will first formulate the conclusion as 'no integer that is positive and even and greater than 2 is prime. [We will make 'I' mean 'is an integer', 'Q' mean 'is positive', 'E' mean 'is even', 'G' mean 'is greater than 2' and 'P' mean 'is prime'.] We would formulate this conclusion symbolically as:
(∀x){[(Ix∧Qx)∧(Ex∧Gx)]→¬Px}[So this would be something like, for all x, if x is a positive integer and x is even and greater than 2, then it is not prime. We will do our proof by assuming the antecedent with the intention of deriving the consequent. But the antecedent will not be universally quantified. Rather, we will select a constant.]
(Agler 338)
| 1 | | (Ia∧Qa)∧(Ea∧Ga) | A |
(Agler 338)
[I am not following the next part. Let me quote it first.]
This says to assume that some randomly selected integer ‘a’ from a universe of discourse consisting of positive integers is an even integer greater than 2. From this assumption, the definition of a prime number, and the fact that every even number greater than 2 is divisible by 2, we can infer that this randomly selected integer is not prime.
(Agler 338)
| 1 | | (Ia∧Qa)∧(Ea∧Ga) | A |
| . | | . | . |
| . | | . | . |
| . | | . | . |
| k | | ¬Pa | . |
(Agler 338-339)
[It seems like Agler is saying that through a series of steps, which is guided by the definition of prime number, we can derive ¬Pa. In order to do that, I would think that somehow we would need already to have established that (∀x){[(Ix∧Qx)∧(Ex∧Gx)]→¬Px} or something that somehow functions to say that ¬Pa can be derived somehow from this formula or its parts. I am not sure why Agler leaves out the steps. Perhaps it is too obvious and/or also too lengthy. Or perhaps we are supposed to somehow derive ¬Pa from the definition somehow. But in that case, I do not understand the omitted lines. Or maybe the idea is that we do some sort of indefinite series of checks for each constant to determine semantically the truth value, and maybe furthermore this is some kind of inductive proof. No, probably not. At any rate, after having established this derivation, we can then use conditional introduction to obtain the conclusion structure but with all constants 'a' and then use universal introduction to get the goal proposition.]
| 1 | | (Ia∧Qa)∧(Ea∧Ga) | A |
| . | | . | . |
| . | | . | . |
| . | | . | . |
| k | | ¬Pa | . |
| k+1 | [(Ia∧Qa)∧(Ea∧Ga)]→¬Pa | 1–k,→I |
| k+2 | (∀x){[(Ix∧Qx)∧(Ex∧Gx]→¬Px} | k+1,∀I |
(Agler 339)
[Agler then shows this general pattern now with a proof for the Pythagorean theorem. I again do not understand how things work in the omitted parts. But the idea seems to be the following. What we say about some randomly selected constant we can also say about all constants. I am probably missing the idea here, so let me quote.]
As one final example, consider the general structure of Euclid’s proof of the Pythagorean theorem involving a randomly selected right triangle. This is proposition I.47 in Euclid’s Elements. The conclusion of the proof is the following: For every right triangle, the square of the hypotenuse is equal to the sum of the squares of the legs. That is, c2 = a2 + b2. |
We can prove this by beginning with an assumption. That is, assume some randomly selected Euclidean triangle has an angle equal to 90 degrees. That is, assume ΔABC where ∠ACB is 90°. From this assumption, various assumptions about space and lines, and more general facts about triangles in general, we derive the consequence that the randomly selected triangle is such that the square of the hypotenuse is equal to the square of its two sides. After deriving this consequence, a use of ‘→Ι’ is applied in order to exit the subproof, and then the conditional is generalized.
(Agler 340)
| 1 | | ∠ACB where ∠ACB is 90° | A |
| . | | . | . |
| . | | . | . |
| . | | . | . |
| k | | c2 = a2 + b2 | . |
| k+1 | ABC where ∠ACB is 90° → c2 = a2 + b2 | 1–k,→I |
| k+2 | For all right-angled triangles, c2 = a2 + b2 | k+1,∀I |
(Agler 340)
The proof of the Pythagorean theorem thus involves an inference from an arbitrarily selected individual constant to a universal statement about all right triangles.(Agler 340)
Agler then has us consider the following incorrect uses of the rule.
| 1 | Fbc∧Fbd | P |
| 2 | Fbc | 1∧E |
| 3 | Fbd | 1∧E |
| 4 | (∀x)(Fxc) | 2∀I—NO! |
| 5 | (∀x)(Fbx) | 2∀Ι—NO! |
| 6 | (∀x)(Fxd) | 3∀I—NO! |
| 7 | (∀x)(Fbx) | 3∀I—NO! |
(Agler 340)
[Recall that the first restriction of universal introduction is that the constant being substituted not appear as a premise or as an assumption in an open subproof. In line 4, 'b' is substituted, but it appears in the premise. In line 5 'c' is substituted, but it also appears in line 1. Lines 6 and 7 similarly substitute for 'b' and 'd' respectively, which appear in the premise.] Lines 4 through 7 all break the restriction that we cannot substitute for a constant appearing in the premises or in an open subproof (Agler 340).
Agler then shows a violation of this restriction in terms of a
| 1 | Fbb | P |
| 2 | | Raa | A |
| 3 | | (∀x)Rxx | 2∀I—NO! |
(Agler 340)
Here, the assumption is still open, as we have not discharged it yet. So we cannot substitute for 'a', which appears in that open assumption. But, if we do discharge the assumption, we can use universal introduction and substitute for the constant that appears in that discharged assumption. Agler shows that in this example.
| 1 | Fbb | P |
| 2 | | Raa | A |
| 3 | | Raa∨Pa | 2∨I |
| 4 | Raa→(Raa∨Pa) | 2–3→I |
| 5 | (∀x)[Rxx→(Rxx∨Px)] | 4∀I |
(Agler 341)
[Recall that the second restriction was that the constant being substituted cannot appear in the final universally quantified formula.] Agler now gives some examples that break the second restriction on universal introduction and then in the final line shows an instance that does not break the second restriction.
| 1 | (∀x)(Pxx→Lb) | P |
| 2 | Pcc→Lb | 1∀E |
| 3 | (∀y)(Pyc→Lb) | 2∀I—NO! |
| 4 | (∀y)(Pcy→Lb) | 2∀I—NO! |
| 5 | (∀y)(Pyy→Lb) | 2∀I |
(Agler 341)
Agler then gives us his strategic rule SQ#3(∀I)
SQ#3(∀I): When the goal proposition is a universally quantified proposition ‘(∀x)P,’ derive a substitution instance ‘P(a/x)’ such that a use of (∀I) will result in the desired conclusion.
(Agler 341)
Agler illustrates with a proof whose goal proposition is (∀x)(Rxx→Rxx).
| 1 | | Rcc | A |
| 2 | | Rcc | 1R |
| 3 | Rcc→Rcc | 1–2→I |
| 4 | (∀x)(Rxx→Rxx) | 3∀I |
(Agler 341)
This example shows us that in order to get the goal proposition, which has the form (∀x)P, we needed to first obtain one of the form P(a/x). We can see then in the next example how by deriving a form with the universal quantifier in it will not help us arrive upon our goal proposition.
| 1 | | (∀x)Rxx | A |
| 2 | | (∀x)Rxx | 1R |
| 3 | ∀x)Rxx→(∀x)Rxx | 1–2→I |
(Agler 341)
[Recall the strategic rule for existential introduction: "SQ#2(∃I): When using (∃I), aim at deriving a substitution instance ‘P(a/x)’ such that a use of (∃I) will result in the desired conclusion".] Just like with the strategic rule for existential introduction, we for this rule also think backwards from the conclusion (Agler 342). He has us consider this proof.
⊢ (∀x)[Rxx→(Sxx∨Rxx)]
(Agler 342)
[By working backward, we know that we will want to derive Raa→(Saa∨Raa) so that from it we can derive (∀x)[Rxx→(Sxx∨Rxx)] by means of universal introduction. As we have no premises, we will need to do this by means of assumptions in subproofs. Given it is a conditional, if we assume the antecedent and can derive the consequent, we can then derive this formula in the main proof. Suppose we assume Raa. How might we derive from it Saa∨Raa? We see that Raa, which we assumed is also in the disjunction. So by using disjunction introduction, we can disjoin to Raa any arbitrary formula. So we will disjoin to it Saa, which will allow us to eventually derive the goal proposition, as seen in these steps below.]
| 1 | | Raa | A/Saa∨Raa |
| 2 | | Saa∨Raa | 1∨I |
| 3 | Raa→(Saa∨Raa) | 1–2→I |
| 4 | (∀x)[Rxx→(Sxx ∨ Rxx)] | 3∀I |
(Agler 342)
8.1.4 Existential Elimination (∃E)
[For existential elimination, we begin with an existentially quantified expression. We then assume that predicate with some constant which has not appeared in the premises or in an active proof or subproof. We then derive some other proposition that does not contain this constant, and we derive that new proposition in the main proof.]
| Existential Elimination (∃E) From an existentially quantified expression ‘(∃x)P,’ an expression ‘Q’ can be derived from the derivation of an assumed substitution instance ‘P(a/x)’ of ‘(∃x)P’ provided (1) the individuating constant ‘a’ does not occur in any premise or in an active proof (or subproof) prior to its arbitrary introduction in the assumption ‘P(a/x),’ and (2) the individuating constant ‘a’ does not occur in proposition ‘Q’ discharged from the subproof. | (∃x)P | P(a/x) | . | . | . | Q Q | ∃E |
(Agler 342)
Agler provides this simple example.
| 1 | (∃x)Px | P |
| 2 | | Pa | A/∃E |
| 3 | | (∃y)Py | 2∃I |
| 4 | (∃y)Py | 1,2–3∃E |
(Agler 343)
Recall that existential elimination has two restrictions. We might ask:
(1) Does the individuating constant ‘a’ occur in any premise or in an active proof (or subproof) prior to its arbitrary introduction in the assumption ‘P(a/x)’?As we can see, the above example does not violate either restriction, so the inference is valid.
(2) Does the individuating constant ‘a’ occur in proposition ‘Q’ discharged from the subproof?
(Agler 343)
Agler gives another example.
(∃x)Px ⊢ (∃x)(Px∨¬Mx)
(Agler 343)
| 1 | (∃x)Px | P |
| 2 | | Pa | A/∃E |
| 3 | | Pa∨¬Ma | 2∨I |
| 4 | | (∃x)(Px∨¬Mx) | 3∃I |
| 5 | (∃x)(Px∨¬Mx) | 1,2–4∃E |
(Agler 343)
This example above shows a valid use of the rule.
Agler now has us consider this one. [(∃z)(Wz∧Mz)⊢(∃z)Wz∧(∃z)Mz. As we can see, first we will use existential elimination in an assumption to get the conjunction with constants. Then we decompose it into its constituent parts. From each of these we use existential introduction to derive existentially quantified formulas with variables z. We then combine them with conjunction introduction, and derive the goal proposition in the main proof using existential elimination.]
| 1 | (∃z)(Wz∧Mz) | P |
| 2 | | Wa∧Ma | A/∃E |
| 3 | | Wa | 2∧E |
| 4 | | Ma | 2∧E |
| 5 | | (∃z)Wz | 3∃I |
| 6 | | (∃z)Mz | 4∃I |
| 7 | | (∃z)Wz∧(∃z)Mz | 5,6∧I |
| 8 | (∃z)Wz∧(∃z)Mz | 1,2–7∃E |
(Agler 343-344)
Treating ‘Wx’ = x is white and ‘Mx’ = x is a moose, line 1 reads, Something is a white moose. From this proposition, Something is white, and something is a moose is inferred.
(Agler 344)
Agler will now examine some incorrect uses of the existential elimination that are invalid because they violate one of the restrictions. The following example will break the first restriction.
| 1 | Ea→(∀x)Px | P |
| 2 | (∃x)Ex | P |
| 3 | | Ea | A |
| 4 | | (∀x)(Px) | 1,3→E |
| 5 | (∀x)Px | 2,3–4∃E—NO! |
(Agler 344)
Note that 'a' occurs in the first premise. There is nothing wrong with us assuming it in line 3. But there is something wrong in using existential elimination to extract (∀x)Px from the subproof, because (∀x)Px was made by substituting for the 'a' which occurred in the premise (Agler 344). Agler illustrates why this is invalid by using English sentences.
| 1 | If 3 is even, then every number is prime. | P |
| 2 | Some number is even. | P |
| 3 | . | |
| 4 | . | |
| 5 | Therefore, every number is prime. | 2,3–4 ∃E—NO! |
(Agler 344-345)
Agler now gives an example that does not violate this restriction.
| 1 | (∃x)(Pxx∧Qxx) | P |
| 2 | | Paa∧Qaa | A/∃E |
| 3 | | Qaa | 2∧E |
| 4 | | (∃x)Qxx | 3∃I |
| 5 | (∃x)Qxx | 1,2–4∃E |
(Agler 345)
But in the following case, restriction 1 is violated.
| 1 | (∀x)(∃y)Txy | P |
| 2 | (∃y)Tay | 1∀I |
| 3 | | Taa | A/∃E |
| 4 | | (∃x)Txx | 3∃I |
| 5 | (∃x)Txx | 2,3–4∃E—NO! |
(Agler 345)
Again, the problem here is that the variable in line 5 is substituting for a constant in the subproof that appeared already in the second premise.
With this in mind, Agler formulates strategic rule SQ#4(∃E):
SQ#4(∃E) Generally, when deciding upon a substitution instance ‘P(a/x)’ to assume for a use of (∃E), choose one that is foreign to the proof.[The second restriction, recall, is that the constant being substituted by the derived formula be not found in that derived formula itself.] Agler will now give an example of a proof that violates the second restriction.
(Agler 345)
| 1 | (∃z)(Wzz∧Mz) | P |
| 2 | | Wbb∧Mb | A/∃E |
| 3 | | Wbb | 2∧E |
| 4 | | (∃x)(Wbx) | 4∃I |
| 5 | (∃x)(Wbx) | 1,2–5∃E—NO! |
(Agler 345-346)
In line 4, we substituted x for the second constant 'b' in 'Wbb', leaving the first 'b' intact. This on its own is fine, but then we cannot make the derivation in line 5 using existential elimination, because we substituted x for 'b', but 'b' is found in the derived formula too (Agler 346). Agler further explains why this is invalid: "consider that line 1 only refers to there being at least one object z that is both ‘Wzz’ and ‘Mz.’ While we could validly infer ‘(∃x)(Wzz),’ we could never validly infer a specific object constant" (Agler 346). [I did not follow that explanation so well. Perhaps the idea is that we know that some constant holds for W, but we do not know which, so we cannot infer line 5.]
Note also that while the assumption in existential elimination is based on an existentially quantified formula, the formula that we eventually derive would be a universally quantified one, as in this example.
| 1 | (∀x)Px | P |
| 2 | (∃x)Zx | P |
| 3 | | Za | A/∃E |
| 4 | | (∀x)Px | 1R |
| 5 | (∀x)Px | 2,3–4∃E |
(Agler 346)
Agler then has us consider one final proof. [(∃y)Py→(∀y)Ry, (∃x)Px⊢(∀y)Ry. If we could obtain
(∃y)Py then we can derive (∀y)Ry. But there would not be a way it seems to directly convert (∃x)Px to (∃y)Py. However, if we assume a substitution for (∃x)P, then we can use existential introduction to get (∃y)Py. This will allow us to use conditional elimination to get the goal proposition, which we would then place into the main proof.]
| 1 | (∃y)Py→(∀y)Ry | P |
| 2 | (∃x)Px | P/(∀y)Ry |
| 3 | | Pa | A/∃E |
| 4 | | (∃y)Py | 3∃I |
| 5 | | (∀y)Ry | 1,4→E |
| 6 | (∀y)Ry | 2,3–5∃E |
(Agler 346)
Agler, David. Symbolic Logic: Syntax, Semantics, and Proof. New York: Rowman &; Littlefield, 2013.
Some changes to the book quotations may have been made, as based on: http://markdfisher.com/wp-content/uploads/2014/02/PHIL_012_ONLINE_SYLLABUS_SP14-3-1.pdf .
.
No comments:
Post a Comment