Standard method of solution to predicate logic word problem with tableaux method Given problem (from a Penn State PDF on logic):
"Translate the following argument into the predicate calculus, and use appropriate methods to establish its validity or invalidity.
Anyone who can solve all logic problems is a good student. No student can solve every logic problem. Therefore, there are logic problems that no student can solve."
Is there a standard approach to solving problems like this? My approach was to define:


*

*Sx: x is a student

*Gx: x is good

*Lxy: x can solve logic problem y
Then the sentences can be translated as:


*

*$\forall x (\forall y Lxy \Rightarrow (Gx \land Sx))$

*$\neg\exists x(Sx\land\forall yLxy)$

*$\therefore\exists y\forall x(Sx \Rightarrow\neg Lxy)$


The full statement then is:
$$
((\forall x (\forall y Lxy \Rightarrow (Gx \land Sx)))\land(\neg\exists x(Sx\land\forall yLxy)))\Rightarrow(\exists y\forall x(Sx \Rightarrow\neg Lxy))
$$
The first question is whether or not this is an acceptable logic-form of the sentence and whether there is a more standard/generally 'better' statement (such as excluding Gx, which is superfluous but necessary to state the sentence in its original form).
My Tableaux Method proof of logical validity was as follows:


*

*$\neg(((\forall x (\forall y Lxy \Rightarrow (Gx \land Sx)))\land(\neg\exists x(Sx\land\forall yLxy)))\Rightarrow(\exists y\forall x(Sx \Rightarrow\neg Lxy)))$

*$(\forall x (\forall y Lxy \Rightarrow (Gx \land Sx)))\land(\neg\exists x(Sx\land\forall yLxy))\\\neg(\exists y\forall x(Sx \Rightarrow\neg Lxy))$

*$\forall x (\forall y Lxy \Rightarrow (Gx \land Sx))\\\neg\exists x(Sx\land\forall yLxy)\\\neg\forall x(Sx \Rightarrow\neg Lxo)$

*$\forall y Loy \Rightarrow (Go \land So)\\\neg(So\land\forall yLoy)\\\neg(Sa \Rightarrow\neg Lao)$

*$Sa\\\neg\neg Lao\\a)\space\neg\forall yLoy\\b)\space Go\land So$

*$a)\space\neg Lob\\b)\space Go\\b) \space So\\b)\space 1)\space\neg So\\b)\space 2)\space\neg\forall yLoy$

*$b)\space 2)\space\neg Lob$


Is this valid? Can I utilise o for arbitrary variables and just change them at will to contradict with predicates with bounded 'new' variables? If so, branch "a" contradicts $\neg Lao$ at 6a with $\neg\neg Lob$ at 4, by choosing o = b and o = a, respectively. Branch "b1" contradicts $\neg So$ at 6b1 with $So$ at 6b. Branch "b2" contradicts $\neg Lob$ at 7b2 with $\neg\neg Lao$ at 4, again by making the proper substitutions.
Thus the logical validity of the initial statement is proved if, as I suspect, this is an acceptable method of both framing the problem and solving the tableau? Thanks for any help/suggestions.
 A: With some rewriting, we can put the tableau in this form:
$$\begin{gather}
\forall x(\exists y (\neg Lxy) \vee (Sx \wedge Gx)) \\
\forall x(\exists y (\neg Lxy) \vee \neg Sx) \\
\forall y(\exists x(Sx \wedge Lxy))
\end{gather}
$$
We normally first instantiate existential quantifiers, but the outermost quantifiers are all universal.  Hence we introduce a fresh constant (which you call $o$) and work on the third line (which we bring to the top):
$$\begin{gather}
\exists x(Sx \wedge Lxo) \\
\forall x(\exists y (\neg Lxy) \vee (Sx \wedge Gx)) \\
\forall x(\exists y (\neg Lxy) \vee \neg Sx)
\end{gather}
$$
At this point we have an outermost existential quantifier, so we focus on it:
$$\begin{gather}
Sa \wedge Lao \\
\exists y (\neg Lay) \vee (Sa \wedge Ga) \\
\exists z (\neg Laz) \vee \neg Sa
\end{gather}
$$
(Renaming of $y$ in the third line is not necessary, but stresses the fact that the two quantifiers are independent.)
It's clear that proper instantiation of $y$ and $z$ leads to satisfaction.  
We clearly need more than one logic problem in the domain, but nothing to the contrary is said in the problem statement.
