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 source, where source is a function that assigns to each language source a set source of sentences, and source is a relation between structures for the language source and elements of source. In particular, source is ordinary first-order logic, i.e., source is the function assigning to the language source the set of first-order sentences built from the constants in source, 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 source in the usual way, nor that the relation source 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 source contain infinitely long conjunctions or disjunction, or quantifiers other than source and source (e.g., “there are infinitely many source such that dots”), or perhaps infinitely long quantifier prefixes. To emphasize that “sentences” in source need not be ordinary sentences of first-order logic, in this chapter we use variables source, source, dots to range over them, and reserve source, source, dots for ordinary first-order formulas.
Definition: model class and elementary equivalence
Let source denote the class source. If the language needs to be made explicit, we write source. Two structures source and source for source are elementarily equivalent in source, written source, if the same sentences from source are true in each.
Definition: normal abstract logic
An abstract logic source for the language source is normal if it satisfies the following properties:
(source-Monotonicity) For languages source and source, if source, then source.
(Expansion Property) For each source there is a finite subset source of source such that the relation source depends only on the reduct of source to source; i.e., if source and source have the same reduct to source then source if and only if source.
(Isomorphism Property) If source and source then also source.
(Renaming Property) The relation source is preserved under renaming: if the language source is obtained from source by replacing each symbol source by a symbol source of the same arity and each constant source by a distinct constant source, then for each structure source and sentence source, source if and only if source, where source is the source-structure corresponding to source and source.
(Boolean Property) The abstract logic source is closed under the Boolean connectives in the sense that for each source there is a source such that source if and only if source, and for each source and source there is a source such that source. Similarly for atomic formulas and the other connectives.
(Quantifier Property) For each constant source in source and source there is a source such that
where source and source is the expansion of source to source assigning source to source.
(Relativization Property) Given a sentence source and symbols source, source, dots, source not in source, there is a sentence source called the relativization of source to source, such that for each structure source:
where source is the substructure of source with domain source (see the rem labeled substructure), and source is the expansion of source interpreting source, source, dots, source by source, source dots, source, respectively (with source).
Definition: expressive comparison of logics
Given two abstract logics source and source we say that the latter is at least as expressive as the former, written source, if for each language source and sentence source there is a sentence source such that source. The logics source and source are equivalent if source and source.
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 source has the Compactness Property if each set source of source-sentences is satisfiable whenever each finite source is satisfiable.
Definition: downward Lowenheim Skolem property
source 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 source 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 source, but the theorem is true nonetheless, provided the L\"owenheim--Skolem property holds.
Theorem: partial isomorphism in a normal logic
Suppose source is a normal logic with the L\"owenheim--Skolem property. Then any two structures that are partially isomorphic are elementarily equivalent in source.
Proof
Suppose source, but for some source also source while source. By the Isomorphism Property we can assume that source and source are disjoint, and by the Expansion Property we can assume that source for a finite language source. Let source be a set of partial isomorphisms between source and source, and with no loss of generality also assume that if source and source then also source.
source is the set of finite sequences of elements of source. Let source be the ternary relation over source representing concatenation, i.e., if source then source holds if and only if source is the concatenation of source and source; and let source be the ternary relation such that source holds for source and source if and only if source and source. Pick new 3-place predicate symbols source and source and form the structure source having the universe source, having source as a substructure, and interpreting source and source by the concatenation relations source and source (so source is in the language source).
Define source, source, source, source, source and source analogously. Since by hypothesis source, there is a relation source between source and source such that source holds if and only if source and source are isomorphic and satisfy the back-and-forth condition of the defn labeled partialisom. Now, let source be the structure whose domain is the union of the domains of source and source, having source and source as substructures, in the language with one extra binary predicate symbol source interpreted by the relation source and predicate symbols denoting the domains source and 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 source; path node at (2,2) large source; path node at (6,2) large source; path node at (3.5,1) large source; path node at (7.5,1) large source; node (Idom) at (2.8,2) ; node (Irng) at (5.2,2) ; draw[<->, bend left] (Idom) to node large source (Irng) ;
captionThe structure source with the internal partial isomorphism.
The crucial observation is that in the language of the structure source there is a first-order sentence source true in source saying that source and source (this requires the Relativization Property), as well as a first-order sentence source true in source saying that source via the partial isomorphism source. By the L\"owenheim--Skolem Property, source and source are jointly true in an enumerable model source containing partially isomorphic substructures source and source such that source and source. 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 source, with source finite, and assume also that there is an source such that for any two structures source and source, if source and source then also source. Then source is equivalent to a first-order sentence, i.e., there is a first-order source such that source.
Proof
Let source be such that any two source-equivalent structures source and source agree on the value assigned to source. 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 source, up to logical equivalence. Now, for each fixed structure source let source be the conjunction of all first-order sentences source true in source with source (this conjunction is finite), so that source if and only if source. Then put source; this disjunction is also finite (up to logical equivalence).
The conclusion source follows. In fact, if source then for some source we have source, whence also source (by the hypothesis of the lemma). Conversely, if source then source is a disjunct in source, and since source, also source.
Theorem: Lindstrom's theorem
[Lindstr\"om's Theorem] Suppose source has the Compactness and the L\"owenheim--Skolem Properties. Then source (so source is equivalent to first-order logic).
Proof
By the lem labeled lindstrom, it suffices to show that for any source, with source finite, there is source such that for any two structures source and source: if source then source and source agree on source. For then source is equivalent to a first-order sentence, from which 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 source by the corresponding algebraic statement that source.
Given source, suppose towards a contradiction that for each source there are structures source and source such that source, but (say) source whereas source. By the Isomorphism Property we can assume that all the source'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 source's otherwise). Let source be the union of all the source's, i.e., the unique minimal structure having each source as a substructure. As in the proof of the thm labeled abstract p isom, let source be the extension of source with domain source, in the expanded language comprising the concatenation predicates source and source.
Similarly, define source, source and source. Now let source be the structure whose domain comprises the domains of source and source as well as the natural numbers source along with their natural ordering source, in the language with extra predicates representing the domains source, source, source and source as well as predicates coding the domains of source and source in the sense that:
The structure source also has a ternary relation source such that source holds if and only if source.
Now there is a sentence source in the language source augmented by source, source, source, etc., saying that source is a discrete linear ordering with first but no last element and such that source, source, and for each source in the ordering, source holds if and only if source.
Using the Compactness Property, we can find a model source of source in which the ordering contains a non-standard element source. In particular then source will contain substructures source and source such that source and source. But now we can define a set source of pairs of source-tuples from source and source by putting source if and only if source, where source is the length of source and source. Since source is non-standard, for each standard source we have that source, and the set source witnesses the fact that source. But by the thm labeled abstract p isom, source is source-equivalent to source, a contradiction.
Source disclosures
- TR029-SOURCE-001: The frozen source omits the superscript marker before the star on the domain of structure N. The reader restores domain of structure N star; the source remains unchanged source