Finite model theory

Finite model theory

Finite model theory is a subfield of model theory that focuses on properties of logical languages, such as first-order logic, over finite structures, such as finite groups, graphs, databases, and most abstract machines. It focuses in particular on connections between logical languages and computation, and is closely associated with discrete mathematics, complexity theory, and database theory.

Many important results of first-order logic and classical model theory fail when restricted to finite structures, including the compactness theorem, the Craig interpolation lemma, the Los-Tarski preservation theorem, the Downward Löwenheim-Skolem theorem, and Gödel's completeness theorem. The essential problem is that in this context, first-order logic is not sufficiently expressive. By extending first-order logic with operators such as transitive closure and least fixed point, and by using fragments of second-order logic, we obtain new logics that have more interesting properties over finite structures.

One important subfield of finite model theory, descriptive complexity, connects the expressivity of various logical languages with the capabilities of various abstract machines. For example, if a language can be expressed in first-order logic with a least fixed point operator added, a Turing machine can determine in polynomial time (see P) whether a given string is in the language. Descriptive complexity allows results to be transferred between computational complexity and mathematical logic and gives additional evidence that the standard complexity classes are "natural." Neil Immerman states "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."cite book | last = Immerman | first = Neil | authorlink = Neil Immerman | title = Descriptive Complexity | year = 1999 | publisher = Springer-Verlag | location = New York | id = ISBN 0-387-98600-6 | pages = 6]

Another important result of finite model theory are the zero-one laws, which establish that many types of logical formulas hold for either almost all or almost no finite structures. For example, the proportion of graphs of size "n" that are connected approaches one as "n" approaches infinity, while the proportion that contain an isolated vertex approaches zero. In fact the same is true of any graph property that can be checked in polynomial time: it either approaches one or approaches zero. This has ramifications for randomized algorithms on large finite structures.

Finite model theory also studies finite restrictions of logic, such as first-order logic with only a fixed limit of "k" variables.

External links

* [ R. Fagin] . [ Finite model theory-a personal perspective] . Theoretical Computer Science 116, 1993, pp. 3-31.
* Jouko Väänänen. [ A Short Course on Finite Model Theory] . Department of Mathematics, University of Helsinki. Based on lectures from 1993-1994.
* [ Finite Model Theory Homepage] at Aachen University of Technology, including a list of open problems
* [ Finite Model Theory References] , a database of references related to finite model theory


Wikimedia Foundation. 2010.

Look at other dictionaries:

  • Model theory — This article is about the mathematical discipline. For the informal notion in other parts of mathematics and science, see Mathematical model. In mathematics, model theory is the study of (classes of) mathematical structures (e.g. groups, fields,… …   Wikipedia

  • Finite model property — In logic, we say a logic L has the finite model property (fmp for short) if there is a class of models M of L (i.e. each model M is a model of L) such that any non theorem of L is falsified by some finite model in M. Another way of putting this… …   Wikipedia

  • Actor model theory — In theoretical computer science, Actor model theory concerns theoretical issues for the Actor model.Actors are the primitives that form the basis of the Actor model of concurrent digital computation. In response to a message that it receives, an… …   Wikipedia

  • Type (model theory) — In model theory and related areas of mathematics, a type is a set of first order formulas in a language L with free variables x1, x2,…, xn which are true of a sequence of elements of an L structure . Loosely speaking, types describe possible… …   Wikipedia

  • NIP (model theory) — In model theory, a branch of mathematical logic, a complete theory T is said to satisfy NIP (or not the independence property ) if none of its formulae satisfy the independence property, that is if none of its formulae can pick out any given… …   Wikipedia

  • Pregeometry (model theory) — Pregeometry, and in full combinatorial pregeometry, are essentially synonyms for matroid . They were introduced by G. C. Rota with the intention of providing a less ineffably cacaphonous alternative term. Also, the term combinatorial geometry,… …   Wikipedia

  • Age (model theory) — In model theory, a branch of mathematical logic, the age of a structure (or model) A is the class of all finitely generated structures which are embeddable in A (i.e. isomorphic to substructures of A ). This concept is central in the construction …   Wikipedia

  • Theory (mathematical logic) — This article is about theories in a formal language, as studied in mathematical logic. For other uses, see Theory (disambiguation). In mathematical logic, a theory (also called a formal theory) is a set of sentences in a formal language. Usually… …   Wikipedia

  • Finite-state machine — State machine redirects here. For infinite state machines, see State transition system. For fault tolerance methodology, see State machine replication. SFSM redirects here. For the Italian railway company, see Circumvesuviana. A finite state… …   Wikipedia

  • Finite state machine — A finite state machine (FSM) or finite state automaton (plural: automata ) or simply a state machine, is a model of behavior composed of a finite number of states, transitions between those states, and actions. A finite state machine is an… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”

We are using cookies for the best presentation of our site. Continuing to use this site, you agree with this.