Stability theory, Permutations of Indiscernibles, and Embedded Finite Models^{∗}

John Baldwin^{†}

Department of Mathematics, Statistics, and Computer Science University of Illinois at Chicago E-mail: jbaldwin@math.uic.edu

Michael Benedikt

Bell Laboratories 1000 E. Warrenville Rd. Naperville, IL 60566 E-mail: benedikt@research.bell-labs.com

April 10, 1998

Abstract

We show that the expressive power of first-order logic over finite models embedded in a model M is determined by stability-theoretic properties of M. In particular, we show that if M is stable, then every class of finite structures that can be defined by embedding the structures in M, can be defined in pure first-order logic. We also show that if M does not have the independence property, then any class of finite structures that can be defined by embedding the structures in M, can be defined in first-order logic over a dense linear order. This extends known results on the definability of classes of finite structures and ordered finite structures in the setting of embedded finite models. These results depend on several results in infinite model theory. Let I be a set of indiscernibles in a model M and suppose (M, I) is elementarily equivalent to (M_{1}, I_{1}) where M_{1} is |I_{1}|^{+}-saturated. If M is stable and (M, I) is saturated then every permutation of I extends to an automorphism of M and the theory of (M, I) is stable. Let I be a sequence of <-indiscernibles in a model M, which does not have the independence property, and suppose (M, I) is elementarily equivalent to (M_{1}, I_{1}) where (I_{1}, <) is a complete dense linear order and M_{1} is |I_{1}|^{+}-saturated. Then (M, I)-types over I are order-definable and if (M, I) is ℵ_{1}-saturated every order preserving permutation of I can be extended to a back-and-forth system.

1 Introduction

A major research current in both finite and infinite model theory has been the classification of structures via the combinatorial objects that can be defined within them. In infinite ‘classical’ model theory one prototypical classification program is stability theory. One set of stability-theoretic results focuses on structures that admit no definable order. It is shown that these structures (the stable structures) are much better behaved than structures that do admit orders: e.g. the former have few types, and always admit universal domains. Another dividing line of interest is between structures that do or do not admit an infinite parametrically definable independent family: those that do not are said to be without the independence property. This class of structures includes the stable ones, but it also encompasses many ordered structures, such as real closed ordered fields, that have a nicely behaved definability theory.

∗primary classification: 03C45, secondary classification: 68P15, 03C40 †partially supported by NSF-93-8768

In finite model theory there has been a line of work with a somewhat similar flavor: the investigation of the impact of the existence of an order relation on logics over finite structures. For example, there has been much work comparing the expressivity of various predicate logics on ordered structures with that on unordered structures [12], with bounding the expressive power of first-order logic and fragments of second-order logic on ordered structures [12], and with proving the presence of an almost sure linear order according to various probability measures on finite structures [17].

This work aims at showing one connection between these two lines of research: we extend results on the expressiveness of first-order logic on finite models to the situation where finite models are embedded in a fixed infinite structure. Logics that deal with this ‘hybrid setting’ have been studied recently in connection with database theory. In particular, it has been shown that many interesting properties of finite structures that are not first-order definable (such as the parity of a set or the connectivity of a graph) remain undefinable for finite structures that are embedded in structures satisfying appropriate conditions. Results in the literature, starting with [29] and continuing through [6] and [4], show that under certain conditions on the model (e.g. o-minimal in [6], quasi o-minimal in [4]) no new queries can be defined other than those already definable on finite ordered structures, provided that we restrict our attention to permutation invariant queries (see the definition of generic in Section 2). Here we extend these broader ‘collapse’ results as well to structures without the independence property, a very broad model-theoretic class that includes the examples of [6] and [4] and also includes all stable structures. The connection between generic query expressibility and this class is interesting not only due to the scope of the class, but also because of the connection of this class with many probabilistic and algorithmic issues, such as machine learning [25].

In addition, we prove a stronger result for stable structures; we show that any permutation-invariant queries that are definable in a stable structure are definable not just over order but over the trivial structure, and hence are pure first-order definable in the sense of finite model theory.

The collapse theorems above follow from results concerning ‘model theory over a predicate’. amd the paper can also be seen as a contribution to this topic. Fix languages L^{−} ⊂ L with the predicate P in L but not L^{−}. Much of this work (e.g. [31], [19], [24]) focuses on the extent to which the properties of an L^{−}-structure N determine the properties of an L-structure M with P (M) = N. Our work varies in two ways. To some extent we switch the emphasis by starting with M and asking about properties of the expansion of M obtained by adding a predicate for a subset. More important, instead of considering an arbitrary subset as in the work just described or a submodel as in ([33],[30]), we insist that the set be a collection of (order) indiscernibles. We prove that in a theory without the independence property, types over an indiscernible sequence (of a complete linear order) are order-definable with parameters from the sequence. We show that permutations of sets of indiscernibles in ‘pseudo-small’ stable L^{+}-saturated models extend to automorphisms of the models, and we show that a pseudo-small expansion of a stable theory is stable.

Organization and quick summary Section 2 introduces the main definitions in the paper, gives a more detailed overview of previous work on embedded finite structures, and states the main theorems of the paper. Section 3 presents the key tool: a quantifier reduction theorem for models with a predicate for an indiscernible set. In Sections 4 and 6 we prove this quantifier reduction theorem for stable theories and theories without the independence property, respectively. As a prelude to the second proof, a key definability result for types over ordered sequences of indiscernibles in theories without the independence property is proved in Section 5. Section 7 uses these results to prove the results for embedded finite model theory. Section 8 contains the results on infinite model theory over a predicate. Section 9 gives conclusions and discusses future work. The reader primarily interested in results on query languages may want to start by reading just Section 2 and Section 7.

2 Embedded finite model theory

The following basic definitions provide a framework for the model-theoretic results dealt with in this paper. Most of the terminology below comes from the database literature; see [1] for a general discussion of the notions of genericity given below, and [8] for a discussion of collapse results.

Let 𝕌 be an infinite set, and let S be a finite relational language. A boolean query on 𝕌, Q, is a collection of S-structures with domain a finite subset of 𝕌. Since we will not discuss any nonboolean queries, we will drop the word boolean and just talk about queries on 𝕌, or 𝕌-queries. Technically, we should preface ‘query’ with an S to indicate which finite set of additional relational symbols are used in the query; then our theorems would be about ‘all S-queries’ or (see below) ‘all order S-queries’. Following common practice we suppress this parameter. A generic query on 𝕌 is a query that is closed under S-isomorphism. An abstract query Q is a collection of isomorphism types of finite S-structures. Given an abstract query Q and set 𝕌, Q defines a generic query Q_{𝕌} by considering all finite S-structures embedded in 𝕌 whose isomorphism type is in Q. Clearly a generic query on an infinite 𝕌 determines an abstract query. Finite model theory investigates the collection of abstract queries and (equivalently) generic queries that are definable in predicate logics. Well-known results include that the abstract query of all even-cardinality sets (the parity query) and the set of connected graphs are not first-order definable.

Now let L be a language disjoint from S, and let M be an L-structure with domain 𝕌. For any S-structure A with domain contained in 𝕌, M(A) denotes the unique L ∪ S-structure that expands M and agrees with A on the interpretation of the predicates in S. Such an A is what we mean by an embedded finite model.

Given a first-order sentence ϕ in L ∪ S, the query defined by ϕ is the set of S-structures A with domain a finite subset of 𝕌 such that that M(A) ⊧ ϕ. We say ϕ is generic if the query defined by it is generic. Given a 𝕌-query Q we say it is first-order over M if there is ϕ ∈ L ∪ S that defines Q. An abstract query Q is called first-order over M if there is a first-order ϕ ∈ L ∪ S that defines Q_{𝕌}.

For a model M, we let

F O(M) be {Q : Q is first-order definable over M}

F O_{GEN}(M) be {Q : Q is generic and Q is first-order definable over M}.

These two classes are the basic objects of study in this paper. In particular, we can compare the generic queries definable in different models M, since a generic query “makes sense” in any model.

A pure first-order query is an abstract query that is definable over the structure ⟨𝕌, =⟩ by an {S, =}-formula ψ. The results in [20] imply that any pure first-order abstract query is first-order definable in the sense of finite model theory. That is, if a set of isomorphism types is definable over the trivial infinite structure, then it is the collection of finite models of a first-order sentence. Note that these two notions are a priori incomparable: in the first case the quantifiers range over 𝕌 and in the second case only over a finite set. The following easy fact was used in [6] and [28]:

Remark 2.1 If M′ and M are elementarily equivalent L-structures and the abstract query Q is defined by ϕ over M, then Q is also defined by ϕ over M′.

For, if Q were not defined by ϕ over M′, there would be a finite S-structure A′ witnessing the fact. Let n = |A|, and assume A′ ∈ Q but M′(A′) ⊧ ¬ϕ. The statement that there is an S-structure A′ of size n with the isomorphism type of A′ such that M′(A′) ⊧ ¬ϕ can be expressed as a single L -sentence, hence it must hold in M as well.

Using this we see that the collection F O_{GEN}(M) is actually an invariant of the theory of M. In this paper, then, we will focus on F O_{GEN}(M) rather than F O(M).

We prove a number of collapse results by providing conditions on a structure such that if certain kinds of generic queries are definable with the help of symbols from L, they can be defined without them. The first such result is:

First Main Result :

Theorem 2.2 Let 𝕌 be infinite and M be a stable L-structure with domain 𝕌. If Q is a first-order definable generic query over M, then Q is a pure first-order query.

We call this a generic collapse theorem, and say that an M satisfying the above implication, i.e an M satisfying:

If Q ∈ F O_{GEN}(M) then Q is pure first-order

exhibits generic collapse to equality. Hence our first main result is that stable theories have generic collapse to equality.

A model M is stable if it does not admit a parametrically definable linear-order (on tuples). More precisely, there is no ϕ(x⃗, y⃗) such that it is consistent with the theory of M that there are ⟨a⃗_{n} : n ∈ ω⟩ such that ϕ(a⃗_{m}, a⃗_{n}) ↔ m < n.

Standard model theory references such as [3], [10], [18], [32] or [34] discuss stable theories at length, give several alternative definitions, and give numerous examples of stable structures. Standard examples of stable theories include algebraically closed fields, theories of equivalence relations, and any complete theory of abelian groups. The prototypical unstable structures are linearly-ordered structures, e.g. a real closed ordered field, and the random graph.

We now weaken the notion of genericity to deal with properties of linearly-ordered structures.

Let S be a finite relational language. An abstract (boolean) order query Q is a collection of linearly ordered S-structures which is closed under {S, <}-isomorphism.

If (𝕌, <) is a linearly ordered infinite set, then an abstract order query induces a query on this structure which satisfies a weaker kind of genericity. A local map is a partial function on 𝕌. Given ⟨𝕌, <⟩, an S-structure A and a local map f whose domain contains the domain of A, fA is the image structure induced by f. A query on ⟨𝕌, <⟩, Q is locally order generic if it is preserved by local order-preserving maps on ⟨𝕌, <⟩. For any infinite linearly ordered structure O and abstract query Q, the query Q_{O} induced on O is locally order generic. Conversely, any locally order generic query naturally determines an abstract order query.

Let L be a language disjoint from S, let L′ = L ∪ {<}, and let M be an L′-structure with domain 𝕌. For any S-structure A with domain contained in 𝕌, M(A) denotes the unique L ∪ {S, <}-structure that expands M and agrees with A on the interpretation of the predicates in S. We say that an abstract order query Q is first-order over M if there is a ϕ ∈ L ∪ {S, <} that defines Q: that is (A, <) ∈ Q ↔ M(A) ⊧ ϕ

We can now study the class F O_{og}(M) of order-generic queries definable over any ordered structure M. Our goal is to show that for certain ordered structures, F O_{og}(M) is as small as it can be. An abstract order query Q is order definable if it is defined over the structure ⟨𝕌, <⟩ by an {S, <}-formula ψ.

Second Main Result :

Theorem 2.3 Let (𝕌, <) be an infinite linear order and M an L ∪ {<}-structure that expands (𝕌, <), which does not have the independence property. If Q is a first-order definable locally order generic query over M, then Q is an order-definable query.

Roughly, a class does not have the independence property (has NIP) if it does not admit an infinite parametrically defined class of definable sets which can be satisfied independently; the formal definition is below. Theorem 2.3 generalizes all previous collapse results, since the classes involved all satisfied NIP. Classes without the independence property include all stable structures, all o-minimal and quasi-o-minimal structures (e.g. additive number theory), all C-minimal structures [26] (e.g. regular trees), and all linear orders (even with unary predicates) [32]. Particular examples of interest include the real field (with exponentiation) and the p-adic numbers, Q_{p}. Further, structures in NIP admit a Vapnik-Chervonenkis dimension, which implies that every parametrically definable family is PAC-learnable [25]. Some other studies are in [23] and [32]. In [34], Shelah proves a fundamental dichotomy : Every unstable theory either has the independence property or the strict order property (roughly, interprets a linear order). The protypical structure with the independence property is the random graph.

Definition 2.4 1. The formula ϕ(x⃗, y⃗) has the m-independence property in T if there exists a set of m, lg(x)-tuples b⃗_{1}, … b⃗_{m} such that for every X ⊆ {1, …, m}, there is an a⃗_{X} such that ϕ(b⃗_{i}, a⃗_{X}) holds if and only if i ∈ X.

2. ϕ does not have the independence property in T just if for some integer m, ϕ(x⃗, y⃗) does not have the m-independence property in T.

3. T does not have the independence property (T ∈ NIP) if no ϕ has the independence property in T. A model does not have the independence property if its theory does not have it.

It is shown in [8] that the parity query is definable in the random graph; this shows the necessity of the hypothesis in Theorem 2.3 that T does not have the independence property. Both instability and the independence property are preserved under taking reducts.

We also give a result comparing the generic queries definable over a model M with the generic queries definable over a linear-order. It is known that there are generic queries that are expressible by making use of an order on the structure which are not pure first-order. An example, due to Gurevich, is given in [1], and a consequence of this example for embedded finite model theory is that F O_{GEN}(⟨𝕌, =⟩) is a proper subset of F O_{GEN}(⟨𝕌, <⟩) for any linear order < ^{1}. However, our next main result shows that adding extra structure beyond order does not yield new generic queries, when the model does not have the independence property.

We will establish the following variant of Theorem 2.3.

Theorem 2.5 Let 𝕌 be infinite and M be an L-structure with domain 𝕌 that does not have the independence property. If Q is a first-order definable generic query over M, then Q is definable over any dense linear order without endpoints.

A model satisfying the second sentence of Theorem 2.5 is said to have generic collapse to order.

Note that in the collapse result above, and in the corollaries below, there is no assumption that the model M contains a definable (partial or total) order.

Since it is known that any abstract order query definable in an infinite linear order is definable as a class of finite ordered structures (this follows, for example, from the natural/active collapse result for o-minimal structures in [6], but was probably known earlier), Theorem 2.5 yields:

1Here is a slight variant on his example. Let the query language contain the similarity type for Boolean algebras. Now in this language require that the structure is a Boolean algebra. Since each element of a finite Boolean algebra is a join of atoms, first order quantification over the entire structure codes monadic second order quantification over the set of atoms. Now using the order, one can assert there are an even number of atoms by saying there is a subset X of the atoms such that every other atom is in X.

Corollary 2.6 Let 𝕌 be infinite and M be an L-structure with domain 𝕌 that does not have the independence property. If Q is a first-order definable generic query over M, then the abstract order query defined by Q (i.e the class of linearly ordered expansions of isomorphism types in Q) is definable by a formula in {S, <}.

As a further corollary we have:

Corollary 2.7 Let S contain a single binary relation symbol. If M does not have the independence property, then the following queries are not first-order definable over M: parity, transitive or deterministic transitive closure of a graph; maximal matching in a bipartite graph; Eulerian cycle.

Proof: The examples are known not to be expressible over ordered structures [1]. □_{2.7}

It follows from this that parity and connectivity are not definable in abelian groups, algebraically closed fields, and the many other stable structures. It also follows that the separating example of Gurevich mentioned above is not expressible in stable structures.

The study of expressibility over embedded finite structures began in connection with a particular database formalism, constraint databases, in [21] (there are other frameworks for studying “mixed” structures, particularly the one presented in [15]). [21] focused on the real ordered group and ordered field. Both Theorem 2.3 and Corollary 2.7 were proved in the special case of the real ordered group in [29]. This result was extended to o-minimal structures in [6] and extended to quasi-o-minimal structures in [4]. In contrast, it is easy to verify that there are models M for which any recursive query can be expressed over M (for example, ⟨N, +, ∗, <⟩); hence collapse of any sort fails for such structures.

Many of the results on collapse in the previous literature rely implicitly or explicitly on the use of indiscernibles (the first explicit use being [28]). The results on collapse theorems for o-minimal and quasi-o-minimal structures rely on the ‘locality property’ of o-minimal/quasi-o-minimal theories: this property is used to extend certain mappings on indiscernibles. The locality property does not apply to stable theories, so the approach here relies instead on an analysis of expansions of models by a set of indiscernibles.

3 Quantifier Reduction in Expansions by Indiscernibles

The main tool for proving collapse results will be a theorem about extending a permutation of a set of indiscernibles to a family of partial isomorphisms. This approach to proving collapse is patterned on [6] and [28], but the extension result we need (Theorem 7.3) requires quite a bit of machinery to prove. In this section we outline a set of results (proved in the ensuing 3 sections) about expansions of structures by a predicate for an indiscernible set or sequence. These results will be used in the Section 7 to prove the key result, Theorem 7.3, about extending mappings on indiscernibles.

3.1 The Setting

We fix a first order theory T for a countable language L. Let < be a binary relation symbol. If for some model M of T an infinite subset of M is linearly ordered by an L-formula, we may take < to be this ordering; otherwise it is a new symbol.

For any set of formulas Δ and set A of elements of some model of T, p = tp_{Δ}(b⃗/A) (the Δ-type of b⃗ over A) denotes the collection of A-instances of formulas from Δ satisfied by b⃗. If the length of b⃗ is r, we say p is a (Δ, r)-type. If Δ is just =, we say p is an equality type. If Δ is just {=, <}, we say p is an order type or <-type.

If Δ is all of L, we say L-type. For finite sequences t⃗_{1}, t⃗_{2}, we write t⃗_{1} ≡_{A,Δ} t⃗_{2}, if t⃗_{1} and t⃗_{2} have the same Δ-type over A; we frequently omit Δ if it clear from context. By an equality formula we mean a quantifier-free formula in equality and by an order formula we mean a quantifier-free formula in order and equality.

Definition 3.1 A set I is the (range of) a set (sequence) of (Δ, L)-indiscernibles if any a⃗, b⃗ in I which have the same Δ-type have the same L-type. If Δ = {x = y} then we say I is a set of pure indiscernibles; if Δ = {x < y, x = y} then we say I is a sequence of order indiscernibles.

In the rest of the paper we will prove results about a set of Δ-indiscernibles, where Δ is {x = y} or {x < y, x = y}. In our results about pure indiscernibles we will always assume that T is stable, and in results about orderindiscernibles we assume only T ∈ NIP. Note that in the latter case we are not assuming that < is contained in L. We will call the first case ‘the equality case’ and the second case ‘the order case’; in the order case we will always take I to be an order-indiscernible set relative to some dense order without endpoints.

We note that such indiscernibles always exist: there is a model M of T, which contains an infinite linearly ordered subset I of <- indiscernibles, and the order can be taken to be a complete dense linear order without endpoints [10]. A basic result of stability theory (e.g. [3] V.1.3) asserts that if T is stable I must be a set of pure indiscernibles.

We will assume, until noted otherwise, that

• If T is stable Δ = {x = y}; otherwise Δ = {x = y, x < y}

• L^{+} is L ∪ Δ plus a unary predicate P.

• M^{+} is M expanded to interpret P by I and < by the ordering of the indiscernible sequence.

• T^{+} denotes the theory of (M, I).

We will call the set I or, more precisely, the structure (M, I) small if further

• M is |I|^{+}-saturated.

• if Δ = {=, <}, then the order type of ⟨I, <⟩ is a complete dense linear-order.

If the L^{+}-structure (N, J) is elementarily equivalent to a small (M, I), J or (N, J) is called pseudo-small, and the theory T^{+} of a small model is called a pseudo-small theory, since a model of T^{+} ‘thinks’ the set of indiscernibles is small.

Unless explicitly denied, henceforth T^{+} is a pseudo-small theory.

Notes on Pseudo-smallness: Those interested in the connection of pseudo-small structures to collapse results may want to look ahead to Lemma 7.5. In the ordered case, the completeness of ⟨I, <⟩ ensures that for any model (M′, I′) of T^{+}, the reduct to L is definably complete: for any L-formula ϕ(x, y⃗) and any m⃗ in M, if {c ∈ I : ϕ(c, m⃗)} is a bounded subset of I, then it has a least upper bound. This holds in a small model (M, I) using completeness, and tranfers using elementary equivalence.

The main result stated in this section is a quantifier-reduction result for each of the theories T^{+}. Namely, we show that if T is stable and I is a set of indiscernibles in M ⊧ T then every relation on M defined by an L^{+}-formula can be defined by one in which only bounded quantification over the set of indiscernibles is allowed. We show the analogous result for a theory T, which does not have the independence property, where I is a sequence of order indiscernibles. As a corollary to this we eventually show that T^{+} depends only on T and the L-types realized in I.

Definition 3.2 1. A formula is basic if it is a Boolean combination of L-formulas and Δ-formulas (i.e. equalities, if Δ = {x = y}, or inequalities and inequalities if Δ = {x = y, x < y}).

2. An L^{+}-formula ϕ is P -bounded if it is in the least collection of formulas containing the basic formulas and closed under Boolean operations and the quantifications ∃x ∈ P and ∀x ∈ P.

Henceforth ∀w⃗ ∈ P abbreviates ∀w_{1} ∈ P … ∀w_{i} ∈ P.

By the usual method of obtaining prenex normal forms, every P -bounded formula is equivalent to one consisting of a string of P -bounded quantifiers followed by a basic formula. We want to show that every L^{+}-definable relation is definable using only quantification over the indiscernibles. That is, our goal is to prove

Theorem 3.3 (The Main Reduction Theorem ) Let T be a stable theory (a theory without the independence property) and let T^{+} be a pseudo-small extension of T. For each formula ϕ(x⃗) ∈ L^{+}, there is an equivalent P -bounded formula ϕ′(x⃗). That is,

T^{+} ⊧ ∀x⃗ [ϕ(x⃗) ↔ ϕ′(x⃗)].

3.2 Some Assumptions and Reductions.

The proof of Theorem 3.3 will take up the next three and a half sections.

The following key assumption amounts to assuming our reduction result holds for basic formulas. The definability of types over all sets is tantamount to the definition of stability, so the assumption is clear for stable theories. For theories without the independence property, we prove it in Section 5. Our argument will use this definability of L-types to establish Theorem 3.3 by induction on formulas.

Assumption 3.4 For every basic formula ϕ(x⃗, y⃗) there is a quantifier free Δ-formula ψ(w⃗, y⃗) such that for every model (M, I) of T^{+} if I is a set of (Δ, L)-indiscernibles in M then for every m⃗ ∈ M there is a c⃗m⃗ ∈ I such that

∀y⃗ ∈ P [ψ(c⃗m⃗, y⃗) ≡ ϕ(m⃗, y⃗)].

The following lemma shows that P-bounded formulas have defining schema, which will be useful both in proving the reduction results and in applying them to query collapse.

Lemma 3.5 Let M^{+} ⊧ T^{+}. For each P-bounded formula ϕ(x⃗, y⃗) there is a P-bounded formula δ(w⃗, y⃗) that is a defining schema for ϕ over I: That is, for each m⃗ in M there is c⃗m⃗ in I such that

M^{+} ⊧ ∀y⃗ ∈ P [ϕ(m⃗, y⃗) ↔ δ(c⃗m⃗, y⃗)].

Proof: Let ϕ(x⃗, y⃗) be normalized as (Q_{1}z_{1}) … (Q_{k}z_{k}) η(x⃗, y⃗, z⃗) where the Q_{i}’s are P -bounded quantifiers and η is a basic formula. By Assumption 3.4 there is a defining schema η′(y⃗, z⃗, w⃗) for η(x⃗, y⃗, z⃗) over I. That is,

M^{+} ⊧ ∀x⃗ ∃w⃗ ∈ P ∀y⃗ ∈ P ∀z⃗ ∈ P [η(x⃗, y⃗, z⃗) ↔ η′(y⃗, z⃗, w⃗)].

Consider δ(w⃗, y⃗) given by (Q_{1}z_{1}) … (Q_{K}z_{k}) η′(y⃗, z⃗, w⃗). It is easy to verify that δ(w⃗, y⃗) is a P-bounded formula and a defining schema for ϕ: For each m⃗ ∈ M choose c⃗m⃗ ∈ I so that ∀y⃗ ∈ P ∀z⃗ ∈ P (η(m⃗, y⃗, z⃗) ↔ η′(y⃗, z⃗, c⃗m⃗)). Then δ(c⃗m⃗, y⃗) defines the ϕ-type of m⃗ over I. □_{3.5}

Looking ahead a bit, the main application of the above result is the definability of all L^{+}-types over I.

Corollary 3.6 ( Corollary to as-yet-unproved Theorem 3.3 ) For every L^{+}-formula ϕ(x⃗, y⃗) there is a Δ-formula ψ(w⃗, y⃗) such that for every m⃗ there is a c⃗m⃗ ∈ I such that

∀y⃗ ∈ P [ψ(c⃗m⃗, y⃗) ↔ ϕ(m⃗, y⃗)].

That is, all L^{+}-types over I are Δ-definable.

Proof. By Theorem 3.3 and Lemma 3.5 there is a P-bounded formula δ(w⃗, y⃗) and for each m⃗ in M there is c⃗m⃗ in I such that:

M^{+} ⊧ ∀y⃗ ∈ P [ϕ(m⃗, y⃗) ↔ δ(c⃗m⃗, y⃗)].

Rewrite δ(w⃗, y⃗) as (Q_{1}z_{1}) … (Q_{k}z_{k}) η(w⃗, y⃗, z⃗) where the Q_{i}’s are P -bounded formulas bounding z_{i} and η ∈ L. Now using the Δ-indiscernibility of I, it easy to show by induction on quantifiers that (Q_{1}z_{1}) … (Q_{k}z_{k}) η(w⃗, y⃗, z⃗) is equivalent over I to a Δ-formula. □_{3.6}

Definition 3.7 Fix a structure M, finite sets Δ, Δ_{1} of formulas, and I a set (Δ, L)-indiscernibles. For A, A_{0}, A_{1} finite subsets of I with A ⊆ A_{1} and some n⃗ ∈ M, p = tp(n⃗/A_{1}) Δ_{1}-splits in A over A_{0} if there exist sequences c⃗, d⃗ ∈ A which have the same Δ-type over A_{0}, but for some β ∈ Δ_{1}, c⃗ and d⃗ disagree on n⃗ for β. (That is, ¬[β(n⃗, c⃗) ↔ β(n⃗, d⃗)]).

If A = A_{1}, the ‘in A’ is omitted; frequently A_{1} will be I. (In e.g. [34] this is called (Δ, Δ_{1})-splitting, but we will always have Δ fixed so we write only one parameter.) When Δ_{1} = {β} we say there is a β-split for n⃗ over A_{0}. Since the second β in the phrase ‘p = tp_{β}(n⃗/A_{1}) does not β-split’ is redundant, it is often omitted. Note that if p = tp_{β}(n⃗/A_{1}) does not β-split over a finite subset C of A_{1}, then there is a quantifier free Δ-formula δ(w⃗, y⃗) and a c⃗ ∈ C such that for any a⃗ ∈ A_{1},

β(n⃗, a⃗) ↔ δ(c⃗, a⃗).

Here δ is the disjunction of the finitely many, necessarily quantifier free (by quantifier elimination in the theories of equality and dense-linear order), complete Δ-types over C of elements that satisfy β. We say p = tp_{β}(n⃗/A_{1}) is Δ-defined over C.

We now show that to prove the main quantifier reduction lemma, it suffices to handle a certain class of ∃∀ formulas.

Proposition 3.8 Let I be a set of (Δ, L)-indiscernibles in L-structure M. Suppose that (M, I) satisfies Assumption 3.4 and the following condition. For every basic formula β(x_{1}, …, x_{n}, z, y⃗) and for every Δ-formula δ(w⃗, y⃗) with y_{1}, … y_{R} = y⃗, the formula

γ(x⃗) = ∃z ∃w⃗ ∈ P ∀y⃗ ∈ P [β(x⃗, z, y⃗) ↔ δ(w⃗, y⃗)]

is equivalent in M^{+} to a P-bounded formula.

Then every L^{+}-formula is equivalent in T^{+} = Th(M, I) to a P -bounded formula.

Proof: We first observe that the assertion that every L^{+}-formula is equivalent to a P -bounded formula is preserved by L^{+}-elementary-equivalence. Thus we need only establish this assertion in (M, I) to get it as a consequence of T^{+}. For quantifier-free L^{+}-formulas, the assertion follows by relativizing to P (e.g. replace ¬P (x) by ∀y ∈ P (y ≠ x)). To prove the conclusion by induction on quantifier rank, it suffices to remove one existential unbounded quantifier from the front of a P-bounded formula. That is, to convert ρ(x⃗) = ∃z(Q_{1}y_{1}) … (Q_{R}y_{R})β(x⃗, z, y⃗) to a P-bounded formula. But, by Assumption 3.4, for each L-formula β and for any Δ-schema δ defining β, ρ(x⃗) is equivalent to:

∃z ∃w⃗ ∈ P ∀y⃗ ∈ P (β(x⃗, z, y⃗) ↔ δ(w⃗, y⃗)) ∧ (Q_{1}y_{1}) … (Q_{R}y_{R})δ(w⃗, y⃗).

Applying the hypothesis of this proposition and induction we can convert this statement to a P -bounded formula; hence the proposition is proved. □_{3.8}

Thus, to prove our main quantifier reduction result for a pseudo-small T^{+}, we need only show the hypothesis of Proposition 3.8 holds in an |I|^{+}-saturated model M of T. In the next sections we will give separate arguments for this in the stable and not independence property cases.

4 Quantifier Reduction in Expansions by Indiscernibles: Stable Case

Throughout this section we assume M is an L-structure for a stable theory T, I is a set of L-indiscernibles (i.e. we fix Δ as {x = y}), and M is |I|^{+}-saturated. Note that since equality is in L, for the purposes of this section a basic formula is just an L-formula.

We fix β(x_{1}, …, x_{n}, z, y_{1}, …, y_{R}) ∈ L; our goal will be to show the stable part of Theorem 3.3 by showing the reduction in the hypothesis of Proposition 3.8 holds for every equality-formula δ(w⃗, y⃗). We begin by verifying Assumption 3.4, and fixing some notation in the process.

The trace of a formula ϕ(m⃗, y⃗) on I is the set of c⃗ from I satisfying ϕ(m⃗, c⃗). If M is a model of a stable theory, the trace of an L-formula on an arbitrary subset is uniformly defined with parameters in that set. If the set is a set of indiscernibles then the formula can be taken to involve only equality. In the next definition, we consider a sequence x⃗, z in two parts only for easy reference in the application.

Lemma 4.1 For every L-formula β(x⃗, z, y⃗) there is a (quantifier-free) equality formula ψ(w⃗, y⃗) satisfying: for every m⃗, b there is a c⃗_{m⃗,b} ∈ I such that

∀y⃗ ∈ P [β(m⃗, b, y⃗) ↔ ψ(c⃗_{m⃗,b}, y⃗)].

Proof. By stability ([3] III.1.24), for any formula β(x⃗, z, y⃗) there is a formula δ(w⃗, y⃗) such that for any m⃗, b, for any set F, there is a c⃗ ∈ F such that for all f⃗ ∈ F, β(m⃗, b, f⃗) ↔ δ(c⃗, f⃗). By indiscernibility, we can find an equality formula ψ(w⃗, y⃗) which is equivalent, for all w⃗, y⃗ in I, to δ. □_{4.1}

The following definitions establish crucial notation for the remainder of the proof.

Notation 4.2 (J = J_{β}) We have fixed β(x_{1}, …, x_{n}, z, y_{1}, …, y_{R}) ∈ L. Now fix an equality formula ψ(w⃗, y⃗) which provides a uniform definition for the trace of β on I^{R}. Let J = J_{β} be the length of w⃗.

Definition 4.3 1. δ(c⃗, y⃗) is correct for m⃗, d on X if for every L-tuple e⃗ ∈ X, β(m⃗, d, e⃗) ↔ δ(c⃗, e⃗).

2. Two formulas ϕ(x⃗, w_{1}, … w_{i}) and ϕ′(x⃗, w_{1}, … w_{i}) are called w⃗, I-equivalent if

∀x⃗ ∀w_{1} ∈ P, … ∀w_{i} ∈ P [ϕ(x⃗, w_{1}, …, w_{i}) ↔ ϕ′(x⃗, w_{1}, …, w_{i})].

Let C and E be subsets of I. We say tp_{β}(m⃗, d/I) splits in E over every proper subset of C if for every proper subset C′ of C, there are tuples t⃗_{1}, t⃗_{2} ∈ E such that t⃗_{1} ≡_{C′} t⃗_{2} and ¬[β(m⃗, d, t⃗_{1}) ↔ β(m⃗, d, t⃗_{2})].

To establish the hypothesis of Proposition 3.8, we show the formula ∃z ∃w⃗ ∈ P ∀y⃗ ∈ P [β(x⃗, z, y⃗) ↔ δ(w⃗, y⃗)] is equivalent on M^{+} to a P-bounded formula. We introduce an auxiliary formula ψ_{δ}(x⃗, w⃗).

Definition 4.4 (ψ_{δ}) For any equality-formula δ(w_{1}, …, w_{n}, y_{1}, …, y_{R}), let ψ_{δ}(x⃗, w_{1}, … w_{n}) denote the L^{+}- formula such that, for arbitrary m⃗ and c⃗ ∈ I ψ_{δ}(m⃗, c⃗) holds if and only if the c_{i} are distinct and for some d,

1. δ(c⃗, y⃗) defines tp_{β}(m⃗, d/I) and

2. tp_{β}(m⃗, d/I) splits over every proper subset of C, where C is the range of c⃗.

Proposition 4.5 For every m⃗ there exists n ≤ J_{β} and an equality formula δ(w_{1}, … w_{n}, y⃗) such that for some c⃗ from I, ψ_{δ}(m⃗, c⃗) holds.

Proof. First, choose any set c⃗_{1} such that ψ(c⃗_{1}, y⃗) defines tp_{β}(m⃗, d/I). Then choose a minimal subset of c⃗_{1}, enumerated by c⃗, over which tp_{β}(m⃗, d/I) does not split. Now, tp_{β}(m⃗, d/I) is, in fact, defined over c⃗ (by the disjunction of the equality types over c⃗ of sequences e⃗ satisfying β(m⃗, d, e⃗)); this formula is the required δ. □_{4.5}

Let D_{J} be a finite set of equality formulas such that every equality formula δ′(w_{1}, … w_{i}, y⃗) with i ≤ J = J_{β} is equivalent to one in D_{J}. Applying Proposition 4.5, we see that for each δ(w⃗, y⃗) there is a subset S of D_{J} such that for all m⃗ in M, we have M^{+} ⊧ ∃w⃗ ∈ P ∃z ∀y⃗ ∈ P [β(m⃗, z, y⃗) ↔ δ(w⃗, y⃗)] if and only if M^{+} ⊧ ⋁_{δ′∈S} ∃w⃗ ∈ P ψ_{δ′}(m⃗, w⃗). It follows that the hypothesis of Proposition 3.8 and thus Theorem 3.3 for the stable case follow from

Lemma 4.6 (Goal Lemma for Stable Case) For each L-formula β(x⃗, z, y⃗) and each equality formula δ(w_{1}, … w_{n}, y⃗) with lg(w⃗) ≤ J_{β}, ψ_{δ}(x⃗, w⃗) is w⃗,I equivalent to a P-bounded formula. That is, there is P-bounded ψ′(x⃗, w⃗) such that:

T^{+} ⊧ ∀x⃗ ∀w⃗ ∈ I [ψ_{δ}(x⃗, w⃗) ↔ ψ′(x⃗, w⃗)].

We will prove Lemma 4.6, by downward induction on the length of w⃗, starting at J_{β}. We first need the following observation.

Proposition 4.7 If tp_{β}(m⃗, d/I) does not split over X_{0} ⊂ I, δ(c⃗, y⃗) is correct for m⃗, d on X ⊃ X_{0}, and |X − X_{0}| ≥ R then δ(c⃗, y⃗) defines tp_{β}(m⃗, d/I).

Proof. If tp_{β}(m⃗, d/I) does not split over X_{0} then tp_{β}(m⃗, d/I) is defined over X_{0}. This definition is equivalent to δ since every equality type of an R-tuple over X_{0} is realized in X and tp_{β}(m⃗, d/I) does not split over X_{0}.

□_{4.7}

4.1 Inductive proof of Lemma 4.6

We now start the proof of Lemma 4.6. We have fixed β and J = J_{β} in Notation 4.2. We begin with the base case, n = J. Let J′ = max{J + R, 2JR} + 1.

Definition 4.8 (ψ′_{δ}) Let ψ′_{δ}(x⃗, w_{1}, …, w_{J}) hold of m⃗, c⃗ if and only if the c_{i} are distinct and there exist E = {e_{1}, …, e_{J′}} containing C, the range of c⃗, and a d such that

1. tp_{β}(m⃗, d/I) splits in E over every proper subset of C,

2. and δ(c⃗, y⃗) is correct for m⃗, d on E .

Since the arbitrary d is chosen after the set E is selected from P and the conditions i) and ii) are expressible in L, ψ′_{δ} is a P-bounded formula.

Claim 4.9 ψ′_{δ}(m⃗, c⃗) holds if and only if ψ_{δ}(m⃗, c⃗) holds.

That is, ψ′_{δ} holds if and only if there is some d such that δ(c⃗, y⃗) defines tp_{β}(m⃗, d/I) and tp_{β}(m⃗, d/I) splits over every proper subset of c⃗.

Proof of Claim 4.9. The implication from ψ_{δ} to ψ′_{δ} is immediate, since we can always witness all the necessary splittings with 2JR ≤ J′ elements.

Suppose the converse fails. Then we have a C = {c_{1}, … c_{J}} , E = {e_{1}, … e_{J′}} containing C and m⃗, d satisfying ψ′_{δ} for which the β-type of m⃗, d over I is not given by δ. By the definition of J, we know that there is a set S ⊆ I of size at most J such that the β-type of m⃗, d over I is definable over S. If S is contained in E, then we are done by Proposition 4.7, since the size of E guarantees that it contains R elements not in S . So assume that S − E is nonempty. Then S − C is nonempty, and since |S| ≤ |C| = J we infer there is a c_{0} in C − S.

Letting C_{0} = C − {c_{0}}, we know, by assumption that there is a splitting over C_{0} with witness tuples t_{1} and t_{2} lying completely in E. Let t′_{1} and t′_{2} be obtained from t_{1} and t_{2} by replacing any occurrence of c_{0} with an element in E −(C ∪S). Such elements exist since the size of E is bigger than 2J. Since c_{0} ∉ S, we have t_{i} ≡_{S} t′_{i}. As tp_{β}(m⃗, d/I) does not split over S, this implies that t′_{1} and t′_{2} still witness a split for tp_{β}(m⃗, d/I) over C_{0}.

But t′_{1} and t′_{2} are contained in E and have the same equality type over C ( they have the same equality type over C_{0} since the t_{i}’s did, and neither of them contains c_{0}). Hence, δ(c⃗, y⃗) must agree on t′_{1} and t′_{2}. This and the last sentence in the previous paragraph contradict the fact that δ(c⃗, y⃗) is correct on E. □_{4.9}

For n = J(= J_{β}) we have found an appropriate P -bounded formula ψ′_{δ} which is equivalent to ψ_{δ}. We turn to the induction step. Suppose we have Lemma 4.6 for each i with n < i ≤ J; we will prove that ψ_{δ}(x⃗, w_{1}, … w_{n}) is w⃗, I-equivalent to a P-bounded formula. The result follows easily from

Proposition 4.10 There is an n′ such that for any m⃗ and C = {c_{1}, … c_{n}}, ψ_{δ}(m⃗, c⃗) if and only if the c_{i} are distinct and for every set G with |G| < n′, there is a set E of size at most J′′ = max(n′ + 2JR + 1, 3J + 1) containing G and a d such that tp_{β}(m⃗, d/I) equality splits in E over every proper subset of C, and δ(c⃗, y⃗) is correct for m⃗, d on E.

Since the clauses after ‘and a d such that’ are definable in L this proposition provides a P-bounded formula equivalent to ψ_{δ}.

Proof of Proposition 4.10. The implication from ψ_{δ}(m⃗, c⃗) is immediate for any n′ taking E to be G plus 2JR witnesses for splitting. We will choose n′ below so the converse holds.

We first need some further notation to employ the induction hypothesis. For n < j ≤ J, let DEF (j) denote the set of equality formulas δ′(w_{1}, …, w_{j}, y⃗) in w_{1}, …, w_{j} and y_{1}, …, y_{R}. Note that up to equivalence DEF (j) is finite.

Let p(n, r) be a function such that for any finite subset A of I there is a set A′ ⊆ I with |A′| < p(|A|, r) such that all ({=}, r)-types over A are realized in A′. It is easy to see that for equality one such function is n + r.

For each δ′ ∈ DEF (j) we know that ψ_{δ′}(x⃗, w⃗) is w⃗, I-equivalent to a P-bounded formula. By Lemma 3.5, each ψ_{δ′}(x⃗, w⃗) type over I has a P-bounded defining schema. Let m′ be the number of parameters which occur in any of these definitions, Now choose n′ = p(m′ + J, R). We show that this n′ suffices for Proposition 4.10.

Let a⃗ = ⟨a_{1}, …, a_{m′}⟩ (not necessarily distinct) from I be such that for each δ′ ∈ DEF (j), the ψ_{δ′}(x⃗, w⃗)-type of m⃗ over I is definable (by an equality-formula) over a_{1}, …, a_{m′}. Such an a⃗ exists because the trace on I of a P -bounded formula is definable in equality (as shown in the proof of Corollary 3.6).

Let G be a finite set of size at most n′ such that every ({=}, R + J)-type over a⃗c⃗ is realised in G.

We now apply the hypothesis of Proposition 4.10 to this G. Then we have a⃗c⃗ ⊂ G ⊂ E ⊂ I, and a d such that tp_{β}(m⃗, d/I) splits in E over every proper subset of c⃗ and δ(c⃗, y⃗) is correct for m⃗, d on E. We claim that δ(c⃗, y⃗) is correct for m⃗, d on I so ψ_{δ}(c⃗, m) holds. Suppose not. Then δ(c⃗, y⃗) does not define tp_{β}(m⃗, d/I). By Proposition 4.7, since δ(c⃗, y⃗) is correct on G and G contains c⃗ as well as R elements not in c⃗, there must be a β-split for m⃗, d over c_{1}, …, c_{n}.

We now note the following:

Claim 4.11 There are c_{n+1}, …, c_{H}, with H ≤ J, such that tp_{β}(m⃗, d/E) splits over every proper subset of c_{1}, …, c_{H} but not over c_{1}, …, c_{H}.

Proof of claim: We know that there is S = {s_{1}, …, s_{H}} with H ≤ J such that tp_{β}(m⃗, d/E) is equality-defined over S. We will show that each c_{i} for i ≤ n must be in this set S so for i > n we can take s_{i} for the required c_{i}. Suppose not and fix c in C but not in S. Let e⃗_{1}, e⃗_{2} in E realize a splitting over C − {c}: that is, e⃗_{1} and e⃗_{2} have the same equality type over C − {c} but ¬[β(m⃗, d, e⃗_{1}) ↔ β(m⃗, d, e⃗_{2})].

We first show that e⃗_{1}, e⃗_{2} can be taken to exclude c. Since there is no splitting for tp_{β}(m⃗, d/E) over S and c ∉ S, we can replace c in the e⃗_{i}’s by any other element of E distinct from c and the other elements of S without changing the truth value of β(m⃗, d, e⃗_{i}). So we may assume that the original e⃗_{1}, e⃗_{2} do not contain c. Hence we now know e⃗_{1}, e⃗_{2} have the same equality type over C, since they agree on C − {c} and neither contains c.

But there is no splitting for tp_{β}(m⃗, d/E) over C either, since δ(c⃗, y⃗) is correct on E; hence we can uniformly replace any elements of e⃗_{1} and e⃗_{2} that are in S − C by elements of E − (C ∪ S) without changing the truth value of β(m⃗, d, e⃗_{i}) (note that there are at most |S| ≤ J elements to replace and E − (C ∪ S) contains more than J elements to replace these elements with). Thus, we can assume that e⃗_{1} and e⃗_{2} contain only elements of S that are in C. However, we now have that e⃗_{1} and e⃗_{2} agree on all elements of S, since they agree on C and have no elements from S − C. This contradicts the fact that tp_{β}(m⃗, d/E) does not equality-split over S. □_{4.11}

Note that tp_{β}(m⃗, d/I) is defined by δ′(c_{1}, …, c_{H}, y⃗), where δ′ is an equality formula.

Claim 4.12 Fix any {b_{n+1}, … b_{H}} ⊆ I and d such that tp_{β}(m⃗, d/I) is defined over C^{+} = {c_{1}, … c_{n}, b_{n+1}, … b_{H}} by δ′(c_{1}, … c_{n}, b_{n+1}, … b_{H}, y⃗). For any sequence of distinct elements f⃗ of length R in I, if f⃗ ∩ {b_{n+1}, … b_{H}} ⊆ G then [β(m⃗, d, f⃗) ↔ δ(c_{1}, … c_{n}, f⃗)].

Proof. Consider a counterexample f⃗: f⃗ ∩ {b_{n+1}, …, b_{H}} is contained in G and ¬[β(m⃗, d, f⃗) ↔ δ(c_{1}, … c_{n}, f⃗)]. Since there is no β-split for m⃗, d over C^{+}, we know ¬[β(m⃗, d, f⃗′) ↔ δ(c_{1}, … c_{n}, f⃗′)] for any f⃗′ ∈ I with f⃗′ ≡_{C^{+}} f⃗. Since E realizes every R + J type over C, we can choose an f⃗′ ∈ E with f⃗′ ≡_{C} f⃗ and f⃗ ∩ G = f⃗′ ∩ G. But f⃗ ∩ {b_{n+1}, …, b_{H}} is contained in G. So f⃗′ ≡_{C^{+}} f⃗. This contradicts the hypothesis that δ(c⃗, y⃗) is correct for m⃗, d on E. □_{4.12} Now we claim:

Claim 4.13 Given any finite subset S of I, there is a d_{S} in M such that for all f⃗ ∈ S, β(m⃗, d_{S}, f⃗) ↔ δ(c_{1}, …, c_{n}, f⃗) holds.

Proof of claim 4.13. Fix any finite S ⊂ I. Replace all elements in {c_{n+1} … c_{H}}−G by distinct elements of I not in a⃗∪{c_{1} … c_{n}}∪S to choose h_{n+1}, …, h_{H} such that h_{n+1}, …, h_{H} ≡_{a⃗c⃗} c_{n+1}, … c_{H} and H = {h_{n+1}, …, h_{H}}−G is disjoint from S. (This is easy since a⃗ ∪ {c_{1} … c_{n}} is contained in G.) Then, ψ_{δ′}(m⃗, c_{1}, …, c_{n}, h_{n+1}, … h_{H}) holds, since the ψ_{δ′}-type of m⃗ does not equality-split over a⃗. By the definition of ψ_{δ′}, there is a d_{S} such that for any tuple of distinct elements f⃗ ∈ I, ⊧ [β(m⃗, d_{S}, f⃗) ↔ δ′(c_{1}, …, c_{n}, h_{n+1}, … h_{H}, f⃗)]. Claim 4.12 implies β(m⃗, d_{S}, f⃗) ↔ δ(c_{1}, …, c_{n}, f⃗) holds whenever f⃗ ∩ H is empty. But S ∩ H = ∅, so β(m⃗, d_{S}, f⃗) ↔ δ(c_{1}, …, c_{n}, f⃗) holds for all f⃗ ∈ S as required; this completes the proof of Claim 4.13. □_{4.13}

Claim 4.13 and compactness and the saturation of M^{+} provide a d to witness ψ_{δ}(m⃗, c_{1}, …, c_{n}). Hence we now have a proof of Proposition 4.10, and hence a proof of Lemma 4.6 and Theorem 3.3 for the stable case. □_{4.10}

5 Type definability in theories without the independence property

In this section we prove a definability result for types over sequences of order indiscernibles in models of a theory without the independence property. This result is a step to proving Theorem 3.3 for the ordered case. It is also of independent interest and does not depend on the hypotheses and conventions stated earlier; hence we suspend our various conventions and state explicitly the hypotheses of this section. We will apply the result in the next section to verify Assumption 3.4.

Definition 5.1 1. The formula ϕ(x⃗, y⃗) has the m-independence property in T if there exists a set of m, lg(x)-tuples b⃗_{1}, … b⃗_{m} such that for every X ⊆ m, there is an a⃗_{X} such ϕ(b⃗_{i}, a⃗_{X}) holds if and only if i ∈ X.

2. ϕ does not have the independence property in T (lacks IP, for short) just if for some integer m, ϕ(x⃗, y⃗) does not have the m-independence property in T.

3. T does not have the independence property if no ϕ has the independence property in T. A model does not have the independence property if its theory does not have it.

We work with T a complete countable L-theory which does not have the independence property. M is an arbitrary model of T. We have a set I from M linearly ordered by <, such that ⟨I, <⟩ is a sequence of order indiscernibles and is a complete dense linear order. Nothing is asserted about the properties of < on the rest of M, and we do not assume that < is in L.

The trace of a formula ϕ(m⃗, y⃗) on I is the set of c⃗ from I satisfying ϕ(m⃗, c⃗). We noted in Lemma 4.1 that if M is a model of a stable theory, the trace of an L-formula on a set of indiscernibles is uniformly defined by an equality formula with parameters in that set. We now prove the analogous result in a theory without the independence property: defining the trace of a formula on a sequence of order indiscernibles by an order formula with parameters from the indiscernibles. It appears that this definability result is new even in the extremely restricted case that one assumes T is a O-minimal theory and I is a sequence of indiscernibles that is complete for the given order. The definability result is:

Theorem 5.2 If M lacks IP and I is order-indiscernible with order type a complete dense linear order then for every L-formula ϕ(x⃗, y⃗) there is a <-formula ψ(w⃗, y⃗) such that for every m⃗ there is a c⃗m⃗ ∈ I such that

∀y⃗ ∈ P [ψ(c⃗m⃗, y⃗) ≡ ϕ(m⃗, y⃗)].

Note: We prove the lemma above assuming that I is ordered by a complete dense linear order. However, the above statement is a property of the theory of (M, I), and so it remains true in any model (M′, I′) elementary equivalent to such an (M, I). Thus, we can apply it to any pseudo-small structure.

Marker and Steinhorn [27] and Pillay [30] proved an analogous result: in an o-minimal theory, types over a model which is Dedekind complete are definable. We ask whether this result holds for any theory without the independence property where the models are linearly ordered.

The following definitions are needed before beginning the proof of Theorem 5.2. Let S ⊆ I^{n} for some n. We say e⃗ ∈ I^{n} is a boundary point of S if there are points in S and S^{c} in every neighborhood of e⃗ in the product topology on I^{n}: i.e. if it is on the topological boundary of S in the usual sense. Given a finite set of points F in I^{n}, an equivalence class for F is the set of points in I^{n} satisfying some complete 1-type in < over F; i.e. a maximal set of points in I^{n} satisfying all the same inequalities over F. If c⃗_{1}, …, c⃗_{i−1} is a sequence of vectors from I^{R}, we denote by C_{i} the union of the ranges of the c⃗_{j}, for j < i. Note that an equivalence class for F is definable in < over F and is a connected (in the product topology) subset of I^{n}. This is because a complete dense linear order is connected (Completeness implies that every open set S is a union of disjoint intervals that are maximal in S. This plus density easily implies connectedness). Since every equivalence class is a product of intervals, and an interval within a complete order is complete, we get the above.

The key definition is:

A coherent sequence of boundary points for a set S is a (finite or infinite) sequence of vectors c⃗_{1}, …, c⃗_{n} … from I^{n} such that any c⃗_{i} is a boundary point of S ∩ E_{i} relative to the subspace topology in E_{i}, where E_{i} is the equivalence class of c⃗_{i} over C_{i}. Put another way: a sequence is coherent if for any neighborhood O of c⃗_{i} in I^{n}, O ∩ E_{i} intersects both S and S^{c}.

A boundary point cover for S is a maximal coherent sequence of boundary points for S.

We say the m-tuples ⟨p_{i} : i < ω⟩ are pairwise disjoint if their ranges are disjoint.

We actually prove the following proposition, which entails Theorem 5.2.

Proposition 5.3 Let S be an L-definable subset of I^{R}, where I is a sequence of indiscernibles in a model M without the independence property. Then the following hold.

1. Every finite coherent sequence of boundary points for S extends to a finite boundary point cover for S.

2. If C is a finite boundary point cover for S, then S is definable from < over C, and hence S does not split over the union of all elements in C.

3. For any formula θ(x⃗, y⃗) from L, there is an integer K_{θ} that bounds the size of a coherent set of boundary points for the set {y⃗ : θ(y⃗, m⃗)} uniformly for every m⃗ in M.

The following (which does not require completeness of the order) is the key result.

Lemma 5.4 Suppose γ(x_{1} … x_{R}, y⃗) does not have the independence property in T. There is K such that for any a⃗, there cannot be a coherent sequence ⟨p⃗_{i} : i < K⟩ of boundary points for D = {b⃗ ∈ I^{R} : γ(b⃗, a⃗)}.

Proof of Lemma 5.4: Suppose γ does not have the m-independence property. Choose K large enough so that: for any sequence ⟨p⃗_{i} : i ∈ K⟩ we can choose a subsequence with length m whose elements all realize the same <-type over the empty set and such that the type of the ordered pair of vectors ⟨p⃗_{i}, p⃗_{j}⟩ is independent of i and j (subject to i < j). Such a K exists by Ramsey’s theorem, and we claim that this K works. Suppose not, and consider a coherent sequence ⟨p⃗_{i} : i ∈ K⟩ for a set D ⊂ I^{R} of the form {b⃗ : γ(b⃗, a⃗)}. Replace the sequence with a subsequence ⟨p⃗_{i} : i ∈ m⟩ satisfying the additional restrictions just described. Note that coherence implies that any neighborhood of p⃗_{i} contains elements of D and D^{c} that are of the same type as p⃗_{i} over P_{i−1}.

Let E_{i} be the equivalence class of p⃗_{i} over P_{i−1}. Let s be the set of indices k < R such that p⃗_{i}(k) = p⃗_{i+1}(k) holds for some (hence all, by the property of the chosen subsequence) i. Let t = s^{c}, let g⃗ be the common value of the p⃗_{i}|s, and let Dg⃗ be {f⃗ ∈ I^{t} : f⃗ ∪ g⃗ ∈ D}. Since ⟨p⃗_{i} : i ∈ m⟩ is a coherent sequence of boundary points for D, we get p⃗_{i}|t is a coherent sequence of boundary points for Dg⃗. Moreover, since every pair ⟨p⃗_{i}, p⃗_{j}⟩ for i < j has the same type, the p⃗_{i}|t are pairwise disjoint. (If p⃗_{i}(k) = p⃗_{j}(n) for some i ≠ j, k ≠ n, then p⃗_{i}(k) = p⃗_{j}(n) for all i ≠ j, and hence p⃗_{i}(k) = p⃗_{j}(k), which implies k is in s). The fact that p⃗_{i}|t are a pairwise disjoint coherent sequence of boundary points for Dg⃗ allows us to easily construct for any subset X of m a sequence q_{i}^{X} of elements of I^{t} such that the order type of ⟨q_{i}^{X} : i < m⟩ over the empty set does not depend on X but q_{i}^{X} ∈ Dg⃗ if and only if i ∈ X.

But now, by concatenating the above q_{i}^{X} with g⃗, we get for any subset X of m a p_{i}^{X} in I^{R} such that the order type of ⟨p_{i}^{X} : i < m⟩ over the empty set does not depend on X but γ(p_{i}^{X}, a⃗) if and only if i ∈ X.

This observation and the order indiscernibility of I shows that for each X ⊂ m there are e⃗_{1} … e⃗_{m} and a^{X} such that γ(e⃗_{i}, a^{X}) if and only if i ∈ X, which contradicts the assumption that T does not have the m-independence property. □_{5.4}

We use the following simple topological observation at several other stages in the main argument.

Observation 5.5 For any R, if X is a connected (in the product topology) subset of I^{R} and Y is a subset of I^{R} such that both X ∩ Y and X ∩ Y^{c} are nonempty then X contains a boundary point of Y.

Proof. If no point in X is a boundary-point of Y we could partition X into two open (in the product topology) sets: namely, points with an open set around them contained in Y, and points with an open set around them contained in the complement of Y. This contradicts the connectedness of X. □_{5.5}

The following is an observation about complete dense orders:

Lemma 5.6 Suppose that ⟨I, <⟩ is a complete dense linear order. If B_{i} = {b⃗_{1}, … b⃗_{i}} is a coherent sequence of boundary points of D ⊆ I^{R} then either D is quantifier-free definable in the structure ⟨I, <⟩ from parameters in (the union of the ranges of) B_{i}, or we can add a new element b⃗_{i+1} and extend the coherent sequence.

Proof. Fix such a coherent sequence B = {b⃗_{1} …, b⃗_{i}}. Partition the tuples in I^{R} according to their type over {b⃗_{1} …, b⃗_{i}}, and let E be the corresponding equivalence relation. The equivalence classes are definable from B_{i}, so if D is not definable there must be some equivalence class C that contains both points in D and points not in D.

Define g⃗ as follows. Let t ⊆ R be {j : for some c⃗ ∈ C there is k ≤ i with b⃗_{k}(j) = c⃗(j)}. For j ∈ t, let g⃗(j) = e if for some k ≤ i and some (equivalently all, since the elements of c are indiscernible over B_{i}) c⃗ ∈ C, b⃗_{k}(j) = c⃗(j) = e. Since C has at least two points, we must have t ≠ R. Let s denote the complement of t in R. Let Dg⃗ be the collection of functions r⃗ ∈ I^{s} such that r⃗ ∪ g⃗ is in D and let Cg⃗ be those r⃗ mapping s to I, such that r⃗ ∪ g⃗ ∈ C.

Since Cg⃗ is all realizations of a type over B_{i} ∪ g⃗, it is an equivalence class and is thus connected (using the completeness, as remarked in the beginning of this section); by Observation 5.5 there is a Dg⃗-boundary-point f⃗ in Cg⃗. Let b⃗_{i+1} = g⃗ ∪ f⃗ (considered as functions). Then b⃗_{i+1} is a boundary-point of D ∩ C in C as required.

□_{5.6}

This establishes all three parts of Proposition 5.3. Since T does not have the independence property, for each formula θ(x⃗, y⃗) there is, by Lemma 5.4, a bound K_{θ} on the length of a coherent sequence of boundary points for D = {i⃗ ∈ I : θ(m⃗, i⃗)}. By Lemma 5.6 every coherent sequence of boundary points extends to a maximal coherent sequence, and D is definable by a quantifier free order formula over the elements in this sequence, since the sequence is a boundary point cover. □_{5.3}

We can remove the restriction that (I, <) be a complete dense linear order if we weaken the definability conclusion. Recall that a linear order is weakly o-minimal if every definable subset is a disjoint union of convex sets.

Corollary 5.7 If M lacks IP and I is a densely ordered sequence of order-indiscernibles with order type then for every L-formula ϕ(x⃗, y⃗) the trace of ϕ on (I, <) is a disjoint union of convex sets. That is, the induced structure on (I, <) is weakly o-minimal.

Proof. Since I is a sequence of order indiscernibles we can find an elementary extension N of M and a sequence of order indiscernibles J ⊂ N such that (J, <) is the completion of (I, <). Now applying Theorem 5.2, every definable subset of J is a union of intervals. Thus, the trace on I is a union of convex sets. □_{5.7}

6 Quantifier Reduction in Expansions by Indiscernibles:

theories without the independence property

6.1 Preliminaries

Let T be an L-theory without the independence property. Fix an |I|^{+}-saturated model M of T and a complete densely ordered sequence I of order indiscernibles in M. Let M^{+} = (M, I, <) be the result of expanding M by interpreting < as < and P as I. There is no assumption that (M, I) does not have the independence property. Throughout this section T^{+} is the theory of M^{+}.

Our goal is to show the ‘order part’ of Theorem 3.3. In the context of this section, a basic formula is a Boolean combination of formulas in < and in L. Note that the trace on I of a basic formula is a Boolean combination of order formulas and the traces of L-formulas. Since the latter are order definable by Theorem 5.2, and the definition is quantifier free since the ordering is dense, we have Assumption 3.4. Hence it suffices to show that the hypothesis of Proposition 3.8 holds.

We fix a basic formula β(x⃗, d, c⃗), with the goal of showing that the reduction in the hypothesis of Proposition 3.8 holds.

Definition 6.1 For any m⃗, d in M let B_{m⃗,d} denote {c⃗ ∈ I : β(m⃗, d, c⃗)}. Fix K = K_{β} so that for any m⃗, d, a coherent sequence of boundary points for B_{m⃗,d} has at most K elements.

Definition 6.2 (ν_{δ}) For any quantifier-free order formula δ(w_{1}, …, w_{n}, y_{1}, …, y_{R}), let ν_{δ}(x⃗, w_{1}, … w_{n}) be the L^{+}-formula such that, for arbitrary m⃗ and c⃗ ∈ I we have ν_{δ}(m⃗, c⃗) holds if and only if for some d, δ(c⃗, y⃗) defines tp_{β}(m⃗, d/I).

We say a sequence b⃗_{1} … b⃗_{n} is σ-good if the union of the ranges of the b⃗_{i} is ordered so that b⃗_{1} … b⃗_{n} is a boundary point cover for the set of c⃗ ∈ I such that σ(b⃗_{1}, …, b⃗_{n}, c⃗) holds.

To prove the hypothesis in Proposition 3.8, and hence to complete the proof of Theorem 3.3 it clearly suffices to show each ν_{δ} is equivalent to a P-bounded formula. We will actually deal not with ν_{δ} directly, but with a “boundary-point” version, that is easier to induct upon.

Definition 6.3 (ρ_{σ}) Let σ(w⃗_{1} … w⃗_{n}, y_{1}, … y_{R}) be a quantifier-free order-formula in L with no parameters. Let ρ_{σ}(x⃗, w⃗_{1}, …, w⃗_{n}) hold of m⃗, b⃗_{1} … b⃗_{n} if and only if there is d in M such that b⃗_{1} … b⃗_{n} form a boundary-point cover for B_{m⃗,d}, and σ(b⃗_{1}, …, b⃗_{n}, y⃗) defines tp_{β}(m⃗, d/I).

We will prove by downward induction on n that for any <-formula σ, ρ_{σ} is equivalent to a P -bounded formula. It follows from this that every ν_{δ} is equivalent to a P -bounded formula, since

Proposition 6.4 ν_{δ}(x⃗, w_{1}, …, w_{n}) holds of m⃗, c_{1}, … c_{n} iff there are i ≤ K, b⃗_{1} … b⃗_{i} from I and σ(w_{1}, …, w_{i}, y⃗) such that

1. δ(c⃗, y⃗) and σ(b⃗, y⃗) are equivalent on I,

2. ρ_{σ}(m⃗, b⃗_{1} … b⃗_{i}) holds,

3. and ρ_{σ}(m⃗, b⃗′_{1} … b⃗′_{i}) holds for any b⃗′_{1} … b⃗′_{i} ≡C⃗ b⃗_{1} … b⃗_{i}.

Proof of Proposition: For one direction: suppose that ν_{δ}(x⃗, w_{1}, …, w_{n}) holds of m⃗, c_{1}, … c_{n}, with d a witness. Proposition 5.3 implies that there is a boundary point cover b⃗_{1}, … b⃗_{i} for the set B_{m⃗,d} with i ≤ K and a (quantifier-free) order formula σ(b⃗, w⃗) defining B_{m⃗,d}. Suppose b⃗′_{1}, … b⃗′_{i} is such that b⃗′_{1} … b⃗′_{i} ≡C⃗ b⃗_{1} … b⃗_{i}. The statement that b⃗_{1}, … b⃗_{i} is a boundary point cover for the set defined by δ(c⃗, y⃗) is equivalent, by quantifier elimination in ⟨I, <⟩, to a quantifier-free order formula in c⃗, b⃗. As b⃗′_{1} … b⃗′_{i}, c⃗ also satisfies this formula, b⃗′_{1} … b⃗′_{i} is also a boundary point cover for B_{m⃗,d}.

For the other direction: if the conclusion holds, δ(c⃗, y⃗) and σ(b⃗, y⃗) are equivalent on I and ρ_{σ}(m⃗, b⃗_{1} … b⃗_{i}) holds; thus ν_{δ}(m⃗, c⃗) holds. □_{6.4}

We prove the following lemma by reverse induction on n, the number of w variables.

Lemma 6.5 ( Goal Lemma for Order Case) Every ρ_{σ}(x⃗, w⃗) is w⃗, I equivalent to a P -bounded formula.

Since K is the limit on the size of a boundary point cover, ρ_{σ} is clearly equivalent to false when the number of variables n is greater than K. So we can use n = K + 1 as an easy base case of our induction: we proceed to the induction step.

We now assume that for each σ(w⃗_{1}, … w⃗_{i}, y⃗) with i > n, ρ_{σ}(x⃗, w⃗_{1}, … w⃗_{i}) is w⃗, I equivalent to a P -bounded formula. Here we show the same for σ(w⃗_{1}, … w⃗_{n}, y⃗). Letting E_{i} denote the equivalence class of b⃗_{i} over b⃗_{1}, … b⃗_{i−1}, the proof of the induction step will follow from:

Proposition 6.6 Suppose σ(w⃗_{1}, … w⃗_{n}, y⃗) is an order formula. Then there are n′, p′ such that for any m⃗ and b⃗ = ⟨b⃗_{1}, … b⃗_{n}⟩, ρ_{σ}(m⃗, b⃗) holds if and only if b⃗_{1} … b⃗_{n} is σ-good and for every set G with |G| < n′, and for every set of neighborhoods N_{i} around b⃗_{i}, there exist

1. for 1 ≤ i ≤ n, f⃗_{i}, g⃗_{i} in N_{i} ∩ E_{i}, 2. and a set E with |E| < p′ realizing all (<, R)-types over the union of G with the f⃗_{i}, g⃗_{i} and the endpoints

of N_{i},

3. and a d in M

such that σ(b⃗_{1}, … b⃗_{n}, y⃗) is correct for m⃗, d on E and ¬[β(m⃗, d, f⃗_{i}) ≡ β(m⃗, d, g⃗_{i})].

Using this proposition, it is clear that ρ_{σ} is equivalent to a P -bounded formula; since, fixing such an n′ and p′, the formula expressing the conclusion can be expressed as a P -bounded formula.

Let m′ be the sum of the sizes of the defining schema for each ρ′_{σ}, as σ varies over <-formulas with variables w⃗_{1}, … w⃗_{K} and y. Such an m′ exists by the induction hypothesis and Lemma 3.5.

Let n′ = (m′ + n + 1). Let p(n, r) be a function such that for any finite subset A of I there is a set A′ ⊆ I with |A′| < p(|A|, r) such that all ({<}, r)-types over A are realized in A′. Let p′ = p(m′, r). We will show that this n′, p′ witness Proposition 6.6. For this n′ and p′, denote the formula expressing the conclusion of Proposition 6.6 by ρ′_{σ}(m⃗, b⃗).

It is easy to see that ρ_{σ} implies ρ′_{σ}; the required witness d can always be taken to be the witness for ρ_{σ} and the existence of E and f⃗, g⃗ follow from the size of p′ and the fact that b⃗_{1} … b⃗_{n} is σ-good.

We now start the proof of the other implication. Suppose that ρ′_{σ} holds. Let η(x) denote the L-type over m⃗ ∪ I such that η(d) asserts that d is such that σ(b_{1}, … b_{n}, y) defines the β type of m⃗, d over I. It will take several pages to prove

Claim 6.7 The type η is finitely satisfiable.

Proof of Claim 6.7. Let η_{0} be a finite subset of η, and let S be all the constants mentioned in η_{0}. Choose G so that b⃗ = ⟨b⃗_{1}, … b⃗_{n}⟩ is contained in G and for each i with K ≥ i > n and every i-variable <-formula σ(w⃗_{1}, …, w⃗_{i}, y⃗), the ρ_{σ}(x⃗, w⃗_{1}, …, w⃗_{i})-type of m⃗ over I is definable over G.

Choose rectangular neighborhoods N_{i} of the b⃗_{i} for 1 ≤ i ≤ n to separate the b⃗_{i}’s from the elements of G ∪ S that are distinct from b⃗_{i}: that is, choose both the upper u⃗_{i} and lower endpoints l⃗_{i} of N_{i} so that no element of G ∪ S lies in (l⃗_{i}(m), b⃗_{i}(m)) or (b⃗_{i}(m), u⃗_{i}(m)).

Applying the hypothesis of Proposition 6.6 to this G and ⟨N_{i} : i ≤ n⟩, and by the choice of p′, we get the corresponding f⃗_{i}, g⃗_{i}, E and d_{0}. That is, f⃗_{i}, g⃗_{i} ∈ N_{i} ∩ e_{i}, σ(b⃗_{1}, …, b⃗_{n}, y) is correct for B_{m⃗,d_{0}} on E and E realizes all (<, R)-types over G^{+} = G ∪ ⋃_{i}{f⃗_{i}, g⃗_{i}, l⃗_{i}, u⃗_{i}}, where N_{i} = (l⃗_{i}, u⃗_{i}) and ¬σ(b⃗, f_{i}) ↔ σ(b⃗, g_{i}). Let N denote the collection of all components of the endpoint vectors of the N_{i}.

Note that since b⃗ is σ-good, it is a coherent sequence of boundary points for σ(b⃗, y⃗).

Lemma 6.8 There is a coherent sequence of boundary points b⃗′_{i} : i ≤ n for B_{m⃗,d_{0}} such that b⃗′_{i} ∈ N_{i}.

Proof. We define the b⃗′_{i} inductively. Since B_{m⃗,d} changes sign on N_{1}, Observation 5.5 implies that N_{1} contains a boundary point b⃗′_{1}. Let E′_{i+1} denote the equivalence class of b⃗_{i+1} over b⃗′_{1}, … b⃗′_{i}. Given b⃗′_{1}, … b⃗′_{i}, we show that there is b⃗′_{i+1} ∈ N_{i+1} which is a boundary point for B_{m⃗,d} ∩ E′_{i+1}. To do this, it suffices (by Observation 5.5) to show that N_{i+1} ∩ E′_{i+1} contains two points which disagree on B_{m⃗,d}. We will do this by showing that f⃗_{i+1} and g⃗_{i+1} are in the same equivalence class for b⃗′_{1}, … b⃗′_{i}. Let B_{i} denote the union of the ranges of the b⃗_{k} for k ≤ i. We know that they are in the same class E_{i+1} over b⃗_{1}, … b⃗_{i}.

Let s be the set of indices j such that b⃗_{i+1}(j) = b⃗_{m}(n), for some m < i, n ≤ R and let e⃗ = b⃗_{i+1}|s. Then b⃗_{i+1} is a boundary point of the set H of h⃗ ∈ B_{m⃗,d} which extend e⃗ and E_{i+1} ⊆ H. In addition, f⃗_{i+1},g⃗_{i+1}, and b⃗_{i+1} all have the same restriction to s. Let t = s^{c}. Then the range b⃗_{i+1}|t is disjoint from the ranges of the b⃗_{j} for j ≤ i.

Our choice of ⟨N_{j} : j ≤ i⟩ guarantees that for each fixed j ≤ i, the endpoints l⃗_{j} and u⃗_{j} of N_{j} satisfy the same inequalities over b⃗_{i+1}|t that b⃗_{j} satisfies. Hence all points in N_{j} have the same type as b⃗_{j} over b⃗_{i+1}|t. So b⃗′_{j}, in particular, has the same type as b⃗_{j} over b⃗_{i+1}|t. Thus B′_{j} is disjoint from b⃗_{i+1}|t.

Now, the definition of N_{i+1} guarantees that for all points p⃗ in N_{i+1}, p⃗|t satisfies the same inequalities over B′_{i} that b⃗_{i+1}|t does. In particular, B′_{i} is disjoint from a⃗|t for every a⃗ in N_{i+1}. Further, f⃗_{i+1}|t and g⃗_{i+1}|t both satisfy the same inequalities over B′_{i} that b⃗_{i+1} does. Thus, f⃗_{i+1} and g⃗_{i+1} are in the same equivalence class over B′_{i} as required. □_{6.8}

Fix, by Lemma 6.8, b⃗′ = ⟨b⃗′_{i} : i ≤ n⟩ with b⃗′_{i} ∈ N_{i} and b⃗′ a coherent sequence of boundary points for B_{m⃗,d_{0}}.

We argue that if b⃗′ is a maximal coherent sequence of boundary points for B_{m⃗,d_{0}}, then d_{0} realizes η. For then, there is no splitting for B_{m⃗,d_{0}} over b′_{1}, … b′_{n} (i.e. tp_{β}(m⃗, d_{0}/I) does not split over b′_{1}, … b′_{n}). This implies σ(b⃗, y) is correct for m⃗, d_{0} on S. To see this implication, choose for q⃗ ∈ S an e⃗ ∈ E which realizes the same <-type as q⃗ does over G^{+}. Note that, in particular, e⃗ and q⃗ have the same <-type over N and the same <-type over b⃗. But now the fact that the N_{i} separates elements of S − B from B (where B is the range of b⃗) and the fact that b⃗′_{i} lies in N_{i} gives us that tp_{<}(e⃗/b⃗′) = tp_{<}(q⃗/b⃗′): e.g. if e⃗(j) > b⃗′_{i}(k) then there is an endpoint u⃗ of N_{i} such that e⃗(j) > u⃗(j) > b⃗′_{i}(k) and hence q⃗(j) > u⃗(j) > b⃗′_{i}(k), since e⃗ and q⃗ have the same order-type over N. Now, tp_{<}(e⃗/b⃗) = tp_{<} (q/b⃗) implies σ(b⃗, q⃗) ↔ σ(b⃗, e⃗) and σ(b⃗, e⃗) holds if and only if e⃗ ∈ B_{m⃗,d_{0}} as σ(b⃗, y⃗) is correct for m⃗, d_{0} on E. Since there is no splitting for B_{m⃗,d_{0}} over b′_{1}, … b′_{n}, tp_{<}(e⃗/b⃗′) = tp_{<}(q⃗/b⃗′) implies e⃗ ∈ B_{m⃗,d_{0}} if and only q⃗ ∈ B_{m⃗,d_{0}}. Thus, σ(b⃗, y⃗) is correct for m⃗, d_{0} on S and so d_{0} realizes η as required.

Hence, we reduce to assuming b⃗′_{1}, … b⃗′_{n} are not a boundary point cover for B_{m⃗,d_{0}}. By Proposition 5.3 1), these extend to a boundary point cover B^{+} = {b⃗′_{1} … b′_{H}} for B_{m⃗,d_{0}}, with n < H ≤ K. By the choice of B′ = {b′_{n+1}, …, b′_{H}}, some σ′(b′_{1}, …, b⃗′_{H}, y⃗) defines tp_{β}(m⃗, d_{0}/I).

We now want to make use of our induction hypothesis on σ′(b′_{1}, …, b⃗′_{H}, y⃗). Namely, we know that since H > n, the ρ_{σ′} type of m⃗ over I is definable over G. This will be eventually applied in Claim 6.11. Before continuing the argument, we establish a canonical representation for equivalence classes with respect to the order. An equivalence class for some set W, i.e. a complete order type in variables y_{1} … y_{R} over W, is specified by a list of intervals {I_{k} : k ≤ R} with endpoints in W where each I_{k} is either open or a singleton, plus an ordering among the variables y_{1} … y_{R}. This specifies that the class is the intersection of a product of the {I_{k} : k ≤ R}, with the set of R-tuples satisfying the type over ∅ given by the ordering. Given an equivalence class t, we will call the sequence {I_{k} : k ≤ R} the interval sequence for t. Note that in the above definitions, we are talking about intervals I_{k} in the ordering on I, not subsets of I^{R} as in the previous paragraphs. We will refer to an interval with endpoints that are consecutive elements s_{i}, s_{i+1} from some set S = {s_{1}, … < s_{i} < s_{i+1} … < s_{p}} as an S-interval. Given an S-interval I and a function f with domain S, we will talk about the f-image of the interval: namely, the interval whose endpoints are the f-images of the endpoints of I, and which is of the same type as I (half-open, open, etc.). Given a point x in I, the S-interval of x means the smallest S-interval that contains x.

We call a Gb⃗′ interval which is either open or a singleton and that contains an element of E a nice interval. We now note the following

Lemma 6.9 1. If e is an equivalence class for Gb⃗′, and the interval sequence for e contains only nice intervals, then σ′(b⃗′, y⃗) agrees with σ(b⃗, y⃗) on e.

2. Suppose we have a map f on Gb⃗′ that is the identity on G and maps b⃗′ bijectively onto b⃗′′, and such that tp_{<}(b⃗′/G) = tp_{<}(b⃗′′/G). If e is an equivalence class for Gb⃗′′, and the interval sequence for e contains only intervals that are the f-images of nice intervals, then σ′(b⃗′′, y⃗) agrees with σ(b⃗, y⃗) on e.

Proof of Lemma 6.9. To see part 1), notice that σ′(b⃗′, y⃗) and σ(b⃗, y⃗) are constant on any Gb⃗′ equivalence class, in particular on e. Since the interval sequence for e contains only nice intervals, e contains a tuple from E, and σ′(b⃗′, y⃗) and σ(b⃗, y⃗) must agree on this tuple, hence they agree on the whole class.

Part 2) follows from 1) by transferring from Gb⃗′ to Gb⃗′′, noting that the assertion that σ′(b⃗′, y⃗) and σ(b⃗, y⃗) agree on specified intervals with endpoints in Gb⃗′ is part of the type of b⃗′ over Gb⃗. □_{6.9}

Now we will construct a sequence b⃗′′ and a function f so that we can apply part 2) to get the equivalence of σ(b⃗′′, y⃗) and σ(b⃗, y⃗) on all R-tuples from S. We define a function f fixing G (and thus fixing b⃗_{i} for i ≤ n) and mapping b⃗′_{j} to f(b⃗′_{j}) = b⃗′′_{j}. Let {g_{1}, … g_{s}} enumerate G in increasing order, and let g_{0} = −∞, g_{s+1} = ∞. We will define f by cases, looking at the part of Gb⃗′ in each interval (g_{i}, g_{i+1}). For i ≤ s + 1 do the following:

Find a nice Gb⃗′ interval contained in the interval (g_{i}, g_{i+1}). Such an interval (l, u) exists, since E realizes all (<, R)-types over G. If l is not g_{i}, then let f(l) be an element in I lying above g_{i} but below all elements of S in (g_{i}, g_{i+1}). Similarly, if u is not g_{i+1}, then let f(u) be an element in I lying below g_{i+1} but above all elements of S in (g_{i}, g_{i+1}). Define f on the rest of the elements of b⃗′ in (g_{i}, g_{i+1}) so that the order type of Gb⃗′ is preserved. That is, preserve the ordering among the elements of b⃗′ but move all of the elements of b⃗′ ∈ (g_{i}, g_{i+1}) that were strictly below l to the interval (g_{i}, f(l)) and move all b⃗′ ∈ (g_{i}, g_{i+1}) that were above u to the interval (f(u), g_{i+1}). Let f be the identity on the endpoints g_{i}, g_{i+1}.

This completes the construction of b′′. The construction for (g_{1}, g_{2}) is illustrated in Figure 6.1.

It is clear that the resulting b⃗′′ has the same type as b⃗′ over G. We now note the crucial property of this construction.

Observation 6.10 For every R-tuple h⃗ from S, let the Gb⃗′′ equivalence class of h⃗ have interval sequence J_{1}, …, J_{R}. Then each J_{k} is the image under the function f of a nice interval.

Proof: Let i ≤ R be given. We will show that h⃗(i) is in the image of a nice interval. If h⃗(i) is in the interior of its G-interval then the construction guarantees that the Gb⃗′′-interval containing h⃗(i) is the image of a nice interval. If h⃗(i) is an endpoint of its G-interval, then h⃗(i) is in G, hence in E, hence {h⃗(i)} is itself a nice interval. The construction guarantees that f maps every element of b⃗′ ∩ G to itself, hence h⃗(i) is again in the f-image of a nice interval. □_{6.10}

We now put these constructions together to show the finite satisfiability of η.

Claim 6.11 For any finite subset S of I and set of neighborhoods N_{i} about b⃗_{i} for i ≤ n, there is a d_{S} in M and a sequence f⃗_{i}, g⃗_{i} for i ≤ n in N_{i} such that for all f⃗ ∈ S, β(m⃗, d_{S}, f⃗) ↔ σ(b_{1}, …, b_{n}, f⃗) holds and ¬(σ(b⃗, f⃗_{i}) ↔ σ(b⃗, g⃗_{i})) holds for each i ≤ n.

Proof of Claim 6.11: The f⃗_{i}, g⃗_{i} for i ≤ n that are required in the conclusion of the claim are the f⃗_{i}, g⃗_{i} : i ≤ n chosen at the beginning of the proof of Claim 6.7. Let b⃗′′ be as constructed just before Observation 6.10.

We argue that ρ_{σ′}(m⃗, b⃗′′_{1}, …, b⃗′′_{n}, b⃗′′_{n+1}, … b⃗′′_{H}) holds. The ρ_{σ′}-type of m⃗ over I is definable by a P -bounded formula over G, by the defining property of G, and since G ⊂ I this formula is equivalent over I to a <- formula. Hence the ρ_{σ′}-type of m⃗ over I does not <-split over G. But ρ_{σ′}(m⃗, b⃗′_{1}, …, b⃗′_{H}) holds, and hence ρ_{σ′}(m⃗, b⃗′′_{1}, …, b⃗′′_{n}, b⃗′′_{n+1}, … b⃗′′_{H}) does also, since b⃗′′ and b⃗′ have the same <-type over G.

Figure 1: The Construction of the mapping f from Gb⃗′ to Gb⃗′′.

Now, by the definition of ρ_{σ′}, we get a d_{S} such that for any tuple of distinct elements f⃗ ∈ I, ⊧ [β(m⃗, d_{S}, f⃗) ↔ σ′(b⃗′′, f⃗)]. Since g⃗, b⃗′_{1}, … b⃗′_{H} and g⃗, b⃗′′_{1}, … b⃗′′_{H} satisfy the same quantifier free order type, σ′(b⃗′′, y⃗) agrees with σ(b⃗, y⃗) on the image of the g⃗b⃗′-equivalence classes on which σ′(b⃗′, y⃗) agrees with σ(b⃗, y⃗). quantifier-free order type: By the construction of b⃗′′, these classes include every R-tuple from S. So we have β(m⃗, d_{S}, f⃗) ↔ σ(b⃗_{1}, …, b⃗_{n}, f⃗) holding for all f⃗ ∈ S. This completes the proof of Claim 6.11. □_{6.11}

Claim 6.11 implies Claim 6.7, the type η is finitely satisfiable, which completes the proof of Proposition 6.6. This finishes the proof that the hypothesis of Proposition 3.8 is satisfied. Hence Theorem 3.3 for theories without the independence property is proved. □_{6.7, 6.6, 3.3}

7 Applications of the Quantifier Reduction Results to Query Collapse Theorems

We now apply the results on reductions of indiscernibles proved in the previous sections. We apply them to prove the expressivity results on embedded finite structures stated in Section 2, and also to prove a number of other interesting facts about expansions of models by indiscernibles. We start in Subsection 7.1 by stating a consequence of the reductions that captures all we actually need from the previous sections for the query collapse statements. Subsection 7.2 starts the applications to query collapse; we present a lemma allowing us to concentrate a number of finite partial counterexamples into a single infinite counterexample. Then we combine that result with the extension result of the previous section to prove the main collapse results stated at the beginning of the paper.

7.1 Extending Maps on Indiscernibles

We need to fix some notation. Recall that a partial L-isomorphism from a structure A to a structure B is an injective map from a subset of A to B which preserves relations from L. We recall the term ‘partially isomorphic’ from [12] and [10], which is also referred to as ‘back-and-forth equivalence’ [18].

Definition 7.1 For any language L, two L-structures A and B are partially L-isomorphic, written A≈_{L,p}B if there exists a non-empty family J of partial L-isomorphisms which have the back and forth property: for each j ∈ J and x in A or B there is j′ ∈ J that extends j with x in the domain or range of the graph of j′.

Note that if A≈_{L,p}B, then A and B are elementarily equivalent in any sublanguage of L.

Notation 7.2 Let I be a subset of N and let L^{∗} be the expansion of L^{+} by constants {c_{α} : α < |I|}. Fix a permutation g of I and an enumeration {a_{α} : α < |I|} of I. Then N_{1}^{g} is the expansion of N where c_{α} is interpreted as a_{α} and N_{2}^{g} is the expansion of N where c_{α} is interpreted as g(a_{α}). We will omit the g if it is fixed in context.

Note that N_{1}≈_{L^{∗},p}N_{2} implies that the partial isomorphisms in the back-and-forth system can be taken to all extend g.

Here is the result that is relevant for collapse theorems:

Theorem 7.3 Let N be a model that is stable (does not have the independence property) and I be a set (sequence) of (order) indiscernibles. Suppose that (N, I) is pseudo-small and that (N, I) is ω_{1}-saturated.

For any permutation g on I (order-preserving permutation of I),

N_{1}^{g}≈_{L^{∗},p}N_{2}^{g}.

Proof: We use Δ to mark whether we are in the order or equality case. Note that in the order case, pseudosmall requires the (N, I) to be elementarily equivalent to (N′, I′), where I′ is an order-indiscernible sequence of complete dense order type. The quantifier-reduction results proved in Section 6 are all properties of the L^{+}-theory, and hence carry over from small (N′, I′) to pseudo-small (N, I).

It suffices to show the collection of pairs of finite sequences ⟨a⃗, b⃗⟩ such that ⟨N_{1}, a⃗⟩ is L^{∗}-elementary equivalent to ⟨N_{2}, b⃗⟩ form a back-and-forth system. So suppose ⟨N_{1}, a⃗⟩ is L^{∗}-elementarily equivalent to ⟨N_{2}, b⃗⟩, and a′ is an element of N_{1}. We shall find b′ such that ⟨N_{1}, a⃗, a′⟩ is L^{∗}-elementarily equivalent to ⟨N_{2}, b⃗, b′⟩.

It suffices to find, a b′ such that for each ρ(x, w⃗, v⃗) in L^{+}, the g-image of the ρ(x, w⃗, v⃗)-type of a′, a⃗ over I is the same as the ρ(x, w⃗, v⃗)-type of b′, b⃗ over I.

By Corollary 3.6, we know that there is a quantifier-free Δ-formula γ_{ρ}(v⃗, v′) such that the ρ-type of a′, a⃗ over I is definable by an instance of γ_{ρ}. That is, there is i⃗_{ρ} ∈ I such that for each c⃗ ∈ I γ_{ρ}(c⃗, i⃗_{ρ}) holds if and only if ρ(a′, a⃗, c⃗). Let j⃗_{ρ} be g(i⃗_{ρ}). Since ⟨N_{1}, a⃗⟩ is L^{∗}-elementarily equivalent to ⟨N_{2}, b⃗⟩, and ⟨N_{1}, a⃗⟩ satisfies ∃x∀v⃗ ∈ P (γ_{ρ}(v⃗, i⃗_{ρ}) ↔ ρ(x, w⃗, v⃗)), we have ⟨N_{1}, b⃗⟩ satisfies ∃x∀v⃗ ∈ P (γ_{ρ}(v⃗, j⃗_{ρ}) ↔ ρ(x, w⃗, v⃗)). Let I_{0} be the union of the ranges of all the sequences i⃗_{ρ} and let q(x) be the type over I_{0} ∪ {a⃗} containing the formulas ∀v⃗ ∈ P (γ_{ρ}(v⃗, i⃗_{ρ}) ↔ ρ(x, a⃗, v⃗)) for all L^{+}-formulas ρ. Then I_{0} is countable and the type g_{1}(q) (where g_{1} = g ∪ ⟨a⃗, b⃗⟩) over the countable set J_{0} ∪ {b⃗}, where J_{0} = g_{1}(I_{0}), is also consistent. So by ω_{1}-saturation of (N, I) we can choose b′ to realize g_{1}(q) and complete this part of the back-and-forth. The other direction of the back-and-forth is done by a symmetric argument, completing the theorem. □_{7.3}

7.2 Connecting Query Collapse to Indiscernibles, and Proof of the Main Collapse Theorems

We state the connection between indiscernibles and query collapse results. Specifically, we give a general model theoretic argument that applies in both the stable and not independence property case, and which connects the query collapse questions mentioned in the introduction to results about indiscernibles. This technique is implicit in [6] and is explicit — in a slightly different formalism – in [4]. The proofs presented here use elementary extension arguments patterned directly on the proof of Lindstrom’s theorem reported in [13] and somewhat reminiscent of [4], rather than nonstandard analysis as in [6].

We then use the connection results (Lemma 7.5) and the results in the previous section on definability of types over I in L^{+} to prove the expressivity results on embedded finite structures stated in Section 2, As before, we will use a parameter Δ to mark whether we are in the order or unordered case: Δ is either {=} or {=, <}.

Let M be an L∪Δ-structure with an infinite domain 𝕌. Let A⃗_{n}, B⃗_{n} be a sequence of finite relations interpreting the symbols of S in 𝕌. We will sometimes write A_{n}, B_{n} for the stucture whose universe is the union of the domains of the relations A⃗_{n}, B⃗_{n} (the active domain).

For any two S-structures A and B we write A =_{n,S,Δ} B or say the structures are n, S, Δ equivalent if the two structures agree on the first n sentences of the language with vocabulary {S ∪ Δ}. Two frequent uses of this notation will be (𝕌, A⃗_{n}) =_{n,S,Δ} (𝕌, B⃗_{n}) and A_{n} =_{n,S,Δ} B_{n} where A⃗_{n}, B⃗_{n} are finite relations on 𝕌. We will often omit Δ when it is equality and just write =_{n,S}. Note that the expressions (M, A⃗) and M(A) mean the same thing.

Remark 7.4 Since the relativization of any Δ-sentence to dom A⃗ can be expressed as a sentence about (𝕌, A⃗_{n}), for any A_{n}, B_{n} with (𝕌, A⃗_{n}) =_{n,S,Δ} (𝕌, B⃗_{n}) and A_{n} ⊧ ϕ but B_{n} ⊧ ¬ϕ there are A′_{n}, B′_{n} with finite domains contained in 𝕌 such that A′_{n} =_{n,S,Δ} B′_{n}, A′_{n} ⊧ ϕ, and B′_{n} ⊧ ¬ϕ. The converse also holds.

Recall from the first section that M =< 𝕌, …⟩ exhibits collapse to equality if every Δ-generic query definable over M is definable in the structure ⟨𝕌, =⟩.

We will consider various ‘collapse theorems’. In each case a failure to collapse will yield a family of finite structures as in the hypotheses of the next lemma. We will apply this lemma to produce a single infinite counterexample. Then we will apply the definability of types to eliminate that counterexample. In Lemma 7.5), when < is in Δ , we know only that < is a linear order of the indiscernibles; nothing is known about the behavior of < on the rest of the model.

Lemma 7.5 (Concentration Lemma) Let I be a set (Δ, L) indiscernibles in a structure M with universe 𝕌. Suppose there are finite Δ ∪ S-interpretations A⃗_{n}, B⃗_{n} with dom A_{n}, dom B_{n} ⊆ I with (I, Δ, A⃗_{n}) =_{n,S} (I, Δ, B⃗_{n}) and (M, A⃗_{n}) ⊧ ϕ and (M, B⃗_{n}) ⊧ ¬ϕ.

Then there is a model M′ of T h(M), a set of Δ-indiscernibles I′ in M′ with (M, I) ≡_{L^{+}} (M′, I′), two infinite S-interpretations T⃗ and U⃗ with domains in I′, and a map f on I′ such that f is an isomorphism from (I′, T⃗, Δ) to (I′, U⃗, Δ) but M′(T⃗) ⊧ ϕ and M′(U⃗) ⊧ ¬ϕ.

Proof. Let L^{+} = L ∪ Δ ∪ {P} where P is a new unary predicate symbol, and let ⟨M, I⟩ be the L^{+}-structure where P is interpreted by I. Form L^{++} by adding further unary predicate symbols T⃗, U⃗ corresponding to the symbols in S and, for each n, two n + 2-ary functions symbols f_{n} and g_{n}.

The following sentences describe approximations to a back-and-forth. Let χ_{i}(x_{1}, … x_{n}, x) for i < ω enumerate the n + 1-ary formulas in Δ ∪ T⃗ and χ′_{i}(x_{1}, … x_{n}, x) for i < ω enumerate the associated n + 1-ary formulas in Δ ∪ U⃗. Then for any r < ω, let θ_{n,r}(P, T⃗, U⃗, f_{n}, g_{n}) contain the assertion that f_{n} and g_{n} act within P and the conjunction of

∀x⃗ ∈ P, ∀y⃗ ∈ P, ∀x ∈ P (∃y ∈ P ( ⋀_{0<i<r}(χ_{i}(x⃗, x) ↔ χ′_{i}(y⃗, y))) → ⋀_{0<i<r}(χ_{i}(x⃗, x) ↔ χ′_{i}(y⃗, f_{n}(x⃗, y⃗, x))))

and

∀x⃗ ∈ P, ∀y⃗ ∈ P, ∀x ∈ P (∃y ∈ P ( ⋀_{0<i<r}(χ_{i}(x⃗, x) ↔ χ′_{i}(y⃗, y))) → ⋀_{0<i<r}(χ_{i}(x⃗, g_{n}(x⃗, y⃗, y)) ↔ χ′_{i}(y⃗, y))) .

Let Γ^{∗} be a collection of L^{++}-sentences which assert:

1. dom T⃗ ⊂ P, dom U⃗ ⊂ P.

2. the L^{+}-theory of (M, I, Δ).

3. ϕ(T⃗), ¬ϕ(U⃗).

4. for each n, r, θ_{n,r}(P, T⃗, U⃗, f_{n}, g_{n}).

The consistency of finite subsets of item 4 follows from (I, Δ, A⃗_{n}) =_{n,S} (I, Δ, B⃗_{n}). Let M′ be a countable model of Γ^{∗} and suppose I, U⃗, T⃗, f_{n}, g_{n} interpret P, U⃗, T⃗, f_{n}, g_{n}. Then, the f_{n} and g_{n} determine a back-and-forth system which guarantees that (P, Δ, U⃗) and (P, Δ, T⃗) are isomorphic Δ ∪ S-structures, giving us the required isomorphism f. □_{7.5}

We combine Theorem 7.3 with Lemma 7.5 to get the collapse results. We begin with stable T and generic queries.

Theorem 7.6 Let M ⊧ T where T is stable. Every generic query Q which is L ∪ S-definable by a formula ϕ in M is S-definable in M.

Proof. If Q is not defined by any formula θ in S, there are finite relations A⃗_{n}, B⃗_{n} with dom A_{n}, dom B_{n} ⊆ 𝕌 with (𝕌, A⃗_{n}) =_{n,S} (𝕌, B⃗_{n}) and M(A_{n}) ⊧ ϕ and M(B_{n}) ⊧ ¬ϕ. By Remark 7.4 we have (possibly rechoosing the A_{n}, B_{n}) that A_{n} =_{n,S} B_{n}. Fix a countable set of indiscernibles I = {i_{0}, i_{1}, …} in M. By Remark 2.1, we can replace M by an |I|^{+} saturated model and thus assume (M, I) is pseudo-small. Let A⃗′_{n} (B⃗′_{n}) be the image of A⃗_{n} (B⃗_{n} ) under an injective map taking the domain of A⃗_{n} (B⃗_{n}) to finite subsets of I. Then we have A⃗′_{n} =_{n,S} B⃗′_{n}, M(A⃗′_{n}) ⊧ ϕ and M(B⃗′_{n}) ⊧ ¬ϕ. The first statement follows from the fact that we are taking isomorphic images of all relations in S, and the second from the genericity of ϕ. Reversing the use of Remark 7.4, we may assume, (I, A⃗′_{n}) =_{n,S} (I, B⃗′_{n}).

We now have the hypotheses of Lemma 7.5 with Δ = {x = y} (for (I, A⃗′_{n}), (I, B⃗′_{n})); we apply that result to get a model (M′, I′). Let the infinite S-structures T⃗, U⃗ and the function f on I′ witness the conditions on M′ guaranteed in Lemma 7.5. Let N^{∗} be an ω_{1}-saturated model of Th(M′, I′, T⃗, S⃗, f). So in N^{∗} we have (I, U⃗) and (I, T⃗) are S-isomorphic but ϕ(T⃗) and ¬ϕ(U⃗) hold; moreover, N^{+} = N^{∗}|L^{+} is pseudo-small. Expand N^{+} to models N_{1} and N_{2} for the language L^{∗} as defined in Notation 7.2.

Now, we apply Theorem 7.3: this tells us exactly that there is a family of partial-isomorphisms between N_{1} and N_{2} that each extend f. Since f is an S-isomorphism and U⃗, T⃗ are contained in I, the back and forth system shows, in fact, that (N_{1}, T⃗) and (N_{2}, U⃗) are L^{∗} ∪ S-elementarily equivalent. Now we have a contradiction, since the reducts of these models to L ∪ S disagree on the sentence ϕ. □_{7.6}

We can now derive immediately the following:

Theorem 2.2: Let 𝕌 be infinite and M be a stable L-structure with domain 𝕌. If Q is a first-order definable generic query over M, then Q is a pure first-order query.

We now show the analagous results to Theorem 7.6 for collapse to order. We first have

Theorem 2.3 : Let (𝕌, <) be an infinite linear order and M an L ∪ {<}-structure with domain 𝕌, which does not have the independence property. If Q is a first-order definable locally order generic query over M, then Q is an order definable query.

Proof. Suppose not and let ϕ witness that M does not have locally-generic collapse to order ( i.e. ϕ ∈ L ∪ S defines a locally-generic query Q but Q is not definable over the reduct (𝕌, <)). Since Q is not defined over (𝕌, <), there are finite relations A⃗_{n}, B⃗_{n} with dom A_{n}, dom B_{n} ⊆ 𝕌 with (𝕌, A⃗_{n}) =_{n,S,<} (𝕌, B⃗_{n}) and M(A⃗_{n}) ⊧ ϕ and M(B⃗_{n}) ⊧ ¬ϕ. As in the proof of Theorem 7.6, we may assume A_{n} =_{n,S,<} B_{n}. And, again by Remark 2.1, we may assume M is ω_{1}-saturated and contains a countable set I that is order indiscernible and complete densely ordered by the original order <. Thus, (M, I) is pseudo-small. Let A⃗′_{n} (B⃗′_{n}) be the image of A⃗_{n} (B⃗_{n} ) under an order-preserving injective map taking the domain of A⃗_{n} (B⃗_{n}) to a finite subset of I. Then we have A⃗′_{n} =_{n,S,<} B⃗′_{n}. M(A⃗′_{n}) ⊧ ϕ and M(B⃗′_{n}) ⊧ ¬ϕ. The first statement follows from the fact that we are taking images of all relations in S and preserving order, and the second from the local genericity of ϕ.

Invoking Remark 7.4 again, we have the hypotheses of Lemma 7.5 with Δ as {x = y, x < y}. We get a model with a sequence of order indiscernibles which contains S ∪ {=, <}-isomorphic (I, Δ, T⃗) and (I, Δ, U⃗), but with M(T) ⊧ ϕ and M(U) ⊧ ¬ϕ. We finish the proof exactly as in the the last paragraph of the proof of Theorem 7.6, using Theorem 7.3 for theories without the independence property. □_{2.3}

Finally, we derive

Theorem 2.5 : Let 𝕌 be infinite and M be an L-structure with domain 𝕌 that does not have the independence property. If Q is a first-order definable generic query over M, then for any dense linear order (without endpoints) ⟨D, <⟩, Q is definable over ⟨D, <⟩.

Proof. Suppose Q is not definable over some dense linear order ⟨D, <⟩, but Q is defined by ϕ ∈ L ∪ {S} over M. Let I be a set of indiscernibles in M that is ordered by a dense linear order without endpoints (not necessarily in L). By the genericity of Q and the completeness of the theory of dense-linear order without endpoints, we know that Q is not definable in the structure ⟨I, <⟩.

Once again there are finite relations A_{n}, B_{n} with dom A_{n}, dom B_{n} ⊆ I and (I, <, A⃗_{n}) =_{n,S,<} (I, <, B⃗_{n}) and M(A_{n}) satisfies ϕ while M(B_{n}) doesn’t satisfy ϕ (where the latter follows from the definability of Q by ϕ). Again, we have the hypotheses of Lemma 7.5 and we construct (M′, I′). We now have a model (M′, I′) which is pseudo-small and in which I is linearly ordered by < (although we know nothing of < on the rest of M). Moreover, there are S ∪ {<}-isomorphic (I, Δ, T⃗) and (I, Δ, U⃗), but with M(T) ⊧ ϕ and M(U) ⊧ ¬ϕ.

By applying Theorem 7.3, we get that this isomorphism extends to a family of partial-isomorphisms of (M′, I′), and this gives a contradiction exactly as in the proof of Theorem 7.6. □_{2.5}

We have shown that models without the independence property exhibit generic collapse to order. One can ask if the converse holds: are there models with the independence property that also have generic collapse? The answer is yes: generic collapse requires only that the model be well-behaved locally: e.g. within some definable or ∞-definable set. A model that is the disjoint union of a stable structure and the badly-behaved structure ⟨N, +, ∗, <⟩ will thus still exhibit generic collapse.

The following result crystalizes the principle behind the arguments of this section and indicates a wider but difficult to specify collection of generalizations.

Theorem 7.7 Let M be a structure which contains an infinite set I of (order)-indiscernibles such that any (order)-permutation of I can be extended to a back-and-forth system. Then M exhibits generic collapse to equality (order).

Two interesting open problems are: does generic collapse to order hold in a model if and only if some definable set has NIP; does generic collapse to equality hold if and only if the model has nonempty stable part (defined in [23]).

8 The theory of the expanded structure

Let (M, I) be pseudo-small. We prove a number of results about T^{+}, the theory of (M, I). We have studied pseudo-small theories. A priori, each |I|^{+}-saturated model determines its own theory T^{+} which is pseudo-small. Our first result is that for stable theories T and theories without the independence property, the complete theory of a pseudo-small expansion depends only ‘type’ (which we define next) of the indiscernible sequence.

If I is a set of (Δ, L)-indiscernibles in a model M the type Φ of I is the collection types p_{n}(x⃗) where p_{n} is realized by any n (properly ordered) elements of I.

Theorem 8.1 Suppose the complete countable theory T is stable (does not have the independence property). Let M_{1}, M_{2} be models of T and I_{i} is a set of (Δ, L)-indiscernibles (sequence of order-indiscernibles) in M_{i} such that I_{1} and I_{2} realize the same type. If (M_{1}, I_{1}) and (M_{2}, I_{2}) are pseudo-small then

1. For every L^{+}-formula ϕ, there is a P -bounded formula ϕ′(x) which is equivalent to ϕ(x) on both (M_{1}, I_{1}) and (M_{2}, I_{2}).

2. Th(M_{1}, I_{1}, Δ) = Th(M_{2}, I_{2}, Δ).

Proof. The first statement depends on the observation that the reductions in Sections 3, 4, or 6 never depended on the specific model M but only the types of the (Δ, L)-indiscernible set. The second then follows by proving by induction on the quantifier rank of the P -bounded formulas that for any P -bounded ϕ(x⃗) and any (properly ordered) sequences of distinct elements a⃗ ∈ I_{1}, b⃗ ∈ I_{2},

M_{1} ⊧ ϕ(a⃗) if and only if M_{2} ⊧ ϕ(b⃗).

The base step of the induction holds as I_{1} and I_{2} realize the same types and the induction is trivial.

□_{8.1}

We now show that T^{+}, the theory of pseudo-small expansions of models of T is stable and then that if (M, I) is any model of T^{+} such that M is saturated, any permutation of I extends to an automorphism of M. We require one definition and a corollary to our elimination results.

Definition 8.2 Let p ∈ S(C) and f an elementary bijective map from C to D. Then f p denotes {ϕ(x, fc⃗) : ϕ(x, c⃗) ∈ p}.

Lemma 8.3 If (N, P) ⊧ T^{+}, with P (N) = I, C ⊆ N and α is an L-elementary permutation of IC which fixes C pointwise then for any e⃗, e′ ∈ N, if tp_{L}(e′/IC) = αtp_{L}(e⃗/IC) then tp_{L^{+}}(e′/C) = tp_{L^{+}}(e⃗/C).

Proof. We want to show that for any L^{+}-formula ϕ(x⃗, c⃗), M^{+} ⊧ [ϕ(e⃗, c⃗) ↔ ϕ(e⃗′, c⃗)]. By Theorem 3.3, we may assume ϕ is P -bounded. So we show by induction on the number of P -quantifiers that for all P -bounded ϕ, M^{+} ⊧ [ϕ(e⃗, c⃗) ↔ ϕ(e⃗′, c⃗)]. Since tp_{L}(e⃗′/C) = tp_{L}(e⃗/C), the initial stage holds. Now suppose that for L^{+} formulas ψ(w⃗, c⃗) with less than n P -quantifiers, the lemma holds. Let M^{+} ⊧ (∃z ∈ P)θ(e⃗′, z, c⃗) where θ has fewer than n P -quantifiers. Then this is witnessed by some e_{0} ∈ I: M^{+} ⊧ θ(e⃗′, e_{0}, c⃗). Now tp_{L}(e⃗′/IC) = αtp_{L}(e⃗/IC) implies tp_{L}(e⃗′e_{0}/IC) = αtp_{L}(e⃗α(e_{0})/IC). So by induction M^{+} ⊧ θ(e⃗, α(e_{0}), c⃗) and the result follows. □_{8.3}

Corollary 8.4 If T is λ-stable then T^{+} is λ-stable.

Proof. We first show that T^{+} is stable, i.e. stable in some cardinality κ. Since T is stable, T is stable in each κ with κ^{ω} = κ. Fix such a κ and a model (N, I) of T^{+} which is a κ^{+} saturated L^{+}-structure. Let C ⊆ N have power κ. We can expand C′ to C with |C| = |C′| such that I − C is an indiscernible set over C. It suffices to show that only κ one types over C are realized in N. Let E be a complete set of representatives of realizations of the L^{+}-types over C. Define an equivalence relation on E by e ∼ e′ if for some elementary permutation of CI which fixes C pointwise, tp_{L}(e′/IC) = αtp_{L}(e/IC).

For any e, there is a countable subset I_{e} of I such that tp_{L}(e/IC) does not fork over I_{e}C and tp_{L}(e/IC) is the unique nonforking extension of stp_{L}(e/I_{e}C). If tp_{L}(I_{e}/C) = tp_{L}(I_{e′}/C), there is an elementary permutation α of IC which fixes C pointwise and maps I_{e′} to I_{e}. If stp(e′/I_{e}C) = αstp(e/I_{e}C) = q, then tp_{L}(e′/IC) and αtp_{L}(e/IC) are both nonforking extensions of q. Thus, they are equal and e ∼ e′. Thus the ∼ equivalence class of an element e depends only on i) tp_{L}(I_{e}/C) and ii) stp_{L}(e⃗/I_{e}C) . Now there are κ^{ω} choices for i) and κ for ii) by stability so there are only κ-equivalence classes. But by Corollary 8.3, each equivalence class determines an L^{+}-type so we establish stability in L^{+}.

To extend this result to all κ (in which T is stable) we may first assume that T is superstable. This implies that in the second paragraph I_{e} can be chosen finite. So, κ^{ω} at the end of the paragraph becomes κ and the result follows. □_{8.4}

Now we show that every permutation of a set of indiscernible of a saturated model M^{+} of T^{+} extends to an automorphism of M.

Theorem 8.5 Let T be a stable theory, M a model of T, and I a set of indiscernibles in M with (M, I) saturated and (M, I) pseudo-small. Then every permutation of I extends to an automorphism of M.

Proof. Since (M, I) is pseudo-small so by Corollary 3.6 we have every L^{+}-type over I is defined by an equality formula. Let g be a permutation of I. We proceed exactly as in the proof of Theorem 7.3. The only distinction is that the type g_{1}(q) is over J_{0} ∪ {b⃗} where b⃗ now can have any cardinality less than |M|; here we rely on full saturation of the model.

□_{8.5}

In the language of [19] and [24] we have shown that if (M, I) is saturated and pseudo-small, M is symmetric over I; the last argument is essentially the same as Theorem 8 of [24].

Note: It is essential that we extend a permutation of a single set - not a partial isomorphism between two sets of indiscernibles. For example, consider an equivalence relation with two infinite classes. If one set of indiscernibles exhausts one class, while a second of the same size omits a few points of the other class, then no bijection of the two sets can be extended to make the associated M_{1} and M_{2} partially isomorphic, let alone to an automorphism.

9 Conclusions

There are several questions on the scope of the P -bounded reduction theorems proved in the paper. Can we characterize the assumptions on the model and predicate P that allow P -bounded reduction to hold for more general expansions by unary predicates, not just indiscernibles? The results in [6],[4] and [14] are relevant here, since they give sufficient conditions for such reductions over expansions by arbitrary pseudo-finite sets. There are a number of analogies with Poizat’s theory of beautiful pairs [33]. Casanovas and Ziegler [9] have provided a generalization of our results here and of Poizat’s theory to show that if (M, A) is small and A does not have the finite cover property, then (M, A) is stable.

The above work is entirely in a stable context. In the order context we have the following conjecture.

Conjecture 9.1 If T does not have the independence property, then T^{+} does not have the independence property.

The proofs of the bounded-quantifier collapse result here rely on approximation arguments: we approximate a formula asserting the existence of a witness for many elements of I by a particularly nice conjunction of first-order L formulas. In this sense, they seem to be extensions of the results in [22]. We are also interested in seeing if the results here on theories without the independence property can be proved using the techniques of [23]. We are interested in using the techniques to expand a stable theory to get stronger collapse results, such as those given for more restricted theories in [6].

Belegradek, Stoubouskin, and Tsaitlin conjecture in [4] that if M is an expansion of (Z, +, <) and locally ordergeneric queries on M do not collapse to order then the theory of M is undecidable. In view of Theorem 2.3, this conjecture can be reformulated as: any expansion of (Z, +, <) that has the independence property is undecidable.

The structure M is called symmetric over I if every permutation of I extends to an automorphism of M. We have shown that if I is pseudo-small and (M, I) is saturated then M is symmetric over I. One naturally hopes

Conjecture 9.2 If (M, I) is pseudo-small and M is an uncountable saturated model then M is symmetric over I.

Even more strongly we speculate: If M is an uncountable saturated model of a stable theory and I is an indiscernible set, then M is symmetric over I.

This holds by standard stability arguments if the average type of the indiscernibles is regular, which implies the result for superstable T. The results here show that this holds provided ⟨M, I⟩ is elementary equivalent to ⟨M_{0}, I_{0}⟩, where M_{0} is |I_{0}|^{+}-saturated.

Acknowledgements: We would like to acknowlege helpful conversations with a number of people. Marko Djordevich checked the proof of part 1 of Theorem 8.1 and suggested the simple inductive proof of the second. The remark in Theorem 8.5, that the Theorem also holds with the hypothesis of pseudo-small stable replaced by the hypothesis superstable was made by Hrushovski and verified with Pillay. The goal of extending the collapse-to-order results for o-minimal structures in [6] to a class of models closed under reduct was suggested by Jan Van den Bussche.

References

[1] S. Abiteboul, R. Hull, V. Vianu. Foundations of Databases. Addison-Wesley, 1995.

[2] A.K. Ailamazyan, M.M. Gilula, A.P. Stolboushkin and G.F. Shvarts. Reduction of a relational model with infinite domains to the finite-domain case.

[3] J. T. Baldwin. Fundamentals of Stability Theory. Springer-Verlag, 1988.

[4] O.Belagradek, A. Stolboushkin, M. Tsaitlin. Extended order-generic queries. Manuscript. To appear.

[5] O.Belagradek, Ya’acov Peterzil, Frank Wagner. Quasi O-minimal groups. Manuscript. To appear.

[6] M. Benedikt, G. Dong, L. Libkin, L. Wong. Relational expressive power of constraint query languages. In Proceedings of 15th ACM Symposium on Principles of Database Systems, pages 5–17, Montreal Canada, June 1996.

[7] M. Benedikt and L. Libkin. On the structure of queries in constraint query languages. In Proceedings of 11th IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey 1996.

[8] M. Benedikt and L. Libkin. Languages for Relational Databases over Interpreted Structures. In Proceedings of 16th ACM Symposium on Principles of Database Systems, Tuscon Arizona, June 1996.

[9] E. Casanovas and M. Ziegler. Stable theories with a new predicate. preprint.

[10] C.C. Chang and H.J. Keisler. Model Theory. North-Holland Elsevier, 1990.

[11] A. Dawar, S. Lindell, S. Weinstein. First order logic, fixed point logic, and linear order. In Computer Science Logic ’95, LNCS vol. 1092, 1996, pages 161–177.

[12] H.-D. Ebbinghaus and J. Flum. Finite Model Theory. Springer Verlag, 1995.

[13] J. Flum. Characterizing logics. In Model-Theoretic Logics, edited by J. Barwise and S. Feferman, pages 78-91, Springer-Verlag, 1985.

[14] J.Flum and M. Ziegler. Pseudo-finite Homogeneity and Saturation. Preprint. 1997.

[15] E. Grädel and Y. Gurevich. Metafinite model theory. In Proceedings of Logic and Comput. Complexity, LNCS vol. 960, 1994, pages 313–366.

[16] S. Grumbach and J. Su. First-order definability over constraint databases. In Proc. Conf. on Constr. Progr. 95.

[17] L. Hella,P. Kolaitis, and K.Luosto. Almost Everywhere Equivalence of Logics Bulletin of Symbolic Logic, December 1996.

[18] W. Hodges. Model Theory. Cambridge University Press, 1992.

[19] W. Hodges and A. Pillay. Cohomology of Structures and some problems of Ahlbrandt and Ziegler J. London Math. Soc., 50 (1994) 1-16.

[20] R. Hull and J. Su. Domain independence and the relational calculus. Acta Informatica 31:513–524, 1994.

[21] P. Kanellakis, G. Kuper, and P. Revesz. Constraint query languages. JCSS 51 (1995), 26–52.

[22] H.J. Keisler. Finite Approximation of Infinitely Long Formulas. In The Theory of Models Addison, Henkin, and Tarski,eds. North-Holland, 1965,pp 158-169.

[23] H.J. Keisler. Measures and Forking. Annals of Pure and Applied Logic 34 (1987), no. 2, 119-169.

[24] H. Kikyo and A. Tsuboi. On reduction properties. The Journal of Symbolic Logic (59) 1994 900–911.

[25] C. Laskowski. Vapnik-Chervonenkis classes of definable sets. Journal of the London Mathematical Society. Vol. 45 (1992), no. 2, 377-384.

[26] D. Macpherson and C. Steinhorn. On variants of O-minimality. preprint.

[27] C. Marker and C. Steinhorn. Types definable in O-minimal theories. The Journal of Symbolic Logic (59) 1994 185-198.

[28] M. Otto and J. Van den Bussche. First-order queries on databases embedded in an infinite structure. Information Processing Letters, 60 (1996), no. 1,37-41.

[29] J. Paredaens, J. Van den Bussche, and D. Van Gucht. First-order queries on finite structures over the reals. In LICS’95, pages 79–87.

[30] A. Pillay. Definability of types and pairs of O-minimal structures. The Journal of Symbolic Logic (59) 1994 1400-1409.

[31] A. Pillay and S. Shelah. Classification theory over a predicate I. Notre Dame Journal of Formal Logic 26 (1985) 361-376.

[32] Bruno Poizat, Cours de theories de modéles Villeurbanne: Nur al-Mantiq wal-Ma’rifah.

[33] Bruno Poizat. Paires de structure stables. The Journal of Symbolic Logic (48) 1983 239–249.

[34] S. Shelah. Classification Theory and the Number of Nonisomorphic Models North-Holland, 1978.