A question about tableau method for first-order logic

Question

I have a doubt about tableau method for f-o logic.

In Smullyan's book (First-Order Logic, 1968, Dover reprint) the method is defined (pag.53) for formulae but - if I'm not wrong - all examples that we can find in the book are made using sentences (i.e. closed formulae).

In Simpson's Lectures notes (2013), pag.31, the method is stated for sentences.

Is the restriction to closed formula really necessary ?

If not, how I can treat a case like :

$\alpha(x) \rightarrow \forall x \alpha(x)$ ?

Added after the comments

My answer is the following :

due to the fact that an open formula $\alpha$ is valid iff its universal closure $\forall \alpha$ is

we can use the tableaux method in this way :

check for validity, starting with $\lnot \forall \alpha$ : if it closes, then $\alpha$ is valid; if there is an open path, then $\lnot \forall \alpha$ is satisfiable. So also $\lnot \alpha$ is (because $\alpha$ is not valid).

See http://en.wikipedia.org/wiki/Method_of_analytic_tableaux :

The set of formulae to check for validity is here supposed to contain no free variables; this is not a limitation as free variables are implicitly universally quantified, so universal quantifiers over these variables can be added, resulting in a formula with no free variables.

Now, if we apply the method to :

$\alpha(x) \rightarrow \forall x \alpha(x)$

and checking it for validity ( i.e.starting with $\lnot \forall x [\alpha(x) \rightarrow \forall x \alpha(x)]$ ), the tableau will end with $\alpha(a)$ and $\lnot \alpha(b)$. So, we can say that we have checked (what we already know) that the above formula is not valid.

Answer 1

With formula Smullyan means closed formula as you can see on page 46.

Using tableau method you want to know whether a formula is true or false. But a not closed formula is neither true nor false. Now, looking at your formula $\alpha(x) \rightarrow \forall x \alpha(x)$. It is unclear what to make of this formula. Of course, you can interpret this formula as the universally closed sentence $\forall x (\alpha(x) \rightarrow \forall x \alpha(x))$ which can be either true or false.

Edit Sorry for my first confusing note. Of course, you are right that many proof systems also works with formulas. I think, I just mixed up some notions. Nevertheless, I checked the Smullyan's rules again and they work for open formulas. On page 56, he also has an exercise using open formulas, e.g., $(\forall x)(Px \vee C) = (\forall x)Px \vee C)$ where $C$ is a formula where $x$ does not occur free in it.

Your question for $\alpha(x) \rightarrow \forall x \alpha(x)$ works straightforward, since $(\forall x)(\varphi(x) \rightarrow \psi(x)) \implies (\forall x)\varphi(x) \rightarrow (\forall x)\psi(x)$.

However, if you want test satisfiability of $\alpha(x) \rightarrow \forall x \alpha(x)$ you can not use the existential closure of this formula, since this means that in every structure there is an $x$ such that $\alpha(x) \rightarrow \forall x \alpha(x)$ and not that there is a structure $\mathcal{M}$ such that $\forall x(\alpha(x) \rightarrow \forall x\alpha(x))$ holds in $\mathcal{M}$.

Answer 2

As pointed at by Marc, "with formula Smullyan means closed formula as you can see on page 46".

Sentences with parameters are allowed (page 50) where parameters acts as constants.

So, we can say that the tableaux method does not apply to a formula like $P(x) \rightarrow \forall x P(x)$.

But we can apply it to a sentence with parameters like :

$P(a) \rightarrow \forall x P(x)$.

In this case we have the tableau :

F $[ P(a) \rightarrow \forall x P(x) ]$

T $P(a)$

F $\forall x P(x)$

F $P(b)$ [with $b$ new].

So, the tableau does not close and the formula $\lnot ( P(a) \rightarrow \forall x P(x) )$ is satisfiable in a domain $U = \{ a, b \}$ where, if $P^U$ is the interpretation of the predicate $P$, we have that $a \in P^U$ and $b \notin P^U$.

This means that the formula $P(a) \rightarrow \forall x P(x)$ is not valid, because we have found a domain $U$ and an interpretation $I$ of the predicate $P$ such that the formula is not true under $I$ [see page 50].

This is consistent with the fact that $A(x)$ is valid iff $\forall x A(x)$ is [see Exercise on page 51].

In fact, we can start the tableau with :

F $[ \forall x ( P(x) \rightarrow \forall x P(x) ) ]$

and applying Rule D [page 54] we get :

F $[ P(a) \rightarrow \forall x P(x) ]$

From now on, the tableau will be the same as before.

In the end, we can say that the restriction to sentences with parameters is not a real restriction.

I think that we can remove it using formulae with free variables, taking into account that the semantics used by Smullyan is basically the same as Shoenfield (1967).

Shoenfield [page 19] says that :

If $A$ is a formula of $L$ [a f-o language], an $\mathcal{A}$-instance of $A$ is a closed formula of the form $A[i_1, . . , i_n]$ in $L(\mathcal{A})$. A formula $A$ of $L$ is valid in $\mathcal{A}$ if $\mathcal{A}(A') = T$ for every $\mathcal{A}$-instance $A'$ of $A$" [where "we use $i$ and $j$ as syntactical variables which vary through names"].

Starting with an open formula $P(x) \rightarrow \forall x P(x)$, we can apply the tableaux method to its instance $P(a) \rightarrow \forall x P(x)$, and we have the same result as before.