So the question is in the title already. I have to prove the following using first-order logic but I am failing to do so. Please someone help me understand how do I do it?
$\forall x (P(x) \lor Q(x))$ , $\forall y. \neg P(y)$ $\vdash$ $\forall x.Q(x)$
On
$$\forall x (P(x) \lor Q(x)) , \forall y. \neg P(y) \vdash \forall x.Q(x)$$
Start at the end. Keeping an eye on where you want to go will help you get there.
$\dfrac{A}{\forall x~.A[x\backslash t]}{\forall\mathsf{intro}}$ means that when given a predicate you may generalise to a universal by replacing all instances of the arbitrary free variable with a bound variable that does not occur free in the original predicate.
Your consequent is such a universal statement, so you will want this on the bottom of your proof (ie: the root of the tree).
$$\dfrac{~~\vdots\\Q(t)}{\forall x~Q(x)}{\forall\mathsf{intro}}$$
Now we know where to go, let us look at where we start.
$\dfrac{\forall x~.A}{A[t\backslash x]}{\forall\textsf{elim}}$ means that "when given a universal statement, we may infer the predicate with all instances of the bound variable replaced with a free variable."
In your premise of $\forall x~.(P(x)\lor Q(x)$ the predicate is $P(x)\lor Q(x)$ and bound variable is $x$, so the replacement of that with free variable $t$ is: $P(t)\lor Q(t)$.
In your other premise of $\forall y~.\lnot P(x)$ the predicate is $\lnot P(y)$ and bound variable is $y$, so the replacement of that with (the same) free variable $t$ is: $\lnot P(t)$.
So you will be using both of these.
$$\dfrac{~\forall x~.(P(x)\lor Q(x))~}{P(t)\vee Q(t)}{\forall\mathsf{elim}}\qquad\dfrac{\forall y~.\lnot P(y)}{\lnot P(t)}{\forall\mathsf{elim}}$$
These will occur in the undischarged leaves of your tree.
There will possibly be other leaves--which must be discharged assumptions--and the branches will need to be built between these and the root.
One of the things we may derive is a disjunction. So let us seek the rules for eliminating this.
$\dfrac{\lower{1.5ex}{A\vee B}~~\dfrac{[A]\\~~\vdots}{C}~~\dfrac{[B]\\~~\vdots}{C}}{C}{\vee\mathsf{elim}}$ means that when given a derivation of $A\vee B$, a derivation of $C$ from assumed $A$ and a derivation of $C$ from assumed $B$, then we may infer $C$ (and discharge those assumptions).
You have a derivation for $P(t)\vee Q(t)$, you wish to derive $Q(t)$, so you shall need to derive it from assumptions. Well, $Q(t)$ is trivially derived when you assume it, so that leaves deriving it from $P(t)$.
$$\dfrac{\dfrac{~\vdots~}{P(t)\vee Q(t)}\quad\dfrac{[P(t)]^1\\~~\vdots}{Q(t)}\quad\lower{1.5ex}{[Q(t)]^2}}{Q(t)}{\vee\mathsf{elim}^{1,2}}$$
But how? Wait, there is also the other premise, from which we may derive $\lnot P(t)$. So, let us take a look at the rules using negation.
$\dfrac{A~~\lnot A}{\bot}{\lnot\mathsf{elim}}$ means that when given derivations of a predicate and its negation we may infer the contradiction constant (also called falsum or bottom).
Okay, what can we do about that $\bot$ symbol?
$\dfrac{\bot}{B}{\bot\mathsf{elim}}$ means that whenever the contradiction constant is derived, then we may infer any predicate we may desire. This is also known as the principle of explosion, or ex falso quodlibet (EFQ).
We look good to go! You just need to stack it all it together.
$$\phantom{\tiny\dfrac{\dfrac{\dfrac{~\forall x~.(P(x)\lor Q(x))~}{P(t)\vee Q(t)}{\forall\mathsf{elim}}\quad\dfrac{\dfrac{\lower{1.5ex}{[P(t)]^1}\quad\dfrac{\forall y~.\lnot P(y)}{\lnot P(t)}{\forall\mathsf{elim}}}{\bot}{\lnot\mathsf{elim}}}{Q(t)}{\bot\mathsf{elim}}\quad\lower{1.5ex}{[Q(t)]^2}}{Q(t)}{\vee\mathsf{elim}^{1,2}}}{\forall x~.Q(x)}{\forall\mathsf{intro}^t}}$$
So as for the first rule of natural deduction you can only use the elimination of the universal quantifier; can you go on from there?
it is just like PL until (and not including) the last necessary rule.