by Corry Shores
[Search Blog Here. Index-tags are found on the bottom of the left column.]
[Logic & Semantics, Entry Directory]
[David Agler, entry directory]
[Agler’s Symbolic Logic, entry directory]
[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.2 Quantifier Negation (QN)
Brief summary:
The four underived quantifier rules for making proofs in the language of predicate logic (RL) made a derivation system called RD. To this we add the derived equivalence rule quantifier negation (QN) to make the deduction system RD+. And since it is an equivalence rule, QN can apply to quantifiers that are not main operators.
| Quantifier Negation (QN) From a negated universally quantified expression ‘¬(∀x)P,’ an existentially quantified expression ‘(∃x)¬P’ can be derived, and vice versa. Also, from a negated existentially quantified expression ‘¬(∃x)P,’ a universally quantified expression ‘(∀x)¬P’ can be inferred, and vice versa. | ¬(∀x)P ⊣ ⊢ (∃x)¬P
⊣ ⊢ (∀x)¬P | QN QN |
Summary
In the prior section 8.1, we devised a system of deduction for making proofs in the language of predicate logic (RL). That system is called RD. We will now add an equivalence rule, namely, quantifier negation (QN) so that we can complete our proofs more efficiently, and all the rules together with this new addition make RD+. The new rule will help us deal with negated quantifiers.
| Quantifier Negation (QN) From a negated universally quantified expression ‘¬(∀x)P,’ an existentially quantified expression ‘(∃x)¬P’ can be derived, and vice versa. Also, from a negated existentially quantified expression ‘¬(∃x)P,’ a universally quantified expression ‘(∀x)¬P’ can be inferred, and vice versa. | ¬(∀x)P ⊣ ⊢ (∃x)¬P
⊣ ⊢ (∀x)¬P | QN QN |
Agler gives this simple illustration.
| 1 | ¬(∀x)Px | P |
| 2 | (∃x)¬Px | 1QN |
| 3 | ¬(∀x)Px | 2QN |
(Agler 348)
He gives another example that works the same way, but now with a conjunction.
| 1 | ¬(∃z)(Wzz∧Mz) | P |
| 2 | (∀z)¬(Wzz∧Mz) | 1QN |
| 3 | ¬(∃z)(Wzz∧Mz) | 2QN |
(Agler 349)
Agler then shows how this basic procedure works when we have double negations.
| 1 | ￢(∀z)￢(Wzz→￢Mz) | P |
| 2 | (∃x)(Px∧Rx) | P |
| 3 | (∃z)￢￢(Wzz→￢Mz) | 1QN |
| 4 | (∃z)(Wzz→￢Mz) | 3DN |
| 5 | ￢￢(∃x)(Px∧Rx) | 2DN |
| 6 | ￢(∀z)￢(Wzz→￢Mz) | 3QN |
(Agler 349)
Something very important to note is that “Since quantifier negation is an equivalence rule, it can be applied to subformulas within wffs and not merely to whole propositions whose main operator is the negation” (Agler 349). Agler shows this in the following proof.
| 1 | ￢(∀z)￢(∃y)[Wzy→￢(∀x)￢My] | P |
| 2 | ￢(∀z)￢(∃y)[Wzy→(∃x)￢￢My] | 1QN |
| 3 | (∃z)￢￢(∃y)[Wzy→(∃x)￢￢My] | 2QN |
| 4 | (∃z)(∃y)[Wzy→(∃x)￢￢My] | 3DN |
| 5 | (∃z)(∃y)[Wzy→(∃x)My] | 4DN |
(Agler 349)
As we can see, in line 2 we used quantifier negation on a quantifier that is not the main operator.
Agler notes that QN is a derived rule, which means it can be proved using the other underived quantifier quantifiers rules. This means that we need to make proofs that show:
¬(∀x)P⊣ ⊢ (∃x)¬P
¬(∃x)P⊣ ⊢ (∀x)¬P
Agler will make a proof for just ¬(∀x)P⊢(∃x)¬P, and he leaves the remaining three cases for exercises.
| 1 | ￢(∀x)Px | P/(∃x)￢Px |
| 2 | | ￢(∃x)￢Px | A/contra |
| 3 | | | ￢Pa | A/contra |
| 4 | | | (∃x)￢Px | 3∃I |
| 5 | | | ￢(∃x)￢Px | 2R |
| 6 | | Pa | 3–5￢E |
| 7 | | (∀x)Px | 6∀I |
| 8 | | ￢(∀x)Px | 1R |
| 9 | (∃x)￢Px | 2–8￢E |
(Agler 349)
.
No comments:
Post a Comment