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.

  • $\begingroup$ I'll be watching this one. I don't understand tableaux even a little. $\endgroup$ – Malice Vidrine Jan 14 '14 at 10:39
  • $\begingroup$ I don't understand what you're asking. Volunteering to ask what? $\endgroup$ – Malice Vidrine Jan 14 '14 at 11:03
  • $\begingroup$ Any attempt by me to explain the method would be taken almost directly from these notes. I believe the "tableau" of $\neg (Ax\to\forall Ax)$ is open, but I think tableaux work for closed formulae only; I'll have to revise. $\endgroup$ – Shaun Jan 14 '14 at 11:03
  • $\begingroup$ About the example $\alpha(x) \rightarrow \forall x \alpha(x)$ , the only thing I may suppose is this : if I want to test it for vaidity, I'll use its universal closure (because $\alpha(x)$ is valid iff $\forall x \alpha(x)$ is); if I want to test if for satisfiability, I'll use its existential closure (because $\alpha(x)$ is satisfiable iff $\exists x \alpha(x)$ is). Is it right ? $\endgroup$ – Mauro ALLEGRANZA Jan 14 '14 at 11:08
  • $\begingroup$ Not all semantics make $\alpha(x) \to (\forall x)\alpha(x)$ logically valid. I have no idea whether Smullyan's do; I know that, for example, Enderton's do not. $\endgroup$ – Carl Mummert Jan 14 '14 at 11:49

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}$.

  • $\begingroup$ Thanks for the reference to the definition (page 46). But I think that the method is also a proof procedure, and I don't think that (in general) a proof procedure must be restricted to closed formulae ... $\endgroup$ – Mauro ALLEGRANZA Jan 14 '14 at 11:03
  • $\begingroup$ I'm not sure to understand. Following Carl's comment, we know that $\alpha(x) \rightarrow \forall x \alpha(x)$ is not valid. So, if I run the method starting with $\lnot [\forall x(\alpha(x) \rightarrow \forall x \alpha(x) )]$ I will get: (i) $\alpha(a) \rightarrow \forall x \alpha(x)$; (ii) $\alpha(a)$; (iii) $\lnot \forall x \alpha(x)$; (iv) $\lnot \alpha(b)$. So, I've checked that the formula is satisfiable in a universe where $\alpha(a)$ holds and $\alpha(b)$ does not. So, the universal closure of $\alpha(x) \rightarrow \forall x \alpha(x)$ is not valid $\endgroup$ – Mauro ALLEGRANZA Jan 14 '14 at 13:51
  • $\begingroup$ Please note Smullyan, pag.49 : "A formula $A$ is called (first order) satisfiable if it is true in at least one interpretation in at least one universe". $\endgroup$ – Mauro ALLEGRANZA Jan 14 '14 at 14:55
  • $\begingroup$ About the example on page 56, you are right. I if use only the part : $\forall x P(x) \lor C$, I'll get a single path with : $F C$ and $F P(a)$; so the tableau is finished without closing and the formula $\lnot [\forall x P(x) \lor C ]$ is satisfiable. I.e., $\forall x P(x) \lor C$ is not valid. $\endgroup$ – Mauro ALLEGRANZA Jan 14 '14 at 15:21
  • $\begingroup$ Yes, but this does not mean that you can test satisfiability using the existential closure. A formula $\varphi$ is satisfiable iff its universal closure $\forall \varphi$ is. A formula $\varphi$ is valid iff its universal closure $\forall \varphi$ is. $\endgroup$ – Marc Jan 14 '14 at 15:26

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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.