Skip to main content


eCommons@Cornell >
College of Engineering >
Computer Science >
Computer Science Technical Reports >

Please use this identifier to cite or link to this item:
Title: Definability with Bounded Number of Bound Variables
Authors: Immerman, Neil
Kozen, Dexter
Keywords: computer science
technical report
Issue Date: Mar-1987
Publisher: Cornell University
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-theoretic 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.
Appears in Collections:Computer Science Technical Reports

Files in This Item:

File Description SizeFormat
87-818.pdf1.53 MBAdobe PDFView/Open
87-818.ps273.24 kBPostscriptView/Open

Refworks Export

Items in eCommons are protected by copyright, with all rights reserved, unless otherwise indicated.


© 2014 Cornell University Library Contact Us