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.
- $P(t)$ --assumed
- $P(t) \rightarrow Q(t)$ -- universal elimination from the first premise
- $Q(t)$-- modus ponens 1,2
Now I want to make use of the second premise:
- $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?
- $Q(w) \rightarrow R(y)$ -- assumed
- $R(y)$ -- modus ponens 3, 4(can I do this?)
- $R(y)$ -- existential elimination (second premise, 4, 5)
- $P(t) \rightarrow R(y)$ -- implication introduction
- 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?