# If $\mathcal{T}_1$ and $\mathcal{T}_2$ admit quantifier elimination, does $\mathcal{T}$ admit quantifier elimination?

Let $\mathcal{T}_1$ and $\mathcal{T}_2$ be theories with disjoint signatures $\mathcal{L}_1, \mathcal{L}_2$. Form a new language $\mathcal{L} = \mathcal{L}_1 \cup \mathcal{L}_2 \cup \{P_1, P_2\}$, with $P_1, P_2$ unary predicates. For each sentence $\phi_1 \in \mathcal{T}_1$, convert it to a new sentence $\phi$ over $\mathcal{L}$ by asserting that all of its quantified variables satisfy $P_1$; specifically, replace "$\exists x : \_\_\_$" with "$\exists x : P_1 x \land \_\_\_$" and replace "$\forall x : \_\_\_$" with "$\forall x : P_1 x \to \_\_\_$. Do the same for all sentences in $\mathcal{T}_2$, using the predicate $P_2$. Put all of these sentences into a new theory $\mathcal{T}$ over $\mathcal{L}$. Also add axioms:

• $\forall x : \lnot (P_1 x \land P_2 x)$

• $P_1 c$, for each constant symbol $c \in \mathcal{L}_1$, and likewise for $\mathcal{L}_2$;

• $\forall x_1 \ldots x_k : P_1 f(x_1, \ldots, x_k)$, for each $k$-ary function symbol $f \in \mathcal{L}_1$, and likewise for $\mathcal{L}_2$.

Together, all of this makes a theory $\mathcal{T}$ whose models--I think--behave sort of exactly like having a model of $\mathcal{T}_1$ and a model of $\mathcal{T}_2$ separately.

Anyway my concrete question is:

If $\mathcal{T}_1$ and $\mathcal{T}_2$ have quantifier elimination, does $\mathcal{T}$ have quantifier elimination?

which I am unable to prove. Maybe there is a counterexample.

• You probably also want $\forall x\,(P_1 x \lor P_2 x)$? If so, & I think so, you could make your first bulleted axiom $\forall x\,(P_1 x \leftrightarrow \neg P_2 x)$. Perhaps the Craig Interpolation Lemma can help? Lyndon's strengthening, or anyway ideas used in the proof. You have to deal with formulas that mix the two 'worlds'. – BrianO Dec 18 '15 at 12:11

Even if a model $M$ of $\mathcal{T}$ has to be a disjoint union of a model $M_1$ of $\mathcal{T}_1$ and a model $M_2$ of $\mathcal{T}_2$ (taking BrianO's comment into account), by definition of an $\mathcal{L}$-structure, it has to interpret the eventual function or relation symbols of both languages, and such symbol in $\mathcal{L}_i$ will range over $M_{3-i}$ as well. Corresponding formulas (without the specification of $P_i x$ at each instance of a quantifier symbol) may hardly be reduced to quantifier-free formulas modulo $\mathcal{T}$ since $\mathcal{T}$ says nothing about how for instance $f \in \mathcal{L}_1$ behaves for $\overline{x} \in M_2$.

For instance let $\mathcal{T}_1$ be the theory of algebraically closed fields of characteristic $0$ and $\mathcal{T}_2$ be the theory of dense linear orders without extrema. They have quantifier elimination in respectively $\left\langle +,.,-,\ ^{-1},0,1 \right\rangle$ and $\left\langle < \right\rangle$.

Now, $\mathbb{C} \uplus \mathbb{Q}$ * can be made into a model of $\mathcal{T}$ by seing $\mathbb{Q}$ as a subfield of $\mathbb{C}$ and defining the laws $+,.,-,\ ^{-1}$ accordingly, and stating that they range in $\mathbb{C}$ only. Now to interpret $<$, state:

-either that $\mathbb{C} < \mathbb{Q}$, no element of $\mathbb{Q}$ is inferior to an element of $\mathbb{C}$, $<$ behaves as usal on $\mathbb{Q}$ and is always verified in $\mathbb{C}$. This gives a model $M$.

-or that $\mathbb{Q} < \mathbb{C}$, no element of $\mathbb{C}$ is inferior to an element of $\mathbb{Q}$, $<$ behaves as usal on $\mathbb{Q}$ and is always verified in $\mathbb{C}$. This gives a model $M'$.

Mind that this definition of $<$ has nothing in common with the regular one (except when restricted to $\mathbb{Q}$), but that this is allowed by your conditions.

Let $\varphi$ be the sentence $\forall x (\exists y (P_2 y \wedge x.x < y))$.

$M \vDash \varphi$ since for $x \in \mathbb{Q} \uplus \mathbb{C}$, $x.x \in \mathbb{C}$ and $\mathbb{C} < \mathbb{Q}$, so take $y = 0 \in \mathbb{Q}$.

$M' \vDash \neg \varphi$ since for $x \in \mathbb{Q} \uplus \mathbb{C}$, $x.x \in \mathbb{C}$ and no element of $\mathbb{C}$ is inferior to an element of $\mathbb{Q}$.

Now let's assume $\varphi$ is equivalent to a quantifier-free $\mathcal{L}$-sentence molulo $\mathcal{T}$, that is (equivalent to) a disjonction of conjonctions of formulas of the type $q < 0$, or $\neg(q < 0)$ or $q = 0$ or $q \neq 0$ where $q$ is a rational number in $\mathbb{C}$. Then it is equivalent in $M$ and $M'$ to just those of the form $q = 0$ or $\neg(q < 0)$ or $q \neq 0$ since two complex numbers (distinct or not) are inferior to one another in $M$ and $M'$, therefore $\varphi$ is true in $M$ iff there is no instance of a $\neg(q < 0)$ and all appearing in the form $q = 0$ $q$ are indeed zero while those appearing in the form $q \neq 0$ are non-zero. This is the same for $M'$, so $\varphi$ is true in $M'$ iff it's true in $M$ which contradicts the previous claim.

*$A \uplus B := (A \times \{0\}) \cup (B \times \{1\})$ so in my anwser and from the definition on, $\mathbb{C}$ means $\mathbb{C} \times \{0\}$ and $\mathbb{Q}$ means $\mathbb{Q} \times \{1\}$