Semantic tableau with variables

Question

Is it possible to build a tableaux of a formula like this? $P(X,Y) \land P(Y,X)$, $X$ and $Y$ are variables.

To close the tableaux $X$ and $Y$ must to be unified with something isn't it? But how should I choose the value I unify $X$ and $Y$ with?

Answer 1

You can build a tableau for an open formula just like one for a closed formula. An open formula is valid iff its universal closure is valid, but you can just start the tableau with the formula as-is. At the end, you will just have atomic formulas with free variables instead of constants obtained from quantifier rules, but that doesn't prevent those formulas from contradicting each other, resulting in the tableau getting closed.

As an example, consider the valid open formula $\neg(P(X,Y) \land \neg P(X,Y))$. No matter how we interpret the variables (i.o.w., which variable assignment function we choose), the formula can not possibly get false, hence it is true in all structures under all assignments, and this is just the definition of validity. A tableau confirms this:

$\begin{align} 1.\ \ & \neg \neg(P(X,Y) \land \neg P(X,Y)) & (A)\\ 2.\ \ & P(X,Y) \land \neg P(X,Y) & (\neg \neg, 1)\\ 3.\ \ & P(X,Y) & (\land, 2)\\ 4.\ \ & \neg P(X,Y) & (\land, 2)\\ & \times & (3,4) \end{align}$

As you can see, the tableau is closed. We can get a contradiction between formulas with open variables just as well. 4 has the form of the negation of 3, and this is a contradiction.

---

Now for your example, $P(X,Y) \land P(Y,X)$:

$ 1. \hspace{1.5cm} \neg(P(X,Y) \land P(Y,X)) \hspace{1.5cm} (A)\\ \hspace{1.5cm}/ \hspace{4cm} \setminus \\ 2.\ \ \neg P(X,Y) \ \ (\neg \land, 1) \hspace{1cm} 3.\ \ \neg P(Y,X) \ \ (\neg \land, 1)\\ $

This tableau ends with negated atomic formulas whose branches can't be closed, hence the formula is invalid.

A counter model for an open formula will include a counter assignment function that assigns objects to the free varibables; the remaining procedure will be the same: Construct a model that satisfies all of the atomic and none of the negated formulas in the branch. So in this case:

Counter model constructucted from the open branches (the two counter models happen to be identical in this example):
$M = \langle D, I \rangle$ with
$D = \{a,b\}\\ I(P) = \emptyset\\ v(x) = a, v(y) = b$

The interpretation of $P$ is empty, because there are no atomic formulas to satisfy in the branches. To make sense of the free variables, we assign $x$ to the object $a$, and $y$ to the object $b$.
In this model, neither $\langle v(x), v(y) \rangle = \langle a, b \rangle$ nor $\langle v(y), v(x) \rangle = \langle b, a \rangle$ are $\in I(P)$, so $M \not \models_v P(X,Y)$ and $M \not \models_v P(Y,X)$, and thereby $M \not \models_v P(X,Y) \land P(Y,X)$.
Thus, the combination $M, v$ is a counter example to the claim that for all structures $M$ and assignments $v$, $M \models_v P(X,Y) \land P(Y,X)$, that is, it is a counter model to the validity of the formula.