quantifier restrictions in natural deduction

Question

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:

4. $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?

4. $Q(w) \rightarrow R(y)$ -- assumed
5. $R(y)$ -- modus ponens 3, 4(can I do this?)
6. $R(y)$ -- existential elimination (second premise, 4, 5)
7. $P(t) \rightarrow R(y)$ -- implication introduction
8. 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?

Answer 1

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.