Finite Model Theory
Springer Science & Business Media, Aug 18, 1999 - Mathematics - 360 pages
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.
What people are saying - Write a review
We haven't found any reviews in the usual places.
Other editions - View all
accepts arity assume atomic formulas axiomatizable axioms binary relation cardinality class of finite class of ordered class of structures clause complexity class complexity theory configuration contains Corollary corresponding DATALOG definition denote deterministic digraph duplicator wins effectively strongly captures example Exercise existential finite model finite structures first-order formula first-order logic first-order sentence fixed-point logic FO(DTC FO(LFP FO(LFP)-formula following are equivalent free variables given hence I-DATALOG input tapes intentional symbols isomorphism isomorphism type Lemma length lexicographic ordering LFP operator log space-bounded LOGSPACE logspace reductions model theory monotone natural numbers nontrivial obtained oracle machine oracle tapes ordered structures partial isomorphism polynomial positive Pow(A preceding proof Proposition PSPACE quantifier rank quantifier-free r-structures regular expressions relation symbol satisfies second-order logic sequence spoiler Str[r strongly captures PTIME subformula subset Suppose Theorem totally defined transitive closure tuples Turing machine unary vocabulary
Page 344 - Society, 1989. [Kol90] Ph. G. Kolaitis. Implicit definability on finite structures and unambiguous computations. In Proc. 5th IEEE Symp. on Logic in Computer Science, pages 168-180, 1990.
Page 346 - L. Pacholski and W. Szwast, The 0-1 law fails for the class of existential second-order Godel sentences with equality, Proc.
Page 344 - December 1977. [Imm88] N. Immerman. Nondeterministic space is closed under complement. SIAM Journal ' on Computing, 17:935-938, 1988.