We consider the question, of longstanding interest, of realizing types in regular ultrapowers. In particular, this is a question about the interaction of ultrafilters and theories, which is both coarse and subtle. By our prior work it suffices to consider types given by instances of a single formula. In this article, we analyze a class of formulas φ whose associated characteristic sequence of hypergraphs can be seen as describing realization of first- and second-order types in ultrapowers on one hand, and (...) properties of the corresponding ultrafilters on the other. These formulas act, via the characteristic sequence, as points of contact with the ultrafilter D, in the sense that they translate structural properties of ultrafilters into model-theoretically meaningful properties and vice versa. Such formulas characterize saturation for various key theories , yet their scope in Keisler’s order does not extend beyond Tfeq. The proof applies Shelah’s classification of second-order quantifiers. (shrink)

We initiate a systematic study of the class of theories without the tree property of the second kind — NTP2. Most importantly, we show: the burden is “sub-multiplicative” in arbitrary theories ; NTP2 is equivalent to the generalized Kimʼs lemma and to the boundedness of ist-weight; the dp-rank of a type in an arbitrary theory is witnessed by mutually indiscernible sequences of realizations of the type, after adding some parameters — so the dp-rank of a 1-type in any theory is (...) always witnessed by sequences of singletons; in NTP2 theories, simple types are co-simple, characterized by the co-independence theorem, and forking between the realizations of a simple type and arbitrary elements satisfies full symmetry; a Henselian valued field of characteristic is NTP2 if and only if the residue field is NTP2 , so in particular any ultraproduct of p-adics is NTP2; adding a generic predicate to a geometric NTP2 theory preserves NTP2. (shrink)