Trees and finite satisfiability: proof of a conjecture of Burgess.
George Boolos · Notre Dame Journal of Formal Logic · 1984
The method of trees, expounded in such books as Jeffrey's [2] and Smullyan's [3], provides a sound and complete positive algorithmic test for unsatisfiability (and hence, for validity as well). 1 On occasion, the method can also be used to demonstrate finite satisfiability, i.e., truth in some model with a finite domain.Applied to the sentence 3xFx, for example, the method yields the one-branch tree: ixFx Fa , from which the argument of the usual completeness proof proves the existence of a model with a one-element domain in which the sentences 3xFx and Fa are both true.But the method does not invariably demonstrate the finite satisfiability of a finitely satisfiable sentence.VxlyRxy, for example, is true in every one-element model in which R is interpreted as the identity relation.Applied to this sentence, the method produces the infinite one-branch tree: *I am grateful to John Burgess, Hugues Leblanc, and Perry Smith for helpful correspondence.The content of the present paper was (re-)discovered by Smith soon after its main result was found.I am also grateful to R. C.