Deduction by Daniel Bonevac Chapter 7 Quantified Natural Deduction
Quantified Natural Deduction As with truth trees, natural deduction in Q depends on the addition of some new rules to handle the quantifiers. They are: Existential Introduction Existential Exploitation Universal Exploitation Universal Proof
Existential Introduction I Existential introduction is an unrestricted rule that permits one to move from any predicate logic formula containing a constant to that same formula, now bound by an existential quantifier and with a constant substituted for all occurrences of the corresponding variable. Examples Fa xfbx xfx Fb xfx y xfyx y( xfx Fy) The justification simply cites the line number on which the original formula occurs and I.
Existential Exploitation E Existential exploitation is a restricted rule that permits one to move from an existentially quantified formula to one in which the quantifier has been removed and aconstant has been substituted for the variable bound by the existential quantifier, provided that the constant has not already occurred anywhere in the proof. Examples xfx y xfyx y( xgxa Fy) Fa xfbx xgxa Fb In each case, the introduced constant must have occurred nowhere else in the proof. The justification cites the line number on which the original formula occurs and E.
Example 1 Here is an example of a bad proof that involves a misuse of E. 1. Fa A 2. Fa xgx A 3. Show: x(fx & Gx) 4. xgx E, 1,2 5. Ga E 4 6. Fa & Ga &E, 1,5 7. x(fx & Gx) I, 6 The mistake here occurs on line 5. The constant a had already occurred. I is properly executed. This derivation can not be performed. It is not a valid inference.
Universal exploitation E Universal exploitation is an unrestricted rule that permits one to move from a universally quantified formula to one in which the quantifier has been removed and a constant has been substituted for the variable bound by the quantifier. Examples xfx y xfyx y(fy Gb) Fa xfbx Fb Gb You will note that in the third example we exploited to the constant b. This is not an option with E. Again, the justification cites the line number on which the original formula occurs and E.
Example 2 Here is an example involving proper use of all three rules. 1. x(fx yfxy) A 2. zfz A 3. Show: x yfxy 4. Fa E, 2 5. Fa yfay E, 1 6. y Fay E 4,5 7. x yfxy I, 6
Universal Proof In this system of natural deduction, there is no such thing as a rule of universal introduction. To accomplish the same goal we introduce the rule of universal proof. The rule of universal proof says that in order to prove a universally quantified statement, you simply prove an instantiated form of that statement. This works only provided that the constants used are new to the proof. Examples: Show xfx Show x(fx v ygya) Show Fa Show (Fb v ygya) Notice that in the second example, the second show line required the use of the constant b because a is already in the proof. Remember, as with existential exploitation, this restriction applies to the entire proof, not just the line being used.
Quantifier Negation Rules QN Quantified natural deduction is greatly aided by the following derivable rules known collectively as QN, for quantifier negation. vav vav v Av v Av These rules are directly analogous to & and v. Some of the proofs of these rules are tricky, but their intuitive justification is easy. When we negate a universally quantified statement like All dogs bark we are saying that there is at least one dog that doesn t bark. Similarly, when we negate an existentially quantified statement like Some dogs bark we are saying that every dog is such that it does not bark. Note that the double lines indicate that these formulas are equivalent. Hence, they can be substituted one for the other.
Example 3 Here is an example in which universal proof and quantifier negation is properly used. 1. x(fx & Gx) A 2. Show: x (Fx Gx) 3. Show: Fa Ga 4 Fa ACP 5. x (Fx & Gx) QN, 1 6. (Fa & Ga) E, 5 7. Fa v Ga &, 6 8. Ga ve*, DN 4,7 9. Ga,8
Strategies As with truth trees, natural deduction proofs are best pursued by exploiting the restricted rules first and using the power of the unrestricted rules. This means: When doing a universal proof, set it up before exploiting any other unrestricted rules. Exploit existentially quantified formulas before exploiting universally quantified ones. Use quantifier negation rules early in order to identify hidden existentially quantified formulas. Examine the existing formulas carefully to determine when it will be useful to use E to create a formula with specific constant. Remember that, unlike the truth tree rules, there is never a time when you are prevented from deploying a rule on a formula multiple times. You just must do so in accord with the restrictions when they exist.