Trees and finite satisfiability: proof of a conjecture of Burgess (Q2266003)

The standard method of trees (e.g. Jeffrey) does not provide an effective method for demonstrating the finite satisfiability of an arbitrary finitely satisfiable sentence. However, that method may be modified as follows. For the rule of existential instantiation (EI), substitute the rule new EI: if \(\exists xFx\) occurs on a branch, bifurcate into \(n+1\) branches \(F(b_ 1)\), \(F(b_ 2)\),..., \(F(b_ n)\), F(a), where \(b_ 1,...,b_ n\) are the constants already occurring on that branch, and a is a constant not occurring on that branch. A branch is finished if no more rules apply to it, and open if no sentence and its negation occur on it. It can be shown that if a tree generated by a sentence A is finite, finished and open then A is finitely satisfiable. Burgess has conjectured that any finitely satisfiable sentence can be shown to be so by this method. This paper proves the conjecture by proving that if A is finitely satisfiable, then some branch on a tree generated from A by the new method is finite, finished and open. Note that in the diagram p. 195, the second Raa should be Rba.