An important dividing line in the class of unstable theories is being
${\mathrm{NSOP}}_{1}$, which is more general
than being simple. In
${\mathrm{NSOP}}_{1}$
theories forking independence may not be as well behaved as in stable
or simple theories, so it is replaced by another independence notion,
called Kimindependence. We generalise Kimindependence over models in
${\mathrm{NSOP}}_{1}$ theories to
positive logic — a proper generalisation of full firstorder logic where negation is not built
in, but can be added as desired. For example, an important application is that we can add
hyperimaginary sorts to a positive theory to get another positive theory, preserving
${\mathrm{NSOP}}_{1}$
and various other properties. We prove that, in a thick positive
${\mathrm{NSOP}}_{1}$ theory,
Kimindependence over existentially closed models has all the nice properties that it is known to
have in an
${\mathrm{NSOP}}_{1}$ theory
in full firstorder logic. We also provide a Kim–Pillay style theorem, characterising which thick
positive theories are
${\mathrm{NSOP}}_{1}$
by the existence of a certain independence relation. Furthermore, this independence
relation must then be the same as Kimindependence. Thickness is the mild assumption
that being an indiscernible sequence is typedefinable.
In full firstorder logic Kimindependence is defined in terms of Morley sequences in
global invariant types. These may not exist in thick positive theories. We solve this by
working with Morley sequences in global Lascarinvariant types, which do exist in thick
positive theories. We also simplify certain tree constructions that were used in the study of
Kimindependence in full firstorder logic. In particular, we only work with trees of finite
height.
