I am a beginner in logic, which I am learning on my own. I am aware of the fact that a quantifier tableau with open branches doesn’t always show the formula under consideration is falsified- unless there are no more rules to apply.
Consider the following statement: 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.
If we let $Ex:$ $x$ is a student, $Gx:$ $x$ is good, and $Lxy:$ $x$ solves problem $y$ the statement is translated into the formula:
$$\bigg[\Big(\forall x\big((\forall y Lxy)\Rightarrow(Ex\wedge Gx)\big)\Big)\wedge\Big(\forall x\big((\forall y Lxy)\Rightarrow\neg Ex\big)\Big)\bigg]\Rightarrow\Big[\exists y\big(\forall x (Lxy\Rightarrow \neg Ex)\big)\Big]$$
Now, intuitively I can see that we can falsify the formula if we have two students, two problems, and one student solves problem 1 but not 2 while the other solves problem 2 but not 1.
Below is my attempt at a using a tableau to obtain the desired falsification. \begin{matrix} & & & T\;\forall x((\forall y Lxy)\Rightarrow(Ex\wedge Gx))& \\ & & & T\;\forall x((\forall y Lxy)\Rightarrow\neg Ex)& \\ & & & F\;\exists y(\forall x (Lxy\Rightarrow \neg Ex))\;(1)& \\ & & & F\;\forall x(Lxp\Rightarrow\neg Ex)\;(2)& \\ & & & F\;Lap\Rightarrow\neg Ea& \\ & & & \boldsymbol{T\;Lap}& \\ & & & F\;\neg Ea& \\ & & & \boldsymbol{T\; Ea}& \\ & & & T\;(\forall y Lay)\Rightarrow\neg Ea& \\ & F\;\forall y Lay& & & T\;\neg Ea\\ & \boldsymbol{F\; Laq}\; (3)& & & F\;Ea\\ & F\;\forall x(Lxq\Rightarrow\neg Ex)\; (4)& & & \rm{\bf{X}}\\ & F\;Lbq\Rightarrow\neg Eb\; (5)& & & \\ & \boldsymbol{T\; Lbq}& & &\\ & F\;\neg Eb& & &\\ & \boldsymbol{T\; Eb}& & &\\ & T\;(\forall y Lby)\Rightarrow\neg Eb& & &\\ F\;\forall y Lby& & T\;\neg Eb& & \\ \boldsymbol{F\; Lbp}\; (6)& & F\; Eb& &\\ & & \rm{\bf{X}}& & & &\\ \end{matrix}
(2) is an instantiation of (1) for $y=p$, and because we do not want the branch to close we need a new problem $q\neq p$ in (3). (4) is an instantiation of (1) for $y=q$, and we need a new student $b\neq a$ in (5) so that the branch does not close. Finally, in (6), in order for the branch not to close we need a new problem $r\neq q$. But if we assume that there are exactly two students and exactly two problems, then $r$ must be $p$.
Hence, the open branch provides the desired falsification of the formula (in bold): Both $a$ and $b$ are students. Student $a$ solves problem $p$ and does not solve problem $q$, while student $b$ solves problem $q$ but not problem $p$.
Am I correctly using the Tableau method in order to produce a falsification of the formula? What concerns me is that although I can read off a valuation falsifying the formula, there are still rules to be applied. On the other hand, applying them does not affect the fact that I already can read that valuation.
Hence, if one judiciously constructs a tableau so that a valuation falsifying the formula under consideration can be read from an open branch, does it matter if there are still rules to apply? I suspect not, since if the valuation which can be read falsifies the formula under consideration that means the rules left to apply have no impact on the truth/falsity of the formula.
Edit: I just noticed that this question is related to the same statement, but it does not answer my question.