THEORIES IN FINITE MODEL THEORY

John T. Baldwin

Department of Mathematics, Statistics and Computer Science University of Illinois at Chicago

May 4, 1999

Finite model theory stands at the intersection of complexity theory and model theory. Most of the work thus far in finite model theory is analogous to work in 1950’s style model theory of first order logic. That is, the focus is on the study of properties of the logic: expressibility, preservation theorems, criteria for equivalence among models. Around 1960, with Vaught’s paper [22], which is still required reading, infinite model theory took a decisive turn by concentrating on the study of theories. This was a natural tack in that case since first order logic is well-equipped to study theories of intrinsic mathematical interest; e.g. real closed fields, algebraically closed fields, Peano arithmetic. I will discuss here the possibilities of studying theories in finite model theory. This is not such an obviously well-motivated topic; however, it is natural to consider not only all finite structures for a language but various subclasses.

First order theories arise in finite model theory as ‘limit theories’. For example the almost sure theory of finite L-structures is (in the presence of a 0-1 law) a complete first order theory. In [2] we have exploited stability theoretic properties of the almost sure theory to answer questions about various logics on the finite structures. Here, however, we want to discuss theories with finite models.

1 L^{n}-theories

What classes of finite models admit a structure theory which it is profitable to study? We need a notion of complete theory which is both sufficiently weak – it must admit arbitrarily large finite models – that there is something to study and sufficiently strong that one can say something about the class of models. Our candidate is a complete theory in L^{n}: logic with n-variables. The similarity of the models of such a theory is guaranteed because they are equivalent with respect to n pebble games. Such works as [5, 7, 6, 1, 9, 10, 16] began the development of ‘Vaught-style’ model theory for finite variable logic.

The developments described here are heavily influenced by the work in abstract infinitary model theory carried on by e.g. Grossberg, Hyttinen, Lessmann, Shelah. This is natural because finite and infinitary logic share a salient distinction from first order logic: compactness fails. The particular results reported here are primarily due to Hyttinen [15, 14], Djordjević [8], and Hedman [12].

Here are some examples; they are all routine except item 3 which relies on deep results of Cherlin, Harrington, and Lachlan [4] which will be discussed below.

1. Vector spaces over a finite field (L^{3}-complete)

2. For any complete T, T_{n}, the L^{n} sentences of T.

3. If a first order theory is categorical in all powers, T is axiomatized by a single sentence plus an axiom of infinitity. For n large enough to include that sentence, T_{n} is L^{n}-complete.

4. An equivalence relation with class size specified below n.

5. The n-extension axioms

6. dense linear order

7. For any structure A, the L^{n}-theory of A.

The first difficulty in developing this theory is to find an appropriate notion of type over the empty set. This was accomplished by Hyttinen; we use the formulation of Djordjević.

Definition 1.1 Let M ⊧ T, B ⊆ M, a ∈ M.

tp_{L^{n}}(a/B, M) = {ϕ(x, b) : M ⊧ ϕ(a, b)}

where:

1. a, x, b etc are finite sequences, b ∈ B

2. ϕ(x, a) ∈ L^{n}

NOTE BENE:

1. Even if A is finite the conjunction of the type need not be in L^{n}.

2. We need the parameter M.

3. We write tp_{L^{n}}(A, M) or Th_{L^{n}}(A, M) for tp_{L^{n}}(a, ∅, M) where a enumerates A.

4. S_{n}^{k}(A, M) = {tp_{L^{n}}(a, A, N) : a ∈ N^{k} and M ≺_{n} N}

5. S_{n}^{n}(T) = S_{n}^{n}(∅, M) (any M ⊧ T).

The number of L^{n}-n-types is called the size of an L^{n} theory [1, 5]. This is a particularly important invariant because of the connections with calculations on the relational machines of Arbiteoul and Viani.

Just observing the construction of the Scott sentence of a finite model, we have:

Fact 1.2 1. If an L^{n}-theory T has a finite model, S_{n}^{n}(T) is finite.

2. If S_{n}^{n}(T) is finite, then T is axiomatized by a single sentence of L^{n}.

Note that for dense linear order S_{3}^{3}(T) is finite but there are no finite models. Beginning in the 60’s and brought to full fruition by Shelah the classification

of first order theories and their models has become a major component of model theory. There is a deep pure theory and recent applications to real algebraic geometry and Diophantine geometry.

A key insight of Shelah is that one can classify complete first order theories by counting types. For a complete first order theory, we denote by S(A) the collection of complete 1-types over A. We explain in a few paragraphs why the parameter M is not needed in this context.

The complete first order theory T is ω-stable if for every infinite A,

|S(A)| ≤ |A|.

The complete first order theory T is stable if for some infinite κ, |A| = κ implies |S(A)| ≤ |A|.

These notions can also be expressed in terms of rank functions and combinatorial properties of formulas. They are crucial tools for computing n(T, κ), the number of nonisomorphic models of T with cardinality κ.

We want to develop a similar kind of theory for L^{n} theories.

Definition 1.3 A complete L^{n}-theory T is stable if there is no L^{n}-formula ϕ(x, y) with the order property, i.e. such that in some model M of T there are sequences a_{i}, b_{j} for i, j < ω such that

ϕ(a_{i}, b_{j}) iff i < j.

Working entirely in finite models we could talk about arbitrarily long sequences satisfying these conditions. Hyttinen has taken a different definition and there is continuing discussion about the proper framework for this study.

Definition 1.4 A complete L^{n}-theory T is ω-stable if for every M ⊧ T and every infinite A ⊆ M, and every m

|S_{L^{n}}^{m}(A, M)| = |A|

.

Theorem 1.5 If T is a stable theory in k-variable logic then in any model of M of T only countably many L^{k}-types are realized over any countable sets.

This is based on old rank computations by Shelah but one must be careful working with incomplete theories. Various variants have been shown by Djordjević, Hyttinen, Lessmann and myself. There are foundational questions about which definition of stable/ω-stable to take. However, all the possibilities agree if the theory T has the amalgamation property so we discuss this concept in detail in the next section. In particular, while the last theorem yields that stable theories T in n-variable logic S_{n}^{n}(T) finite and with the amalgamation property are ω-stable in sense defined; this conjecture remains open in the absence of amalgamation.

2 The Amalgamation Property

A ⟶ B means there is an embedding f from A to B.

Definition. The class (K_{0}, ⟶) satisfies the amalgamation property (AP) if for any situation:

[figure: A; M; N]

with Th_{L^{n}}(A, M) = Th_{L^{n}}(A, N) there exists an N_{1}

such that [figure: A; M; N_{1}; N]

and Th_{L^{n}}(A, N_{1}) = Th_{L^{n}}(A, M) = Th_{L^{n}}(A, N).

Any complete first order theory has the amalgamation property for elementary embeddings. Thus, in a first order theory the meaning of S(A, M) does not depend on M, which justifies our omission of M in defining this notion for first order theories.

There are complete L^{n} theories which do not have the amalgamation property for L^{n}-elementary embeddings. E.g. Thomas [21, 20] has constructed for n ≥ 4 theories T_{n} which have nonisomorphic models of the same finite cardinality and no larger models. He has similar examples with infinite models.

Further examples of theories with only finitely many finite models were constructed by Poizat [18], Cherlin [3] and unintentionally by Gurevich and Shelah [11] - multipedes. Still further examples appear in the work of Martin Grohe [9]; essentially for Diophantine equations with a finite number of solutions he constructs a complete theory T in an appropriate L^{n} with such that the set of cardinalities of finite models of T is the same as the set of solutions of the equation. In each case, in view of Djordjević’s work such examples are either unstable or don’t have the amalgamation property.

There are a number of questions which arise around the amalgamation property.

Question Is there an L^{n}-theory which is complete in first order logic but does not have the L^{n}-amalgamation property?

Rosen has observed that, if not, the work reported on below yields that no ℵ_{0}-categorical, stable theory is finitely axiomatizable.

Definition 2.1 An L^{n}-theory T has the independence property if for some L^{n} formula ϕ for every m < ω there exists a model M_{m} and elements A = langlea_{i} : i < m⟩ ∈ M_{m} for such that for every X ⊂ m each type

p_{X} = {ϕ(v, a_{i}) : i ∈ X}

is consistent.

More precisely for each X, there is a model M_{X} containing A such that for each X, Y (M_{X}, A) and (M_{Y} , A) are L^{n} equivalent and p_{X} is realized in M_{X}. Note that in the absence of amalgamation the p_{X} do not have to be simultaneously realizable.

Problem Construct a complete theory in L^{4} which has the independence property in the sense of Definition 2.1 but such that ϕ does not satisfy the m-extension axiom for sufficiently large m.

In the absence of amalgamation, Hyttinen [15] proves that a natural notion of ω-stability is equivalent to the conjunction of ‘not the order property’ and ‘not the independence property’. He calls it stability rather than ω-stability but this seems a misnomer to me. Hyttinen’s paper [15] takes place in a somewhat more abstract setting and a number of results are proved without the amalgamation property.

Definition 2.2 A structure M is L^{n}-κ-saturated if for every A ⊂ M with |A| < κ, every L^{n}-elementary extension N of M, if a ∈ N, tp_{L^{n}}(a, A, N) is realized in M.

Theorem 2.3 (Hyttinen, Djordjević) If T has the L^{n}-amalgamation property then for any κ, every model of T can be L^{n}-embedded in an L^{n}-κ-saturated model.

Note that if T is the L^{3}-theory of (Z, +, 1), there is no countable countably L^{3}-saturated model. The following example illustrates L^{n}-saturation.

Consider the structure (M, E) where:

1. E is an equivalence relation.

2. There is one class of each finite cardinality.

3. There are infinitely many infinite classes.

M is L-saturated but not L^{n} saturated for any n. Fix m > n. Let a_{0}, … a_{m−1} enumerate one equivalence class. The L^{n}-type p = {xEa_{1}, x ≠ a_{i} : i < m} is omitted in M. Note that p is inconsistent with the first order theory of (M, a) but consistent with the first order theory of M. All finite equivalence classes in an L^{n} saturated model of T will have cardinality at most n.

The following theorem unites the methods of stability theory and finite model theory.

Theorem 2.4 (Djordjević)

1. If a stable L^{k}-theory T with the amalgamation property has only finitely many L^{k}-types then T can be extended to an L-theory which is ω-categorical and ω-stable.

2. It follows that T has arbitrarily large finite models.

Here is a sketch of the proof.

1. Let T^{c} be the theory of an L^{n}-saturated model.

2. Prove T^{c} is ℵ_{0}-categorical and stable.

3. Using ω-stablity of T, show that T^{c} is ω-stable.

4. The Zilber/ Cherlin-Harringon-Lachlan theorem [4] asserts: An ω-stable, ℵ_{0}-categorical T has the strong finite model property: If M ⊧ T and M ⊧ ψ then some finite substructure of N of M models ψ.

5. Apply this result to ψ - the sentence axiomatizing the L^{n} theory T. (In fact this yields arbitrarily large finite models.) A stronger variant of Item

4 shows that there is a single finite sentence which along with sentences asserting the universe is infinite axiomatizes the complete theory. The Zilber/Cherlin-Harrington-Lachlan theorem was a major result in stability theory. It heralded the importance, first pointed out by Zilber of understanding the geometric nature of dependence. Here we consider only one of the possibilities.

Definition 2.5 A dependence relation is trivial if whenever a depends on a set B, a depends on a single element of B.

Theorem 2.6 (Hyttinen) Let T be a complete theory in L^{n} which has amalgamation and with S_{n}^{n}(T) finite. Suppose T is stable and forking is trivial. Then, for every m there is a finite m-saturated model M of T.

Hytinnen assumed T has arbitrarily large finite models, but this follows from Theorem 2.4.

3 Finite Variable logic in infinite model theory

In another direction, there are interesting applications of finite-variable logics in infinite model theory. A fundamental problem in infinite model theory has been to understand ‘axioms of infinitity’. The question of whether a single first order sentence could have only infinite models and be totally categorical (i.e only one model of each infinite cardinality) motivated the work of Zilber and Cherlin Harrington Lachlan described above. They showed there was no such sentence but every totally categorical theory is axiomatized by a single sentence plus a schema asserting the universe is infinite. This schema employs infinitely many variables.

There are known examples [17] of finitely axiomatizable ℵ_{1}-categorical theories. But it is unknown whether any such are strongly minimal. A theory T is strongly minimal if every definable subset of a model of T is either finite or cofinite. They are the building blocks of ℵ_{1}-categorical theories.

Hedman has studied which complete first order theories and in particular which strongly minimal theories admit a finite-variable axiomatization. This work has deep connections with ‘involved groups’ [13]; a classical question of Abraham Robinson [19] becomes, Are algebraically closed fields finite variable axiomatizable?

Theorem 3.1 (Hedman)

1. Eliminating functions for relations does not affect finite variable axiomatizability.

2. (in the air) If T is ℵ_{0}-categorical, T is finitely variable axiomatizable if and only T is finitely axiomatizable.

3. If T is a strongly minimal theory with trivial algebraic dependence then T is axiomatized by sentences in some L^{n} in a language with (infinitely many) constants.

For problems and links to other workers in finite model theory consult: http://www-mgi.informatik.rwth-aachen.de/FMT/

I have notes, links and papers at http://www.math.uic.edu/ jbaldwin

References

[1] S. Abiteboul and V. Vianu. Generic computation and its complexity. In 23rd ACM Symposium on Theory of Computing, pages 212–219, 1991.

[2] J.T. Baldwin. Stability, the finite cover property and 0-1 laws. preprint 1998.

[3] G.L. Cherlin. Theories categorical in power n + 2. manuscript, 1982.

[4] G.L. Cherlin, L. Harrington, and A.H. Lachlan. ℵ_{0}-categorical, ℵ_{0}-stable structures. Annals of Pure and Applied Logic, 28:103–135, 1985.

[5] A. Dawar. Types and indiscernibles in finite models. In J. Makowsky, editor, Logic Colloquium ‘95, 199?

[6] A. Dawar, S. Lindell, and S. Weinstein. Infinitary logic and inductive definability. Information and Computation, 119:160–175, 1995.

[7] A. Dawar, S. Lindell, and S. Weinstein. First order logic, fixed point logic, and linear order. In H. Kleine-Büning, editor, Computer Science Logic ’95, pages 161–177. Springer-Verlag: LNCS 1092, 1996.

[8] Marko Djordjević. Finite variable logic, stability, and finite models. preprint, 199?

[9] M. Grohe. Large finite structures with few L^{k}-types. In Proceedings 12th IEEE Symp. of Logic in Computer Science, pages 216–227, 1997.

[10] M. Grohe. Finite variable logics in descriptive complexity. The Bulletin of Symbolic Logic, 4:345–398, 1998.

[11] Y. Gurevich and S. Shelah. On finite rigid structures. The Journal of Symbolic Logic, 61:549–562, 1996.

[12] Shawn Hedman. Finitary axiomatizations of strongly minimal theories. Ph.D. thesis, University of Illinois at Chicago, 199?

[13] E. Hrushovski. Finitely axiomatizable ℵ_{1}-categorical theories. Journal of Symbolic Logic, 79:838–844, 1994.

[14] T. Hyttinen. Forking in finite models. preprint.

[15] T. Hyttinen. On stability in finite models. preprint.

[16] Martin Otto. Bounded Variable Logics and Counting. Springer Verlag, Heidelberg, 1996. Lecture Notes in Logic:9.

[17] M. G. Peretyatkin. An example of an ω_{1}-categorical finitely axiomatizable theory. Algebra and Logic, 19:202–229, 1980. translated from Algebra y Logica.

[18] Bruno Poizat. Deux ou trois choses je sais de L_{n}. The Journal of Symbolic Logic, 47:641–648, 1982.

[19] A. Robinson. Metamathematical problems. The Journal of Symbolic Logic, 38:500–515, 1973.

[20] Simon Thomas. Theories with finitely many models II. manuscript, 198?

[21] Simon Thomas. Theories with finitely many models. Journal of Symbolic Logic, pages 374–776, 1986.

[22] R.L. Vaught. Denumerable models of countable theories. In Infinitistic Methods, Proc. Symp. Foundations of Math., Warsaw, 1959, pages 303– 321. Oaństwowe Wydawnictwo Naukowe, Warsaw, 1961.