In model theory, a branch of mathematics, an imaginary element of a structure is roughly a definable equivalence class. These were introduced by , and elimination of imaginaries was introduced by .
Definitions M is a model of some theory. x and y stand for n-tuples of variables, for some natural number n. An equivalence formula is a formula φ(x, y) that is a symmetric and transitive relation. Its domain is the set of elements a of Mn such that φ(a, a); it is an equivalence relation on its domain. An imaginary element a/φ of M is an equivalence formula φ together with an equivalence class a. M has elimination of imaginaries if for every imaginary element a/φ there is a formula θ(x, y) such that there is a unique tuple b so that the equivalence class of a consists of the tuples x such that θ(x, b). A model has uniform elimination of imaginaries if the formula θ can be chosen independently of a. A theory has elimination of imaginaries if every model of that theory does (and similarly for uniform elimination).
Examples ZFC set theory has elimination of imaginaries. Peano arithmetic has uniform elimination of imaginaries. A vector space of dimension at least 2 over a finite field with at least 3 elements does not have elimination of imaginaries.
References