|
|
Introduction to Logic
|
Tools for Thought
|
|
Given ∀x.∀y.(p(x,y) ⇒ q(x)), we know that ∀x.(∃y.p(x,y) ⇒ q(x)). In general, given a universally quantified implication, it is okay to drop a universal quantifier of a variable outside the implication and apply an existential quantifier of that variable to the antecedent of the implication, provided that the variable does not occur in the consequent of the implication.
|
Our proof is shown below. As usual, we start with our premise. We use Universal Elimination ti instantiate that sentence using a new placeholder. We then start a subproof with an existential sentence as assumption. We then make another assumption by instantiating the target of the existential sentence and a new placeholder. We use Universal Elimination to strip away the quantifier from our conclusion in line 2. We use Implication Introduction to produce an implication and Universal Introduction to produce a universally quantified version of the implication. We then use Existential Elimination to infer q([c]). Finally, we generalize using Universal Introduction.
1. | ∀x.∀y.(p(x,y) ⇒ q(x)) | Premise |
2. | ∀y.(p([c],y) ⇒ q([c])) | Universal Elimination: 1 |
3. | ∃y.p([c],y) | Assumption |
4. | | Assumption |
5. | | Universal Elimination: 2 |
6. | | Implication Elimination: 5, 4 |
7. | p([c],[d] ⇒ q([c]) | Implication Introduction: 4, 6 |
8. | ∀y.(p([c],y) ⇒ q([c])) | Universal Introduction: 7 |
9. | q([c]) | Existential Elimination: 3, 8 |
10. | ∃y.p([c],y) ⇒ q([c]) | Implication Introduction: 3, 9 |
11. | ∀x.(∃y.p(x,y) ⇒ q(x)) | Universal Introduction: 10 |
|
The relationship holds the other way around as well. Given ∀x.(∃y.p(x,y) ⇒ q(x)), we know that ∀x.∀y.(p(x,y) ⇒ q(x)). We can convert an existential quantifier in the antecedent of an implication into a universal quantifier outside the implication.
|
Our proof is shown below. Once again, we start with our premise. We create a new placeholder and use Universal Elimination to strip away the quantifier in the premise to expose the implication. We start a subproof by making an assumption. We make an assumption using another new placeholder. We turn the assumption into an existential sentence to match the antecedent of the premise in line 2. Then, we apply Implication Elimination to derive q([c]). We use Implication Introduction to create an implication. Finally, we generalize using two applications of Universal Introduction.
1. |
∀x.(∃y.p(x,y) ⇒ q(x)) |
Premise |
2. |
∃y.p([c],y) ⇒ q([c]) |
Universal Elimination: 1 |
3. |
p([c],[d]) |
Assumption |
4. |
∃y.p([c],y) |
Existential Introduction: 3 |
5. |
q([c]) |
Implication Elimination: 2, 4 |
6. |
p([c],[d]) ⇒ q([c]) |
Implication Introduction: 3, 5 |
7. |
∀y.(p([c],y) ⇒ q([c])) |
Universal Introduction: 6 |
8. |
∀x.∀y.(p(x,y) ⇒ q(x)) |
Universal Introduction: 7 |
|
Use the arrow keys to navigate.
Press the escape key to toggle all / one.
|
|