Standard method of solution to predicate logic word problem with tableaux method

Question

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:

1. $\forall x (\forall y Lxy \Rightarrow (Gx \land Sx))$
2. $\neg\exists x(Sx\land\forall yLxy)$
3. $\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:

1. $\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)))$
2. $(\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))$
3. $\forall x (\forall y Lxy \Rightarrow (Gx \land Sx))\\\neg\exists x(Sx\land\forall yLxy)\\\neg\forall x(Sx \Rightarrow\neg Lxo)$
4. $\forall y Loy \Rightarrow (Go \land So)\\\neg(So\land\forall yLoy)\\\neg(Sa \Rightarrow\neg Lao)$
5. $Sa\\\neg\neg Lao\\a)\space\neg\forall yLoy\\b)\space Go\land So$
6. $a)\space\neg Lob\\b)\space Go\\b) \space So\\b)\space 1)\space\neg So\\b)\space 2)\space\neg\forall yLoy$
7. $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.

Answer 1

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.