In the category of sets, we have a bijective correspondence (up to isomorphism) between surjective functions on and equivalence relations on , where a surjective function is taken to the equivalence relation gotten by pulling back the diagonal of , and an equivalence relation is taken to the function which projects onto the set of -classes. If we replace Set with the category of definable sets of a first-order theory , this correspondence generally fails, because when is a definable equivalence relation, there may not be a corresponding definable . That is to say, internal congruences in are not generally effective.
We say that:
has uniform elimination of imaginaries if the above correspondence does hold, that is, if internal congruences in are effective.
has elimination of imaginaries if for every definable set , there exists a formula and a tuple with the same sort as such that uniquely satisfies
Inside a saturated model , elimination of imaginaries is equivalent to the following statement: for every definable set , there exists a tuple such that for all , setwise if and only if pointwise.
Poizat noticed that having elimination of imaginaries allows one to develop a classical Galois theory classifying definably-closed extensions of small parameter sets in terms of the closed subgroups of a profinite automorphism group in any sufficiently saturated model of .
The imaginary elements of a theory are precisely -classes, where is a -definable equivalence relation on .