More on trees and finite satisfiability: The taming of terms (Q1098832)

This note extends a result of \textit{G. Boolos} from his ``Trees and finite satisfiability: Proof of a conjecture of Burgess'' [ibid. 25, 193-197 (1984; Zbl 0561.03004)]. Boolos showed that a new rule for the existential quantifier suggested by Burgess, together with usual tableaux rules, gives a simple method of testing for finite satisfiability of first-order sentences without function symbols. The authors point out that in a first-order language with function symbols the standard tableaux rule for the universal quantifier sometimes leads to only infinite models. The authors present a tableux rule for occurrences of function symbols after all of their arguments places have been replaced with constants by use of old rules. They prove that their new rule along with the other rules dealt with by Boolos provides a test for finite satisfiability.