Semantic Tableaux in First-Order logic

Question

I have the following and I know for a fact that it does not end. I use all my rules and I don't have the same method at all.

∀x∃yQ(x,y)→∃xQ(x,x):F  
           ↓
∀x∃y Q(x,y):T, ∃xQ(x,x):F  
           ↓  
      Q(c1,c1):F  
           ↓  
     ∃y Q(c1,y):T  
           ↓
       Q(c1,c2):T
          ↓
       Q(c2,c2):F
          ↓
       Q(c2,c3):T **
          ...

Where I place the ** i am not sure because as far as I understand ∃y:T is already used, why can I use it again if the rules state that i can only be used once on a branch on a formula.

please help.

Answer 1

We have the following formulas: let $\phi:=$"$\forall x\exists y.Q(x,y)$", this supposed to be true, and let $\psi:=$"$\exists x.Q(x,x)$", this is supposed to be false, that is, $\lnot\psi\equiv$"$\forall x.\lnot Q(x,x)$" to be true.

So, (thinking in a model where $Q$ is interpreted by a concrete binary relation, but formally working on syntactics level), if we start out from any constant symbol $c_1$, by $\lnot\psi$ we must have $Q(c_1,c_1):{\tt F}$, and because of $\phi$ there must exist an element (in any model that satisfies $\lnot(\phi\to\psi)$) $y$ such that $Q(c_1,y):{\tt T}$. We can thus introduce another constant symbol $c_2$ for $y$, together with the assumption $Q(c_1,c_2):{\tt T}$.

And the story goes on. Because of $\lnot\psi$, we must have $Q(c_2,c_2):{\tt F}$, and because of $\phi$ there must exist an $y$ such that $Q(c_2,y):{\tt T}$, we can introduce a next constant symbol $c_3$ for such an $y$, and so on...