## Paper: Definability with Bounded Number of Bound Variables (at LICS 1987)

**Neil Immerman Dexter C. Kozen**

### 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} }