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)$


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


2 Answers 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 :

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.

  • $\begingroup$ Thanks you very much for your comprehensive comment. So far I found out $\exists$ quantifier must create new constant in every occurrence of the quantifier, for example $\exists x \forall y R(x,y) \vee \exists P(x)$ doesn't imply $\forall y R(a,y) \vee P(a)$ it must be $\forall y R(a,y) \vee P(b)$ is it true? and the $\forall$ quantifier is free to use any constant that so far has been created via the $\exists$ quantifier, yes? and a tree is consistent if there is at least one consistent path. $\endgroup$
    – M a m a D
    Feb 27, 2015 at 14:13
  • 1
    $\begingroup$ @Drupalist - To be precise, the main conncetive is $\lor$; thus, you have first to "unpack" it generating two paths, because the rule for $\lor$ branches : the left one with ∃x∀yR(x,y) and the right one with ∃P(x). Then you must go on with the two branches : on the left with ∀yR(a,y) and on the right with P(b). Then, in order to be sure to find the "correct" silution, you have to instantiate $\forall$ with all the new constants introduced; in this case one time with a and a second with b. $\endgroup$ Feb 27, 2015 at 14:21
  • 1
    $\begingroup$ @Drupalist - we are "looping" on the same point ... In general, with a formula like $\exists xQ(x) \land \exists xP(x)$ we are not licensed to assume that the objects satisfying respectively $Q$ and $P$ are the same objcet. This is the reason way the rule need a new constant... $\endgroup$ Feb 27, 2015 at 14:50
  • 1
    $\begingroup$ @Drupalist As Mauro pointed out, it's a question of scope of the quantifiers. Try to think about the difference between $\exists x(Px\land Rx)$ and $(\exists xPx)\land(\exists xRx)$. In the first case, some object has both properties $P$ and $R$. In the second case, some object has property $P$ and some other object has property $R$. These statements are not equivalent. Although the second statement is perfectly valid, you could write it as $(\exists xPx)\land(\exists yRy)$ to make things easier. $\endgroup$
    – Demosthene
    Mar 1, 2015 at 13:58
  • 1
    $\begingroup$ @Demosthene So quantifiers are some thing like local variables in programming, every local variable has its own value in its scope and it is independent of its occurrences any where else. Thank you $\endgroup$
    – M a m a D
    Mar 1, 2015 at 14:04

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).

  • $\begingroup$ Is there any restriction on predicates? as an example if in $\exists P(x)$ we write $P(a)$ is it true to deduce $R(a)$ from $\forall y R(y)$? I mean a witness for $P$ is used in $R$. $\endgroup$
    – M a m a D
    Mar 1, 2015 at 13:34
  • 1
    $\begingroup$ @Drupalist You could absolutely do that. The idea is that, if you have a certain number of existential statements, you don't know whether or not they might refer to the same elements, so you need to introduce new constants each time. However, universal statements are just that - universal. So if something is $P$, and everything is $R$, necessarily that something which is $P$ must also be $R$. $\endgroup$
    – Demosthene
    Mar 1, 2015 at 13:51

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .