Natural Deduction Proof with Quantifiers Proof Validation Only using natural deduction prove:
$$\frac{\forall x P(x) \\ \forall x \lnot Q(x) \lor \forall yQ(y) \\ \exists x [P(x) \rightarrow \lnot Q(x)]}{\therefore \forall x \lnot Q}$$
My solution:
$1. \space \forall x P(x) \qquad \qquad \qquad premise\\ 2. \space \forall x \lnot Q(x) \lor \forall y Q(y) \qquad premise\\ 3. \space \exists x [P(x) \rightarrow \lnot Q(x)] \qquad premise \\ \boxed{4. \space x_o \qquad \qquad \qquad \qquad arbitrary \\ \boxed{5. \space y_o \space P(y_o) \rightarrow Q(y_o) \qquad assumption \\ 6. \space \lnot Q(x_o) \ \lor \forall yQ(y) \qquad \forall-elim(2,4) \\ 7. \space \lnot Q(x_o) \lor Q(y_o) \qquad \forall-elim(2,5) \\ \boxed{8.\space y_o\space Q(y_o) \qquad\qquad assumption \\ 9.\space \lnot Q(y_o) \qquad \qquad \rightarrow-elim(5)\\ 10. \space F \qquad \qquad \lnot-elim(8-9)\\ 11. \space \lnot Q(x_o) \qquad \qquad F-elim (10)}\\ \boxed{12. \space \lnot P(x_o) \qquad \qquad assumption \\ 13. \space P(x_o) \qquad \qquad \forall-elim(1,4) \\ 14. \space F \qquad \qquad \lnot-elim(12-13) \\ 15.\space \lnot Q(x_o) \qquad \qquad F-elim(15)}\\ 16. \space \lnot Q(x_o) \qquad \qquad \lor-elim (8-11,12-15)}\\17. \space \lnot Q(x_o) \qquad \qquad \exists-elim(3,5-16)} \\ 18. \forall x\lnot Q(x_o) \qquad \qquad \forall-intro(4-17)$
From the last version I changed the domain on the variables to be seen easier.
Question 1: I think I can change the domain to the second premise because they are two different domains, right?
Question 2: Lines 12 - 15, is this valid?
Question 3: For lines 4 - 7, I said $x_o$ is arbitrary so it can cancel out the for all statement. Is it valid to do it like I did for 6 and 7?
 A: 


*¬() ∨∀() ∀−(2,4)


That line is incorrect. In order to apply $\forall E$, Universal Quantifier needs to be the main logical connective.



*¬()∨−(8−11,12−15)


To use $\lor E$, a statement whose main logical connective is a disjunction needs to appear in previous lines; I cannot see such statement there.
A possible proof could be:
$
\def\fitch#1#2{\quad\begin{array}{|l}#1\\\hline#2\end{array}}
\def\Ae#1{\qquad\mathbf{\forall\,Elim}\colon #1 \\}
\def\Ai#1{\qquad\mathbf{\forall\,Intro}\colon #1 \\}
\def\Ee#1{\qquad\mathbf{\exists\,Elim}\colon #1 \\}
\def\Ei#1{\qquad\mathbf{\exists I}\colon #1 \\}
\def\R#1{\qquad\mathbf{R}\colon #1 \\}
\def\ci#1{\qquad\mathbf{\land\,Intro}\colon #1 \\}
\def\ce#1{\qquad\mathbf{\land\,Elim}\colon #1 \\}
\def\oe#1{\qquad\mathbf{\lor\,Elim}\colon #1 \\}
\def\ii#1{\qquad\mathbf{\to Intro}\colon #1 \\}
\def\ie#1{\qquad\mathbf{\to Elim}\colon #1 \\}
\def\be#1{\qquad\mathbf{\leftrightarrow E}\colon #1 \\}
\def\bi#1{\qquad\mathbf{\leftrightarrow I}\colon #1 \\}
\def\fi#1{\qquad\mathbf{\bot\,Intro}\colon #1 \\}
\def\qi#1{\qquad\mathbf{=I}\\}
\def\qe#1{\qquad\mathbf{=E}\colon #1 \\}
\def\ne#1{\qquad\mathbf{\neg E}\colon #1 \\}
\def\ni#1{\qquad\mathbf{\neg I}\colon #1 \\}
\def\IP#1{\qquad\mathbf{IP}\colon #1 \\}
\def\X#1{\qquad\mathbf{\bot\,Elim}\colon #1 \\}
\def\DNE#1{\qquad\mathbf{DNE}\colon #1 \\}
$
$
\fitch{1.\,\forall xP(x)\\
2.\,\forall x\lnot Q(x) \lor \forall xQ(x)\\
3.\,\exists x(P(x) \to \lnot Q(x))
}{
  \fitch{4.\,[a]}{
    \fitch{5.\,\forall x \lnot Q(x)}{
     6.\,\lnot Q(a) \Ae{6}
}\\
    \fitch{7.\,\forall x Q(x)}{
     \fitch{8.\,[b]\,P(b) \to ¬Q(b)}{
       9.\,P(b) \Ae{1}
       10.\,\lnot Q(b) \ie{8,9}
       11.\,Q(b) \Ae{7}
       12.\,\bot \fi{10,11}
}\\
13.\,\bot \Ee{3,8-12}
14.\,\lnot Q(a) \X{13}
}\\
15.\,\lnot Q(a) \oe{2,5-6,7-14}
}\\
16.\,\forall x~\lnot Q(x) \Ai{4,15}
}
$
