Generalizing finitemodel theory
from TUTORIAL
Published online by Cambridge University Press: 30 March 2017
Summary
Abstract. We overview work on languages for querying finite structures, where the finite structures “live” inside some infinite interpreted structure. The goal is to take the query languages that have been investigated in finite model theory —first-order logic, second-order logic, fixpoint logic, etc. — and find natural extensions of them that take into account the ambient structure. Most of our discussion will be on first-order query languages. From the point of view of model theory, this means we fix an infinite structure and look at first-order formulas with additional relational predicates that range over finite sets; thus our languages lie between first-order logic and weak second order logic. The bulk of the survey consists of characterization theorems stating what sorts of queries can be defined in these logics. Not surprisingly, the expressiveness of first-order queries is determined by the model theory of the infinite structure. When the structure has a decision procedure, one can ask how complex it is to evaluate these formulas, in terms of the size of the finite structure that is plugged in for the free relational parameters. That is, we can consider formulas in these logics as templates for standard formulas, and ask how decision procedures behave as the templates are instantiated differently. The model-theoretic perspective and the symbolic computation perspective turn out to be closely connected. We also discuss applications of the results to spatial databases and to abstract complexity.
Introduction. ClassicalFiniteModelTheory andDescriptiveComplexity Theory [25, 17] give results about the expressiveness and complexity of logics over finite relational structures. This paper surveys work generalizing finite model theory to the situation where there is some infinite interpreted structure M where the finite relations live. We want to talk about logics that can access both the finite structure and the infinite background model; what classes are definable within such a logic, and what can we say about them with respect to computability and complexity? Answering these questions requires a suitable model of definability in the presence of built-in structure, as well as a notion of complexity appropriate when one works in an abstract setting, possibly over noneffective domains. There are several candidate approaches to logics over finite models “with a background structure”, and for each of these there are multiple complexity models one could compare against.
- Type
- Chapter
- Information
- Logic Colloquium '03 , pp. 3 - 24Publisher: Cambridge University PressPrint publication year: 2006