NIP theories (also known as dependent theories or shatterproof theories) are a class of theories generalizing stable theories, but allowing for an ordering. Aside from stable theories, important examples are real closed fields, ACVF, -adically closed fields, and o-minimal theories.

## Definitions

Fix some complete theory , with monster model . A formula is said to have the independence property if there exist and such that for every and , Note that the variables and could be tuples, and the location of the semi-colon matters.

A formula is said to be NIP if it does not have the independence property.

It turns out that the following conditions are equivalent:

• The formula has the independence property.
• The formula has the independence property, where means .
• For every finite sets and and , there exist and such that holds if and only if , for every and . So every bipartite graph can be embedded into the graph of , in some sense.
• There is an indiscernible sequence and a such that holds if and only if is odd.

A theory is said to be NIP if no formula has the independence property, i.e., every formula is NIP. A non-trivially equivalent condition is that every formula with a singleton is NIP. That is, when checking NIP, one only needs to check formulas with a singleton. This is a useful criterion when we have some control over one-dimensional definable sets, such as in the case of strongly minimal, o-minimal, or C-minimal theories.

## Properties

Like most classification-theoretic boundaries, NIP is preserved under adding imaginary sorts (passing to ), under reducts, and under naming parameters with new constant symbols.

Stable theories are NIP. In fact they are exactly the NIP theories which are also simple, or which are also NSOP.

Forking in NIP theories does not have many of the nice properties of forking in simple theories; for example, symmetry can fail, and forking can differ from dividing. However, it is still a useful tool. Here are some of the results on forking and dividing in NIP theories:

• Forking is equivalent to Lascar invariance: a global type forks (i.e., divides) over a base set if and only if it is Lascar invariant over . This can be expressed in two equivalent ways: (1) is -invariant for every model containing ; (2) for every -indiscernible sequence and formula , whether or not does not depend on . This result was proven by Shelah or Adler or someone.
• Forking is equivalent to KP invariance: a global type forks (i.e., divides) over a base set if and only if it is -invariant. This was proven by Hrushovski and Pillay.
• Forking and dividing agree over models, even on the level of formulas. That is, a formula forks over a model if and only if it divides over . Moreover, in the o-minimal or c-minimal setting, one can replace "model" with "arbitrary set." These facts were proven by Chernikov and Kaplan (maybe building off the results of Hrushovski and Pillay, in the o-minimal and C-minimal setting).

Some facts from stable group theory generalize to the NIP setting. For example, always exists (the smallest type-definable subgroup of bounded index). This was proven by Shelah; a proof appears in a paper by Hrushovski, Peterzil, and Pillay. Maybe also exists, depending on what exactly means. But and need not agree, unlike in the stable case. For example, if is the circle group, or any compact definable group in RCF, then is the topological connected component of , while is the infinitesimal neighborhood of the origin.

Also, always exists; someone proved it, maybe.

A version of Baldwin-Saxl exists for NIP groups. It says that if is a type-definable group in an NIP theory, and is a formula, then there is an integer such that any finite intersection of relatively definable subgroups cut out by is an intersection of at most of them.

## Generically stable types

In NIP theories, there is a well-defined notion of generically stable types, which have many of the properties of types in stable theories. A global -invariant type is said to be generically stable if it satisfies one of the following equivalent conditions:

• The type equals .
• For every global invariant type , we have .
• The Morley sequence of is totally indiscernible (over the empty set)
• is definable, and finitely satisfiable in some small set.
• is definable, and finitely satisfiable in every small model containing (todo: check this condition)
• Β [Voting by Morley sequencesβ¦]
• For every , is the unique non-forking extension of .

In light of the last bullet point, it makes sense to say that a complete type over a set is generically stable: this means that is stationary, and the unique nonforking global extension of is generically stable.

Even outside of the NIP setting, there is a notion of a generically stable type, but it is much more constrained, and the above equivalences fail.

Generically stable types are equivalent to stably dominated types in ACVF, and play an important role there. But there are many theories, such as RCF and -adically closed fields, in which all generically stable types are trivial. In these settings, one must instead look at generically stable measuresβ¦

## Keisler measures

"Smooth measures" exist.

Also, all measures are Borel type-definable.

## [Counting types; dependent dreams]{#Counting_types;_dependent_dreams .mw-headline}

If is a cardinal, is something like the supremum of cardinals such that there is a linear order of cardinality which has at least -many Dedekind cuts. Under some set-theoretic assumptions, for every , though under other set-theoretic assumptions, one has for some . At any rate, ZFC does not decide the matter.

Shelah proved (something like) the following result:

• If is NIP, then the number of types over a set of size is at most , for (some/all/sufficiently large?) .
• If is not NIP, then for every there is a set of size such that there are -many types over said set.

Consequently, one can characterize NIP theories (in some models of ZFC) by a type-counting description, in the same way that one can characterize stable theories by counting types.

Wait, maybe the above result was for types, where is a NIP or non-NIP formulaβ¦

(Historical note: the original proof that NIP could be checked on formulas with a singleton, was using this criterion?)

## Types over finite sets

NIP formulas can be characterized by counting types over finite sets. If is a formula, consider the function which maps to the maximum number of -types over a set of size . The Sauer-Shelah lemma says that one of two things happens:

• for every , in which case has the independence property.
• grows polynomially, in which case is NIP.

It is conjectured that the polynomial growth can be witnessed by a uniform definability of types over finite sets. Specifically, it is conjectured that if is an NIP formula, then there is some formula such that for every finite set and every -type over , there exist such that for , the formula is in if and only if holds. So is the -definition of . Of course any type over a finite set is definable over that set, but the conjecture is that the definition can be chosen uniformly across all finite sets. This conjecture turns out to be equivalent to a conjecture in machine learning.

The conjecture is known in the case when the ambient theory is NIP, i.e., when all formulas are NIP. This was proven byβ¦ ::: ::: :::