Definability with bounded number of bound variables (Q922523)

A model-theoretic method for establishing the k-variable property is given in the paper. To study the k-variable property is important from the temporal logic point of view. A first-order theory satisfies the k- variable property if every formula is, under the theory, equivalent to a formula with at most k bound variables. The method used in the paper to establish the k-variable property is based on a variant of the Ehrenfeucht-Fraissé game. Results in the literature for linear orders are unified and simplified by the method. Some new k-variable properties for various theories of bounded-degree trees are established. These results imply the existence of a finite basis for the first-order expressible temporal connectives over tree models of bounded degree.