1
$\begingroup$

Universal elimination and existential introduction are easy. But when it comes to existential elimination and universal introduction, there are some restrictions which I don't fully understand.

Let me give an example:

Show that if ∀x(P(x) → Q(x)) and ∃xQ(x) → R(y) are true, then ∀x(P(x) → R(y)) is true by natural deduction.

  1. $P(t)$ --assumed
  2. $P(t) \rightarrow Q(t)$ -- universal elimination from the first premise
  3. $Q(t)$-- modus ponens 1,2

Now I want to make use of the second premise:

  1. $Q(t) \rightarrow R(y)$ -- assumed

I am not sure but I think I cannot do that since the constant $t$ has been used before. Should I give it another letter and proceed like this?

  1. $Q(w) \rightarrow R(y)$ -- assumed
  2. $R(y)$ -- modus ponens 3, 4(can I do this?)
  3. $R(y)$ -- existential elimination (second premise, 4, 5)
  4. $P(t) \rightarrow R(y)$ -- implication introduction
  5. universal introduction of 7

Can somebody please explain how to go before/after the line 4 so that existential elimination and universal generalization wouldn't be a problem?

EDIT:

After thinking and thinking I have come up with this

$\\1.\forall x(P(x)\rightarrow Q(x))$ - premise

$\\2. \exists xQ(x) \rightarrow R(y)$ -premise

$\\3.\forall zP(z)$ -assumed

$\\4.Q(a)\rightarrow R(y)$ -assumed

$\\5.P(a)\rightarrow Q(a)$ -universal\ elimination from \1

$\\6. P(a)$ -universal\ elimination\ from\ 3

$\\7. Q(a)$ -modus ponens\ 5,6

$\\8. R(y) $-modus ponens \ 4,7

$\\9. R(y) $-existential \ elimination \ 2,4,8

$\\10. \forall z P(z) \rightarrow R(y)$ -implication \ introduction\ 3, 9

$\\11. P(a)$ - assumed

$\\12. P(a) \rightarrow R(y) $- universal\ elimination from\ 10

$\\13. R(y) $- modus ponens\ 11,12

$\\14. P(a) \rightarrow R(y) $-implication\ introduction\ 11, 13

$\\15. \forall x(P(x) \rightarrow R(y)) $- universal introduction from\ 14

Can anybody tell me if this contains any errors?

$\endgroup$
  • $\begingroup$ Wait... ∃xQ(x) → R(y) isn't clear. Does that mean ((∃xQ(x)) → R(y)) or does it mean (∃x(Q(x)→ R(y))? $\endgroup$ – Doug Spoonwood Oct 24 '15 at 22:06
  • 1
    $\begingroup$ @DougSpoonwood the existential quantifier only affects the first term, Q(x), not the whole compound proposition. So it is the former in your sentence. $\endgroup$ – user2694307 Oct 24 '15 at 22:08
  • 1
    $\begingroup$ The EDIT part is wrong; see at Doug's answer below. You cannot apply $\exists$-elim that way in step 9. $\endgroup$ – Mauro ALLEGRANZA Oct 25 '15 at 7:25
3
$\begingroup$

You get to Q(t) in step 3. So, just use existential introduction to infer ∃xQ(x). Then infer R(y) by modus ponens. Then us conditional introduction to get to (P(t) $\rightarrow$ R(y)).

Now, note that we have no assumptions in place, only the hypotheses which you gave which we aren't going to discharge. Neither of them contain the variable 't'. Thus, we can use universal introduction to infer the conclusion ∀x(P(x) → R(y)).

The restriction on the universal introduction rule just says that we can't replace the letter when we have that letter in some hypothesis or assumption in effect. But, we didn't have any such assumption or hypothesis with 't' in it in effect when we used the universal introduction rule above, and thus it works out as valid.

$\endgroup$
  • $\begingroup$ ecourses.uprm.edu/pluginfile.php/62781/mod_resource/content/1/… Could you look at page 3. It says Existential Instantiation (E.I.): From a premise (∃x)ϕ(x) We may conclude ϕ(w) where w is a special “restricted constant” that has not been used before in the proof, and ϕ(w) is the result of substituting w for every free occurrence of x in ϕ(x). $\endgroup$ – user2694307 Oct 24 '15 at 22:05
  • $\begingroup$ The fact that I'm reluctant to use Q(t) is that I have used t in my assumptions which was undischarged at that time, namely P(t). Isn't this something avoids writing Q(t)? $\endgroup$ – user2694307 Oct 24 '15 at 22:06
  • $\begingroup$ I didn't use existential instantiation here. Since you've clarified that ∃xQ(x) → R(y) means ((∃xQ(x)) → R(y)), it follows that if you can infer ∃xQ(x) by existential generalization, you can infer R(y) by modus ponens. Then with discharging the temporary assumption, you can use universal generalization. $\endgroup$ – Doug Spoonwood Oct 24 '15 at 22:12
  • $\begingroup$ Now I see your point, thank you so much. It doesn't even take 10 steps to show this. I'd also be glad if you commented on my "long" solution's correctness. But thank you anyway again. $\endgroup$ – user2694307 Oct 24 '15 at 22:19

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.