In Smullyan's book First-order logic the famous method of analytic tableaux for first-order logic is described. There are four rules for the two quantifiers $\forall$ and $\exists$:
- the $δ$-rules handle $F[∀x.\psi]$ and $T[∃x.\psi]$
- the $\gamma$-rules handle $F[∃x.\psi] $ and $T[∀x.\psi]$
I want to consider a language without function symbols, with uninterpreted constants only and consider a more controlled version of the so-called liberalized versions of the rules that go as follows:
- the formulas $T[ψ ∧\phi ]$, $F[ψ ∧\phi ]$, $T[ψ \vee\phi ]$, $F[ψ \vee\phi ]$ are developed as usual and have precedence over the application of quantifier rules.
- if at a certain stage of the construction the formula $T[\forall x.\psi]$ is developed, then for every constant $c$ already appearing on the branch this formula appears into we add to the same branch the instance $T[\psi[c/x]]$, providing that the constant c has not already been used in the same (*) rule application and the formula $T[\forall x.\psi]$ remains in the same branch. Similarly for $F[\exists x.\psi]$.
- if at a certain stage of the construction the formula $T[\exists x.\psi]$ is developed, then for every constant $c$ already appearing on the branch this formula appears into, a new branch is created in which $T[\exists x.\psi]$ is replaced by $T[\psi[c/x]]$, providing that the constant c has not already been used in the same (*) rule application. Similarly for $F[\forall x.\psi]$.
- if all the branches generated by the a application of a $\delta$-rule terminate with a contradiction, then we backtrack to the point in which that rule generated them and we create a new branch in which $T[\exists x.\psi]$ is replaced by $T[\psi[b/x]]$, where $b$ is a new constant non already appeared in the branch.
- as soon as there is a branch with no contradiction and with no applicable rule (all the $\delta$ and $\gamma$ rules have been applied on each constant) the entire tableau construction terminates.
MY QUESTION: Is this method guaranteed to terminate and find a finite model for every starting formula that is finitely satisfiable? In other words is it a sound, complete and computable procedure for all finitely satisfiable first-order formulas with no function symbols?
(*) We assume that each subformula $\varphi$ of the original formula appearing in the root is labeled by a unique label that is shared by each instance of $\varphi$ in a way that we can keep track of the fact that formulas appearing later on in the tableau come from the same specific original subformula.