I picked the page describing uniform elimination of imaginaries at random, read a little about it, and it seems like an interesting concept. I haven't read much of the surrounding text because I want to use it later as a source of additional, basic exercises.
I'm trying to understand whether an $L$-structure has uniform elimination of imaginaries or not.
Wilfrid Hodges' A shorter model theory contains the following definition as an alternative definition of uniform elimination of imaginaries. However, it has fewer (meta-level) quantifiers than the primary definition, so I want to take it as the primary definition for personal use.
Let $A$ be an $L$-structure.
The following is a quote from page 117, with a small difference in notation $\vec{a}$ vs $\bar{a}$.
Another way of saying
this[that $A$ has uniform elimination of imaginaries] is that for every equivalence formula $\theta(\vec{x}, \vec{y})$ of $A$ there is a function $F$ which is definable without parameters, taking tuples as values, such that for all $\vec{a_1}$ $\vec{a_2}$, $\vec{a_1}$ is $\theta$-equivalent to $\vec{a_2}$ if and only if $F(\vec{a_1}) = F(\vec{a_2})$
My high-level question is: what does the above definition mean?. Here are the specific things about it that are confusing.
- Do we have one property called "uniform of elimination of imaginaries" or one property for each $n$ with $n$ being the length of the tuples $\vec{x}, \vec{y}, \cdots$?
- Is the formula $\theta$ allowed to contain parameters?
- What exactly is an equivalence formula $\theta$? I suspect that an equivalence formula $\theta$ is a formula defining an $A$-relation of arity $2*n$ that is an equivalence relation when construed as a binary relation on $A^n$. I am not certain though. $\theta$ could also be constrained to be some kind of congruence or constrained to respect the structure of $A$ in some way.
- Why are we insisting that $F$ be $0$-definable?
- $F$, intuitively, seems a lot like an ordered pair function $a, b \mapsto (a, b)$. This, intuitively, seems like it would knock out finite structures of cardinality other than $0$ or $1$. Is that intentional? (and is my reasoning right?)
- Does "$\vec{a_1}$ is $\theta$-equivalent to $\vec{a_2}$" mean the same thing as "$\theta(\vec{a_1}, \vec{a_2})$ is true"?
Best Answer
For a general discussion of the significance of this notion, you can see my answer here.
I will now try to answer your many questions - in an order of my choosing.
A high-level answer: It means that the structure $A$ admits definable quotients for all definable equivalence relations.
Your suspicion is correct. I dislike Hodges's terminology here, though. Instead of "equivalence formula $\theta$", I prefer to say "definable equivalence relation $E$".
Yes.
We have one property called "uniform elimination of imaginaries". For a particular definable equivalence relation $E$, we can talk about a structure (uniformly) eliminating the $E$-imaginaries. But "$A$ (uniformly) eliminates imaginaries" means that $A$ (uniformly) eliminates $E$-imaginaries for all definable equivalence relations $E$.
No, your reasoning is incorrect, because a definable function is allowed to produce tuples as outputs. Here $F$ is defined by a formula $\varphi_F(\overline{x},\overline{y})$, where $\overline{x}$ and $\overline{y}$ are tuples of variables, such that $A\models \forall \overline{x}\exists^!\overline{y}\, \varphi_F(\overline{x},\overline{y})$. Then $F(\overline{a})$ is the unique $\overline{b}$ such that $A\models \varphi_F(\overline{a},\overline{b})$.
A pragmatic reason is this: One of the main technical benefits of uniform elimination of imaginaries is that we can "code" definable sets by tuples. That is, suppose $\varphi(\overline{x},\overline{y})$ is a formula. A $\varphi$-definable set is a definable set $\varphi(A,\overline{b})$ for some tuple of parameters $\overline{b}$. Note that different choices of parameters can define the same set, so $\overline{b}$ is not a perfect "code" for $\varphi(A,\overline{b})$. But now consider the equivalence relation $E$ defined by $\overline{b}E\overline{b}'$ if and only if $\forall \overline{x}\,(\varphi(\overline{x},\overline{b})\leftrightarrow \varphi(\overline{x},\overline{b}'))$. Let $F$ be the definable function eliminating $E$-imaginaries. Now $F(\overline{b})$ is tuple canonically associated to $\varphi(A,\overline{b})$ in the sense that if $\varphi(A,\overline{b})= \varphi(A,\overline{b}')$, then $F(\overline{b}) = F(\overline{b}')$.
This has the following useful consequence: if $\sigma$ is an automorphism of $A$, then $\sigma$ fixes the definable set $\varphi(A,\overline{b})$ setwise iff $\varphi(A,\overline{b}) = \varphi(A,\sigma(\overline{b}))$ iff $\overline{b}E\sigma(\overline{b})$ iff $F(\overline{b}) = F(\sigma(\overline{b}))$ iff $\sigma$ fixes $F(\overline{b})$ pointwise. But this last step, commuting $F$ and $\sigma$, requires $F$ to be $0$-definable. If $F$ is definable with parameters in $C$, we would have to restrict attention to automorphisms fixing $C$ pointwise.
No, not in the definition. But there's a trick which allows us to show that if a structure uniformly eliminates imaginaries, it also uniformly eliminates $E$-imaginaries for $C$-definable equivalence relations $E$ (by $C$-definable functions $F$).
Suppose $\theta(\overline{x},\overline{x}',\overline{c})$ is a formula with paramters $\overline{c}$ defining an equivalence relation $E_{\overline{c}}$. Consider a formula $\theta'(\overline{x},\overline{z},\overline{x}',\overline{z}')$ expressing the following: "$\overline{z} = \overline{z}'$, and if ($\theta(\overline{x},\overline{x}',\overline{z})$ defines an equivalence relation $\overline{x}E\overline{x}'$), then $\theta(\overline{x},\overline{x}',\overline{z})$." This formula $\theta'$ defines an equivalence relation $E'$. Let $F'(\overline{x},\overline{z})$ be the $0$-definable function eliminating $E'$-imaginaries. Then $F(\overline{x}) = F'(\overline{x},\overline{c})$ is a $\overline{c}$-definable function eliminating $E_{\overline{c}}$-imaginaries.