Paper: Definability with Bounded Number of Bound Variables (at LICS 1987)
Abstract
A theory satisfies the k-variable property if every first-order formula is equivalent to a formula with at most k bound variables (possibly reused). Gabbay has shown that a fixed time structure satisfies the k-variable property for some k if and only if there exists a finite basis for the temporal connectives over that structure. We give a model-theretic method for establishing the k--variable property, involving a restricted Ehrenfeucht-Fraisse game in which each player has only k pebbles. We use the method to unify and simplify results in the literature for linear orders. We also establish new k-variable properties for various theories of bounded-degree trees, and in each case obtain tight upper and lower bounds on k. This gives the first finite basis theorems for branching-time models.
BibTeX
@InProceedings{ImmermanKozen-DefinabilitywithBou, author = {Neil Immerman and Dexter C. Kozen}, title = {Definability with Bounded Number of Bound Variables}, booktitle = {Proceedings of the Second Annual IEEE Symposium on Logic in Computer Science (LICS 1987)}, year = {1987}, month = {June}, pages = {236--244}, location = {Ithaca, NY, USA}, publisher = {IEEE Computer Society Press} }