Why is elimination of imaginaries important?

There are many reasons why you might care about elimination of imaginaries. Here are a few:

  1. If $T$ eliminates imaginaries, and $M\models T$, then any structure interpretable in $M$ is actually definable in $M$. For example, suppose $G$ is a definable group in $M$. This means that there is a definable set $X\subseteq M^n$ for some $n$ and a definable function $\cdot\colon X^2\to X$ such that $(X,\cdot)$ is group. Now suppose $H\subseteq G$ is a definable normal subgroup. To form the quotient group $G/H$, we consider definable equivalence relation, namely $a\sim b$ if and only if $ab^{-1}\in H$. If $T$ eliminates imaginaries, then $G/H$ (which is a priori only interpretable) is actually isomorphic to a definable group in $M$, and the quotient function $G\to G/H$ is definable. So the category of definable groups in $M$ is closed under quotients.

  2. If $T$ eliminates imaginaries, then we have elements which "code" definable sets. Here's how this works: Suppose $\varphi(x,y)$ is a formula. For any $b\in M$, we write $\varphi(M,b) = \{a\in M\mid M\models \varphi(a,b)\}$ for the set defined by $\varphi(x,b)$. Now, it could be that different parameters $b$ give the same definable set. So we consider the following definable equivalence relation: $$b\sim b'\iff \varphi(M,b) = \varphi(M,b')$$ If $T$ eliminates imaginaries, then the equivalence class $[b]_\sim$ can be identified with a real tuple $c$. And you can prove that the definable set $\varphi(M,b)$ is fixed setwise by an automorphism $\sigma$ if and only if the tuple $c$ is fixed pointwise by $\sigma$. This neat trick is often technically useful.

  3. In stable theories, we have a notion called forking independence, which identifies, for any type $p(x)\in S_x(A)$ and any larger set $A\subseteq B$, a class of "independent" (non-forking) extensions $p(x)\subseteq q(x)\in S_x(B)$. If $T$ eliminates imaginaries, then forking has a very useful property called stationarity: whenever $A = \text{acl}(A)$, any type $p(x)\in S_x(A)$ has a unique non-forking extension in $S_x(B)$.

To any theory $T$, we can associate a theory $T^{\text{eq}}$ in a larger language $L^{\text{eq}}$, such that $T^{\text{eq}}$ eliminates imaginaries and otherwise shares essentially all of the model-theoretic properties of $T$. So for technical purposes, when we're proving things about general theories, it is safe to assume that any theory under consideration eliminates imaginaries.

This is analogous to the situation for quantifier elimination: We can replace any theory $T$ by its Morleyization, which eliminates quantifiers and otherwise shares essentially all of the model-theoretic properties of $T$.

But in both situations, moving to $T^{\text{eq}}$ or moving to the Morleyization entails expanding the language. And if you want to do detailed work with a particular theory, it helps to work with a small, mathematically natural language, where you have some hope of understanding all of the quantifier-free definable sets. This is why people work hard to prove quantifier elimination and elimination of imaginaries in theories of interest, without dramatically expanding the language all the way to $T^{\text{eq}}$ or the Morleyization.


I'm a beginner and this is unfair if I try to add something to Alex Kruckman's perfect answer. But I've seen an interesting tip as an idea for the importance of this concept in general. Roughly speaking, suppose we are in the category of sets, one can hold a bijective correspondence between surjective functions on given set, say $X$, and equivalence relations on $X$. Now if we go into the category of definable sets of a first-order theory, let say $Def(T)$, this correspondence generally fails, because when $E$ is a definable equivalence relation, maybe there doesn't exist corresponding definable surjective function $f_{E}$.