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.

  • $\begingroup$ 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'. $\endgroup$ – 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\}$


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.