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.