1. Introduction
One of the most exciting areas of research in modern model theory is the classification along various dividing lines of non-simple but otherwise tame theories, especially theories for . The first two of these properties, introduced in
[12], require the nonexistence of certain trees:
Definition 1.1.
A theory is if there does not exist a formula and tuples so that is consistent for any , but for any , is inconsistent. Otherwise it is .
Definition 1.2.
A theory is if there does not exist a formula and tuples so that is consistent for any , but for incomparable and , is inconsistent. Otherwise it is .
The property is introduced in [29] as part of a family of notions for :
Definition 1.3.
A theory is (that is, does not have the n-strong order property) if there is no definable relation with no -cycles, but with tuples with for . Otherwise it is .
Fact 1.4.
([29], [12]) Simple theories are , and theories are for .
In [30] it is shown that , the model companion of the theory of parametrized equivalence relations, is but not simple; a limited number of further examples have since been found by various authors. Yet the main problem, posed by Džamonja and Shelah in [12], has remained unsolved:
Problem 1.5.
Are all theories ? Are all theories ?
In this paper we answer the latter question in the positive:
Theorem 1.6.
All theories are .
One reason for the significance of this problem comes from Shelah and Usvyatsov’s proposal in [30] to characterize classes of theories both internally in terms of the structure of their sufficiently saturated models, and externally in terms of orders on theories. The theories have a deep external characterization: under the generalized continuum hypothesis, Džamonja and Shelah [12] show that maximality in the order , an order related to the Keisler order, implies a combinatorial property related to , which Shelah and Usvyatsov then show in [30] to be the same as ; later, Malliaris and Shelah in [24] show the equivalence between and -maximality under the generalized continuum hypothesis. On the other hand, theories can be characterized internally not only in terms of trees, but through the theory of independence, in analogy with stability theory. It is well known that simple theories are characterized as those theories where forking and dividing behave in certain ways as they do in stable theories; for example, symmetry of forking characterizes simple theories. In [16], Kaplan and Ramsey show that Kim-forking, or forking witnessed by invariant Morley sequences, is the correct way of extending the theory of forking to theories from simple theories. By relaxing the requirement of base monotonicity, they extend the Kim-Pillay characterization of simple theories in terms of the existence of abstract independence relations to theories, and, more concretely, characterize theories by the symmetry of Kim-independence, by the independence theorem for Kim-independence, and by a variant of Kim’s lemma in simple theories, asserting that Kim-dividing of a formula, rather than dividing, is witnessed by any invariant Morley sequence. Our result that theories coincide with theories therefore shows a surprising agreement between dividing lines related to Keisler’s order and dividing lines related to independence.
We outline the paper and give a word on the strategy for the proof. In section 3, we develop in general theories a version of a construction used by Chernikov and Kaplan in [6] to study forking and dividing in theories. In [1], Adler initiated the study of abstract relations between sets in a model, generalizing some of the properties of forking-independence, coheirs, and other concrete relations from model theory, and provided a set of potential axioms for these relations. We notice that the construction of Chernikov and Kaplan can be relativized to relations between sets satisfying certain axioms, obtaining new relations between sets from old ones, and iterate this construction to obtain a canonical class of coheirs in any theory.
In section 4, we study this canonical class of coheirs in theories. Before the development of Kaplan and Ramsey’s theory of Kim-independence in theories in [16], Chernikov [5] proposed finding a theory of independence for theories, and the proof of our main result comes from our efforts to answer this proposal. Just as in [6], Chernikov and Kaplan’s construction gives maximal classes in the dividing order of Ben Yaacov and Chernikov [33], we show that in theories our variant of this construction gives minimal classes in the restriction of this order to coheir Morley sequences, proving an analogue of Kim’s lemma. As a by-product of this construction, we also initiate the theory of independence in a class related to the theories of Ahn and Kim [2], the study of which was further developed by Ahn, Kim and Lee in [3], showing that under this assumption Kim-forking and Kim-dividing coincide for coheir Morley sequences. (See [20] for the question of finding an analogue for theories of the role that theories play relative to simple theories, and developing Kim-independence in that analogue; that Kim-forking coincides with Kim-dividing for coheir Morley sequences in a related class gives us preliminary evidence that completes this analogy.)
In section 5, we investigate behavior similar to theories in theories. We introduce the notion of Conant-independence, which will generalize the relation defined by in the free amalgamation theories introduced by Conant [8] (based on concepts used to study the isometry groups of Urysohn spheres in [32]); see the following section. While it will end up coinciding with Kim-independence in our case, we studied a version of Conant-independence in a potentially strictly , potentially generalization of free amalgamation theories in [26]. Conant-independence in theories can be defined as Kim-independence relative to canonical Morley sequences, just as is Kim-independence relative to free amalgamation Morley sequences (as in lemma 7.7 of [8]); it can also be defined by forcing Kim’s lemma on Kim-independence, requiring a formula to divide with respect to every Morley sequence instead of just one, as suggested in tentative remarks of Kim in [17] in his discussion of strong dividing in subtle theories. We show that many of Ramsey and Kaplan’s arguments on Kim-independence in theories in [16] can be generalized to Conant-independence in theories, including a chain condition, symmetry and a weak independnece theorem. (But as is apparent in [8] and [26], similar behavior can occur in a theory, which is why the following section is essential to the proof of our main result.)
In section 6, we conclude the proof of Theorem 1.6. One consequence of Conant’s free amalgamation axioms (say, the freedom, closure and stationarity axioms, in Defintion 2.1 in [8]) is the following:
Let denote free amalgamation and , , and with . Then there is some with and .
We will have shown in the prior section that Conant-independence is symmetric, and that a similar fact holds, roughly, when replacing free amalgamation with canonical coheirs and with Conant-independence. Conant shows in [8] that modular free amalgamation theories must either be simple or (see [14] for a related result on countably categorical Hrushovski constructions), starting with a failure of forking-independence to coincide with (because forking-independence cannot be symmetric unless a theory is simple) and using the above fact to build up a configuration giving . Starting, analogously, with the assumption that an theory is , so Kim-dividing independence is not symmetric and therefore fails to coincide with Conant-independence, we simulate Conant’s construction of an instance of . In short, we show that a theory is either or . But a theory is of course not , so it must be .
2. Preliminaries
We let denote sets, potentially with an enumeration depending on context, and denote tuples of variables. We let denote a sufficiently saturated model of a theory and let denote an elementary submodel. We write to denote the union (or concatenation) of the sets and , and write , , etc. for infinite sequences (or sometimes trees) of tuples or an infinite linearly ordered set.
Roughly following the axioms for abstract independence relations in [1], as well as others that are standard in the literature, we define the following axioms for relations between sets over a model:
Invariance: For all , implies .
Full existence: For , there is always some with .
Left extension: If and , there is some with .
Right extension: If and , there is some with .
Left monotonicity: If and , then
Right monotonicity: If and , then
(We will refer to the two previous properties, taken together, as monotonicity.)
Symmetry: If then
Coheirs and Morley sequences
A global type is a complete type over . For for , we say is finitely satisfiable over or a coheir extension of its restriction to if every formula in is satisfiable in . Global types finitely satisfiable in are invariant over : whether belongs to for a formula without parameters, depends only on the type of the parameter over . We write to denote that is finitely satisfiable in . We let denote . The relation (over models) is well-known to satisfy all of the above properties other than symmetry. We say , for potentially finite, is a coheir sequence over if for . We say a coheir sequence , for infinite, is moreover a coheir Morley sequence over if there is a fixed global type finitely satisfiable in so that for . The type of a coheir Morley sequence over (indexed by a given set) is well-known to depend only on , and coheir Morley sequences are known to be indiscernible; the type of a coheir sequence over depends only on the global coheirs over extending the .
theories and Kim-dividing
In this paper we use nonstandard terminology: Kim-dividing, etc. are defined in terms of Morley sequences in invariant types over rather than finitely satisfiable types over in [16]. The reason why we do this is that is known to satisfy left extension. This will do us no harm for our main result, though when we briefly consider Kim-forking in some theories, we will note the nonstandard usage.
Definition 2.1.
A formula Kim-divides over if there is an coheir Morley sequence starting with so that is inconsistent (equivalently, -inconsistent for some : any subset of size is inconsistent). A formula Kim-forks over if it implies a (finite) disjunction of formulas Kim-dividing over . We write , and say that is Kim-dividing independent from over if does not include any formulas Kim-dividing over .
The following follows directly from Proposition 5.2 of [7]; see also Proposition 3.22 of [16] (where the evident argument for the version for invariant types is given) and Theorem 5.16 of [16] for the full symmetry characterization of .
Fact 2.2.
Symmetry of implies .
theories
A characterization of as - was proven by Kim and Kim in [18], where they also introduce the notion of weak -, prove that it implies , and conjecture that it also implies :
Definition 2.3.
The theory has weak - if there exists a formula and tuples so that is consistent for any , but for pairwise incomparable with common meet, is inconsistent.
Later, Chernikov and Ramsey, in Theorem 4.8 of [7], claim to show that weak - implies , but their proof is incorrect; the embedded tree in the proof of that theorem is not actually strongly indiscernible over the parameter set . In an earlier version of this paper, we used this result. In this section, we will introduce an equivalent form of that will suffice for our argument, and use the same method as [7] to give a proof that will work to show this equivalence despite failing for weak -.
Definition 2.4.
(Proposition 2.51, item IIIa, [102]). A list is a descending comb if and only if it is an antichain so that , and so that, for ,
So for example, all descending combs of length have the same quantifier-free type in the language as the descending comb ; meanwhile, is an example of a lexicographically ordered antichain that is not a descending comb.
Definition 2.5.
(Definitions 11 and 12, [31]) For tuples of elements of , we write to mean that has the same quantifier-free type in the language as . For a tree-indexed set of tuples and an -tuple of elements of , we write , and call strongly indiscernible over a set if for all tuples of elements of with , .
Fact 2.6.
(Theorem 16, [31]; see [28] for an alternate proof) Let be a tree-indexed set of tuples, and a set. Then there is strongly indiscernible over so that for any tuple of elements of and , if for all , then .
Definition 2.7.
The theory has - if there exists a formula and tuples so that is consistent for any , but for any descending comb , is inconsistent.
Lemma 2.8.
For any , a theory has if and only if it has -.
Proof.
() The property - follows directly from Fact 4.2, [7].
() We follow the proof of theorem 4.8 of ([7]), which is incorrect for the claimed result. Let witness with the formula . By fact 2.6, we can assume is strongly indiscernible (as paths and descending combs are preserved under -equivalence), and will produce a witness to . Let (so that, say, will form a descending comb), and let be maximal so that
|
|
|
is consistent; by consistency of the paths, will be at least , and by inconsistency of descending combs of size , will be at most . Let . We see that, say, sits strictly above the meets of any two or more of the for in the order , and is incomparable to and lexicographically to the left of when , so the appropriately tree-indexed subset of consisting of those with (that is, where ) really is strongly indiscernible over . By strong indiscernibility of and the fact that is consistent, is consistent; let realize it, and by Ramsey, compactness and an automorphism over , we can assume is indiscernible over . On the other hand, for , we see that is inconsistent, by strong indiscernibility of and inconsistency (by maximality of ) of (noting that, say, contains ). This is exactly what the “path collapse lemma,” Lemma 4.6 of [7], tells us that we need to obtain .
∎
Though the proof of Theorem 4.8 of [7] is incorrect, that theorem (albeit, not a “local” version) will be a corollary of our main result, Theorem 1.6, and the result of [18] that weak - implies . (Note that is just weak -).
Corollary 2.8.1.
(to Theorem 1.6) For any , a theory has weak - if and only if it has .
3. Canonical coheirs in any theory
The following section will require no assumptions on . Iterating a similar construction to the one used by Chernikov and Kaplan in [6] to prove the equivalence of forking and dividing for formulas in theories, we will contruct a canonical class of coheir extensions in any theory. This class will end up satisfying a variant of the “Kim’s lemma for Kim-dividing” in theories (Theorem 3.16 of [16]) when considered in a theory.
Proposition 3.1.
Let be any theory. Consider relations between sets over a model that are stronger that , satisfy invariance, monotonicity, full existence and right extension, and satisfy the coheir chain condition: if and is a coheir Morley sequence starting with , then there is some with and each term of satisfying . There is a weakest such relation .
The “weakest” clause is not necessary for the main result, but we include it anyway to show our construction is canonical.
We start by relativizing the notions of Kim-dividing, Kim-forking, and quasi-dividing (Definition 3.2 of [6]) to an -invariant ideal on the definable subsets of .
Definition 3.2.
Let be an -invariant ideal on the definable subsets of . A formula -Kim-divides over if there is a coheir Morley sequence starting with so that for some , the intersection of some (any) -element subset of belongs to . We say -Kim-forks over if it implies a (finite) disjunction of formulas -Kim-dividing over . We say -quasi-divides over if there are with so that .
We say if .
The proof of the following lemma is adapted straightforwardly from the proof of the “broom lemma” of Chernikov and Kaplan (Lemma 3.1 of [6]). For the convenience of the reader we give a simplified proof of the modified version; note that this version is just a rephrasing in terms of ideals of Lemma 4.19 in [4]:
Lemma 3.3.
(“-broom lemma”) Suppose
|
|
|
with -Kim-dividing over with respect to and . Then there are some with so that . In particular, -Kim-forking implies -quasi-dividing over .
Proof.
We need the following claim:
Claim 3.4.
Let begin a coheir Morley sequence in a global type finitely satisfiable over . Let and let be any tuple. Then there are so that begin a coheir Morley sequence and . (The same is true for Coheir morley sequences themselves, rather than just their initial segments).
Proof.
Left extension for gives a global type finitely satisfiable over extending both and . Now take a coheir Morley sequence in and apply an automorphism. The parenthetical is similar.
∎
Now we can prove the lemma by induction on . Write as , and let . Let be a global coheir extension of . Let be such that and for and . By the claim, find so that and for . Then we can assume . From , together with for , it is easy to check for , and therefore
|
|
|
for .
Now for we have . Let for . Then
|
|
|
But by choice of the ,
|
|
|
Now for , because , will be of the form for -Kim-dividing over . So, as the first of steps, we can apply and the inductive hypothesis on to find some conjunction of conjugates of (which will therefore be a conjunction of conjugates of ) so that
|
|
|
Repeating more times, we are done.
We now begin our construction. The following terminology comes from the notion of strong finite character (used in e.g. [7]).
Definition 3.5.
Let be an invariant relation between sets over a model. We say that satisfies quasi-strong finite character if for complete types over some model , is type-definable.
Definition 3.6.
Let be an invariant relation between sets over a model satisfying monotonicity, right extension and quasi-strong finite character, and fix a complete type over a model .
(1) A set of formulas is -inconsistent with respect to if there is no with and for all .
(2) A formula -Kim-divides with respect to if there is a coheir Morley sequence starting with so that is -inconsistent with respect to .
(3) A formula -Kim-forks with respect to if it implies a disjunction of formulas -Kim-dividing with respect to .
(4) A formula -quasi-divides over with respect to if there are with and -inconsistent with respect to .
Lemma 3.7.
(1) The sets defined by formulas so that is -inconsistent with respect to form an -invariant ideal .
(2) A set is -inconsistent with respect to if and only if some finite subset is (so its conjunction defines a set in the ideal .)
Proof.
For (1), it suffices to show (a) that if , and is -inconsistent with respect to , then is -inconsistent with respect to , and (b) that if both and are -inconsistent with respect to then so is . For (a), suppose otherwise; then there is some realization of with and . By right extension, we can assume . But then , and by right monotonicity, , contradicting that is -inconsistent with respect to . For (b), suppose otherwise; then there is some realization of with and ; without loss of generality, , and by right monotonicity, , contradicting that is -inconsistent with respect to . The proof of (a) also gives us the fact that a set is -inconsistent with respect to if some finite subset is (so its conjunction defines a set in the ideal ). To complete (2), we show the “only if” direction. If is -inconsistent with respect to then there is no realization of with . But the set of realizations of that satisfy is, by quasi-strong finite character, type-definable. So by compactness, there must be some finite so there is no realization of with . But if there is a realization of with , then we can even get by right-extension, so will be as desired.
∎
Corollary 3.7.1.
For all formulas, -Kim-forking with respect to implies -quasi-dividing with respect to .
Proof.
By Lemma 3.7, -Kim-dividing with respect to is just -Kim-dividing. Apply Lemma 3.3 to .
∎
Lemma 3.8.
If a formula is -inconsistent with respect to , then it is -inconsistent with respect to any complete type extending . So the same is true for -Kim-dividing and -Kim-forking.
Proof.
Suppose otherwise. Then there is a realization of with . So by left monotonicity, , but realizes , a contradiction.
∎
We are now in a position to study derived independence relations:
Definition 3.9.
Let be an invariant relation between sets over a model satisfying monotonicity, right extension and quasi-strong finite character. Then we define to mean that does not contain any formulas -Kim-forking with respect to .
Lemma 3.10.
Suppose is an invariant relation between sets over a model satisfying monotonicity, right extension, quasi-strong finite character, and full existence. Then so is .
Proof.
Invariance is obviously inherited from . Quasi-strong finite character is by construction and right extension is also standard from the construction: if but, for some there is no with , then must imply a disjunction of formulas with parameters in -Kim-forking with respect to ; some formula in must then imply this disjunction, which will then -Kim-fork with respect to , contradicting . Right monotonicity is by definition. Left monotonicity is Lemma 3.8. It remains to show full existence; the proof is a straightforward generalization of the proof of Lemma 3.7 of [6]. By right extension, it suffices to show that for any tuple (the “existence” property that is implied by full existence). Suppose otherwise; then contains a formula for that -Kim-forks over . By Corollary 3.7.1, -quasi-divides over . Since , this just means that . But since , this contradicts full existence for .
∎
The next observation is required to produce a relation with the coheir chain condition:
Lemma 3.11.
Let be as in Lemma 3.10 and suppose . Then for a coheir Morley sequence starting with , there is with and each term of satisfying . In particular, implies , so -Kim-forking implies -Kim-forking.
Proof.
Suppose otherwise: then for , is -inconsistent with respect to , so by part (2) of Lemma 3.7, some finite subset must be -inconsistent with respect to . This gives us a formula in that -Kim divides with respect to , a contradiction.
∎
Note that satisfies the assumptions of Lemma 3.10. Now define inductively, , . Let . Then because -Kim-forking implies -Kim-forking, and means that does not contain a -Kim-forking formula for any , right extension and quasi-strong finite character are standard. Monotonicity and invariance follows from monotonicity and invariance of the . By right extension for , full existence for would follow from the existence property for any , but this just follows from full existence for each of the . Finally, the coheir chain condition follows from Lemma 3.11 together with quasi-strong finite character for the and compactness.
It remains to show that is the weakest relation implying and satisfying these properties. Let be some other such relation and assume by induction that implies Assume ; we show . Suppose otherwise; by right extension for , we can assume contains a formula that -Kim-divides with respect to . Let be a coheir Morley sequence starting with witnessing this. Then by the coheir chain condition for , there is some with , so in particular by induction, and with for , so in particular with satisfying , a contradiction.
This completes the proof of Proposition 3.1.
4. Canonical coheirs in theories
The goal of this section is to prove a version of “Kim’s lemma for Kim-dividing” for canonical Morley sequences in theories.
Lemma 4.1.
Let be a type over . Then it has a global extension so that for all tuples , if , then . So in particular, is a global coheir of .
Proof.
In a very large , full existence and invariance for , and an automorphism, gives us a realization of with . Now take to be , and the lemma follows by monotonicity on the left.
∎
Definition 4.2.
We call as in Lemma 4.1 a canonical coheir, and a coheir Morley sequence in it a canonical Morley sequence.
Theorem 4.3.
Let be . Suppose a canonical Morley sequence witnesses Kim-dividing of a formula over . Then there is a finite bound (depending only on and the degree of Kim-dividing witnessed by the canonical Morley sequence) on the length of a coheir sequence over of realizations of so that is consistent. In particular, every coheir Morley sequence starting with witnesses Kim-dividing of over .
To start, we introduce the notion of a coheir tree in a general theory .
Definition 4.4.
Let be any type over . We say that a tree of realizations of is a coheir tree in if
(1) for each , (the sequence consisting of the subtrees above a fixed node) is a coheir Morley sequence over .
(2) there are global coheir extensions of so that for each , .
The key lemma of this section allows us to construct coheir trees in any theory so that sequences of nodes with common meet are canonical Morley sequences. Abusing the language by nodes, paths, etc. we often refer to the tuples which they index; the term “descending comb” will have a similar meaning in a tree of finite height or a set of subtrees as it does in .
Lemma 4.5.
Let be any type over . Let be a canonical coheir extension of . Let be a coheir sequence over of realizations of . Then there is a coheir tree indexed by , any path of which, read in the direction of the root, realizes , and descending comb of which, read in lexicographic order, begin a canonical Morley sequence in .
Proof.
We need the following claim:
Claim 4.6.
If and is a coheir tree in , then there is some with (so in particular ) each term of which satisfies .
Proof.
Let ; we find as desired. The proof is by downward induction on : suppose is already constructed, and we construct . First, comes directly from the chain condition. Second, by left extension for , find some copy of over with and some arbitrary term of satisfying the conjugate to of (that is, from Definition 4.4). Then use the chain condition to find some with and . Finally, using monotonicity on the right, discard all the terms of other than the one corresponding to the chosen term of , to obtain .
∎
Now by induction, it suffices to show this for a coheir sequence assuming is already constructed for . First, we find a long coheir sequence of realizations of so that each node of satisfies ; then having taken it long enough, we can find a coheir Morley sequence with the same property, preserving the condition on descending combs. (Any descending comb inside of these copies will either lie inside of one copy of , so will of course begin a descending Morley sequence inside of by the induction hypothesis, or will consist of a descending comb inside one copy followed by an additional node of a later copy for , which will indeed continue the Morley sequence in begun by the previous nodes.) Suppose already constructed; taking in the above claim and , we can choose to be the given by the claim.
Now let be a global extension, finitely satisfiable in , of . Then we take as the new root, guaranteeing the condition on paths. Now reindex accordingly.
We can now prove Theorem 4.3. Let be a canonical coheir extension of and the degree of Kim-dividing for witnessed by a canonical Morley sequence in . Let be a coheir sequence over of realizations of so that is consistent. Then the coheir tree given by the previous lemma gives the first levels of an instance of -: the -dividing witnessed by canonical Morley sequences in gives the inconsistency condition for descending combs of size , and the consistency of gives the consistency of the paths. So if is without bound, we must have - for by compactness, and thus by lemma 2.8. This concludes the proof of 4.3.
We have some applications of this proof to a notion related to the theories introduced by Ahn and Kim in [2], and studied in greater depth by Ahn, Kim and Lee in [3], assuming the analogue of lemma 2.8. The result for theories would be interesting because while theories are [2], as Ahn, Kim and Lee have shown in [3], there are examples of theories. The following is the original definition from [2]:
Definition 4.7.
The theory has (the negation of the antichain tree property) if there does not exist a formula and tuples so that is -inconsistent for any , but for pairwise incompararable , is consistent.
In [3], Ahn, Kim and Lee define a theory to have - if the above fails replacing -inconsistency with -inconsistency, and show that for any , a theory fails to be (that is, has -) if and only if it has -. That is, they show the analogue for theories of results of Kim and Kim in [18] on theories, but of not those claimed by Chernikov and Ramsey in [7], nor of the above Lemma 2.8. One might ask whether, for any , the following definition is equivalent to the failure of :
Definition 4.8.
The theory has - if there exists a formula and tuples so that is -inconsistent for any , but for any descending comb , is consistent.
If so, then the following applies to theories:
Theorem 4.9.
Let be a theory so that, for all , does not have -. Let be any model and any tuple. Then there is a global type extending , finitely satisfiable in , so that for any formula with parameters in , if coheir Morley sequences in this type do not witness Kim-dividing of , no coheir Morley sequence over starting with witnesses Kim-dividing of over .
This follows from the same construction. The following corollary is standard; see Corollary 3.16 of [6] for a similar argument:
Corollary 4.9.1.
If, for all , does not have -, then Kim-forking (with respect to coheir Morley sequences) coincides with Kim-dividing (with respect to coheir Morley sequences).
5. Conant-independence in theories
We introduce a notion of independence which will generalize, in the proof of the main result of this paper, the role played by in the free amalgamation theories introduced in [8]. The notation comes from the related notion of Kim-independence from [16], ; a similar notion involving dividing with respect to all (invariant) Morley sequences is suggested in tentative remarks of Kim in [17].
Definition 5.1.
Let be a model and a formula. We say Conant-divides over if for every coheir Morley sequence over starting with , is inconsistent. We say Conant-forks over if and only if it implies a disjunction of formulas Conant-dividing over . We say is Conant-independent from over , written , if does not contain any formulas Conant-forking over .
Note that this definition differs from the standard definition of Conant-independence given in [26], in that it uses coheir Morley sequences rather than invariant Morley sequences. In [21] Alex Kruckman and the author show how to carry out this proof with the standard Conant-independence. We may also dualize Theorem 3.10 of [19].
Proposition 5.2.
In any theory , Conant-forking coincides with Conant-dividing for formulas, and has right extension.
Proof.
We see first of all that Conant-dividing is preserved under adding and removing unused parameters: it suffices to show that if then Conant-divides over if and only if Conant-divides over . Let be a coheir Morley sequence starting with witnessing the failure of Conant-dividing of the latter; then witnesses the failure of Conant-dividing of the former. Conversely, let be a coheir Morley sequence starting with witnessing the failure of Conant-dividing of ; then by Claim 3.4 and an automorphism there are so that is a coheir Morley sequence starting with , and this will witness the failure of Conant-dividing of . The result is now standard, following, say, the proof in [16] of the analogous fact for Kim-dividing under Kim’s lemma. Suppose Conant-forks over but does not Conant-divide over ; by the above we can assume it implies a disjunction of the form where Conant-divides over . Let be a coheir Morley sequence starting with witnessing the failure of Conant-dividing, so there is some realizing . Then by the pigeonhole principle, there is some so that realizes infinitely many of the . By an automorphism this contradicts Conant-dividing of
Right extension is standard and exactly as in Lemma 3.10: if but there is no with , then must imply a disjunction of formulas with parameters in Conant-forking over ; some formula in must then imply this disjunction, which will then Conant-fork over , contradicting .
∎
The following is immediate from Theorem 4.3:
Corollary 5.2.1.
Let be . Then a formula Conant-divides (so Conant-forks) over if and only if it Kim-divides with respect to some (any) canonical Morley sequence.
We develop the theory of Conant-independence in theories in analogy with the theory of Kim-independence in theories.
Proposition 5.3.
(Canonical Chain Condition): Let be and suppose . Then for any canonical Morley sequence starting with , we can find some indiscernible over ; any such will satisfy .
Proof.
This is similar to the proof of, say, the analogous fact about Kim-independence in theories (Proposition 3.21 of [16]). The existence of such an follows from the previous corollary by Ramsey and compactness. To get , let ; it suffices to show for any . But is a coheir Morley sequence over starting with , each term of which satisfies , so follows.
∎
Theorem 5.4.
Let be . Then Conant-independence is symmetric.
Proof.
Suppose otherwise, so for some , but is Conant-dependent on over . We use to build trees as in the proof of symmetry of Kim-independence for theories (the construction is Lemma 5.11 of [16].) Specifically, what we want is, for any , a tree , infinitely branching at the first levels and then with each for at level followed by a single additional leaf at level , satisfying the following properties:
(1) For ,
(2) For , the subtrees above form a canonical coheir sequence indiscernible over , so by Proposition 5.3, is Conant-independent over from those branches taken together.
Suppose already constructed; we construct . We see that the root of is Conant-independent from the rest of the tree, : for this is just the assumption , where we allow , while for this is (2). So by extension we find (so guaranteeing (1)), to be the root of , with . Then by Proposition 5.3, find some canonical Morley sequence starting with indiscernible over , guaranteeing (2), and reindex accordingly.
Now let (so is assumed to have parameters in ) witness the Conant-dependence of on over and let be the (strict) bound supplied by Theorem 4.3. We show gives the first levels of an instance of - for , giving a contradiction to by compactness and lemma 2.8. Consistency of the paths comes from (1). As for the inconsistency of a descending comb of size , it follows from (2) (and the same reasoning as in the proof of Lemma 4.5) that a descending comb forms a coheir sequence, so the inconsistency follows by choice of .
∎
Note that by constructing a tree of size and using an Erdős-Rado version of fact 2.6 (see Lemma 5.10 of [16] for a result of this kind for similar kind of indiscernible tree, itself based on Theorem 1.13 of [15]), we could have assumed the tree we constructed in the above proof to be strongly indiscernible. It follows that we could have only used that if a canonical Morley sequence witnesses Kim-dividing of a formula, then so does any coheir Morley sequence; the statement of Theorem 4.3 is somewhat stronger. (In fact, by using a local version of the chain condition–if and , then there is some coheir Morley sequence so that , for , and –we could have avoided Theorem 4.3 altogether up to this point, but we have not yet found a suitable replacement for the below “weak independence theorem” that does not require it. We leave the details to the reader.)
We next aim to prove a version of the “weak independence theorem.” To formulate this, we need the following strengthening of Lemma 4.1:
Lemma 5.5.
Let be a type over . Then there is some global extension of so that, for all tuples if with , then for any there is with so that extends to a canonical coheir of . So in particular, is a canonical coheir of .
Proof.
Working again in a very large , find with using full existence for . Find a realization of in and let be its type over . Now suppose and with , and let . Then there is some with . Because , there is some with . Together with , it follows that . And extends to , which it remains to show is canonical. But by right monotonicity, , so the result follows by left monotonicity (see also the proof of Lemma 4.1).
∎
Definition 5.6.
We call as in Lemma 5.5 a strong canonical coheir, and a coheir Morley sequence in it a strong canonical Morley sequence.
The proof of the following is as in Proposition 6.10 of [16]:
Proposition 5.7.
(Weak Independence Theorem) Assume is . Let , , , and extends to a strong canonical coheir of . Then there exists a realization of with .
Proof.
We start with the following claim, proven exactly as in [16] but with canonical rather than invariant Morley sequences:
Claim 5.8.
There exists some with and .
Proof.
It is enough by symmetry of to find with and . If (leaving implied, throughout the proof of this claim, any parameters in in types and formulas), then by and symmetry we have , so because we know that contains no formulas Conant-forking over . It suffices to show consistency of
|
|
|
Otherwise, by compactness and equivalence of Conant-forking with Conant-dividing, we must have for some with Conant-dividing over . By symmetry, . So Proposition 5.3 yields a canonical Morley sequence starting with and indiscernible over . So
|
|
|
But because contains no formulas Conant-dividing over and is a canonical Morley sequence, is consistent, so and therefore is consistent. But this contradicts the fact that Conant-divides over .
∎
We now complete the proof of the proposition. Let (with parameters in left implied); we have to show that has a realization with . So for with , it suffices to show that has a realization with . Using , we find with ; using Lemma 5.5, we can assume extends to a canonical coheir of its restriction to . So begins a canonical Morley sequence over , and by Proposition 5.3 and an automorphism, there is some with and therefore , and with indiscernible over . By we have that realizes , and by we have that realizes .
6. and theories
We are now ready to prove that if is , it is . The proof follows Conant’s proof (Theorem 7.17 of [8]) that certain free amalgamation theories are either simple or . As anticipated in Section 5, will play the role of , while (strong) canonical Morley sequences will play the role of Morley sequences in the free amalgamation relation. This makes sense, as Lemma 7.6 of [8] shows that is just Kim-independence with respect to Morley sequences in the free amalgamation relation, while Conant-independence in a theory is Kim-independence with respect to canonical Morley sequences. Similarly to how Conant uses free amalgamation and to show that a (modular) free amalgamation theory is either simple or , we will show by strong canonical types and that if is , then
is either or
and therefore must be . (In [26], we generalize Conant’s work by studying abstract independence relations in potentially strictly or theories, finding a more general set of axioms for these relations than Conant’s free amalgamation axioms under which the - dichotomy holds and showing relationships with Conant-independence for invariant rather than coheir Morley sequences–note that in Conant’s free amalgamation theories, this is just .)
Assume is and suppose is . Obviously Kim-dividing independence, , implies ; the reverse implication would imply that is symmetric, contradicting by Fact 2.2. So there are with Kim-dividing dependent on over ; let , and let be a coheir Morley sequence over starting with such that is -inconsistent for some . The following corresponds to Claim 1 of the proof of Theorem 7.17 in [8], but requires a different argument; see also [23] and footnote 1 of [27], for another argument involving the proof of Proposition 3.14 of [16]:
Claim 6.1.
We can assume . More precisely, there are with and some coheir Morley sequence over starting with such that, for , is -inconsistent.
Proof.
In particular there is no realization of with . Let be the maximal value of without this property, and . Then is a coheir Morley sequence starting with . Let realize , and let . Then by maximality and symmetry, there is no realization of with . So there is no coheir Morley sequence starting with , every term of which realizes . But by , symmetry and Proposition 5.3, there is some -indiscernible canonical Morley sequence starting with so that . So let be and with . Since contains , and are as desired.
∎
Now replace with and with , as in claim 6.1; let be such that is -inconsistent, by compactness. We have , in analogy with Claim 2 of the proof of Theorem 7.17 of [8], because and clearly implies .
Fix a strong canonical coheir extension of . We wish to construct, by induction, a configuration with the following properties:
(1) For the sequence beginning with for and then continuing with for , is a strong canonical Morley sequence in .
(2) For ,
(3) for any .
Then by (1) gives consistent sequences of instances of , while (2) gives inconsistent pairs by claim 6.1, so we can get an instance of from this configuration exactly as in the argument at the end of the proof of Theorem 7.17 in [8], which we will reproduce for the convenience of the reader.
We make repeated use of symmetry for throughout. Suppose already constructed. We start by adding , and then add . If we take then (1) and (2) are preserved up to this point, and (3) is preserved by the following claim (which also holds of Kim-independence in theories):
Claim 6.2.
If and extends to an -invariant type , then .
Proof.
By Proposition 5.3, let be an -indiscernible canonical Morley sequence over starting with . Choose , so for , . Since form a coheir Morley sequence with for , by 5.2, so as .
Now by and the fact that is still a (strong) canonical Morley sequence up to this point, we can find a realization of for by Proposition 5.3 and an automorphism. Take , so ; then this together with (3) allows us to apply Proposition 5.7 to the conjugate of under an automorphism taking to , and . This and an automorphism (over , taking the Conant-independent joint realization of and to ) gives us our desired (as the image of under this automorphism.)
Now having constructed the configuration, let realize the consistent set of instances of coming from , and let , , , . As in the proof of Theorem 7.17 of [8], these satisfy the hypotheses of the following fact:
Fact 6.3.
(Corrected version of proposition 7.2, [8])
Suppose there are sequences , , and , so that
(i) for all and for all
(ii) for all , is inconsistent
Then is .
So is .
This concludes the proof of the main result of this paper.
Acknowledgements The author would like to thank Mark Kamsma and Itay Kaplan, as well as seminar participants at Hebrew University of Jerusalem, Imperial College London, and Université Claude Bernard Lyon 1 for many helpful edits and comments.