Finite Model Theory

✍ Scribed by Heinz-Dieter Ebbinghaus and Jörg Flum

• Publisher: Springer
• Year: 1999/2006
• Tongue: English
• Leaves: 373
• Edition: Second Revised and Enlarged Edition 1999
• Category: Library

✦ Synopsis

Finite model theory, the model theory of finite structures, has roots in clas­ sical model theory; however, its systematic development was strongly influ­ enced by research and questions of complexity theory and of database theory. Model theory or the theory of models, as it was first named by Tarski in 1954, may be considered as the part of the semantics of formalized languages that is concerned with the interplay between the syntactic structure of an axiom system on the one hand and (algebraic, settheoretic, . . . ) properties of its models on the other hand. As it turned out, first-order language (we mostly speak of first-order logic) became the most prominent language in this respect, the reason being that it obeys some fundamental principles such as the compactness theorem and the completeness theorem. These principles are valuable modeltheoretic tools and, at the same time, reflect the expressive weakness of first-order logic. This weakness is the breeding ground for the freedom which modeltheoretic methods rest upon. By compactness, any first-order axiom system either has only finite models of limited cardinality or has infinite models. The first case is trivial because finitely many finite structures can explicitly be described by a first-order sentence. As model theory usually considers all models of an axiom system, modeltheorists were thus led to the second case, that is, to infinite structures. In fact, classical model theory of first-order logic and its generalizations to stronger languages live in the realm of the infinite.

✦ Table of Contents

Cover
Title
Copyright
Preface
Table of Contents
1. Preliminaries
2. The Ehrenfeucht-Fraissé Method
2.1 Elementary Classes
2.2 Ehrenfeucht’s Theorem
2.3 Examples and Fraissé’s Theorem
2.4 Hanf s Theorem
2.5 Gaifman's Theorem
3. More on Games
3.1 Second-Order Logic
3.2 Infinitary Logic: The Logics L_∞ω and L_ω_1ω
3.3 The Logics FO^s and L^s_∞ω?
3.3.1 Pebble Games
3.3.2 The s-Invariant of a Structure
3.3.3 Scott Formulas
3.4 Logics with Counting Quantifiers
3.5 Failure of Classical Theorems in the Finite
4. 0-1 Laws
4.1 0-1 Laws for FO and L^ω_∞ω
4.2 Parametric Classes
4.3 Unlabeled 0-1 Laws
4.3.1 Appendix
4.4 Examples and Consequences
4.5 Probabilities of Monadic Second Order Properties
5. Satisfiability in the Finite
5.1 Finite Model Property of FO^2
5.2 Finite Model Property of ∀^2∃^*-Sentences
6. Finite Automata and Logic: A Microcosm ofFinite Model Theory
6.1 Languages Accepted by Automata
6.2 Word Models
6.3 Examples and Applications
7. Descriptive Complexity Theory
7.1 Some Extensions of First-Order Logic
7.2 Turing Machines and Complexity Classes
7.2.1 Digression: Trahtenbrot's Theorem
7.2.2 Structures as Inputs
7.3 Logical Descriptions of Computations
7.4 The Complexity of the Satisfaction Relation
7.5 The Main Theorem and Some Consequences
7.5.1 Appendix
8. Logics with Fixed-Point Operators
8.1 Inflationary and Least Fixed-Points
8.2 Simultaneous Induction and Transitivity
8.3 Partial Fixed-Point Logic
8.4 Fixed-Point Logics and L^ω_∞ω
8.4.1 The Logic FO(PFPP_TIME)
8.4.2 Fixed-Point Logic with Counting
8.5 Fixed-Point Logics and Second-Order Logic
8.5.1 Digression: Implicit Definability
8.6 Transitive Closure Logic
8.6.1 FO(DTC) < FO(TC)
8.6.2 FO(posTC) and Normal Forms
8.6.3 FO(TC) < FO(LFP)
8.7 Bounded Fixed-Point Logic
9. Logic Programs
9.1 DATALOG
9.2 I-DATALOG and P-DATALOG
9.3 A Preservation Theorem
9.4 Normal Forms for Fixed-Point Logics
9.5 An Application of Negative Fixed-Point Logic
9.6 Hierarchies of Fixed-Point Logics
10. Optimization Problems
10.1 Polynomially Bounded Optimization Problems
10.2 Approximable Optimization Problems
11. Logics for PTIME
11.1 Logics and Invariants
11.2 PTIME on Classes of Structures
12. Quantifiers and Logical Reductions
12.1 Lindström Quantifiers
12.2 PTIME and Quantifiers
12.3 Logical Reductions
12.4 Quantifiers and Oracles
References
Index