Bi-invariant types, reliably invariant types, and the comb tree property
Abstract.
We introduce and examine some special classes of invariant types—bi-invariant, strongly bi-invariant, extendibly invariant, and reliably invariant types—and show that they are related to certain model-theoretic tree properties.
We show that the comb tree property (recently introduced by Mutchnik) is equivalent to the failure of Kim’s lemma for bi-invariant types and is implied by the failure of Kim’s lemma for reliably invariant types over invariance bases. We show that every type over an invariance base extends to a reliably invariant type—generalizing an unpublished result of Kruckman and Ramsey—and use this to show that, under a reasonable definition of Kim-dividing, Kim-forking coincides with Kim-dividing over invariance bases in theories without the comb tree property. Assuming a measurable cardinal, we characterize the comb tree property in terms of a form of dual local character.
We also show that the antichain tree property (introduced by Ahn and Kim) seems to have a somewhat similar relationship to strong bi-invariance. In particular, we show that NATP theories satisfy Kim’s lemma for strongly bi-invariant types and (assuming a measurable cardinal) satisfy a different form of dual local character. Furthermore, we examine a mutual generalization of the local character properties satisfied by NTP2 and NSOP1 theories and show that it is satisfied by all NATP theories.
Finally, we give some related minor results—a strengthened local character characterization of NSOP1 and a characterization of coheirs in terms of invariant extensions in expansions—as well as a pathological example of Kim-dividing.
Key words and phrases:
invariant types, model-theoretic tree properties2020 Mathematics Subject Classification:
03C45Introduction
In neostability theory, it is often useful when a combinatorial tameness property is found to be characterized by some form of Kim’s lemma, which states that dividing along some indiscernible sequence in some class of indiscernible sequences entails dividing along all indiscernible sequences in some other class . Some standard examples are the following:
-
•
( simple) If divides over , then divides along any non-forking Morley sequence in .
-
•
( NTP2) If divides over , then divides along any strict Morley sequence over .
-
•
( NSOP1) If Kim-divides over , then divides along any sequence generated by an -invariant type extending and along any tree Morley sequence in .
An important additional consideration is the existence of the relevant special indiscernible sequences in the second class, possibly with extra restrictions, such as being indiscernible relative to some set of parameters. The modern proof of the symmetry of non-forking in simple theories uses the following fact: ( simple) If , then there is a Morley sequence which is -indiscernible with . Likewise, in the context of NSOP1 theories, symmetry of Kim-independence was shown by Kaplan and Ramsey using a similar but significantly harder to prove fact: ( NSOP1) If , then there is a tree Morley sequence that is -indiscernible with [7]. For NTP2 theories, on the other hand, while symmetry is not expected, similar machinery was used by Chernikov and Kaplan to show that forking and dividing coincide over extension bases. In particular, as part of this argument, they showed that in NTP2 theories, any type over an invariance base extends to a strictly invariant type [5]. Kruckman and Ramsey observed that Chernikov and Kaplan’s proof almost doesn’t rely on the assumption of NTP2 and can be adapted to show that any type over a model extends to a Kim-strictly invariant type [10].
Definition 0.1.
An -invariant type is strictly invariant if whenever , . is Kim-strictly invariant if whenever , .
Fact 0.2 (Kruckman, Ramsey [10]).
( arbitrary) Any type over a model has a Kim-strictly invariant extension.
In 2.15, we generalize 0.2 by showing that any type over an invariance base extends to a Kim-strictly invariant type.
0.2 prompted Kruckman and Ramsey to investigate the following variant of Kim’s lemma as possibly characterizing a good mutual generalization of NTP2 and NSOP1: A theory satisfies new Kim’s lemma if whenever Kim-divides over a model , then it Kim-divides with regards to any Kim-strictly invariant type extending . As described in an upcoming note by Kruckman and Ramsey, a failure of new Kim’s lemma entails the existence of a certain combinatorial configuration mutually generalizing TP2 and SOP1, which they refer to tentatively as the bizarre tree property or BTP, but whether the converse holds is unclear at the moment [10].
The only other previously known general construction of (Kim-)strictly invariant types seems to have been the following fact:
Definition 0.3.
A global type is an -coheir or a coheir over if it is finitely satisfiable in . is an -heir or an heir over if for every -formula , if there is a in the monster such that , then there is a such that .
Fact 0.4.
If is -invariant and is -saturated, then is an -heir for every .
In particular, if is an -heir and , then extends to an -coheir, implying that any type that is both invariant and an heir is strictly invariant. But the property in 0.4 is ostensibly stronger than mere strict invariance.
Definition 0.5.
A global type is an -heir-coheir if is an -heir and an -coheir. is -bi-invariant if it is -invariant and whenever , then extends to a global -invariant type. is strongly -bi-invariant if is -bi-invariant for every .
Note that in an NIP theory, any strictly invariant type is bi-invariant.
One of the contributions of this paper will be to present a couple of novel methods for constructing heir-coheirs, and therefore bi-invariant types. Unlike 0.4, the heir-coheirs we construct will not be strongly bi-invariant. In fact, there seems to be a significant difference between the tasks of constructing bi-invariant and strongly bi-invariant types. In particular, bi-invariance is something that can be accomplished generically on the level of formulas. This can be seen in the following proposition (which we will not use elsewhere in this paper but is motivating and may be of independent interest).
Proposition 0.6.
Let be a countable theory. Let be a countable model with the following weak saturation property:
-
For any -formula , if there is an element in the monster such that is infinite, then there is a such that is infinite.
Let be the set of non-realized -types over . There is a dense set such that for any , any -coheir extending is an -heir.
Proof.
For any -formulas and , if there is a in the monster such that is infinite, find a such that is infinite and let be the set of types in containing . (Note that this set is non-empty since is infinite.) If there is no such , let be the set of types in containing . Let . is a dense open subset of for each . Let . is a dense set.
Now fix . We need to argue that any -coheir is an -heir. Suppose that . Since is an -coheir that is not realized in , must be infinite for every -formula . Since , we have that for some , . Since we can do this for any -formula , we have that is an -heir. ∎
Note that the saturation property in 0.6 is satisfied by any computably saturated model and by any model of a theory that eliminates . It’s also relatively easy to see that 0.6 can fail in models at least as large as the covering number of the ideal of meager sets. Specifically, no coheir of a type over is also an heir.
In [11], Mutchnik introduced a certain combinatorial configuration he called -DCTP2 as part of his proof that NSOP1 and NSOP2 (or equivalently NTP1) are the same. For the sake of simplicity, we will just refer to this condition as the comb tree property or CTP (1.1). CTP will be a major focus of this paper.
In [2], Ahn and Kim introduced the antichain tree property or ATP, which, like BTP, is intended to be a good mutual generalization of TP2 and SOP1. In [3], they show that ATP is always witnessed by a formula with a single free variable and is always witnessed by the -inconsistent version of the condition. Furthermore, in [9], Kim and Lee show that in NATP theories, Kim-forking and Kim-dividing coincide over models and that if new Kim’s lemma holds (in the sense of Kruckman and Ramsey), then coheirs are universal witnesses of Kim-dividing if and only if they are Kim-strict.
It is not hard to show111The fact that ATP implies CTP is immediate from the definition, as discussed in [3], and the fact that CTP implies BTP is a corollary of unpublished results of Kruckman and Ramsey or separately of some of our results here. Specifically, since bi-invariant types are strictly invariant, 1.8 implies that any CTP theory fails the new Kim’s lemma given in [10], whose failure implies BTP. that these three conditions are related. In particular (and in an alphabetically frustrating way), ATP implies CTP, which implies BTP.
The main contribution of this paper will be a characterization of NCTP in terms of a variant of new Kim’s lemma (where Kim-strict invariance is replaced with bi-invariance). We will also give an argument that NATP implies the analogous property with strong bi-invariance, although the converse is unclear.
In Section 2, we will argue that a certain definition of Kim-dividing is natural over invariance bases and extend a result of Mutchnik’s [11, Thm. 4.9] and a result of Kim and Lee’s [9, Rem. 5.10] by showing that under this definition in NCTP theories, Kim-forking coincides with Kim-dividing over invariance bases. We do this by introducing the notions of reliably invariant types and reliable coheirs and show that these always exist over invariance bases and models, respectively, and that these always witness Kim-dividing in CTP theories. This partially remedies a deficiency of our characterization which is that not all types over models extend to heir-coheirs or even strictly invariant types (see [5, Sec. 5.1]). A remaining issue with this is that it is unclear whether NCTP is actually characterized by Kim’s lemma for reliable coheirs.
In Section 3, we give a dual local character characterization of NCTP assuming the existence of a measurable cardinal. We show that NATP theories satisfy a similar form of dual local character, but again the converse is unclear. In Section 3.2, we also discuss a notion of local character mutually generalizing the local character properties that characterize NTP2 and NSOP1 theories and show that it is implied by NATP.
Finally, we would like to thank Alex Kruckman and Nicholas Ramsey for many valuable discussions regarding the ideas in this paper.
1. The comb tree property
Given , we write for the set of such that .
Definition 1.1.
Given an ordinal , a set is a right-comb222In the existing literature, sets satisfying (the mirror image of) this condition are referred to as ‘descending combs,’ but this use of the term relies on an implicit assumption that the comb is enumerated in lexicographic order, which is not normally part of the definition of being a descending comb in a tree. if it is an antichain and satisfies that for any , if there a with , then there is at most one with .
A theory has -CTP if there is a binary tree and a formula such that for any path , is -inconsistent but for any right-comb , is consistent.
has CTP if it has -CTP for some .
Note that since any right-comb is an antichain, any theory with ATP has CTP, as observed in [9, Rem. 5.7]. Another thing to note is that the dual condition of CTP (where paths are consistent and right-combs are -inconsistent), was shown to be equivalent to NSOP1 in [11]. This means that many of our results dualize to give analogous results for NSOP1 theories. We collect these in Appendix A.
1.1. Failure of Kim’s lemma for heir-coheirs from the comb tree property
Definition 1.2.
A subset is dense above if for every , is non-empty. is somewhere dense if there is a such that is dense above . A filter on is everywhere somewhere dense if every is somewhere dense.
In this paper, we will only ever use the term ‘somewhere dense’ to refer to the above property of a subset of a tree. We will never use it in the topological sense. We will also only use the term ‘filter’ to refer to proper filters (i.e., filters that do not contain ).
The following is a fairly standard idea in forcing.
Lemma 1.3.
For any somewhere dense and any , either is somewhere dense or is somewhere dense.
Proof.
Fix such that is dense over . Suppose that for every , fails to be dense above . Then for every , is non-empty, so is dense above . ∎
Lemma 1.4.
Every everywhere somewhere dense filter extends to some everywhere somewhere dense ultrafilter.
Proof.
By transfinite induction it is sufficient to show that if is an everywhere somewhere dense filter and , then either or generates an everywhere somewhere dense filter. So fix some such . By 1.3 we have that for each , either is somewhere dense or is somewhere dense. One of the sets and must be cofinal in . Assume without loss of generality that is cofinal in . This implies that actually is somewhere dense for all . Therefore generates an everywhere somewhere dense filter. ∎
We will see later in 3.1 that the following 1.5 holds even for uncountable languages. That said, the proof in uncountable languages is a bit more technical, so we feel it is appropriate to present the friendlier proof for countable theories first.
Proposition 1.5.
Let be a countable theory. If has CTP, then there is a countable model , a formula , an -heir-coheir , and an -coheir such that and -Kim-divides but does not -Kim-divide.
Proof.
Let and witness that has CTP.
Let be an enumeration of with the property that for each pair , the set is infinite.
Fix a countable model . Let and let . Note that is dense over and . (This will be our induction hypothesis.)
At stage , suppose we have a countable model and and such that is dense over and . Let be an enumeration of all -formulas. To get , , and , perform the following construction:
-
•
If has already been defined and there is a in the monster such that is somewhere dense: Fix some such . Let be a countable model. Find such that is dense over . Find such that , and let .
-
•
If the condition in the previous bullet point fails: Let . Find such that . Let .
Note that in both cases we have ensured that .
After the construction is completed, let . Let be the filter generated by where . Note that since each is dense above , this filter is everywhere somewhere dense. Let be an everywhere somewhere dense ultrafilter extending . Let be the global -coheir corresponding to (i.e., ). Let be any non-realized global -coheir finitely satisfiable in . Note that is uniformly inconsistent (since the ’s form a path in ). Therefore must -Kim-divide.
Claim. .
Proof of claim. Fix an -formula . is actually an -formula for some . By the choice of our enumeration, this means that there was a stage at which was defined and equal to (where is a dummy variable). Since and since is everywhere somewhere dense, we must have chosen the first bullet point at this stage. Hence holds for all , whereby holds for all . Therefore as well. Since we can do this for every -formula , we have that .
Claim. is an heir over .
Proof of claim. Fix an -formula . Once again, there must have been a stage at which was defined and equal to . Suppose that there is a in the monster such that . Since is everywhere somewhere dense, this implies that we chose the first bullet point at stage , so we found some , added this to , and moved to a set satisfying for all . Therefore . Since we can do this for any -formula , we have that is an heir over .
Claim. does not -Kim-divide.
Proof of claim. Recall that is in . Also note that by construction, for each . Let for each . Note that if is an increasing sequence of integers and if for each , then is a right-comb.
Let be a Morley sequence generated by . We have by assumption that for any finite right-comb , is consistent. Suppose that for some (possibly ), we’ve shown that for every finite right-comb , is consistent. For any such , there is an such that for any , is a right-comb. (In particular, this will be true for any sufficiently large .) This implies that is consistent. Hence, by induction, we have that is consistent and so does not -Kim-divide.
Therefore and satisfy the required conditions. ∎
One thing to note is that instead of building the model in the proof of 1.5 at the same time as the filter, we could instead have built a fixed model satisfying the following weak saturation property that is analogous to the one found in 0.6:
-
For every -formula and , if there is a in the monster such that is dense above , then there is a such that is dense above .
This ends up being a bit more work to state than the given proof of 1.5, but this perspective highlights the similarity between 1.5 and 0.6.
Something that is frustrating and interesting is that, at least to the present author, there doesn’t seem to be a clear way to prove the ATP analog of 1.5. That is to say, it is unclear if one can use an instance of ATP to build a failure of Kim’s lemma for strongly bi-invariant types.
Question 1.6.
If has ATP, does it follow that there is a model , a formula , a strongly -bi-invariant type , and an -invariant type such that and -Kim-divides but does not -Kim-divide?
1.2. Characterization of the comb tree property
Proposition 1.7.
Suppose there is a formula and two -invariant types and such that and -Kim-divides but does not -Kim-divide.
-
(1)
If is bi-invariant, then has CTP.
-
(2)
If is strongly bi-invariant, then has ATP.
Proof.
For 1, suppose that is -inconsistent for any Morley sequence generated by .
We will argue by induction that for any , there is a family of parameters realizing such that for each ,
-
•
for each , and
-
•
.
Note that the second condition clearly implies that any path through such a tree is a (reverse) Morley sequence generated by (so in particular, is -inconsistent for any ). The first condition, moreover, implies that any right-comb in the tree is a Morley sequence generated by (in some enumeration). Therefore for any right-comb , is consistent. So if we can show that these trees exist for all , we will have established that has -CTP.
For , the condition is trivial, since there is only a single in the tree.
Suppose we have built such a tree for some . Start the next tree by setting for each . Find . Since is -bi-invariant, we can find an -invariant type extending . Now find such that . By -invariance of , we have that for each , . Finally, let .
Since we can do this for any , by induction, we have that has -CTP.
For 2, then we can build similar trees satisfying the additional property that
-
•
for each antichain of elements of , is a Morley sequence in over .
To see that this is possible, we just need to modify the induction step. Suppose we have built such a tree for some . Start the next tree by setting for each . Find . Since is -bi-invariant, we can find an -invariant type extending . Then we can find such that . Now, let be an antichain of elements of . If , then the statement is trivial. Otherwise, we have that and are each antichains. By the induction hypothesis, this means that is a Morley sequence in and is a Morley sequence in . By construction, this means that realizes the same type over as some initial segment of . Therefore . Since is a Morley sequence in over , this implies that is a Morley sequence in over .
Finally, since we can do this for any , we have that has -ATP. ∎
Theorem 1.8.
A theory has CTP if and only if there is a model , a formula , an -heir-coheir , and an -coheir such that and -Kim-divides but does not -Kim-divide.
Proof.
One issue which we have been ignoring up until now is whether -CTP implies -CTP for . This is an important structural property of SOP1 and ATP. The proofs going into the proof of 1.8 clearly preserve the relevant degree of inconsistency. We have been unable to resolve this question, and likewise we have been unable to show that CTP is always witnessed by a formula in a single free variable. Despite the similarity between CTP and ATP, the proofs of these facts for ATP in [3] seem to rely pretty heavily on nice structural properties of antichains that right-combs do no share (e.g., the fact that an ‘antichain of antichains’ is an antichain, which is used in [3, Lem. 3.20]).
Question 1.9.
If has CTP, does it follow that has -CTP?
Question 1.10.
If has CTP, does it have CTP witnessed by a formula with a single free variable?
One thing to note is that the proofs of these kinds of facts often make good use of indiscernible trees. As observed in [9, Rem. 5.6], CTP is always witnessed by a strongly indiscernible tree. While this will almost certainly be an important tool for studying NCTP theories at some point, we nevertheless find it interesting that tree indiscernibility plays no role in any of the proofs in this paper.
2. Reliably invariant types
2.1. What should Kim-dividing over invariance bases be?
In [7], Kaplan and Ramsey originally defined Kim-dividing in terms of dividing along sequences generated by arbitrary invariant types. Pretty quickly in their analysis, however, it becomes clear that the natural concept is dividing along sequences generated by coheirs. Ramsey has in conversation consistently expressed the opinion that the definition of Kim-dividing in terms of coheirs is more natural. Coheirs satisfy two important properties that arbitrary invariant types do not:
-
•
(Expansion) If is an -coheir and is an expansion of , then there is an -coheir extending .
-
•
(Left extension) If is an -coheir and is a type over extending , then there is an -coheir extending .
In the context of NSOP1 theories (over models), the distinction between these two definitions becomes immaterial given the relevant Kim’s lemma. Dividing along some invariant Morley sequence implies dividing along all invariant Morley sequences. In SOP1 theories, however, a reasonable question, frequently asked by Kruckman, is whether the original definition of Kim-dividing is formula independent, i.e., if and are logically equivalent and Kim-divides over a model , then Kim-divides over . It follows from [9, Thm. 3.10] that in an NATP theory, this is always the case. In Appendix C, we give an example showing that this can fail for ATP theories.
When attempting to define a robust notion of Kim-dividing over invariance bases, one ideally would like to retain the two nice properties of coheirs mentioned above. The issue with expansion, however, is that it characterizes coheirs over invariance bases.
Proposition 2.1.
Fix a set of parameters .
-
(1)
If is an invariance base,333Note that we are only considering invariance with regards to ordinary type, rather than Kim-Pillay or Lascar strong type, although over a set that is an invariance base in this sense, these notions collapse by essentially the same argument as in the proof of 1. then .
-
(2)
Assume that . Fix an -invariant type . The following are equivalent.
-
(a)
For any model and any expansion of , has a completion in that is -invariant.
-
(b)
is finitely satisfiable in .
-
(a)
Proof.
For 1, suppose that is an invariance base. Fix an algebraic type . Since is an invariance base, has an -invariant global extension . Let be the realizations of . Let be a realization of . It must be the case that for some , but by invariance, this implies that .
2b 2a. If is finitely satisfiable in , then there is an ultrafilter on whose average type is . The average type of will be an invariant type extending in any expansion of the theory.
2b 2a. Our proof of this is somewhat technical, so we have opted to put it in Appendix B. ∎
In particular, if is an invariance base, then every type over has an -invariant extension satisfying 2a if and only is a model.
Fortunately, though, expansion seems to be more of a convenience than a necessity. The second property, however, seems to be fairly significant. All of this might suggest focusing on the following special class of invariant types.
Definition 2.2.
A global type is extendibly -invariant if for any extending , extends to an -invariant type.
As we already said, coheirs over models are always extendibly invariant. The example given in Appendix C shows that not all invariant types over models are extendibly invariant.
While extendibly invariant types might seem relatively special, we get them for free over invariance bases.
Proposition 2.3.
Let be a set of parameters.
-
(1)
If there is an extendibly -invariant type, then is an invariance base.
-
(2)
An -invariant type is extendibly -invariant if and only if for every formula and every -formula , if quasi-forks444Recall that a formula quasi-forks over if there is no -invariant type containing . This is equivalent to implying a disjunction of formulas that quasi-divide over . over , then .
-
(3)
If is extendibly -invariant and is the restriction of to , then is extendibly -invariant.
-
(4)
If is the type of an -saturated model, then any -invariant extension of is extendibly -invariant.
-
(5)
If is an invariance base, then every type over extends to an extendibly -invariant type.
-
(6)
If is an extendibly -invariant type, then for any extending , extends to an extendibly -invariant type.
Proof.
1 is immediate. For 2, let be an -invariant type. Suppose that there is some formula and some -formula such that quasi-forks over and . Let be a complete type extending . We now have that has no -invariant global extension, so is not extendibly -invariant.
Now assume that satisfies the condition in 2. Fix extending . We have that for every and every , does not quasi-fork over . By compactness, this implies that there is an -invariant type containing each of these formulas, which implies that .
For 3, let be a type over extending . is consistent. Let be a completion of . We now have that there is an -invariant type extending . The restriction of to is now the required type.
For 4, let be an -invariant extension of . Note that 2 implies that it is sufficient to check that every restriction of to finitely many variables is extendibly -invariant. Let be a restriction to finitely many variables. Let be some type over extending . Let be a realization of and let be the finite tuple of elements corresponding to the variable . By saturation, there is some such that . Therefore, the restriction of to the variables corresponding to witnesses that has an -invariant extension. Since we can do this for any finite tuple of variables, we have that is extendibly -invariant by 2.
Given 2.3, we propose that defining Kim-dividing over invariance bases in terms of extendibly invariant types is likely to be a more robust notion than Kim-dividing defined in terms of arbitrary invariant types. Our strongest evidence that this is a good definition (at least in the context of NCTP theories) is the results of the next section, specifically 2.6. As we discuss at the end of Section 2.2, however, it unclear that this evidence is completely solid. Nevertheless, we find 2.16 fairly compelling.
2.2. Kim’s lemma for reliably invariant types
Definition 2.4.
A sequence is an invariant sequence over if for each and for each .
Definition 2.5.
Given a class of -invariant types , an -invariant type is reliably in if it is in the largest class satisfying that
-
(1)
for any , the restriction is in ,
-
(2)
for any and extending , there is an extending , and
-
(3)
for any and extending , if is the type of an invariant sequence over , then there is an extending .
If is the class of all -invariant types and is reliably in , then we say that is reliably -invariant. If is the class of -coheirs and is reliably in , we say that is a reliable -coheir.
The class exists by the Knaster-Tarski theorem (although it could be empty). Note that reliability clearly implies Kim-strictness. Given 2.15 and the fact that there are types over models with no strictly invariant extensions, we know that it does not always imply strictness.
Proposition 2.6.
If there is a formula , a reliably -invariant type , and an extendibly -invariant type such that and -Kim-divides but does not -Kim-divide, then has CTP.
Proof.
Suppose that is -inconsistent on Morley sequences generated by . For each , we will build a certain configuration from which we can extract a -CTP tree of height . By compactness, we’ll have that has -CTP.
We will build the arrays inductively. For , let be any realization of . Then let and . Note that is an invariant sequence over . Let .
Now suppose we are given the array and a type satisfying the following induction hypotheses:
-
•
The -element sequence is invariant over .
-
•
is reliably -invariant.
-
•
.
-
•
(where is the sequence of length consisting entirely of ’s).
Let for each . Since is reliably -invariant and since , we can find a reliably -invariant type extending . Let . Then find such that and (which we can always do, since is extendibly -invariant). Finally, let be .
By induction we can perform this procedure for as many steps as we like. Fix some and consider the cube . Let be the map from into taking to the unique satisfying that if and only if , if and only if , and if and only if is not defined. Note that for any , only has ’s at its end and either has a final segment of ’s or has no ’s at all.
We would like to argue that is a -CTP tree of height (i.e., satisfies the definition of -CTP except for the requirement that the tree have infinite height).
Claim. For any , .
Proof of claim. Let be the longest initial segment of not containing any ’s. Let be the number of ’s in . It follows by one of the induction hypotheses in the construction of the cube that . The family contains for any with , so the claim follows.
So, in particular, we have that for any path , is -inconsistent.
Claim. For any and , .
Proof of claim. Let be the longest initial segment of not containing any ’s. We then have that has as an initial segment for any (since switches and ). Let be the number of ’s in . By the construction of the cube, we have that for any with initial segment , . The family includes for any , so the claim follows.
This last claim implies that if is a right-comb, then it is a Morley sequence generated by when enumerated in decreasing lexicographic order. In particular, is consistent for any right-comb .
Therefore, by compactness, has -CTP.555We could also just build the -CTP tree directly with part of a cube of the form (taken as a direct limit of the cubes ), but this is a bit more annoying to actually write out. ∎
One notable thing about the above proof is that, despite the advocacy for the concept of extendibly invariant types given in Section 2.1, extendibility is playing a relatively minor role in the proof. We never use the first or second property in 2.5 for the type and extendibility for seems to barely matter in that we throw away all of the ‘siblings’ of the realization of that we build at each step. This raises the question of whether the restriction to extendibly invariant types is necessary.
Question 2.7.
Say that an -invariant type is semi-reliably -invariant if it satisfies 2.5 with the first and second conditions removed (and with the class of all -invariant types). Is it true that if there is a set of parameters , a formula , a semi-reliably -invariant type , and an -invariant type such that and -Kim-divides but does not -Kim-divide, then has CTP?
Another interesting and frustrating thing is that, while reliably -invariant types always exist over extension bases (as we will show in the next section), the construction of reliably invariant types in 2.15 and the construction of bi-invariant types in 1.5 seem to be rather incompatible. 2.15 relies heavily on knowing the precise type over the set , whereas 1.5 is a forcing construction that explicitly needs to avoid committing to a specific complete type before the end. It’s not even clear that the bi-invariant types constructed in 1.5 are extendibly bi-invariant (i.e., have the property that for any type over extending , there is an -bi-invariant type extending ).
Question 2.8.
Does the converse of 2.6 hold? Moreover, if has CTP, does there exist a reliable heir-coheir witnessing this? A reliably bi-invariant type? Extendibly bi-invariant?
It’s far from clear that the definition we’ve given in 2.5 is in some sense the ‘correct’ one. Its motivation is primarily that it is the strongest property that we can guarantee over invariance bases. In particular, while coheirs are always extendibly invariant, it is not clear whether heir-coheirs are always reliably invariant. If this were true we would be able to combine 1.8 and 2.6 and give a statement of Kim’s lemma that both characterizes NCTP and is non-trivial over arbitrary extension bases (and therefore over arbitrary models).
Question 2.9.
Are all heir-coheirs extendible heir-coheirs? In other words, if is an -heir-coheir and is a type over extending , is there an heir-coheir extending ?
Question 2.10.
Are all heir-coheirs reliable coheirs? Reliably invariant?
2.3. Existence of reliably invariant types
Our approach to building reliably invariant types is to build invariant types that are ‘as bi-invariant as possible.’ In order to manage our bookkeeping, we will use a fixed tuples of variables indexed by the monster model.
Definition 2.11.
Let be a fixed monster model of . Let be a fixed enumeration of distinct variables indexed by . Given a formula (with parameters in the monster) and , we write to represent the formula with its variables permuted by in the obvious way (but not its parameters). We write to represent the formula with its parameters permuted by (but not its variables). We will use the same notation for partial types to indicate the image under the corresponding map.
The minimal monster type (over ), , is with the obvious variable assignment. A monster type (over ) is any consistent type extending .
A partial type is -invariant if for any , . is -co-invariant if for any , .
Note in particular that the minimal monster type over is -invariant (trivially) and -co-invariant. Also note that (the deductive closure of) the union of any two -invariant types is -invariant and of any two -co-invariant types is -co-invariant.
When is a tuple of elements of the monster, we may write to represent the corresponding tuple of variables in .
Lemma 2.12.
Fix a set . Let be a maximal666Whenever we talk about maximal partial types among some class, we mean maximal consistent partial types among that class. -co-invariant partial type. For any tuple and any formula , if is consistent with , then there are such that .
Proof.
Suppose that no such exist. Then we’d have that is consistent and -co-invariant, but then by maximality, we’d have that , contradicting the fact that is consistent with . ∎
Lemma 2.13.
Let be a maximal -co-invariant partial type, and let be an invariant sequence over .
-
(1)
If a formula is consistent with , then is consistent with .
-
(2)
If a global type is consistent with , then is consistent with .
Proof.
For 1, since is consistent with , we have by 2.12 that there are such that and for each .
For each positive , let be an -invariant type such that .
By induction, we can build a forest such that
-
•
for each , and
-
•
for each , (where is the length of ).
Let be a completion of . Since for each , we can find a path such that . This implies that is consistent with , so by -co-invariance, is consistent with as well.
2 follows by compactness. ∎
The following proposition says that we can rely on the existence of reliable types.
Theorem 2.14.
Fix a set of parameters and let be a class of -invariant types. Suppose furthermore that
-
(1)
every type over extends to a member of ,
-
(2)
for each tuple of variables , is closed,
-
(3)
is invariant under renaming variables, and
-
(4)
any -invariant type is in if and only if every restriction of it to finitely many variables is in .
Then for every , there is an -invariant that is reliably in .
Proof.
Let be the set of extensions of that are in . Note that since is the intersection of two closed sets, it is closed. Let be the global partial type corresponding to the closed set .
Claim. is -co-invariant.
Proof of claim. Fix . By 3 and 4, is fixed by the action of on the variables . Since the set of global completions of is as well, this implies that and therefore is fixed under the action of . Since we can do this for any , is -co-invariant.
Let be a maximal -co-invariant extension of (which always exists by Zorn’s lemma). Note that is also -invariant.777Normally we couldn’t require a maximal -co-invariant partial type to be -invariant, but since every complete type in is -invariant, any partial type extending is -invariant. Also note that since is a monster type, we have that if is a realization of , then .
Now let be the class of -invariant types satisfying the following property:
-
For any finite sub-tuple of , let be the restriction of to the variables . If , then is consistent.
Note that since is -co-invariant, the above property doesn’t depend on the choice of . We would like to show that the class satisfies the closure properties in 2.5 relative to and therefore every type in is reliably in .
The first closure property is immediate. Note that for small tuples of variables, the second closure property is also immediate. If is an -invariant type in and is a type in extending , then given , we have that and so is automatically consistent. For types with large tuples of variables, the result follows from the fact that for a fixed type over , the set of global extensions of satisfying is closed and so the required result follows by compactness.
Now we need to show that satisfies the third closure property. Again, we first show this for small tuples of variables.
Claim. For any (with a small tuple of variables) and invariant sequence over , if and is a global extension of such that is consistent, then is consistent, where .
Proof of claim. Since is an invariant sequence over , we have by 2.13 that is consistent. Since is a monster type, we have that , so the required partial type is consistent.
Therefore if is any global completion of that is consistent with and is an invariant sequence over , we have that for any , if , then we can find a global completion consistent with and such that .
Again the third closure condition for types with large tuples of variables follows from compactness and the fact that if is an -invariant sequence, then is an -invariant sequence as well.
Therefore satisfies the closure conditions in 2.5 relative to and so , since is the largest class of types satisfying this condition. Finally, if is a type in a small number of variables, we can find a global -invariant type , which is therefore in the class and is therefore reliably in . For types with large tuples of variables, the extension again exists by compactness. ∎
Corollary 2.15.
Fix a set of parameters .
-
(1)
If is an invariance base, then every type extends to a reliably -invariant type.
-
(2)
If is a model, then every type extends to a reliable -coheir.
Proof.
Corollary 2.16.
If is NCTP, then a formula Kim-forks with regards to extendibly invariant types over an invariance base if and only if it Kim-divides with regards to extendibly invariant types over .
Proof.
Suppose that Kim-forks over . Let such that Kim-divides over for each . Let be a reliably -invariant type extending . Let be a Morley sequence generated by . Note that and for each are Morley sequences in reliably -invariant types. By 2.6, we have that is inconsistent for each . Therefore, by the standard argument, we have that is inconsistent. By indiscernibility, this implies that is inconsistent, or, in other words, that Kim-divides over with regards to a reliably -invariant type. Any reliably -invariant type is extendibly -invariant, so we are done. ∎
3. Local Character
3.1. Uncountable languages and dual local character
In the following we will give a characterization of NCTP in terms of a weak dual local character under the assumption that there is a measurable cardinal . We don’t expect this to be necessary, but given the unclear usefulness of this characterization and how straightforward the proof with a measurable cardinal is, we have decided to not pursue a stronger result for the time being. In the next proposition we will also extend 1.5 to uncountable languages.
Proposition 3.1.
Let be a theory in a (possibly uncountable) language . Assume has -CTP witness by the formula .
-
(1)
There is a model with , an -heir-coheir , and an -coheir such that and -Kim-divides but does not -Kim-divide.
-
(2)
For any regular cardinal , there is a model with , a continuous chain of elementary substructures with and for each , and a sequence such that for each , is -inconsistent, and for each , there is an -heir-coheir such that does not -Kim-divide.
Proof.
The proofs of 1 and 2 are nearly the same. If we are proving 1, let , and if we are proving 2, let be as in the statement of the proposition. When we say a model is small, we mean that if we are proving 1 and if we are proving .
Let witness that the formula has -CTP. Let be a small model. Expand with the following predicates:
-
•
A unary predicate , which defines the set .
-
•
A unary predicate , which defines the set .
-
•
A partial order on defined by if and only if .
-
•
The functions and , which we will write as and .
Let be the expanded language.
Let be an enumeration of with the property that for each pair , the set is cofinal in . (Such an enumeration can be defined using any bijection between and .)
Let and be two sequences of distinct unary predicates. For each , let . We will inductively build a sequence of elements and a chain of small structures (with an -structure) where for any , is an -elementary substructure of . Each will be downwards closed under and closed under the functions and . We will call any set closed under these a closed tree. Furthermore, for , we will have , , and . (If we are proving , the ’s will eventually be part of the filter that we use to define our two coheirs.)
Let . At stage , suppose we have our -structure with . Furthermore, suppose that is dense above in (i.e., for any with , there is a such that and ). Let be an enumeration of all -formulas. To get and , perform the following construction:
-
•
If has already been defined and there is an -elementary extension , a closed tree with , and a (in the -monster) such that is dense above in for each and is somewhere dense above in : By Löwenheim-Skolem, we can assume that is small. Let be a small elementary extension. Find with such that holds. By compactness, we may assume that for any , . Let , and let
Note that is dense above in .
-
•
If the condition in the previous bullet point fails: Find a small -elementary extension with a such that and such that for any , . (This is always possible because is a closed tree.) Let , and let .
Note that in both cases we have ensured that and that is not -upper-bounded by any element of . Also note that for every , we have that is dense above in .
Just before limit stage , suppose that we have and for all . Let , which we can regard as an -structure (where ). By compactness, we can find a small model , a closed tree , a set , and such that for all , , , , and is dense above in . If we are proving 2 and axiomatizes a complete -type over , we may moreover assume that there is a realizing such that for all .
After the construction is completed, let . Note that by induction.
Proof of 1. Let . Note that is a closed tree.
Let be the filter generated by , where .
Claim 1. For every , is dense above in .
Proof of claim. Fix a . At each stage with , we ensured that is dense above in . Fix with . Since is the union of a chain, there is an with such that . At stage , we ensured that is dense above . Therefore there is a with . Since , we have that . By elementarity, we also have that . Since we can do this for any with , we have that is dense above in .
The previous claim implies that the filter is everywhere somewhere dense. Therefore we can extend it to an everywhere somewhere dense ultrafilter by the same argument as in 1.4.
Let be the filter generated by . Since for any , we have that is a proper filter. Let be an ultrafilter extending .
Let be the global average type of , and let be the global average type of .
Claim 2. . Moreover, this type is axiomatized by .
Proof of claim. Fix an -formula . is actually an formula for some . By the choice of our enumeration , this means that there was a stage at which was defined and equal to (where is a dummy variable). Since and since is everywhere somewhere dense, we must have chosen the first bullet point at this stage. (In particular, the required condition is satisfied with and .) Hence holds for all . By elementarity, this implies that holds for all as well, implying that holds for all . Therefore as well. Since we can do this for every -formula , we have that and that this type is axiomatized by .
Claim 3. is an heir over .
Proof of claim. Fix an -formula . Once again, there must have been a stage at which was defined and equal to . Suppose that there is a in the monster such that . Since is everywhere somewhere dense, this implies that the conditions for the first bullet point were met (with and and the parameter ). Therefore we added a parameter to such that holds for all . By elementarity, this implies that holds for all . Therefore . Since we can do this for any -formula , we have that is an heir of over .
For any , the set of finite right-combs of cardinality in is definable in the language . Therefore, by elementarity, we have that for any right-comb , is consistent. Likewise, being a -increasing sequence of size is a definable property, so for every path in , is -inconsistent.
Claim 4. does not -Kim-divide.
Proof of claim. The set is in . Likewise, for each , we have that the set is in . Note that if is an increasing sequence of ordinals and if for each , then is a right-comb.
Let be a Morley sequence generated by . By the argument in the paragraph just before Claim 4, we have that for any finite right-comb , is consistent. Suppose that for some (possibly ), we’ve shown that for every finite right-comb , is consistent. For any such , there is an such that for any with , is a right-comb. This implies that is consistent. Hence, by induction, we have that is consistent and so does not -Kim-divide.
Finally, note that since and since is -inconsistent, we have that is -inconsistent for any Morley sequence generated by . Therefore and satisfy the required conditions.
Proof of 2. Say that an -formula is covered by if was defined and equal to at stage . Since is regular, we have by a standard argument that there is a club such that for every , every , and every -formula , there is a such that is covered by .
Fix some . Let . We can now repeat the proofs of the claims in the proof of 1. In particular, we get from Claim 2 that axiomatizes a complete type. Therefore we added an element to realizing this type. From Claims 3 and 4, we get that there is an -heir-coheir extending such that does not -Kim-divide.
Let be an enumeration of in order. Let , , and for each . Since is an -increasing sequence, we have that is -inconsistent, so we are done. ∎
For the following recall that on a measurable cardinal , we can find a normal ultrafilter (i.e., for any sequence of elements of , we have that the diagonal intersection is an element of ). In particular is -complete and also has the property that every is stationary, implying that every club in is in .
Lemma 3.2.
Let be a measurable cardinal. Let be a model of with . Let be a continuous chain of elementary substructures of with for each and . Let be any sequence of elements of .
For any normal ultrafilter on , there is an such that for every , is finitely satisfiable in and .
Proof.
Let . By a standard argument, there is a club such that for any , . Note that since is a club, .
For each , let . By construction we have that for each , . Since and since is -complete, this implies that .
Since is normal, we have that . Consider . We have that for every , and is finitely satisfiable in . Since is a limit ordinal, this implies that is finitely satisfiable in . Since we can do this for any , we are done. ∎
Definition 3.3 ([8, Def. 5.3]).
A set of formulas is a dual type if there is some such that is -inconsistent.
Proposition 3.4.
Let be a measurable cardinal. Let be the unique saturated model of of cardinality . Suppose that there is a dual type over with and a club of small elementary substructures of such that for any , there is a with such that for some -invariant , does not -Kim-divide.
-
(1)
If is -bi-invariant for each , then has CTP.
-
(2)
If is strongly -bi-invariant for each , then has ATP.
Proof.
The proofs of 1 and 2 are nearly identical. We will write the proof of 1. To get the proof of 2, just insert the word ‘strongly’ in the appropriate places.
By a standard argument we may assume that there is a continuous chain of small elementary substructures of such that and . Let be a normal ultrafilter on . For each , let be a formula with such that for some -bi-invariant , does not -Kim-divide.
By -completeness, there is a and a formula such that for every , . By 3.2, there is an such that for every , is finitely satisfiable in and .
For any , we now have that for any global coheir finitely satisfiable in , if is a Morley sequence generated by , then is -inconsistent for some . On the other hand, we have that does not -Kim-divide where is an -bi-invariant type satisfying . Therefore has CTP. ∎
Corollary 3.5.
Fix a complete theory . If there is a measurable cardinal , then the following are equivalent.
-
(1)
has CTP.
-
(2)
There is a model with , a dual type over , and a club of small elementary substructures of such that for any , there is a with such that for some -bi-invariant , does not -Kim-divide.
-
(3)
The same as 2, but with each an -heir-coheir.
It seems likely that 3.5 does not require a large cardinal, but nevertheless the question needs to be asked.
Question 3.6.
Does 3.5 hold without the existence of a large cardinal?
Finally, we can essentially ask 1.6 again.
Question 3.7.
Does 3.5 hold for ATP if the types are assumed to be strongly bi-invariant?
3.2. NATP implies generic stationary local character
Simplicity, NTP2, and NSOP2 all have characterizations in terms of some kind of local character (which we will state in sub-optimal forms for the sake of exposition):
-
•
is simple if and only if it satisfies local character: There is a such that for every global type , there is an with such that does not divide over .
-
•
is NTP2 if and only if it satisfies generic local character: There is a such that for every global type and every with , there is an with such that for any , if , then does not divide over [4].
-
•
is NSOP1 if and only if it satisfies stationary local character: There is a such that for any global type , the set is stationary in the set of models of size less than [8].
Note that in all three of these, (Kim-)dividing coincides with (Kim-)forking.
Given the existence of these characterizations, when Kruckman visited the logic group at the University of Maryland in 2020, we tried to come up with a reasonable mutual generalization of generic local character and stationary local character. The idea being that this would be a nice complimentary approach to trying to mutually generalize NTP2 and NSOP1. We came to the following definition.
Definition 3.8.
For any type and any small with , we write for the following condition:
-
For any -formula and any such that and , does not Kim-divide over .
We say that satisfies generic stationary local character888Perhaps stationarily generic local character would be a more correct name, but it doesn’t quite roll off the tongue. It also doesn’t generalize well to the club version discussed in 3.14. if for every , there is a such that for every -saturated model , every type , and every with ,
is stationary in .
As it turns out, however, generic stationary local character is probably too strong to characterize NBTP in that its failure actually implies ATP.
Lemma 3.9.
Fix . For any -saturated model , any with , and any -invariant type , the set is a club in .
Proof.
The set in question is clearly closed, so we just need to show that it is unbounded. Fix with . Given , we can find a model with such that for any -formula , if there is a in the monster such that , then there is a such that . Let . We have that is an heir over . ∎
Proposition 3.10.
Suppose that does not satisfy generic stationary local character. Then there is a small model , a formula , a strongly -bi-invariant type , and an -invariant such that -Kim-divides but does not -Kim-divide.
Proof.
Let witness that fails generic stationary local character. Let . Note that there are at most -invariant types for any with .
There is a -saturated model , a type , and an with such that is not stationary in . This means that there is a club such that for every model with , there is a such that and Kim-divides over . By induction, we can build a continuous chain of elementary substructures of and a sequence of formulas in such that for each , and Kim-divides over . For each , let be an -invariant type.
For each , let . By 3.9, each is a club in . Therefore the diagonal intersection and also are clubs. For each , let be the least such that . This is a regressive function, so by Fodor’s lemma, there is a and a stationary set such that for all . Since the number of -formulas is less than , there is a stationary set such that for any and in , . Since the number of -invariant types is at most , there is a stationary set such that for any and in , . Let and let .
We now have that is a Morley sequence generated by over . Since is consistent, we have that is consistent as well. Furthermore, has the property that is an -heir for each . Therefore is strongly -bi-invariant. Finally, we have that Kim-divides over . Therefore has ATP by 1.7. ∎
Corollary 3.11.
If is NATP, then it satisfies generic stationary local character.
In our opinion the lesson of 3.10 and 3.11 is that it is unlikely that NCTP will be characterized by something like 3.8. It is difficult to imagine how to tune the forbidden configuration so that it will build bi-invariant types but not also strongly bi-invariant types.999Naturally, this would be a non-issue if it does turn out that CTP and ATP are equivalent.
Broadly speaking, Propositions 0.6 and 1.5 would seem to indicate that bi-invariance is expected generically at the level of formulas, whereas 3.10 indicates that strong bi-invariance is expected generically at the level of partial types.
Of course, 3.11 is unsatisfactory in a couple of different ways. First of all, it is not a characterization.
Question 3.12.
If satisfies generic stationary local character, does it follow that is NATP?
But also the local character characterizations of simplicity, NTP2, and NSOP1 have tighter cardinal bounds than we have stated. Our proof of 3.10 shows that if generic stationary local character fails at , then we can build an instance of ATP from any -saturated m del. For all three of the aforementioned conditions, it is known that this is witnessed by any -saturated model. The proofs of these tighter bounds rely on more detailed structural understandings of the relevant class of tame theories, and in particular that the tameness condition is characterized by the associated notion of local character.
Question 3.13.
If fails to have generic stationary local character, is this witnessed by models that are -saturated?
For NTP2 in particular, the original statement of generic local character in [4] did not require the big model to have any degree of saturation but instead required that each extends to a strictly invariant type. We could make a similar statement here, more in the vein of 3.4, and drop the requirement that the big model be saturated but require that each extends to a strongly bi-invariant type. We did not opt to highlight this version of 3.10, however, as the interesting thing about the proposition is the fact that we do not need to assume that some configuration of (strongly) bi-invariant types happens to exist, as we do in 3.4.
Finally, in the case of NSOP1, we have done the relevant results in [8] a bit of a disservice. In [8], Kaplan, Ramsey, and Shelah actually prove that in NSOP1 theories, for any global type , the set of -sized models over which does not Kim-divide is a club. This is an instance of the kind of dichotomous behavior you expect from a dividing line: Either every type is ‘good’ on a club of small models or there is a type that is ‘bad’ on a club of small models. Again, however, the proof of this relies heavily on a structural understanding of NSOP1 theories, so it is entirely unclear if something like this would generalize to the present context, which leaves an obvious question.
Question 3.14.
Say that a theory has generic club local character if for any global type and any with , the set is a club in . Is generic stationary local character equivalent to generic club local character?
Appendix A Dual results for NSOP1
In [11, Lem. 2.8], Mutchnik shows that SOP2 is equivalent to the following condition:
-
There is a , a tree , and a formula such that for any path , is consistent but for any right-comb , is -inconsistent.
Furthermore, by the main result of [11], this is equivalent to SOP1. In [9], Kim and Lee show that the above condition is equivalent to the above condition with a tree indexed by . Essentially all of the proofs given in this paper are insensitive to this duality, so we can freely conclude several new results for NSOP1 theories. (Some of our results, such as 1.7, are trivial when dualized, however.)
Proposition A.1 (Dual of 1.5 and 3.1 part 1).
If has SOP1, then there is a model , a formula , an -coheir , and an -heir-coheir such that and -Kim-divides but does not -Kim-divide.
We also no longer need the measurable cardinal in the following result, as the hard part has already been done for us in [8].
Proposition A.2 (Dual of 3.5).
Fix a complete theory . The following are equivalent.
-
(1)
has SOP1.
-
(2)
There is a model with , a type over , and a club of small elementary substructures of such that for any , there is a with such that for some -bi-invariant , -Kim-divides.
-
(3)
The same as 2, but with each an -heir-coheir.
Appendix B Characterization of coheirs in terms of invariant extensions in expansions
Here we will give the proof that 2b implies 2a in 2.1. Recall the following: means that . satisfies all of the axioms of a strict independence relation except for possibly base monotonicity (see [1, Sec. 1]101010Although note that there are some errors in this source. See [6] for a full account of the relevant results with correct proofs.). In particular, this means that satisfies full existence: For any , , and , there is a such that .
First we will need a lemma.
Lemma B.1.
Let be a set of parameters satisfying . Let , , and be fresh unary predicate symbols. Let and let . For any -formula , let be the result of replacing each instance of with and each instance of with in .
Let . For any -saturated, -homogeneous111111By -homogeneous we mean that for any tuples and realizing the same type with , there is an automorphism taking to . model , there is an -structure such that
-
•
,
-
•
forms a partition of , and
-
•
for any -formula , .
Proof.
Fix and as in the statement of the lemma. Note that since is -saturated as a model of , we have that for any tuples and with and , and realize the same -type over as well (by a back-and-forth argument).
Let be the theory consisting of the elementary diagram of , an axiom asserting that is a partition of the universe, , and for each -formula .
Clearly we just need to show that is consistent. We will prove this by building an expansion of in a forcing extension that is a model of . By absoluteness, this will imply that each finite subset of is consistent and so itself is consistent.
Let be a forcing poset whose conditions are pairs of the form , where , , , and . The ordering is given by extension, i.e., if and only if and . Let be a generic filter for this poset and consider the forcing extension . Let and . It is clear that forms a partition of . Let be the -structure . We just need to show that for each -sentence , . Fix an -formula and a tuple and suppose that . By the truth lemma, there is a forcing condition such that . By full existence, we have that for any condition , there is a (in the monster in ) such that and (i.e., ). In particular, and so . Since is -saturated in , we may assume that . Since the forcing poset is invariant under , we have that and so forces this as well. Since we can do this for any , we have that . Therefore . Since this is true for any , we have that . Since was arbitrary, satisfies the required axiom schema.
Finally, since is not satisfied in , we have that . ∎
Now we can complete the proof of 2.1.
Proof that 2b implies 2a in 2.1.
Fix a set of parameters and let be an -invariant type that is not finitely satisfiable in . Fix an -formula and a parameter such that and is not satisfiable in . Let . Let be a -saturated, -homogeneous model of . By -saturation we may assume that the parameter is in . Let be a new unary predicate. Expand with so that .
Let be the extension of guaranteed by B.1. By a standard model-theoretic argument, we may assume (by passing to a sufficiently saturated and homogeneous elementary extension if necessary) that there is an automorphism (of as an -structure) such that . (Note that does not necessary fix all of .) Now let be the equivalence relation on with equivalence classes . Consider the expansion . Note that is still an automorphism of this structure. Note also that for any . Let be an -invariant extension of . Since , we must have that concentrates on one of the -equivalence classes other than the class containing , but these classes are not fixed by , so we have a contradiction. Therefore no such extension can exist. ∎
One thing to note about this proof is that in the expansion, the set is not algebraically closed in . This raises a question.
Question B.2.
Which invariant types satisfy the following property?
-
For any model and any expansion of , has a completion in that is -invariant.
Appendix C An example of Kim-dividing only along non-extendibly invariant types
Let be a language with three sorts: (for graph), (for orders), and (for points). has a unary relation and a binary relation . We have four unary functions, which we will think of as two unary functions with codomain : and . Given and in , we’ll write for the -preimage of and we’ll write for the -preimage of . Finally, we have a ternary relation on , which we’ll write as a parameterized binary relation for .
Let be the formula that says , , and there is an -edge from some element of to some element of .
Let be the model companion of the universal theory that says
-
•
is a triangle-free graph relation,
-
•
, , , and always hold,
-
•
if , then for any , is a linear order on , and
-
•
for any , if for some and , then .
It is not hard but also not entirely pleasant to establish that this the finite models of this universal theory form a Fraïssé class with free amalgamation. Furthermore, is the theory of its Fraïssé limit and has quantifier elimination.
Fix a model of . Fix and and outside of such that , the only edge between and is , and and hold.
Lemma C.1.
The formula Kim-divides over .
Proof.
Let be the global -invariant type extending entailing for all in the monster, if and only if and , and if and only if . By quantifier elimination, this entails a complete -invariant.
If we find , then we’ll have , implying that is inconsistent. ∎
Lemma C.2.
If Kim-divides with respect to an -invariant type , then .
Proof.
For any -invariant type , . Furthermore, we necessarily have that , so the only thing to check is that if , then there is an -edge between some element of and some element of .
Suppose that this doesn’t happen. Then if is a Morley sequence generated by , we’ll have that there are no -edges between any pair of elements of , implying that is consistent, contradicting the fact that this formula Kim-divides along Morley sequences generated by . Therefore . ∎
Let be the monster model of .
Lemma C.3.
is an -indiscernible set.
Proof.
First note that does not hold for any . Therefore for any , is trivial on . By quantifier elimination, this implies that any two -tuples of distinct elements of have the same type over , so is an -indiscernible set. ∎
Let be an element of .
Lemma C.4.
If is an -invariant type, then .
Proof.
Assume for the sake of contradiction that . Define a relation on by if and only if . Note that is clearly -invariant. Since , the restriction of to needs to be a linear order, but there are no -invariant linear orders on , since it is an -indiscernible set. ∎
Proposition C.5.
If Kim-divides along an -invariant type , then has no -invariant completions.
References
- [1] Hans Adler. A geometric introduction to forking and thorn-forking. Journal of Mathematical Logic, 09(01):1–20, June 2009.
- [2] JinHoo Ahn and Joonhee Kim. SOP1, SOP2, and antichain tree property, 2020.
- [3] JinHoo Ahn, Joonhee Kim, and Junguk Lee. On the antichain tree property. Journal of Mathematical Logic, 23(02), December 2022.
- [4] Artem Chernikov. Theories without the tree property of the second kind. Annals of Pure and Applied Logic, 165(2):695–723, February 2014.
- [5] Artem Chernikov and Itay Kaplan. Forking and dividing in NTP2 theories. The Journal of Symbolic Logic, 77(1):1–20, 2012.
- [6] Gabriel Conant and James Hanson. Separation for isometric group actions and hyperimaginary independence. Fundamenta Mathematicae, 259(1):97–109, 2022.
- [7] Itay Kaplan and Nicholas Ramsey. On Kim-independence. Journal of the European Mathematical Society, 22(5):1423–1474, January 2020.
- [8] Itay Kaplan, Nicholas Ramsey, and Saharon Shelah. Local character of Kim-independence. Proceedings of the American Mathematical Society, 147(4):1719–1732, January 2019.
- [9] Joonhee Kim and Hyoyoon Lee. Some remarks on Kim-dividing in NATP theories, 2022.
- [10] Alex Kruckman and Nicholas Ramsey. Kim’s Lemmas and tree properties. ASL Special Session on Model-theoretic Classification Program, II, 2022.
- [11] Scott Mutchnik. On NSOP2 theories, 2022.