Lably
Skip to content

Finite model theory

Branch of logic

  • 11 min read
  • 5 chapters

Related on Lably

Through Logic, Interpretation (logic) and Structure (mathematical logic)

Lab · Class 11Binary and Logic GatesLab · Class 6–12Build a World & Wire Logic (Blockworld)Lab · Class 9StatisticsLab · Class 8–9Factorisation

Since many central theorems of model theory do not hold when restricted to finite structures, finite model theory is quite different from model theory in its methods of proof. 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). These invalidities all follow from Trakhtenbrot's theorem.

While model theory has many applications to mathematical algebra, finite model theory 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 of finite model theory are: descriptive complexity theory, database theory and formal language theory.

Axiomatisability

A common motivating question in finite model theory is whether a given class of structures can be described in a given language. For instance, one might ask whether the class of cyclic graphs can be distinguished among graphs by a FO sentence, which can also be phrased as asking whether cyclicity is FO-expressible.

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. Similarly, any finite collection of finite structures can always be axiomatized in first-order logic. Some, but not all, infinite collections of finite structures can also be axiomatized by a single first-order sentence.

Characterisation of a single structure

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

Problem

A structure like (1) in the figure can be described by FO sentences in the logic of graphs like

  1. Every node has an edge to another node: ∀x∃yG(x,y).
  2. No node has an edge to itself: ∀x,y(G(x,y)⇒x≠y).
  3. There is at least one node that is connected to all others: ∃x∀y(x≠y⇒G(x,y)).

However, these properties do not axiomatize the structure, since for structure (1') the above properties hold as well, yet structures (1) and (1') are not isomorphic.

Informally the question is whether by adding enough properties, these properties together describe exactly (1) and are valid (all together) for no other structure (up to isomorphism).

Approach

For a single finite structure it is always possible to precisely describe the structure by a single FO sentence. The principle is illustrated here for a structure with one binary relation R and without constants. To this aim, we introduce first-order variables x1,…,xn that are interpreted as the n elements of the structure. We then introduce the four following formulas:

  1. φ1=⋀i≠j¬(xi=xj) says that there are at least n elements;
  2. φ2=∀y⋁i(xi=y) says that there are at most n elements;
  3. φ3=⋀(ai,aj)∈RR(xi,xj) states every edge of the relation R;
  4. φ4=⋀(ai,aj)∉R¬R(xi,xj) states every non-edge of the relation R.

Finally, the structure is described by the FO sentence ∃x1…∃xn(φ1∧φ2∧φ3∧φ4).

Extension to a fixed number of structures

The method of describing a single finite structure by means of a first-order sentence can easily be extended for any fixed number of structures. A unique description can be obtained by the disjunction of the descriptions for each structure. For instance, for two finite structures A and B with defining sentences φA and φB this would be

φA∨φB.

Extension to an infinite structure

By definition, a set containing an infinite structure falls outside the area that FMT deals with. Note that infinite structures can never be discriminated in FO, because of the Löwenheim–Skolem theorem, which implies that no first-order theory with an infinite model can have a unique model up to isomorphism.

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

Characterisation of a class of structures

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

Problem

The descriptions given so far all specify the number of elements of the universe. 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.

Approach

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

  1. The core idea is that whenever one wants to see if a property P can be expressed in FO, one chooses structures A and B, where A does have P and B doesn't. If for A and B the same FO sentences hold, then P cannot be expressed in FO. In short:
    A∈P,B∉P and A≡B,
    where A≡B is shorthand for A⊨α⇔B⊨α for all FO-sentences α, and P represents the class of structures with property P.
  2. The methodology considers countably many subsets of the language, the union of which forms the language itself. For instance, for FO consider classes FO[m] for each m. For each m the above core idea then has to be shown. That is:
    A∈P,B∉P and A≡mB
    with a pair A,B for each m and α (in ≡) from FO[m]. It may be appropriate to choose the classes FO[m] to form a partition of the language.
  3. One common way to define FO[m] is by means of the quantifier rank qr(α) of a FO formula α, which expresses the depth of quantifier nesting. For example, for a formula in prenex normal form, qr is simply the total number of its quantifiers. Then FO[m] can be defined as all FO formulas α with qr(α) ≤ m (or, if a partition is desired, as those FO formulas with quantifier rank equal to m).
  4. Thus it all comes down to showing A⊨α⇔B⊨α on the subsets FO[m]. The main approach here is to use the algebraic characterization provided by Ehrenfeucht–Fraïssé games. Informally, these take a single partial isomorphism on A and B and extend it m times, in order to either prove or disprove A≡mB, dependent on who wins the game.

Example

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

  1. The idea is to pick A ∈ EVEN and B ∉ EVEN, where EVEN is the class of all structures of even size.
  2. We start with two ordered structures A2 and B2 with universes A2 = {1, 2, 3, 4} and B2 = {1, 2, 3}. Obviously A2 ∈ EVEN and B2 ∉ EVEN.
  3. For m = 2, in a 2-move Ehrenfeucht–Fraïssé game on A2 and B2 the duplicator always wins, and thus A2 and B2 cannot be discriminated in FO[2], i.e. A2⊨α⟺B2⊨α for every α ∈ FO[2].
  4. Next we have to scale the structures up by increasing m. For example, for m = 3 we must find an A3 and B3 such that the duplicator always wins the 3-move game. This can be achieved by A3 = {1, ..., 8} and B3 = {1, ..., 7}. More generally, we can choose Am = {1, ..., 2m} and Bm = {1, ..., 2m−1}; for any m the duplicator always wins the m-move game for this pair of structures*.
  5. Thus EVEN on finite ordered structures cannot be expressed in FO.

Sign in to keep reading

4 more chapters are free with a Lably account.

More in Topics in mathematics

DiameterStraight line segment that passes through the centre of a circleSmoothnessDegree of differentiability of a function or mapGroup actionTransformations induced by a mathematical groupMonotonic functionOrder-preserving mathematical functionCountable setMathematical set that can be enumeratedEllipsoidQuadric surface that looks like a deformed sphere