Characterizations of monadic NIP
Abstract.
We give several characterizations of when a complete first-order theory is monadically NIP, i.e. when expansions of by arbitrary unary predicates do not have the independence property. The central characterization is a condition on finite satisfiability of types. Other characterizations include decompositions of models, the behavior of indiscernibles, and a forbidden configuration. As an application, we prove non-structure results for hereditary classes of finite substructures of non-monadically NIP models that eliminate quantifiers.
1991 Mathematics Subject Classification:
03C45An appendix has been added, containing two corrections. The first involves replacing indiscernible-triviality with endless indiscernible triviality (both defined in Definition 3.8) in Theorem 1.1. The second withdraws the claimed proof that is not 4-wqo in Theorem 1.2. We have added red text and strikethroughs noting the affected results.
1. Introduction
It is well known that many first order theories whose models are tame can become unwieldy after naming a unary predicate. Arguably the best known example of this is the field of complex numbers. Its theory is uncountably categorical, but after naming a predicate for the real numbers, the expansion becomes unstable. A more extreme example is the theory of infinite dimensional vector spaces over a finite field, in a relational language. The theory is totally categorical, but if, in some model , one names a basis , then by choosing specified sum sets of basis elements, one can code arbitrary bipartite graphs in expansions of by unary predicates.
As part of a larger project in [BS], Baldwin and Shelah undertook a study of this phenomenon. They found that a primary dividing line is whether admits coding i.e., there are three subsets of a model of and a formula that defines a pairing function . If one can find such a configuration in a model of , some monadic expansions of are wild. The primary focus in [BS] was monadically stable theories, i.e. theories that remain stable after arbitrary expansions by unary predicates. Clearly, the two theories described above are stable, but not monadically stable. They offered a characterization of monadically stable theories within the stable theories via a condition on the behavior of non-forking. This allowed them to prove that monadic stability yields a dividing line within stable theories: models of monadically stable theories are well-structured and admit a nice decomposition into trees of submodels, while if a theory is stable but not monadically stable then it encodes arbitrary bipartite graphs in a unary expansion, and so is not even monadically NIP.
A theory is NIP if it does not have the independence property, and is monadically NIP if every expansion of a model of by unary predicates is also NIP. The behavior of NIP theories has been extensively studied, see e.g., [Pierre]. Soon after [BS], Shelah further studied monadically NIP theories in [Hanf], where he showed they satisfy a condition on the behavior of finite satisfiable types paralleling the condition on the behavior of non-forking in monadically stable theories. He was then able to use this to produce a linear decomposition of models of monadically NIP theories, akin to a single step of the tree decomposition in monadically stable theories.
We dub Shelah’s condition on the behavior of finite satisfiability the f.s. dichotomy, and we consider it to be the fundamental property expressible in the original language describing the dichotomous behavior outlined above. We show the f.s. dichotomy characterizes monadically NIP theories and provide several other characterizations, including admitting a linear decomposition in the style of Shelah, a forbidden configuration, and conditions on the behavior of indiscernible sequences after adding parameters. Definitions for the following theorem may be found in Definitions 3.9, A.4, 3.4, and 3.8. Of note is that all but the first two conditions refer to the theory itself, rather than unary expansions.
In Theorem 1.1, “indiscernible-triviality” has been replaced with “endless indiscernible triviality”.
Theorem 1.1.
The following are equivalent for a complete theory with an infinite model.
-
(1)
is monadically NIP.
-
(2)
No monadic expansion of admits coding.
-
(3)
does not admit coding on tuples.
-
(4)
has the f.s. dichotomy.
-
(5)
For all and , every partial -f.s. decomposition of extends to an (irreducible) -f.s. decomposition of .
-
(6)
is dp-minimal and has endless indiscernible triviality.
We believe that monadic NIP (or perhaps a quantifier-free version) is an important dividing line in the combinatorics of hereditary classes, and provides a general setting for the sort of decomposition arguments common in structural graph theory. For example, see the recent work on bounded twin-width in the ordered binary case, where it coincides with monadic NIP [ST, TW4]. Here, we mention the following conjecture, adding monadic NIP to a question of Macpherson [MacHom]*Question 2.2.7.
Conjecture 1.
The following are equivalent for a countable homogeneous -categorical relational structure .
-
(1)
is monadically NIP.
-
(2)
The (unlabeled) growth rate of is at most exponential.
-
(3)
is well-quasi-ordered under embeddability, i.e. it has no infinite antichain.
From Theorem 1.1, we see that if is not monadically NIP then it admits coding on tuples. This allows us to prove the following non-structure theorem in §5 (with Definition 5.1 defining the relevant terms), in particular confirming and a weak form of from the conjecture, although without any assumption of -categoricity.
In Theorem 1.2, the claim regarding 4-wqo remains unproven.
Theorem 1.2.
Suppose is a complete theory with quantifier elimination in a relational language with finitely many constants. If is not monadically NIP, then has growth rate asymptotically greater than for some and is not 4-wqo.
We also show the following, partially explaining the importance of monadic model-theoretic properties for the study of hereditary classes.
Theorem 1.3.
Suppose is a complete theory with quantifier elimination in a relational language with finitely many constants. Then is NIP if and only if is monadically NIP, and is stable if and only if is monadically stable.
In Section 2, we review basic facts about finite satisfiability, and introduce -f.s. sequences, which are closely related to, but more general than Morley sequences. The results of this section apply to an arbitrary theory, and so may well be of interest beyond monadic NIP. Section 3 introduces the f.s. dichotomy and proves the equivalence of (3)-(6) from Theorem 1.1. Much of these two sections is an elaboration on the terse presentation of [Hanf], although there are new definitions and results, particularly in Section 3.2, which deals with the behavior of indiscernibles in monadically NIP theories. In Section 4 we finish proving the main theorem by giving a type-counting argument that the f.s. dichotomy implies monadic NIP, and by showing that if admits coding on tuples then it admits coding in a unary expansion. In Section 5, we prove Theorems 1.2 and 1.3.
We are grateful to Pierre Simon, with whom we have had numerous insightful discussions about this material. In particular, the relationship between monadic NIP and indiscernible-triviality was suggested to us by him.
1.1. Notation
Throughout this paper, we work in , a large, sufficiently saturated, sufficiently homogeneous model of a complete theory . We routinely consider when is an infinite set. To make this notion precise, we (silently) fix an enumeration of (of ordinal order type) and an enumeration with . Then for all subsequences and is the corresponding subsequence of .
2. -f.s. sequences
Forking independence and Morley sequences are fundamental tools in the analysis of monadically stable theories in [BS]. These are less well-behaved outside the stable setting, but in any theory we may view ‘ is finitely satisfiable in ’ as a statement that is (asymmetrically) independent from over . Following [Hanf], we will use finite satisfiability in place of non-forking, and indiscernible -.f.s. sequences in place of Morley sequences. Throughout Section 2, we make no assumptions about the complexity of .
2.1. Preliminary facts about -f.s. sequences
For the whole of this section, fix a small (typically, ).
Definition 2.1.
Suppose . Then for any (possibly infinite) we say is finitely satisfied in if, for all , there is such that .
One way of producing finitely satisfiable types in comes from average types.
Definition 2.2.
Suppose is a possibly infinite tuple. For any ultrafilter on and any ,
It is easily checked that is a complete type over that is finitely satisfied in . We record a few basic facts about types that are finitely satisfied in . Proofs can be found in either Section VII.4 of [Shc] or in [Pierre].
Fact 2.3.
Let be any model.
-
(1)
For any set and any ( may be an infinite tuple), is finitely satisfied in if and only if for some ultrafilter on .
-
(2)
Suppose is any set of formulas, closed under finite conjunctions, and each of which is realized in . Then there is a complete type extending that is finitely satisfied in .
-
(3)
(Non-splitting) If is finitely satisfied in , then does not split over , i.e., if and , then for any , if and only if .
-
(4)
(Transitivity) If and are both finitely satisfied in , then so is .
Definition 2.4 (-f.s. sequence).
With fixed as above, let be any linearly ordered index set.
-
•
Suppose is any sequence of sets, indexed by . For , denotes , and for , denotes . and are defined analogously.
-
•
For , an -f.s. sequence over , is a sequence of sets such that is finitely satisfied in for every . When we simply say is an -f.s. sequence.
Note that for any , is an -f.s. sequence over if and only if the concatenation is an -f.s. sequence.
We note two useful operations on -f.s. sequences over , ‘Shrinking’ and ‘Condensation’.
Definition 2.5.
Suppose and is an -f.s. sequence over .
-
(1)
‘Shrinking:’ For every , for all , and for all with , we say as a sequence over is obtained by shrinking from as a sequence over .
-
(2)
Condensation:’ Suppose is a condensation, i.e., a surjective map with each a convex subset of . For each , let . We say as a sequence over is obtained by condensation from as a sequence over .
In particular, removing a set of ’s from the sequence is an instance of Shrinking.
Lemma 2.6.
Suppose and is an -f.s. sequence over . Then Shrinking and Condensation both preserve being an -f.s. sequence over . In particular, for any partition into convex pieces, the two-element sequence is an -f.s. sequence over .
Proof.
The statement is immediate for Shrinking, and for Condensation follows by transitivity in Fact 2.3. The last sentence is a special case of Condensation, as the partition defines a condensation with . ∎
Definition 2.7.
If is an -f.s. sequence over , call a simple extension, resp. blow-up if is attained from it by Shrinking, resp. by Condensation. is an extension of if it is a blow-up of a simple extension of over .
Here is one general result, whose verification is just bookkeeping.
Lemma 2.8.
Suppose is an -f.s. sequence, , , and is an -f.s. sequence over with . Then the blow-up
is also an -f.s. sequence.
The next lemma is not used later, but shows that if , then decomposing as an -f.s. sequence gives a chain of elementary substructures approximating .
Lemma 2.9.
Suppose and is any -f.s. sequence with . Then, for every initial segment (regardless of whether or not has a maximum) is an elementary substructure of .
Proof.
We apply the Tarski-Vaught criterion. Choose a formula with from and from such that . If some realizes , then as is finitely satisfied in , there is also a solution in . Otherwise, if there is a solution in , there is nothing to check. ∎
The following argument is contained in the proof of [Hanf]*Part I Lemma 2.6, but the statement here is slightly more general. (The paper [Hanf] is divided into Part I and Part II, with overlapping numbering schemes.)
Proposition 2.10 (Extending the base).
Suppose and is an -f.s. sequence over . For every , there is with and is an -f.s. sequence over .
Proof.
As notation, choose disjoint sets of variables, with for each . For each , choose an ultrafilter on such that .
For a finite, non-empty , let . We will recursively define complete types as follows:
-
•
For a singleton, let .
-
•
For , letting and ,
That is, realizes if and only if realizes and, for every , holds if and only if .
It is easily checked that each is a complete type over and, arguing by induction on , whenever , is the restriction of to . Thus, by compactness, is consistent, and in fact, is a complete type over . Choose any realization of . Then, for each , . Since and , it follows that . Thus, it suffices to choose any satisfying . ∎
2.2. full for non-splitting
Definition 2.11.
We call full (for non-splitting over ) if, for every , every is realized in .
The relevance of fullness is that, whenever is full, every complete type has a unique extension to any set that does not split over . Keeping in mind finite satisfiability as an analogue of non-forking, the next lemma says that ‘types over that are finitely satisfied in are stationary.’
Lemma 2.12 ([Hanf]*Part I Lemma 1.5).
Suppose is full and is finitely satisfied in . Then for any set , there is a unique extending that remains finitely satisfied over .
Proof.
In fact, we can easily describe . A formula if and only if for some (equivalently, for every) from with . The fact that is well-defined is because, being finitely satisfied in , does not split over . ∎
Lemma 2.13 ([Hanf]*Part I Observation 1.6).
Suppose is full and is an -f.s. sequence over . Partition as (not necessarily convex). Then is an -f.s. sequence over if and only if is an -f.s. sequence over .
Proof.
Left to right is obvious. For the converse, we need to show that is finitely satisfied in . To begin, by Proposition 2.10, choose with finitely satisfied in . Note that
Also, since is an -f.s. sequence over , we have both and (by Shrinking) are -f.s. sequences over . By transitivity, the last statement, coupled with finitely satisfied in , implies is finitely satisfied in . Thus, by Lemma 2.12,
As finitely satisfied in , so is . ∎
Lemma 2.14.
Suppose is full and is an -f.s. sequence over . Choose any from and from with and . Then .
Proof.
Let . As , the map fixing pointwise with is elementary. To prove the Lemma, it suffices to show that realizes .
To see this, let be any realization of (anywhere in ). Then . From this it follows that , with the second equality by hypothesis. But also:
-
(1)
is finitely satisfied in since and is finitely satisfied in ; and
-
(2)
is finitely satisfied in since is finitely satisfied in .
Applying Lemma 2.12 to the last three statements implies , i.e., realizes . ∎
We glean two results from Lemma 2.14. The first bounds the number of types realized in an -f.s. sequence, independent of either or .
Lemma 2.15.
For any model , for any -f.s. sequence , and for every , , the number of complete -types over realized in is at most .
Proof.
Because of Condensation, it suffices to prove that for any model and for any -f.s. sequence , at most complete -types are realized in . To see this, choose a full with . By Proposition 2.10, choose with and an -f.s. sequence over . Choose any with . As both and are finitely satisfied in , it follows from Lemma 2.12 that . As there are at most complete -types over , this suffices. ∎
The second is a refinement of the type structure of an -f.s. sequence over a full .
Definition 2.16.
An -f.s. sequence is an order-congruence over if, for all , for all , from , and for all satisfying for , we have
The following is essentially part of the statement of [Hanf]*Part I Lemma 2.6.
Proposition 2.17.
For every model , every -f.s. sequence over any full is an order-congruence over .
2.3. -f.s. sequences and indiscernibles
In this subsection, we explore the relation between -f.s. sequences and indiscernibles. An -f.s. sequence need not be indiscernible (for example, the tuples can realize different types), but when it is, it gives a special case of a Morley sequence in the sense of [Pierre].
We first show indiscernible sequences can always be viewed as -f.s. sequences over some model .
In Lemma 2.18, the “Furthermore” sentence is false.
Lemma 2.18 (extending [Hanf]*Part I Lemma 4.1).
Suppose is infinite and is indiscernible over . (For simplicity, assume is finite). Then there is a model such that is both indiscernible over and is an -f.s. sequence.
Furthermore, if there is some such that is indiscernible over each , then may be chosen so that additionally remains indiscernible over .
Proof.
Expand the language to have built-in Skolem functions while keeping indiscernible, and end-extend to an indiscernible sequence of order-type . (For the ‘Furthermore’ sentence, note this can still be done so the result is indiscernible over each .) Let be the new elements added, and let be reduct of the Skolem hull of to the original language. (If were indiscernible over , then is indiscernible over .) ∎
Armed with this Lemma, we characterize when an infinite is both an -f.s sequence and is indiscernible over . (A paradigm of an indiscernible sequence over that is not an -f.s. sequence is where is an equivalence relation with infinitely many, infinite classes and is a sequence from some -class not represented in .)
Lemma 2.19.
An infinite sequence of -tuples is both indiscernible over and an -f.s. sequence if and only if there is an ultrafilter on such that for every .
Proof.
Right to left is clear, so assume is both indiscernible over and an -f.s. sequence. As is infinite, it contains either an ascending or descending -chain. For definiteness, choose of order type . To ease notation, we write in place of . For each and each formula , let . As is indiscernible over , for all , and because it is an -f.s. sequence, has the finite intersection property. Choose any ultrafilter on containing every . Thus, for any and with ,
Finally, as and is indiscernible over , an easy induction on gives the result. ∎
Using Lemma 2.19, we obtain a strengthening of Lemma 2.18. The lemma below can be proved by modifying the proof of Lemma 2.10, but the argument here is fundamental enough to bear repeating.
Lemma 2.20.
If an infinite is both indiscernible over and an -f.s. sequence, then for any , there is such that and is both indiscernible over and an -f.s. sequence over . Thus, if is an infinite, indiscernible sequence over , then there is a model and a full such that is both indiscernible over and an -f.s. sequence over .
Proof.
For the first sentence, given , and , choose an ultrafilter as in Lemma 2.19. A routine compactness argument shows that we can find a sequence such that for every . As we also have , an easy induction shows that . Now any satisfying suffices.
For the second sentence, given , apply Lemma 2.18 to get an for which is both indiscernible over and an -f.s. sequence, and choose any full . Then apply the first sentence to , , and . ∎
Next, we recall the following characterization of indiscernibility. The relevant concepts first appeared in the proof of Theorem 4.6 of [Morley] and a full proof appears in [Shc]*Lemma I, 2.5.
Lemma 2.21.
Suppose is any sequence of sets indexed by a linear order and let be any set. For each , fix a (possibly infinite) enumeration of and let . Then is indiscernible over if and only if
-
(1)
For all , realizes ; and
-
(2)
Each does not split over .
By contrast, if and is an -f.s. sequence over , then (2) is satisfied, but (1) may fail. In the case where is full, (1) reduces to a question about types over .
Lemma 2.22.
Suppose is full and is an -f.s. sequence over . Then is indiscernible over if and only if for all .
Proof.
In terms of existence of such sequences, we have the following.
Lemma 2.23.
Suppose is full and is finitely satisfied in . Then for every there is an -f.s. sequence over of realizations of , hence is also indiscernible over .
3. The f.s. dichotomy
We begin this section with the central dividing line of this paper. Although unnamed, the concept appears in Lemma II 2.3 of [Hanf].
Definition 3.1 (f.s. dichotomy).
has the f.s. dichotomy if, for all models , all finite tuples , if is finitely satisfied in , then for any singleton , either or is finitely satisfied in .
It would be equivalent to replace , by sets in the definition above, and this form will often be used. Much of the utility of the f.s. dichotomy is via the following extension lemma.
Lemma 3.2 ([Hanf]*Part I Claim 2.4).
Suppose has the f.s. dichotomy and is any -f.s. sequence. Then for every , there is a simple extension of that includes that is also an -f.s. sequence. Moreover, if is a well-ordering with a maximum element, we may take .
Proof.
Fix any -f.s. sequence and choose any singleton . Let be the maximal initial segment of such that is finitely satisfied in . Note that could be empty or all of . If the minimum element of exists, name it and take ; otherwise, let , where is a new element realizing the cut and put .
Let and for all . We claim that is an -f.s. sequence. To see this, note that while properly extends for any . Thus, is finitely satisfied in , but is not for every .
We first show that is finitely satisfied in . This is immediate if . If not and , by the f.s. dichotomy (with as , as , and as ), we have that is finitely satisfied in . But this, coupled with is finitely satisfied in , would imply is finitely satisfied in , a contradiction.
To finish, we show that for every , is finitely satisfied in . Again, if this were not the case, the f.s. dichotomy would imply is finitely satisfied in . But then, by Shrinking, we would have finitely satisfied in , contradicting our choice above.
For the ‘Moreover’ sentence, the only concern is if is finitely satisfied in . But in this case we may take to be the maximal element of , rather than a new element in . ∎
It is evident that Lemma 3.2 extends to -f.s. sequences over an arbitrary base .
In [BS]*Theorem 4.2.6, the f.s. dichotomy appears as a statement about the behavior of forking rather than non-forking. Namely, forking dependence is totally trivial and transitive on singletons. We may derive similar consequences for dependence from the f.s. dichotomy. This is stated in [Blum]*Corollary 5.22, although missing the necessary condition of full .
Lemma 3.3.
Suppose has the f.s. dichotomy, and fix .
-
(1)
If and are not finitely satisfiable in , then neither is .
-
(2)
is finitely satisfiable in if and only if is finitely satisfied in for all .
-
(3)
Let be full. Then is finitely satisfiable in if and only if is finitely satisfied in for all , .
Proof.
If is finitely satisfiable in , then by the f.s. dichotomy either or is as well. Shrinking then gives a contradiction.
By induction on . Left to right is immediate, so assume is finitely satisfied in for every . Write . By induction we may assume is finitely satisfied in . By the f.s. dichotomy, either is finitely satisfied in and we are done immediately, or else is finitely satisfied in , and we finish using transitivity from Fact 2.3.
Left to right is immediate by Shrinking, so assume is finitely satisfied in for every and . It follows from (2) that is finitely satisfied in for every . To conclude that is finitely satisfied in , we argue by induction on . Let , and by induction assume the statement is true for .
By the f.s. dichotomy, either or is finitely satisfiable in . In the first case we are finished immediately, and in the second we finish by invoking Lemma 2.13. ∎
In the stable case, forking dependence is symmetric as well and so yields an equivalence relation on singletons, which is used in [BS] to decompose models into trees of submodels. In general, the f.s. dichotomy shows finite satisfiability yields a quasi-order on singletons when working over a full . Taking the classes of this quasi-order in order naturally gives an irreducible decomposition of over in the sense of the next subsection, but we sometimes wish to avoid having to work over a full .
3.1. Decompositions of models
In this subsection, we characterize the f.s. dichotomy in terms of extending partial decompositions to full decompositions of models.
Definition 3.4 (-f.s. decomposition).
Suppose is any set.
-
•
A partial -f.s. decomposition of is an -f.s. sequence with .
-
•
An -f.s. decomposition of is a partial -f.s. decomposition with .
-
•
An -f.s. decomposition of is irreducible if, for every and for every , neither nor are finitely satisfied in .
By iterating Lemma 3.2 for every for a given set we obtain:
Lemma 3.5.
Suppose that has the f.s. dichotomy. For any set and any , any partial -f.s. decomposition of has a simple extension to an -f.s. decomposition of over . If the sets were pairwise disjoint, we may choose to be pairwise disjoint as well. Furthermore, if is a well-ordering with a maximum element, we may take .
Proposition 3.6.
has the f.s. dichotomy if and only if for all models (we do not require ) every partial -f.s. decomposition of has an irreducible -f.s. decomposition of extending it.
Proof.
() Suppose partial decompositions extend, and let with finitely satisfiable in , and let with . So is an -f.s. sequence, and can be extended to an -f.s. decomposition of . After Shrinking, we obtain the conclusion of the f.s.-dichotomy.
() Given a partial -f.s. decomposition of , apply Lemma 3.5 to get a simple extension that is an -f.s. decomposition of . By Zorn’s Lemma, it will suffice to show that if there is with and is finitely satisfiable in , then we may blow up the sequence so that and are in distinct parts. Given such , we have is a partial -f.s. decomposition of over . Extending this to a full decomposition of and then applying Lemma 2.8 to prepend and append gives the result. ∎
Remark 3.7.
We could do the above proof over some full to obtain an irreducible -f.s. decomposition that is also an order-congruence.
We note that at the end of [BS], Baldwin and Shelah conjecture that models of monadically NIP theories should admit tree decompositions like those they describe for monadically stable theories, but with order-congruences in place of full congruences.
3.2. Preserving indiscernibility
We begin with some definitions. The definition of dp-minimality given here may be non-standard, but it is proven equivalent to the usual definition with Fact 2.10 of [DGL].
Definition 3.8 (Indiscernible-triviality and dp-minimality).
The first definition is meant to recall trivial forking.
-
•
has indiscernible-triviality if for every infinite indiscernible sequence and every set of parameters, if is indiscernible over each then is indiscernible over .
-
•
has endless indiscernible triviality if for every infinite indiscernible sequence without endpoints and every set of parameters, if is indiscernible over each then is indiscernible over .
-
•
is dp-minimal if, for all indiscernible sequences over any set , every induces a finite partition of the index set into convex pieces , with at most two infinite and every is indiscernible over .
As mentioned in the introduction, the notion of a theory admitting coding was the central dividing line of [BS]. We weaken the definition here to allow the sequences to consist of tuples. Note that even the theory of equality would admit the further weakening of also allowing to consist of tuples.
Definition 3.9 (Admits coding (on tuples)).
A theory admits coding on tuples if there is a formula (with parameters ), sequences , indexed by countable, dense orderings , respectively, and a set , such that is indiscernible over , is indiscernible over , and .
We call a tuple-coding configuration, and let and .
admits coding if we may take and to be sequences of singletons.
A convenient variant for this subsection is a joined tuple-coding configuration, which consists of a formula (with parameters) , a sequence indiscernible over the parameters of , indexed by an infinite linear order , and a set such that for , . Given a joined tuple-coding configuration, indexed by a countable, dense , we may construct a tuple-coding configuration by keeping fixed, choosing open intervals with , and letting and . Conversely, given a tuple-coding configuration with , we may construct a joined tuple-coding configuration by considering the indiscernible sequence whose elements are , restricting to elements with , and replacing by .
The following configuration appears in [Hanf]*Part II Lemma 2.2, and will appear as an intermediate between a failure of the f.s. dichotomy and a tuple-coding configuration.
Definition 3.10.
A pre-coding configuration consists of a with parameters and a sequence , indiscernible over the parameters of , such that for some (equivalently, for every) from , there is such that
-
(1)
;
-
(2)
for all ; and
-
(3)
for all .
We show the equivalence of the existence of these notions with the proposition below. The proof of in the following is essentially from [Hanf]*Part II Lemma 2.3, while is based on [ST]*Lemma C.1. The idea of is that when working over a full , types have a unique “generic” extension by Lemma 2.12. In a failure of the f.s. dichotomy, the extension of to is non-generic, and so can in some sense pick out and from a suitable sequence.
In Proposition 3.11, “indiscernible-triviality” has been replaced with “endless indiscernible triviality”. The adjustments needed for the proof of are minor, but needs an entirely new proof. These appear in Appendix A.1. We have also taken the opportunity to insert into a line about Ramsey and compactness that was omitted.
Proposition 3.11.
The following are equivalent for any theory .
-
(1)
has the f.s. dichotomy.
-
(2)
is dp-minimal and has endless indiscernible triviality.
-
(3)
does not admit coding on tuples.
-
(4)
does not have a pre-coding configuration.
Proof.
: Suppose has the f.s. dichotomy. We begin with showing is dp-minimal. Choose an indiscernible over a set and any element . Applying Lemma 2.20 to (in the theory naming constants for each ) choose a model and a full set such that is both indiscernible over and an -f.s. sequence over . As in the proof of Lemma 3.2, choose a maximal initial segment such that is finitely satisfied in . If has a minimal element , let , and let otherwise. As is full, in either case we have an order-congruence of , so both and are indiscernible over , which suffices.
Next, we show indiscernible-triviality. We may assume is ordered by . The argument here is more involved, as given an infinite, indiscernible and a set over which is indiscernible over each , we cannot apply Lemma 2.20 and maintain the indiscernibility over each . However, the proof of Lemma 2.18 allows us to find a model such that is an -f.s. sequence and is indiscernible over for every . Now, call an element high if is finitely satisfied in . By indiscernibility, if is finitely satisfied in for any , then is high. Let denote the set of high elements, and let be the low (i.e., not high) elements of . As satisfies the f.s. dichotomy, Lemma 3.5 implies has a simple extension (Definition 2.7) to an -f.s. sequence with universe . Moreover, any such simple extension will condense to .
Using this, we argue that is indiscernible over in two steps. First, we argue that is indiscernible over . To see this, fix from and let . From the previous paragraph, is an -f.s. sequence over . So does not split over , and so by Lemma 2.21 it suffices to prove that realizes . Choose any with from and from . To see that , choose an automorphism fixing and an initial segment pointwise that induces an order-preserving permutation of with . Clearly, . It is easily seen that for every singleton , is indiscernible over and, as fixes pointwise, is also low. Thus, any simple extension to will condense to . In particular is finitely satisfied in . Thus, if , by finite satisfiability there would be from such that , which is impossible since fixes pointwise. Thus, is indiscernible over .
Finally, to see that is indiscernible over , choose any , from , from , and from and assume by way of contradiction that . Recall is an -f.s. sequence, so is finitely satisfied in , and so the same formula is true with some from replacing . But this contradicts that is indiscernible over . Thus, is indiscernible over .
: Assume (2) holds, but (3) fails, so there is a joined tuple-coding configuration with countable, dense. By naming constants, we may assume has no parameters. Choose from . By dp-minimality, is partitioned into finitely many convex pieces, indiscernible over , with at most two pieces infinite.
If are in the same convex piece, then taking we get , contradicting our configuration. So suppose and are in different pieces. Then one of the pieces must be infinite, so by symmetry suppose the piece containing is. By indiscernible-triviality is indiscernible over . But then picking some again gives . The convex piece containing might not be endless. But in this case, the convex piece containing must be , which is endless. So we may conclude the argument substituting for and for .
: Assume fails, as witnessed by , , and . By Ramsey and compactness, we may assume that the truth value of depends only on the order-type of . Define a new sequence where . Let
Also let . It is easily verified that is a joined tuple-coding configuration. That admits coding on tuples now follows by the remarks following Definition 3.9.
: Assume that , , , and form a counterexample to the f.s. dichotomy, i.e., is finitely satisfied in , but neither nor are. As is an -f.s. sequence, by Proposition 2.10 choose a full such that is an -f.s. sequence over . Note that by transitivity, we also have finitely satisfied in .
Claim.
There is such that with finitely satisfied in .
Proof of Claim.
We first argue that every finite conjunction of formulas from is satisfied in . To see this choose and ( and may also have hidden parameters from ) and we will show that has a solution in . Let . As is finitely satisfied in , holds for some from . Thus, as and , there is such that holds, which suffices.
Thus, by Fact 2.3(2), there is a complete type extending that is finitely satisfied in . As , there is an element so that realizes , proving the claim. ∎
By Lemma 2.23, choose an -f.s. sequence over of realizations of that is indiscernible over . Fix from . Note that since witness the failure of the f.s. dichotomy, neither nor are finitely satisfied in . As notation, let and . Now, by Shrinking and Condensation,
As is finitely satisfied in and is full, by Lemma 2.13 is an -f.s. sequence over , and so by Lemma 2.8,
As this sequence is an order-congruence, it follows that , so we can choose such that
Thus, since is not finitely satisfied in , neither is . By contrast, for , as both and are finitely satisfied in and are equal by Proposition 2.17, the same is true of . Dually, since is not finitely satisfied in , neither is ; and because is finitely satisfied in for every , we also conclude for all by Proposition 2.17.
Finally, choose such that neither nor has realizations in . Then, letting for each , is a pre-coding configuration with respect to and . ∎
Remark 3.12.
The following observation will be useful in Section 5. A tidy pre-coding configuration is one where for every and . The pre-coding configuration constructed in is tidy, since, choosing so is an -f.s. sequence, implies and are not finitely satisfiable in . But if for then the former type is finitely satisfiable in , and if for , then the latter type is.
The tidiness property extends to the joined tuple-coding configuration constructed in and so ultimately to the tuple-coding configuration as well. That is, from a failure of the f.s. dichotomy, we construct a tuple-coding configuration with for every , and .
4. The main theorem
We recall the main theorem from the introduction. Note that whereas Clauses (1) and (2) discuss monadic expansions of , Clauses (3)-(6) are all statements about itself.
In Theorem 4.1, “indiscernible-triviality” has been replaced with “endless indiscernible triviality”.
Theorem 4.1.
The following are equivalent for a complete theory with an infinite model.
-
(1)
is monadically NIP.
-
(2)
No monadic expansion of admits coding.
-
(3)
does not admit coding on tuples.
-
(4)
has the f.s. dichotomy.
-
(5)
For all and , every partial -f.s. decomposition of extends to an (irreducible) -f.s. decomposition of .
-
(6)
is dp-minimal and has endless indiscernible triviality.
The equivalences of - are by Proposition 3.6 and Proposition 3.11. We note that is easy: Choose a monadic expansion that admits coding, say via an -formula defining a bijection from the countable sets . By adding a new unary predicate for a suitable , the formula can define the edge relation of an arbitrary bipartite graph on , and in particular of the generic bipartite graph. Thus, is not monadically NIP.
Thus, it remains to prove that and , which are proved in the next two subsections.
4.1. If has the f.s. dichotomy, then is monadically NIP
The type-counting argument in this section is somewhat similar to that in [Blum], showing that monadic NIP corresponds to the dichotomy of unbounded partition width versus partition width at most . Both arguments use the tools from Sections 2 and 3 to decompose the model and count the types realized in a part of the decomposition over its complement. However, while Blumensath decomposes the model into a large binary tree, our decomposition takes a single step.
Definition 4.2.
Suppose is any sequence of pairwise disjoint tuples and suppose is any model. An -partition of is any partition with for each .
Definition 4.3.
For any and , let denote the number of complete types over realized by tuples in .
We will be primarily interested in the case where is very large, and is significantly smaller than . The following lemma is similar to Lemma 2.15, removing the requirement that the partition is convex but adding a finiteness condition.
For the rest of this section, recall the notation from the first part of Definition 2.4.
Lemma 4.4.
If has the f.s. dichotomy, then for every well-ordering with a maximum element, for every indiscernible sequence of pairwise disjoint tuples and every , there is an -partition of such that for every finite .
Proof.
By Lemma 2.20, choose a model of size and a full with for which is an -f.s. sequence over . (Note that might not contain .) By Lemma 3.5 choose a simple extension of with . Thus, is an -partition of . For a given finite and , let and let . As is an order-congruence over by Lemma 2.17, is determined by and the order type of the finite set . There are only finitely many such order types, and as , there are at most complete types over . So for every finite . ∎
On the other hand, if a theory has the independence property, then no uniform bound can exist.
Lemma 4.5.
Suppose that has IP, as witnessed by with and . For every there is an order-indiscernible , and a model such that for every -partition of , for some finite .
Proof.
In the monster model, choose an order-indiscernible that is shattered, i.e., there is a set such that holds if and only if . Note that for distinct , there is some such that . Let be any model containing and let be any -partition of . As , while , by applying the pigeon-hole principle times (one for each coordinate of ) one obtains , also of size , and a finite such that for each . As and there are at most types over , we can find of size such that is constant among . It follows that for distinct . As , it follows that . ∎
To show that the behaviors of Lemma 4.4 and Lemma 4.5 cannot co-exist, we get an upper bound on the number of types realized in a finite monadic expansion. Such a bound is easy for quantifier-free types, and the next lemma inductively steps it up to a bound on all types. The following two lemmas make no assumptions about .
For each , define an equivalence relation on by: if and only if and for every formula of quantifier depth at most . Clearly, if and only if for every . To get an upper bound on , for each , let .
Lemma 4.6.
For any , , and , . Thus, .
Proof.
The second sentence follows from the first as if and only if for every . For the first sentence, we give an alternate formulation of to make counting easier. For each , let be the equivalence relation on given by:
-
•
if and only if and ; and
-
•
if and only if and, for every , there is such that , and vice-versa,
For each , let . It is clear that and by the definition of we have for each , so the lemma follows from the fact that if and only if , whose verification amounts to proving the following claim.
Claim.
If the quantifier depth of is at most , then for all partitions , for all , and for all , if , then .
Proof of Claim.
By induction on . Say is chosen with the quantifier depth of is at most . Fix a partition and choose , with . Assume . There are two cases. If there is some such that , then by the inductive hypothesis. On the other hand, if there is such that , use to find such that . Thus, the inductive hypothesis implies , so again . ∎
∎
The following transfer result is the point of the previous lemma. Again, it will be used when is significantly smaller than .
Lemma 4.7.
Let be any model and let be any expansion of by finitely many unary predicates. Then .
Proof.
For each , expanding by unary predicates can increase the number of quantifier-free -types by at most a finite factor, i.e. , so . The result now follows from Lemma 4.6. ∎
Finally, we combine the lemmas above to obtain the goal of this subsection.
Proposition 4.8.
If has the f.s. dichotomy, then is monadically NIP.
Proof.
By way of contradiction assume that is not monadically NIP, but has the f.s. dichotomy. Let be an expansion by finitely many unary predicates that has IP. Choose a cardinal . Let with as in Lemma 4.5, so for any -partition of there is with .
Let be the -reduct of . As remains -order-indiscernible, and has the f.s. dichotomy, choose an -partition of as in Lemma 4.4, so for every . Since is a unary expansion of , for every , by Lemma 4.7. This this contradicts our ability to find an from the previous paragraph for the chosen -partition of . ∎
Lemma 2.15 and the arguments in this subsection seem to indicate that, for a generalization of the structural graph-theoretic notion of neighborhood-width [Gur] similar to Blumensath’s generalization of clique-width [Blum], monadic NIP should correspond to a dichotomy between bounded and unbounded neighborhood-width.
4.2. From coding on tuples to coding on singletons
This subsection provides the final step, , in proving Theorem 4.1 by showing that if admits coding on tuples, then some monadic expansion admits coding (i.e., on singletons). For the result of this subsection, since admitting coding on tuples immediately implies is not monadically NIP, we could finish by [BS]*Theorem 8.1.8, which states that if has IP then this is witnessed on singletons in a unary expansion. But the number of unary predicates used would depend on the length of the tuples in the tuple-coding configuration, which would weaken the results of Section 5.
Deriving non-structure results in a universal theory from the existence of a bad configuration is made much more involved if the configuration can occur on tuples. If one is willing to add unary predicates, arguments such as that from [BS] mentioned above will often bring the configuration down to singletons. A general result in this case is [Blum]*Theorem 4.6 that (under mild assumptions) there is a formula defining the tuples of an indiscernible sequence in the expansion adding a unary predicate for each “coordinate strip” of the sequence. The results of [Sim21] indicate the configuration can often be brought down to singletons just by adding parameters, instead of unary predicates, but these arguments seem difficult to adapt to tuple-coding configurations. Another approach, which we use here, is to take an instance of the configuration where the tuples have minimal length, and argue that the tuples then in many ways behave like singletons.
Definition 4.9.
Given a tuple-coding configuration , indexed by disjoint countable dense orderings , an order-preserving permutation of (resp. ) naturally gives rise to permutation of (resp. ; call such permutations of and standard permutations.
A tuple-coding configuration as above is regular if whenever (including cases with ), is a standard permutation of corresponding to an element of fixing , and is a standard permutation of corresponding to an element of fixing .
By Ramsey and compactness, if admits coding on tuples via the formula , then it admits a regular tuple-coding configuration via the same formula .
Definition 4.10.
Let be a tuple-coding configuration with countable, dense. The pair with is a witness for if there are open intervals with such that for all , we have .
A tuple-coding configuration has unique witnesses up to permutation if for every , the only witnesses for are of the form for some a permutation of and some a permutation of
Lemma 4.11.
Let be a regular tuple-coding configuration for , with minimal. Then this configuration has unique witnesses up to permutation.
Proof.
Suppose not, and let be a witness for , such that for any . First, if either or , then regularity immediately implies that is not a witness. So let be the subsequence of intersecting , and the subsequence of intersecting . Either or so assume the former.
Let be an open interval such that . Let be the formula obtained by starting with , and then replacing the subtuple with the variables ; so we have plugged the elements of as parameters into . For each , let be the restriction of to the coordinates corresponding to . Then is also a regular tuple-coding configuration, contradicting the minimality of . ∎
The following Lemma completes the proof of Theorem 4.1.
Lemma 4.12.
Suppose admits coding on tuples. Then admits coding in an expansion by three unary predicates.
Proof.
Choose a tuple-coding configuration
with as small as possible. By the remarks following Definition 4.9. we may assume this configuration is regular, so by Lemma 4.11, it has unique witnesses up to permutation. Let and let be the expansion of interpreting as , as , and as itself. Let
Let be the first coordinate of , and the first coordinate of . Then , and witness coding in via the -formula . ∎
5. Finite structures
In this section, we restrict the language of the theories we consider to be relational (i.e., no function symbols) with only finitely many constant symbols.
Definition 5.1.
For a complete theory and , , the isomorphism types of finite substructures of does not depend on the choice of , so we let denote this class of isomorphism types.
The growth rate of (sometimes called the profile or (unlabeled) speed) is the function counting the number of isomorphism types with elements in .
We also investigate under the quasi-order of embeddability.We say is well-quasi-ordered (wqo) if this class does not contain an infinite antichain, and we say is -wqo if is wqo for every expansion of any model of by unary predicates that partition the universe.
The definition of -wqo is sometimes given for an arbitrary hereditary class rather than an age, with -wqo if the class containing every partition of every structure of by at most unary predicates remains wqo. Our definition is possibly weaker, but then its failure is stronger.
Example 1.
Let . Then is wqo, but not 2-wqo, since contains arbitrarily long finite paths, and marking the endpoints of these paths with a unary predicate gives an infinite antichain.
By contrast, if , then can be shown to be -wqo for all .
The following lemma shows that when considering -wqo, adding finitely many parameters is no worse than adding another unary predicate.
Lemma 5.2.
Suppose is -wqo. If is an expansion of by finitely many constants, then is -wqo.
Proof.
Suppose an expansion by constants is not -wqo, as witnessed by an infinite antichain in a language expanding the initial language by the constants and by unary predicates. Let be the structure obtained from by forgetting the constants, but naming their interpretations by a single new unary predicate. As is -wqo, contains an infinite chain under embeddings. As there are only finitely many permutations of the constants, some embedding in the chain must preserve them, contradicting that is an antichain. ∎
In both Theorem 5.3 and 5.6, the assumption that has quantifier elimination is only used to get that the formula witnessing that admits coding on tuples is quantifier-free, and the formula witnessing the order property in the stability part of Theorem 5.6, so the hypotheses of the theorems can be weakened to only these specific formulas being quantifier-free. This weakened assumption is used in [ST]. From the proof of Proposition 3.11, if the failure of the f.s. dichotomy is witnessed by quantifier-free formulas, then the formula witnessing coding on tuples will be quantifier-free as well.
In Theorem 5.3, the growth rate statement remains intact, but the claim that is not 4-wqo is unproven. See Appendix A.2.
Theorem 5.3.
If a complete theory has quantifier elimination in a relational language with finitely many constants is not monadically NIP, then has growth rate asymptotically greater than for some and is not 4-wqo.
Proof.
Since is not monadically NIP, let
be a regular tuple-coding configuration with unique witnesses up to permutation. The only place we use has QE is to choose quantifier-free. Let expand by unary predicates for , and as well as constants for the parameters of , and let be as in the proof of 4.12. Let be the set of finite substructures that can be constructed as follows.
-
(1)
Pick , , and .
-
(2)
Start with .
-
(3)
For every point added in the previous step, add the four elements and , where are closer to than any other element of , and are closer to than any other element of .
-
(4)
Add the parameters of .
Claim.
For any and , .
Proof of Claim.
Since is quantifier-free, it remains to check that if the existential quantifiers in are witnessed in and then they are witnessed in , and if the universal fails in then it fails in . From the unary predicates at the beginning of , we may let , and . If , the only tuple in that can witness is the rest of the tuple , which will be in because it only contains full tuples, and similarly for witnessing . Since our configuration has unique witnesses up to permutation, if the universal quantifier fails in , this is witnessed by an element with and . By regularity, this failure is also witnessed by some element in . ∎
Given a bipartite graph with edges and no isolated vertices, we may encode it as a structure by starting with tuples for each point in one part and tuples for each point in the other part, and including whenever we want to encode an edge between and . Note that , and this encoding preserves isomorphism in both directions. In the proof of [Rap]*Theorem 1.5, the asymptotic growth rate of such graphs is shown to be at least , which gives the desired growth rate for with the constant depending on the length of the tuples in the tuple-coding configuration. Since expanding by finitely many unary predicates and constants increases the growth rate by at most an exponential factor, we also get the desired growth rate for .
Furthermore, if embeds into , then must be a (possibly non-induced) subgraph of . So we get that is not wqo by encoding even cycles. We expanded by three unary predicates, and by Lemma 5.2 the parameters may be replaced by another unary predicate while still preserving the failure of wqo, so we get that is not 4-wqo. ∎
Remark 5.4.
There is a homogeneous structure, with automorphism group in its product action, that is not monadically NIP and whose growth rate is the number of bipartite graphs with a prescribed bipartition, edges, and no isolated vertices. So the lower bound in this theorem cannot be raised above the growth rate of such graphs. Precise asymptotics for this growth rate are not known, although it is slower than and [CPS]*Theorem 7.1 improves Macpherson’s lower bound to for every .
If Conjecture 1 from the Introduction (in particular ) is confirmed, then the lower bound on the growth rate in Theorem 5.3 would also confirm [Rap]*Conjecture 3.5 that for homogeneous structures there is a gap from exponential growth rate to growth rate at least for some .
Theorem 5.3 is somewhat surprising. Since passing to substructures can be simulated by adding unary predicates, it is clear that if is monadically tame, then should be tame. However, unary predicates can do more, so it seems plausible that could be tame even though is not monadically tame. Our next theorem gives some explanation for why this does not occur, at least when assuming quantifier elimination.
First we need to define stability and NIP for hereditary classes. The following definition is standard and appears, for example, in [ST]*§8.1.
Definition 5.5.
For a formula and a bipartite graph , we say a structure encodes via if there are sets such that .
A class of structures has IP if there is some formula such that for every finite, bipartite graph , there is some encoding via . Otherwise, is NIP.
A class of structures is unstable if there is some formula such that for every finite half-graph , there is some encoding via . Otherwise, is stable.
Equivalently, by compactness arguments, is NIP (resp. stable) if and only if every completion of , the common theory of structures in , is. Note that it suffices to witness that has IP or is unstable using a formula with parameters, since we can remove them by appending the parameters to each .
The sort of collapse between monadic NIP and NIP in hereditary classes observed in the next theorem occurs for binary ordered structures [ST], since there the formula giving coding on tuples is quantifier-free. It also occurs for monotone graph classes (i.e. specified by forbidding non-induced subgraphs), where NIP actually collapses to monadic stability, and agrees with nowhere-denseness [AA].
Theorem 5.6.
Suppose that a complete theory in a relational language with finitely many constants has quantifier elimination. Then is NIP if and only if is monadically NIP, and is stable if and only if is monadically stable.
Proof.
We first consider the NIP case.
Suppose has IP, as witnessed by the formula . By compactness, there is a model of the universal theory of in which encodes the generic bipartite graph. But then is a substructure of some , and naming a copy of in by a unary predicate and relativizing to gives a unary expansion of with IP.
Suppose is not monadically NIP, witnessed by a tuple-coding configuration , , with quantifier-free and containing parameters . By Remark 3.12, we may also assume the configuration is tidy. For any bipartite graph , let contain , tuples from and corresponding to the two parts of , and an element of for each edge of so that encodes on . But by tidiness, encodes on as well.
For the stable case, the backwards direction is the same except using the infinite half-graph in place of the generic bipartite graph. For the forwards direction, if is unstable then by quantifier-elimination is also unstable. If is stable but not monadically stable, then by [BS]*Lemma 4.2.6 is not monadically NIP, so we are finished by the NIP case. ∎
Appendix A Corrigenda
A.1. Indiscernible triviality
In Theorem 1.1 of [MonNIP], several equivalents of a theory being monadically NIP are given. With the definition of indiscernible-triviality given there, (6) is not equivalent, as can be seen by Example 2 below. However, by making a slight variation on the definition of indiscernible-triviality the equivalence of (6) with the other properties is maintained. Call a linear order endless if it has neither a minimum nor a maximum element. Clearly, any endless linear order is infinite.
Definition A.1.
A theory has endless indiscernible triviality if for every endless indiscernible sequence and every set of parameters, if is indiscernible over each then is indiscernible over .
This is the same as the definition of indiscernible-triviality, except that infinite has been replaced by endless.
With this note, we prove the following theorem.
Theorem A.2.
Replacing indiscernible-triviality by endless indiscernible triviality, the six statements described in [MonNIP, Theorem 1.1] are equivalent.
Before launching into the proof of Theorem A.2, we highlight what the problem was in [MonNIP]. The first issue is the Furthermore clause in [MonNIP, Lemma 2.18], used in the proof of [MonNIP, Proposition 3.11]. We thank James Hanson for providing a counterexample to this clause. The second issue is that in the proof of [MonNIP, Proposition 3.11], we assumed that the failure of indiscernible triviality could be witnessed by a -indexed sequence, obliterating the distinction between indiscernible triviality and endless indiscernible triviality. To see that (full) indiscernible triviality can fail in a monadically NIP theory, we thank Artem Chernikov for indicating the following example.
Example 2.
Let be the theory of dense meet-trees as in [Pierre, Section 2.3.1]. By [parigot1982theories, Corollary 2.8], is monadically NIP. (It is also fairly easy to check the quantifier-free type-counting criterion in [MonNIP, Proposition 4.8] over indiscernible sequences of singletons, which is sufficient.) Let , let be a decreasing sequence, and let be such that and . Then is indiscernible over and over , but not over .
In the remainder of this section, we prove Theorem A.2 and indicate where the endlessness assumption is used. The following definition, which appears in [Pierre], is standard.
Definition A.3.
Two sequences and (not necessarily of the same arities) are mutually indiscernible over if is indiscernible over and is indiscernible over .
In [MonNIP], in order to recover Theorem 1.1, it suffices to recover Proposition 3.11, so in the notation there, define
which is identical to the existing (2), but now with endless indiscernible triviality replacing indiscernible-triviality.
Again in the notation of Proposition 3.11, we must show that and that .
The existing proof that is easily modified to show . The only issue is that the convex piece containing might not be endless. But in this case, the convex piece containing must be , which is endless. So we may conclude the argument substituting for and for .
Establishing the implication is more involved, where states that has the f.s. dichotomy. Without going through the problematic , the paper still contains a proof of , where asserts that there does not admit a pre-coding configuration. Before tracing this proof, we recall the relevant definitions from [MonNIP].
Definition A.4.
has the f.s. dichotomy if, for all models , all finite tuples , if is finitely satisfied in , then for any singleton , either or is finitely satisfied in .
Definition A.5.
A pre-coding configuration consists of a with parameters and a sequence , indiscernible over the parameters of , such that for some (equivalently, for every) from , there is such that
-
(1)
;
-
(2)
for all ; and
-
(3)
for all .
In [MonNIP, §4], it is proved (without using [MonNIP, Proposition 3.11]) that if has the f.s. dichotomy, then does not admit coding on tuples, which is condition in [MonNIP, Proposition 3.11]. Thus the implication in [MonNIP, Proposition 3.11] shows that if has the f.s. dichotomy then does not admit a pre-coding configuration. (We take this opportunity to note that after the first sentence in the proof of in [MonNIP, Proposition 3.11], the following should be inserted: “By Ramsey and compactness, we may assume that the truth value of depends only on the order-type of .”)
Evidently, the existence of a pre-coding configuration is a statement about a certain configuration being consistent with , hence one can use Compactness to construct such configurations from many variations. We record two variants in the following lemma.
Lemma A.6.
admits a pre-coding configuration if either of the following hold:
-
(1)
There is a sequence (not necessarily indiscernible) and a formula such that, for every there is such that
-
•
:
-
•
for every ; and
-
•
for every .
-
•
-
(2)
Or there is an indiscernible sequence and a formula such that, for some there is such that
-
•
:
-
•
for every ; and
-
•
for every .
-
•
Proof.
(1) is immediate by Compactness. For (2), we first extend our given indiscernible sequence to an indiscernible sequence , maintaining the extra conditions that for all , and that for all , in three steps, all using Compactness. First, since is an infinite, indiscernible sequence over , for which for every such , by Compactness there is an extension of this segment to maintaining indiscernibility of the entire expanded sequence, as well as . Dually, we can find an extension of maintaining indiscernibility with for every , . Finally, for the middle segment , we only need to maintain indiscernibility. Although the sequence is finite, it is part of an endless indiscernible sequence. Thus, it follows by Compactness that there is an extension of , for which the entire sequence is indiscernible. So we have constructed an indiscernible sequence with some distinguished pair for which a witnessing element exists. However, as is 2-homogeneous and since every induces an automorphism of , we conclude that for every , a witnessing element exists. Thus, we obtain a pre-coding configuration. ∎
We now assume has the f.s. dichotomy. The proof that is dp-minimal in the existing proof of in [MonNIP, Proposition 3.11] is unchanged. In fact, the proof gives the following stronger statement.
Lemma A.7.
If has the f.s. dichotomy, then for every indiscernible sequence and singleton , there is a partition where is either empty or a singleton, such that and are mutually indiscernible over .
In the case where is Dedekind complete, we may assume is a singleton.
We will assume that has the f.s. dichotomy but fails endless indiscernible triviality and eventually arrive at one of the two clauses of Lemma A.6, giving our contradiction. Endlessness of is crucial as once we cut the indiscernible sequence into two mutually indiscernible halves, we still have that each half is an infinite indiscernible sequence and thus can be extended. In a nutshell, this extendibility of each half is what is failing in Example 2.
Lemma A.8.
Suppose has the f.s. dichotomy, is an endless, Dedekind complete linear order, is indiscernible over , but not over for some singleton . Then there are , a finite , and an -definable such that
-
(1)
is indiscernible over ;
-
(2)
The subsequences and are mutually indiscernible over ;
-
(3)
The sequence of truth values of is not constant.
Proof.
Since is not indiscernible over , we apply Lemma A.7, and let be the singleton element of there. Since is endless, choose with . Choose a formula witnessing that is not indiscernible over . By mutual indiscernibility over there must be some for which: for some/every , for some/every , the truth values of the three statements
-
•
;
-
•
;
-
•
are non-constant. Let extend . By Compactness, choose new tuples , such that the extended sequences and remain mutually indiscernible over . Put
and let . This works. ∎
Lemma A.9.
Suppose has the f.s. dichotomy. Then has endless indiscernible triviality.
Proof.
Assume, by way of contradiction, that fails endless indiscernible triviality. An easy induction on gives that there is some finite and singletons for which some endless supports a sequence that is indiscernible over and , but not over . By adding constants to the language we may assume and, as embeds into any endless linear order, we may take . Summarizing, we assume the existence of a sequence that is indiscernible over and individually, but not over . Now, working over , apply Lemma A.8 to this sequence and to obtain , a finite set and an -definable as there. To make the dependence on explicit, write as , so is -definable. As is transitive, we may assume . We summarize the situation from the point of view of , which we now label as . We have:
-
(1)
is indiscernible over ; and
-
(2)
for , we have
-
(a)
is indiscernible over ;
-
(b)
and are mutually indiscernible over ;
-
(c)
The truth value of is non-constant.
-
(a)
Because of (1), there is an automorphism of fixing with for all . Let , the -fold iteration of (this also makes sense for and ). Thus, with the same and , we have that for every , is indiscernible over : and are mutually indiscernible over ; and the truth value of is non-constant. We remark that we have again made crucial use of the endlessness of our indiscernible sequence to extend from a singleton to a whole sequence.
Now, keeping fixed, we ‘couple’ each by its corresponding , and then by Ramsey’s Theorem and Compactness we get that for any endless there are tuples (possibly distinct from the original elements) satisfying the following conditions:
-
(1)
The sequence is indiscernible over ;
-
(2)
For all ,
-
(a)
The sequence is indiscernible over ;
-
(b)
The subsequences and are mutually indiscernible over ; and
-
(c)
The truth values of is non-constant.
-
(a)
The following claim will allow us to define a pre-coding configuration.
Claim 1.
There is a sequence that is indiscernible over with indiscernible over and an -definable formula such that
-
(1)
For all , if and only if ; and
-
(2)
For every singleton and , there is at most one such that .
Proof of Claim.
Consider the sequence obtained above with . As notation, for each write each ‘triple’ as and let be the concatenation of the triple. In what follows we only consider for each . Finally, put
Thus, we have is indiscernible over , and for each we have is indiscernible over and the pair of subsequences and are mutually indiscernible over . Moreover, for any , if and only if .
To get the final clause, choose any and . We know the original sequence is indiscernible over . If it is also indiscernible over , then the truth value of is constant, hence holds for every . On the other hand, if it fails to be indiscernible over , then, working over , we apply Lemma A.8 to the sequence . Choose for which the subsequences and are mutually indiscernible over . Choose such that . Then for any , with , the triple lies in one of the two subsequences. Thus, by indiscernibility we have for all . ∎
Continuing, as is indiscernible over , choose an automorphism such that for every , and also . For each , let denote the -fold composition of , so e.g., , while . As notation, put .
For each , let . There are now two cases, each of which leads to a pre-coding configuration.
Case 1. Some is not well ordered.
Fix such an . Fix a strictly decreasing sequence from and put . Thus describes a subordering of of order type . For , let denote the concatenation and let . That and satisfy the hypotheses of Fact A.6(2) with , , and follows from the following claim.
Claim 2.
-
(1)
;
-
(2)
for all ;
-
(3)
for all .
Proof of Claim.
(1) We have , hence applying gives , i.e., .
(2) We know that for any , , so applying yields .
(3) Since , we have . But then by the final clause of Claim 1, we have for . ∎
Case 2. Not Case 1, i.e., every is well ordered.
In this case, for any , the shifted set
is well ordered as well. Since any well-ordered subset of is nowhere dense, it follows by Baire category that the complement
is not nowhere dense. Thus, contains a strictly decreasing sequence , so has order type . For each , let denote the concatenation , let , and let . Here, we will get an instance of pre-coding via Fact A.6(1), as witnessed by , , and the witnesses for from , once we establish the following claim.
Claim 3.
For every and , the following hold.
-
(1)
;
-
(2)
For all , ; and
-
(3)
For all , .
Proof of Claim.
(1) and (2). By Claim 1(1), we have and for any we have . Applying yields , but for any .
For (3), given , put . Since , , so . Then, applying (and using ) yields , as required. ∎
∎
A.2. Well-quasi-order
In [MonNIP, Theorem 5.3], the proof that is not 4-wqo is flawed. The issue is that the formula is not existential, and thus neither is the formula that we use to define the edges of our graphs. Since the formula is not existential, it need not be preserved by embeddings. Thus the first sentence of the last paragraph of the proof is unjustified.