Model theory

Lindström's Theorem

Reading preferences

Optional display controls need JavaScript. All reading content and navigation work without it.

Source file content/model-theory/lindstrom/lindstrom.tex

Source file content/model-theory/lindstrom/introduction.tex

Introduction

In this chapter we aim to prove Lindstr\"om's characterization of first-order logic as the maximal logic for which (given certain further constraints) the Compactness and the Downward L\"owenheim--Skolem theorems hold (the thm labeled compactness and the thm labeled downward ls). First, we need a more general characterization of the general class of logics to which the theorem applies. We will restrict ourselves to relational languages, i.e., languages which only contain predicate symbols and individual constants, but no function symbols.

Source file content/model-theory/lindstrom/abstract-logics.tex

Abstract Logics

Definition: abstract logic

An abstract logic is a pair L,Lsource, where Lsource is a function that assigns to each language Lsource a set L(L)source of sentences, and Lsource is a relation between structures for the language Lsource and elements of L(L)source. In particular, F,source is ordinary first-order logic, i.e., Fsource is the function assigning to the language Lsource the set of first-order sentences built from the constants in Lsource, and source is the satisfaction relation of first-order logic.

Notice that we are still employing the same notion of structure for a given language as for first-order logic, but we do not presuppose that sentences are build up from the basic symbols in Lsource in the usual way, nor that the relation Lsource is recursively defined in the same way as for first-order logic. So for instance the definition, being completely general, is intended to capture the case where sentences in L,Lsource contain infinitely long conjunctions or disjunction, or quantifiers other than source and source (e.g., “there are infinitely many xsource such that dots”), or perhaps infinitely long quantifier prefixes. To emphasize that “sentences” in L(L)source need not be ordinary sentences of first-order logic, in this chapter we use variables Esource, Fsource, dots to range over them, and reserve Asource, Bsource, dots for ordinary first-order formulas.

Definition: model class and elementary equivalence

Let Mod(L)(E)source denote the class {M:MLE}source. If the language needs to be made explicit, we write ModL(L)(E)source. Two structures Msource and Nsource for Lsource are elementarily equivalent in L,Lsource, written MLNsource, if the same sentences from L(L)source are true in each.

Definition: normal abstract logic

An abstract logic L,Lsource for the language Lsource is normal if it satisfies the following properties:

  1. (Lsource-Monotonicity) For languages Lsource and Lsource, if LLsource, then L(L)L(L)source.

  2. (Expansion Property) For each EL(L)source there is a finite subset Lsource of Lsource such that the relation MLEsource depends only on the reduct of Msource to Lsource; i.e., if Msource and Nsource have the same reduct to Lsource then MLEsource if and only if NLEsource.

  3. (Isomorphism Property) If MLEsource and MNsource then also NLEsource.

  4. (Renaming Property) The relation Lsource is preserved under renaming: if the language Lsource is obtained from Lsource by replacing each symbol Psource by a symbol Psource of the same arity and each constant csource by a distinct constant csource, then for each structure Msource and sentence Esource, MLEsource if and only if MLEsource, where Msource is the Lsource-structure corresponding to Lsource and EL(L)source.

  5. (Boolean Property) The abstract logic L,Lsource is closed under the Boolean connectives in the sense that for each EL(L)source there is a FL(L)source such that MLFsource if and only if MLEsource, and for each Esource and Fsource there is a Gsource such that Mod(L)(G)=Mod(L)(E)Mod(L)(F)source. Similarly for atomic formulas and the other connectives.

  6. (Quantifier Property) For each constant csource in Lsource and EL(L)source there is a FL(L)source such that

    ModL(L)(F)={M:M[a]ModL(L)(E) for some a|M|},source

    where L=L{c}source and M[a]source is the expansion of Msource to Lsource assigning asource to csource.

  7. (Relativization Property) Given a sentence EL(L)source and symbols Rsource, c1source, dots, cnsource not in Lsource, there is a sentence FL(L{R,c1,,cn})source called the relativization of Esource to R(x,c1,cn)source, such that for each structure Msource:

    M[X,b1,,bn]LF if and only if NLE,source

    where Nsource is the substructure of Msource with domain |N|={a|M|:RM(a,b1,,bn)}source (see the rem labeled substructure), and M[X,b1,,bn]source is the expansion of Msource interpreting Rsource, c1source, dots, cnsource by Xsource, b1,source dots, bnsource, respectively (with XMn+1source).

Definition: expressive comparison of logics

Given two abstract logics L1,L1source and L2,L2source we say that the latter is at least as expressive as the former, written L1,L1L2,L2source, if for each language Lsource and sentence EL1(L)source there is a sentence FL2(L)source such that ModL(L1)(E)=ModL(L2)(F)source. The logics L1,L1source and L2,L2source are equivalent if L1,L1L2,L2source and L2,L2L1,L1source.

Source file content/model-theory/lindstrom/ls-property.tex

Compactness and L\"owenheim--Skolem Properties

We now give the obvious extensions of compactness and L\"owenheim--Skolem to the case of abstract logics.

Definition: compactness property

An abstract logic L,Lsource has the Compactness Property if each set Γsource of L(L)source-sentences is satisfiable whenever each finite Γ0Γsource is satisfiable.

Definition: downward Lowenheim Skolem property

L,Lsource has the Downward L\"owenheim--Skolem property if any satisfiable Γsource has an enumerable model.

The notion of partial isomorphism from the defn labeled partialisom is purely “algebraic” (i.e., given without reference to the sentences of the language but only to the constants provided by the language Lsource of the structures), and hence it applies to the case of abstract logics. In case of first-order logic, we know from the thm labeled p isom2 that if two structures are partially isomorphic then they are elementarily equivalent. That proof does not carry over to abstract logics, for induction on formulas need not be available for arbitrary EL(L)source, but the theorem is true nonetheless, provided the L\"owenheim--Skolem property holds.

Theorem: partial isomorphism in a normal logic

Suppose L,Lsource is a normal logic with the L\"owenheim--Skolem property. Then any two structures that are partially isomorphic are elementarily equivalent in L,Lsource.

Proof

Suppose MpNsource, but for some Esource also MLEsource while NLEsource. By the Isomorphism Property we can assume that |M|source and |N|source are disjoint, and by the Expansion Property we can assume that EL(L)source for a finite language Lsource. Let Isource be a set of partial isomorphisms between Msource and Nsource, and with no loss of generality also assume that if pIsource and qpsource then also qIsource.

|M|<ωsource is the set of finite sequences of elements of |M|source. Let Ssource be the ternary relation over |M|<ωsource representing concatenation, i.e., if a,b,c|M|<ωsource then S(a,b,c)source holds if and only if csource is the concatenation of asource and bsource; and let Tsource be the ternary relation such that T(a,b,c)source holds for bMsource and a,c|M|<ωsource if and only if a=a1,ansource and c=a1,an,bsource. Pick new 3-place predicate symbols Psource and Qsource and form the structure M*source having the universe |M||M|<ωsource, having Msource as a substructure, and interpreting Psource and Qsource by the concatenation relations Ssource and Tsource (so M*source is in the language L{P,Q}source).

Define |N|<ωsource, Ssource, Tsource, Psource, Qsource and N*source analogously. Since by hypothesis MpNsource, there is a relation Isource between |M|<ωsource and |N|<ωsource such that I(a,b)source holds if and only if asource and bsource are isomorphic and satisfy the back-and-forth condition of the defn labeled partialisom. Now, let Msource be the structure whose domain is the union of the domains of M*source and N*source, having M*source and N*source as substructures, in the language with one extra binary predicate symbol Rsource interpreted by the relation Isource and predicate symbols denoting the domains |M|*source and |N|*source.

Figure: structure containing an internal partial isomorphism

Shows one ambient structure containing expanded copies of structures M and N. Each copy contains its original substructure, and a two-headed arrow labeled I connects the sequence domains used for the internal partial isomorphism.

Source transcription

[h] centering

Diagram: internal partial-isomorphism construction

A rounded rectangle represents the ambient structure. Two nested circles on the left represent M inside M star, two nested circles on the right represent N inside N star, and a bidirectional curved arrow labeled I links their sequence regions.

Source transcription

[node distance=2cm, auto, thick, >=stealth'] draw [rounded corners] (0,0) -- (8,0) -- (8,4) -- (0,4) -- cycle; draw (2,2) circle (0.5cm); draw (2,2) circle (1.25cm); draw (6,2) circle (0.5cm); draw (6,2) circle (1.25cm); path node at (0.75,3.5) large Msource; path node at (2,2) large Msource; path node at (6,2) large Nsource; path node at (3.5,1) large M*source; path node at (7.5,1) large N*source; node (Idom) at (2.8,2) ; node (Irng) at (5.2,2) ; draw[<->, bend left] (Idom) to node large Isource (Irng) ;

captionThe structure Msource with the internal partial isomorphism.

The crucial observation is that in the language of the structure Msource there is a first-order sentence D1source true in Msource saying that MLEsource and NLEsource (this requires the Relativization Property), as well as a first-order sentence D2source true in Msource saying that MpNsource via the partial isomorphism Isource. By the L\"owenheim--Skolem Property, D1source and D2source are jointly true in an enumerable model M0source containing partially isomorphic substructures M0source and N0source such that M0LEsource and N0LEsource. But enumerable partially isomorphic structures are in fact isomorphic by the thm labeled p isom1, contradicting the Isomorphism Property of normal abstract logics.

Source file content/model-theory/lindstrom/lindstrom-proof.tex

Lindstr\"om's Theorem

Lemma: bounded equivalence implies first-order definability

Suppose EL(L)source, with Lsource finite, and assume also that there is an nsource such that for any two structures Msource and Nsource, if MnNsource and MLEsource then also NLEsource. Then Esource is equivalent to a first-order sentence, i.e., there is a first-order Dsource such that Mod(L)(E)=Mod(L)(D)source.

Proof

Let nsource be such that any two nsource-equivalent structures Msource and Nsource agree on the value assigned to Esource. Recall the prop labeled qr finite: there are only finitely many first-order sentences in a finite language that have quantifier rank no greater than nsource, up to logical equivalence. Now, for each fixed structure Msource let DMsource be the conjunction of all first-order sentences Esource true in Msource with qr(E)nsource (this conjunction is finite), so that NDMsource if and only if NnMsource. Then put D={DM:MLE}source; this disjunction is also finite (up to logical equivalence).

The conclusion Mod(L)(E)=Mod(L)(D)source follows. In fact, if NLDsource then for some MLEsource we have NDMsource, whence also NLEsource (by the hypothesis of the lemma). Conversely, if NLEsource then DNsource is a disjunct in Dsource, and since NDNsource, also NLDsource.

Theorem: Lindstrom's theorem

[Lindstr\"om's Theorem] Suppose L,Lsource has the Compactness and the L\"owenheim--Skolem Properties. Then L,LF,source (so L,Lsource is equivalent to first-order logic).

Proof

By the lem labeled lindstrom, it suffices to show that for any EL(L)source, with Lsource finite, there is nsource such that for any two structures Msource and Nsource: if MnNsource then Msource and Nsource agree on Esource. For then Esource is equivalent to a first-order sentence, from which L,LF,source follows. Since we are working in a finite, purely relational language, by the thm labeled b n f we can replace the statement that MnNsource by the corresponding algebraic statement that In(,)source.

Given Esource, suppose towards a contradiction that for each nsource there are structures Mnsource and Nnsource such that In(,)source, but (say) MnLEsource whereas NnLEsource. By the Isomorphism Property we can assume that all the Mnsource's interpret the constants of the language by the same objects; furthermore, since there are only finitely many atomic sentences in the language, we may also assume that they satisfy the same atomic sentences (we can take a subsequence of the Msource's otherwise). Let Msource be the union of all the Mnsource's, i.e., the unique minimal structure having each Mnsource as a substructure. As in the proof of the thm labeled abstract p isom, let M*source be the extension of Msource with domain |M||M|<ωsource, in the expanded language comprising the concatenation predicates Psource and Qsource.

Similarly, define Nnsource, Nsource and N*source. Now let Msource be the structure whose domain comprises the domains of M*source and N*source as well as the natural numbers source along with their natural ordering source, in the language with extra predicates representing the domains |M|source, |N|source, |M|<ωsource and |N|<ωsource as well as predicates coding the domains of Mnsource and Nnsource in the sense that:

|Mn|={a|M|:R(a,n)};|Nn|={a|N|:S(a,n)};|M|<ωn={a|M|<ω:R(a,n)};|N|<ωn={a|N|<ω:S(a,n)}.source

The structure Msource also has a ternary relation Jsource such that J(n,a,b)source holds if and only if In(a,b)source.

Now there is a sentence Dsource in the language Lsource augmented by Rsource, Ssource, Jsource, etc., saying that source is a discrete linear ordering with first but no last element and such that MnEsource, NnEsource, and for each nsource in the ordering, J(n,a,b)source holds if and only if In(a,b)source.

Using the Compactness Property, we can find a model M*source of Dsource in which the ordering contains a non-standard element n*source. In particular then M*source will contain substructures Mn*source and Nn*source such that Mn*LEsource and Nn*LEsource. But now we can define a set Isource of pairs of ksource-tuples from |Mn*|source and |Nn*|source by putting a,bIsource if and only if J(n*k,a,b)source, where ksource is the length of asource and bsource. Since n*source is non-standard, for each standard ksource we have that n*k>0source, and the set Isource witnesses the fact that Mn*pNn*source. But by the thm labeled abstract p isom, Mn*source is Lsource-equivalent to Nn*source, a contradiction.

Source disclosures