How to define new constants in Tableaux Method of predicate logic

Question

As you all know, in predicate logic when using Tableaux Method the quantifiers must be removed and their variables must be replaced with constants inside the relations and functions. The problem is I don't know how this process must be done. I've read many documentations (like this or this one and lots of other files and web pages) but I'm still unable to solve such problems and I don't know how to assign constants. Here is a few questions in my mind:

• What is the difference between $\forall$ and $\exists$ when introducing new constant?

• Is it true to define the same constant for different variables? as an example replacing $\forall x,y R(x,y)$ with $R(a,a)$ is right or it must be $R(a,b)$?

• Under what conditions we are allowed to use an already used (defined) constant for a variable of a quantifier (I mean the constant is used in the node ancestor)?

• What restrictions must be regarded when introducing constants in different branches?

As an example $\exists y \exists x \forall z (C(x,y,z) \rightarrow \neg C(x,x,x))$ is inconsistent but I failed to prove it, it is the way I tried:

$\exists y \exists x \forall z (C(x,y,z) \rightarrow \neg C(x,x,x))$

$\exists y \exists x \forall z (\neg C(x,y,z) \lor \neg C(x,x,x))$

$\exists y \exists x (\neg C(x,y,\overbrace {a} ^ {Constant}) \lor \neg C(x,x,x))$

$\exists y (\neg C(b,y,a) \lor \neg C(b,b,b))$

$(\neg C(b,d,a) \lor \neg C(b,b,b))$

and it is not a contradiction while I'm sure this formula is inconsistent.

As another example this set of formula is consistent but I don't know how to assign constants to variables of quantifiers, I would be appreciated if you help me with this set.

$\{ \forall x \exists y B(x,y) \rightarrow \neg \exists y \forall x B(x,y) , \exists B(x,x) \}$

I only tried this:

$\exists B(x,x)$

$\forall x \exists y B(x,y) \rightarrow \neg \exists y \forall x B(x,y)$

$\neg \forall x \exists y B(x,y) \vee \neg \exists y \forall x B(x,y)$

$B(a,a)$

but at this point I don't know if it is true to use $a$ in place if $x$ in $\neg \forall x \exists y B(x,y) \vee \neg \exists y \forall x B(x,y)$ or not (because $a$ is used in place of $\exists$ quantifier in another formula)?

Thank you

Answer 1

The existential quantifier allows us to introduce witnesses - dummy constants, if you will. For instance, from $\exists xPx$, you can write $Pa$, but only if $a$ doesn't already exists.

New existential quantifiers will introduce new (different) witnesses each time. Universal quantifiers use these constants and witnesses. So, if one of your premise is $Qb$, then you know that $b$ is part of your domain. So when you see $\forall y Ry$, you know that this must be true for $b$ and you can write $Rb$. Of course, you can also write your universal statements with the witnesses introduced by existential quantifiers.

To sum up: existential quantifiers are used to create NEW constants, universal quantifiers can only be applied to ALREADY DECLARED constants (either by premises or existential quantifiers).

Answer 2

The formula :

$∃y∃x∀z(C(x,y,z) → ¬C(x,x,x))$

is satisfiable; consider :

1) $∃y∃x∀z(C(x,y,z) → ¬C(x,x,x))$

2) $∃x∀z(C(x,a,z) → ¬C(x,x,x))$ --- by rule for $\exists$ : $a$ new

3) $∀z(C(b,a,z) \to \lnot C(b,b,b))$ --- by rule for $\exists$ : $b$ new

4) $C(b,a,a) \to \lnot C(b,b,b)$ --- from 3) by rule for $\forall$ : with $a$

5) $C(b,a,b) \to \lnot C(b,b,b)$ --- from 3) by rule for $\forall$ : with $b$

We can stop here, because we can see that the tree will finish with open paths.

To show that the formula in 1) is satisfiable it is enough to define a model $\mathfrak A$ with domain $A = \{ a,b \}$ such that the ternary relation interpreting the predicate symbol $C$ does not hold neither for $(b,a,a)$ nor for $(b,a,b)$, i.e. $(b,a,a), (b,a,b) \notin C^\mathfrak A$.

In this way, we see that : $\forall z (C(b,a,z) \to \lnot C(b,b,b))$ is satisfied, because the antecedent of the conditional is false for any possible value for $z$.

Thus, also the formula $∃y∃x∀z(C(x,y,z) → ¬C(x,x,x))$ is satisfiable.

---

---

For the second example, you have to apply the method to :

1) $∀x∃yB(x,y) → ¬∃y∀xB(x,y)$

2) $∃B(x,x)$

We start from 2) with the rule for $\exists$ :

3) $B(a,a)$ --- $a$ new

and then we produce two branches; the left one with :

$4_L$) $\lnot ∀x∃yB(x,y)$

and the right one with :

$4_R$) $¬∃y∀xB(x,y)$

Now consider the left one and apply the rule for $\lnot ∀$ :

$5_L$) $\lnot ∃yB(b,y)$ --- $b$ new

$6_L$) $\lnot B(b,a)$ --- rule for $\lnot ∃$

$7_L$) $\lnot B(b,b)$ --- rule for $\lnot ∃$.

We have found the model $\mathfrak A$ satisfying 1) and 2), with domain $A = \{ a,b \}$ such that $(a,a) \in B^\mathfrak A$ and $(b,a), (b,b) \notin B^\mathfrak A$.

We have that : $(a,a) \in B^\mathfrak A$ will satisfy $\exists xB(x,x)$ while $\exists yB(b,y)$ is not satisfied, and thus also $\forall x \exists yB(x,y)$ is not.

Thus, the antecedent of the conditional 1) is false and the conditional is true.

---

---

The rules for the management of quantifiers are quite simple; see :

• Raymond Smullyan, First-Order Logic (1968), page 54.

The so-called "Rules C" for $\forall$ and $\lnot \exists$ must be instantiated with a term whatever, while the so-called "Rules D" for $\exists$ and $\lnot \forall$ need a new term.

The motivation is : "Rules C" operate on $\forall$-prefixed formulae (because $\lnot \exists$ is $\forall \lnot$) : thus, they amount to the valid inference : if $\forall x \varphi$, then $\varphi^x_t$.

"Rules D" instead, operate on $\exists$-prefixed formulae; thus, when we derive $\varphi$ from $\exists x \varphi$, we are not allowed to re-use an already existing (in the proof) term, because the new assumption (expressed by $\exists \varphi$) does not imply that the object satisfying $\varphi$ was one of those already "mentioned" into the proof.