Finite model theory

Model theory is the branch of logic which deals with the relation between a formal language (syntax) and its interpretations (semantics).

Central results of classical model theory that fail for finite structures under finite model theory include the compactness theorem, Gödel's completeness theorem, and the method of ultraproducts for first-order logic (FO).

In other words: "In the history of mathematical logic most interest has concentrated on infinite structures.

To study computation we need a theory of finite structures.

A common motivating question in finite model theory is whether a given class of structures can be described in a given language.

A single finite structure can always be axiomatized in first-order logic, where axiomatized in a language L means described uniquely up to isomorphism by a single L-sentence.

Some, but not all, infinite collections of finite structures can also be axiomatized by a single first-order sentence.

Is a language L expressive enough to axiomatize a single finite structure S?

this would be By definition, a set containing an infinite structure falls outside the area that FMT deals with.

The most famous example is probably Skolem's theorem, that there is a countable non-standard model of arithmetic.

Is a language L expressive enough to describe exactly (up to isomorphism) those finite structures that have certain property P?

Unfortunately most interesting sets of structures are not restricted to a certain size, like all graphs that are trees, are connected or are acyclic.

Thus to discriminate a finite number of structures is of special importance.

Instead of a general statement, the following is a sketch of a methodology to differentiate between structures that can and cannot be discriminated.

We want to show that the property that the size of an ordered structure A = (A, ≤) is even, can not be expressed in FO.

(*) Note that the proof of the result of the Ehrenfeucht–Fraïssé game has been omitted, since it is not the main focus here.

The 0-1 law has been shown to hold for sentences in FO(LFP), first-order logic augmented with a least fixed point operator, and more generally for sentences in the infinitary logic

Another important variant is the unlabelled 0-1 law, where instead of considering the fraction of structures with domain

, one considers the fraction of isomorphism classes of structures with n elements.

This fraction is well-defined, since any two isomorphic structures satisfy the same sentences.

[5] An important goal of finite model theory is the characterisation of complexity classes by the type of logic needed to express the languages in them.

This connection between complexity and the logic of finite structures allows results to be transferred easily from one area to the other, facilitating new proof methods and providing additional evidence that the main complexity classes are somehow "natural" and not tied to the specific abstract machines used to define them.

Specifically, each logical system produces a set of queries expressible in it.

The queries – when restricted to finite structures – correspond to the computational problems of traditional complexity theory.

Some well-known complexity classes are captured by logical languages as follows: A substantial fragment of SQL (namely that which is effectively relational algebra) is based on first-order logic (more precisely can be translated in domain relational calculus by means of Codd's theorem), as the following example illustrates: Think of a database table "GIRLS" with the columns "FIRST_NAME" and "LAST_NAME".

This makes the language more expressive for the price of higher difficulty to learn and implement.

An alternative way is e.g. to introduce a "JOIN" operator, that is: First-order logic is too restrictive for some database applications, for instance because of its inability to express transitive closure.

This has led to more powerful constructs being added to database query languages, such as recursive WITH in SQL:1999.

Thus the logical structure of text search queries can be expressed in propositional logic, like in: Note that the challenges in full text search are different from database querying, like ranking of results.