Definability with bounded number of bound variables
type: Item
instance of: scholarly article
title: Definability with bounded number of bound variables
zbMATH Open document ID: 0711.03004
DOI: 10.1016/0890-5401(89)90055-2
author: Dexter Kozen
author: Neil Immerman
published in: Information and Computation
publication date: 1989-01-01T00:00:00Z
review text: 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.
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 03C30
Mathematics Subject Classification ID: 03B45
Mathematics Subject Classification ID: 03C13
Mathematics Subject Classification ID: 68Q55
zbMATH DE Number: 4168653
zbMATH Keywords: k-variable property
zbMATH Keywords: temporal logic
zbMATH Keywords: Ehrenfeucht-Fraissé game
zbMATH Keywords: bounded- degree trees
zbMATH Keywords: tree models
reviewed by: Jan Šefránek
MaRDI profile type: Publication
full work available at URL: 0890-5401(89)90055-2
OpenAlex ID: W2053510959
cites work: Preservation of expressive completeness in temporal models
cites work: On Moschovakis closure ordinals
cites work: An application of games to the completeness problem for formalized theories
cites work: The computational complexity of logical theories
cites work: Q3674621
cites work: Q3768883
cites work: Q5549024
cites work: Upper and lower bounds for first order expressibility
cites work: Complexity of Boolean algebras
cites work: Definability in dynamic logic
cites work: Deux ou trois choses que je sais de Ln
cites work: Q3949052
cites work: Unbounded program memory adds to the expressive power of first-order programming logic
Recommended article: Bounds and definablity over fields.
Recommended article: Definability via enumerations
Recommended article: Definability in the enumeration degrees
Recommended article: Definability and invariance
Recommended article: Q4706821
Recommended article: Provability with Finitely Many Variables
Recommended article: Q2753675
Recommended article: Definability in low simple theories
Recommended article: Q4281250
Recommended article: Definability in function spaces
description: scientific article; zbMATH DE number 4168653