FOL: How to explain that your countermodel interpretation “works”?

Question

Say, for example, I have this tableau:

How would one go about explaining how the infinite countermodel,

or the finite countermodel,

actually work? In other words, how when looking through the tableau should you apply the truth values in order to prove your counter-interpretation?

Thanks for you help!

n.b. tableau and countermodels from Priest(2001).

Answer 1

Similar to your previous post…

If the tableau does not close, we can use the atomic formulas in it to define an interpretation satisfying the initial formula.

If we stop the tableau at $\lnot Sab$ we have the information needed to define an interpretation $\mathcal I$ with domain $I = \{ a,b \}$ (the ground terms used by the tableau up to that node).

In order to satisfy formula $\lnot Sab$, we need that $(a,b) \notin S^{\mathcal I}$.

This means that we may define : $S^{\mathcal I} = \{ (a,a), (b,b) \}$ to complete the interpretation $\mathcal I$.

Consider now the initial formula; its negation is $\exists x \forall y Sxy$. This formula is falsified by the above interpretation because there is no element $x$ in the domain $I$ such that $Sxy$ holds for all $y$ (i.e. for $a$ and $b$).

This means that the above interpretation satisfies the initial formula and if a formula is satisfiable, its negation is not valid.

Conclusion: having found a tableau that does not close, we have used it to manufacture a counter-model for the formula $\exists x \forall y Sxy$, and this means that the formula is not valid.