A global type in a fixed tuple of variables is a maximal consistent collection of formulas in first-order
logic with parameters from a sufficiently saturated
and strongly homogeneous universal, or "monster," model 
of a complete theory.
For a definable group 
,
a global type concentrating on 
belongs to the type space 
,
and 
acts on it by left translation.
The orbit of a global type is bounded if its cardinal number is smaller than the saturation cardinal of 
.
The existence of a global type with bounded orbit is closely related to definable
amenability. Petrykowski's conjecture
asserted that it implies definable amenability
without additional hypotheses.
