A partial type over a first-order theory is a set of first-order formulas in a fixed finite tuple of variables which is jointly consistent with . A tuple realizes it when it satisfies every formula in the set. A complete type additionally decides every formula in those variables.
New to topics? Read the docs here!