# 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:

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.

• Counterexample to the claim: Two students, two problems. Student 1 can solve problem 1 but not problem 2; Student 2 can solve problem 2 but not problem 1. The hypothesis holds. The conclusion fails. – quasi Jul 5 '17 at 23:13
• All you can claim from the premises is that for every student there's a problem (s)he can't solve: $\forall x(Sx \Rightarrow \exists y (\neg Lxy))$. – Fabio Somenzi Jul 5 '17 at 23:24
• @quasi I suspected something along those lines might be the case but I hadn't thought to reduce it to the simplest example like that, that means something in the reasoning of my tableau is definitely off. – user460377 Jul 6 '17 at 15:11
• @FabioSomenzi That statement is equivalent to sentence 2 in my introduction. – user460377 Jul 6 '17 at 15:15
• Indeed it is. The alleged consequence is obtained by swapping quantifiers. One purpose of the exercise is probably to draw one's attention to the consequences of having quantifiers in the wrong order. – Fabio Somenzi Jul 6 '17 at 15:18

$$\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.
• So maybe if I understand now, I can't for example cancel $So$ with $\neg Sa$ because $So$ is actually $Sa, Sb, Sc,...$ and so choosing any of $Sb, Sc,...$ would be satisfactory? – user460377 Jul 6 '17 at 15:19
• I'd say that $o$ may or may not be $a$. It depends on the interpretations of $a$ and $o$. The conclusion is that $So$ does not contradict $\neg Sa$. – Fabio Somenzi Jul 6 '17 at 15:24