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.
