# Should we not reuse constants in tableaux proofs?

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?

## 1 Answer

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.

• 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? – juan981 May 5 '14 at 16:33
• @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. – Yuval Filmus May 5 '14 at 17:50