I am trying to understand the proof of the following using tableaux: $$ \exists x\forall y.r(x,y) \to \forall x \exists y . r(x,y) $$

This is how it works out: $$ (1) \space \exists x \forall y .r(x,y) \\ (2) \space \lnot(\forall x \exists y . r(x,y)) \\ | \\ (3) \space \forall y.r(a,y) \\ (4) \space \lnot \exists y.r(b,y) \\ (5) \space r(a,a) \\ (6) \space r(a,b) \\ (7) \lnot r(b,a) \\ (8) \lnot r(b,b) $$

I understand that (4) is derived from (2). However, shouldn't that be $$ \lnot \exists y.r(a,y) $$ reusing the constant a which was introduced by (3)? This is because we are expanding the quantifier: $$ \lnot(\forall ...) $$

Can anyone explain?


On the contrary, you never want to reuse constants. Each time you witness an existential quantifier, you should use a different constant. For example, consider the following two sentences:

  1. Some integer is even.

  2. Some integer is odd.

You wouldn't want to instantiate them with the same variable.

  • $\begingroup$ What I do not understand is that under expansion rules for first-order tableaux, I should reuse a term that is already in the branch when I encounter a $$\forall x P(x)$$ or a $$\lnot \exists x P(x)$$. Am I understanding anything wrong here? $\endgroup$ – juan981 May 5 '14 at 16:33
  • $\begingroup$ @juan981 Every time you witness an existential quantifier you need to use a new variable. When witnessing a universal quantifier you can use any expression you want. $\endgroup$ – Yuval Filmus May 5 '14 at 17:50

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.