Finite Model Theory

Finite Model Theory (FMT) is a subarea of model theory (MT). MT is the branch of mathematical logic which deals with the relation between a formal language (syntax) and its interpretations (semantics). FMT is a restriction of MT to interpretations of finite structures, i.e. structures with a finite universe.

• Since many central theorems of MT do not hold when restricted to finite structures, FMT is quite different from MT in proof methods. Failing central results include the compactness theorem, Gödel's completeness theorem, and the method of ultraproducts for first-order logic.
• As MT is closely related to mathematical algebra, FMT became an "unusually effective" instrument in computer science. In other words: "In the history of mathematical logic most interest has concentrated on infinite structures....Yet, the objects computers have and hold are always finite. To study computation we need a theory of finite structures." Thus the main application areas are: descriptive complexity theory, database theory and formal language theory.
• FMT is mainly about discrimination of structures: can a given class of structures be described (up to isomorphy) in a given language, e.g. can all cyclic graphs be discriminated (from the non-cyclic ones) by a First-order (henceforth FO) sentence, i.e. is the property "cyclic" FO expressible.