[proofplan] The implication from quantifier elimination to the tuple condition is immediate once every formula is replaced, modulo $T$, by a quantifier-free formula. Conversely, the tuple condition forces every formula to be determined by its quantifier-free consequences; compactness then extracts finitely many of those consequences and turns them into a single quantifier-free equivalent. Finally, eliminating existential formulas suffices because arbitrary formulas are built from atomic formulas using Boolean connectives and quantifiers, and universal quantifiers are reducible to negated existential quantifiers. [/proofplan] [step:Derive the tuple condition from quantifier elimination] Assume that $T$ has quantifier elimination. Let $n \in \mathbb{N}$, let $M,N \models T$, let $a \in M^n$, and let $b \in N^n$. Assume that $a$ and $b$ satisfy the same quantifier-free $L$-formulas. Let $\varphi(x_1,\dots,x_n)$ be an arbitrary $L$-formula. By quantifier elimination, there is a quantifier-free $L$-formula $\theta(x_1,\dots,x_n)$ such that \begin{align*} T \models \forall x_1 \cdots \forall x_n\bigl(\varphi(x_1,\dots,x_n) \leftrightarrow \theta(x_1,\dots,x_n)\bigr). \end{align*} Since $M,N \models T$, this gives \begin{align*} M \models \varphi(a) &\Longleftrightarrow M \models \theta(a),\\ N \models \varphi(b) &\Longleftrightarrow N \models \theta(b). \end{align*} The hypothesis on quantifier-free formulas gives \begin{align*} M \models \theta(a) \Longleftrightarrow N \models \theta(b). \end{align*} Combining these equivalences yields \begin{align*} M \models \varphi(a) \Longleftrightarrow N \models \varphi(b). \end{align*} Thus $a$ and $b$ satisfy the same $L$-formulas. [/step] [step:Use the tuple condition and compactness to eliminate one formula] Assume the tuple condition in condition 2. Let $\varphi(x_1,\dots,x_n)$ be an arbitrary $L$-formula. Write $x$ for the tuple $(x_1,\dots,x_n)$. If $T \models \forall x\,\neg\varphi(x)$, then $\varphi(x)$ is equivalent modulo $T$ to the quantifier-free contradiction $\bot$. Hence assume that $T \cup \{\exists x\,\varphi(x)\}$ is satisfiable. Define $\Delta_\varphi(x)$ to be the set of all quantifier-free $L$-formulas $\delta(x)$ such that \begin{align*} T \models \forall x\bigl(\varphi(x) \rightarrow \delta(x)\bigr). \end{align*} We claim that \begin{align*} T \cup \Delta_\varphi(x) \cup \{\neg\varphi(x)\} \end{align*} is not satisfiable. Suppose, toward a contradiction, that there are a model $M \models T$ and a tuple $c \in M^n$ such that $M \models \delta(c)$ for every $\delta(x) \in \Delta_\varphi(x)$, while $M \models \neg\varphi(c)$. Define the quantifier-free type of $c$ in $M$ by \begin{align*} \operatorname{qftp}_M(c) := \{\rho(x) : \rho(x) \text{ is quantifier-free and } M \models \rho(c)\}. \end{align*} We show that \begin{align*} T \cup \operatorname{qftp}_M(c) \cup \{\varphi(x)\} \end{align*} is finitely satisfiable. Let $\rho_1(x),\dots,\rho_k(x) \in \operatorname{qftp}_M(c)$, and define the quantifier-free formula \begin{align*} \rho(x) := \rho_1(x) \wedge \cdots \wedge \rho_k(x), \end{align*} with $\rho(x) := \top$ when $k=0$. If \begin{align*} T \cup \{\exists x\,(\varphi(x) \wedge \rho(x))\} \end{align*} were inconsistent, then \begin{align*} T \models \forall x\bigl(\varphi(x) \rightarrow \neg\rho(x)\bigr). \end{align*} Thus $\neg\rho(x) \in \Delta_\varphi(x)$, so $M \models \neg\rho(c)$. But each $\rho_i(x)$ belongs to $\operatorname{qftp}_M(c)$, so $M \models \rho(c)$, a contradiction. Therefore every finite subset is satisfiable. By the [compactness theorem for first-order logic](/theorems/4290) (citing a result not yet in the wiki: [Compactness Theorem](/theorems/2748) for First-Order Logic), there are a model $N \models T$ and a tuple $d \in N^n$ such that \begin{align*} N \models \varphi(d) \end{align*} and \begin{align*} N \models \rho(d) \end{align*} for every $\rho(x) \in \operatorname{qftp}_M(c)$. Hence $c$ and $d$ satisfy the same quantifier-free $L$-formulas: if $\sigma(x)$ is quantifier-free and $M \models \sigma(c)$, then $\sigma(x) \in \operatorname{qftp}_M(c)$, so $N \models \sigma(d)$; if $M \models \neg\sigma(c)$, then $\neg\sigma(x) \in \operatorname{qftp}_M(c)$, so $N \models \neg\sigma(d)$. By the tuple condition, $c$ and $d$ satisfy the same $L$-formulas. Applying this to $\varphi(x)$ gives \begin{align*} M \models \varphi(c) \Longleftrightarrow N \models \varphi(d), \end{align*} contradicting $M \models \neg\varphi(c)$ and $N \models \varphi(d)$. Therefore \begin{align*} T \cup \Delta_\varphi(x) \cup \{\neg\varphi(x)\} \end{align*} is unsatisfiable. Applying compactness again, there are formulas $\delta_1(x),\dots,\delta_m(x) \in \Delta_\varphi(x)$ such that \begin{align*} T \models \forall x\bigl((\delta_1(x) \wedge \cdots \wedge \delta_m(x)) \rightarrow \varphi(x)\bigr). \end{align*} Define the quantifier-free formula \begin{align*} \theta(x) := \delta_1(x) \wedge \cdots \wedge \delta_m(x), \end{align*} with $\theta(x) := \top$ if $m=0$. Since each $\delta_i(x)$ lies in $\Delta_\varphi(x)$, we also have \begin{align*} T \models \forall x\bigl(\varphi(x) \rightarrow \theta(x)\bigr). \end{align*} Thus \begin{align*} T \models \forall x\bigl(\varphi(x) \leftrightarrow \theta(x)\bigr), \end{align*} where $\theta(x)$ is quantifier-free. Since $\varphi(x)$ was arbitrary, $T$ has quantifier elimination. [guided] We want to prove that an arbitrary formula $\varphi(x)$ is equivalent, modulo $T$, to quantifier-free information. The tuple condition says exactly that truth of all formulas is already determined by truth of quantifier-free formulas across models of $T$. The compactness argument turns this semantic determination into a finite quantifier-free formula. Let $x$ denote the tuple $(x_1,\dots,x_n)$. If no tuple in any model of $T$ satisfies $\varphi(x)$, then $\varphi(x)$ is equivalent modulo $T$ to the quantifier-free formula $\bot$, so there is nothing to prove. We therefore assume that $T \cup \{\exists x\,\varphi(x)\}$ is satisfiable. Define $\Delta_\varphi(x)$ to be the set of quantifier-free consequences of $\varphi(x)$ over $T$: \begin{align*} \Delta_\varphi(x) := \{\delta(x) : \delta(x) \text{ is quantifier-free and } T \models \forall x(\varphi(x) \rightarrow \delta(x))\}. \end{align*} The key point is that these consequences determine $\varphi(x)$. Suppose they did not. Then there would be a model $M \models T$ and a tuple $c \in M^n$ such that $c$ satisfies every formula in $\Delta_\varphi(x)$ but does not satisfy $\varphi(x)$. We now force another tuple to have exactly the same quantifier-free behaviour as $c$, while also satisfying $\varphi$. Define \begin{align*} \operatorname{qftp}_M(c) := \{\rho(x) : \rho(x) \text{ is quantifier-free and } M \models \rho(c)\}. \end{align*} We claim that \begin{align*} T \cup \operatorname{qftp}_M(c) \cup \{\varphi(x)\} \end{align*} is finitely satisfiable. Take finitely many formulas $\rho_1(x),\dots,\rho_k(x)$ from $\operatorname{qftp}_M(c)$ and put \begin{align*} \rho(x) := \rho_1(x) \wedge \cdots \wedge \rho_k(x), \end{align*} with $\rho(x) := \top$ if $k=0$. If no model of $T$ realised $\varphi(x) \wedge \rho(x)$, then \begin{align*} T \models \forall x\bigl(\varphi(x) \rightarrow \neg\rho(x)\bigr). \end{align*} Since $\neg\rho(x)$ is quantifier-free, this would put $\neg\rho(x)$ in $\Delta_\varphi(x)$. But $c$ satisfies every formula in $\Delta_\varphi(x)$, so $M \models \neg\rho(c)$. On the other hand, $M \models \rho_i(c)$ for each $i$, hence $M \models \rho(c)$. This contradiction proves finite satisfiability. By the compactness theorem for first-order logic (citing a result not yet in the wiki: Compactness Theorem for First-Order Logic), there are a model $N \models T$ and a tuple $d \in N^n$ satisfying both $\varphi(d)$ and every formula in $\operatorname{qftp}_M(c)$. This makes $c$ and $d$ quantifier-free indistinguishable. Indeed, if a quantifier-free formula $\sigma(x)$ is true of $c$, then $\sigma(x) \in \operatorname{qftp}_M(c)$, so it is true of $d$. If $\sigma(x)$ is false of $c$, then $\neg\sigma(x)$ is true of $c$, so $\neg\sigma(x) \in \operatorname{qftp}_M(c)$, and therefore $\sigma(x)$ is false of $d$. The tuple condition now applies to $c \in M^n$ and $d \in N^n$. Since they satisfy the same quantifier-free formulas, they must satisfy the same formulas. In particular, \begin{align*} M \models \varphi(c) \Longleftrightarrow N \models \varphi(d). \end{align*} But $M \models \neg\varphi(c)$ and $N \models \varphi(d)$, a contradiction. Hence $T \cup \Delta_\varphi(x) \cup \{\neg\varphi(x)\}$ is unsatisfiable. Compactness now gives a finite subcollection $\delta_1(x),\dots,\delta_m(x)$ of $\Delta_\varphi(x)$ such that \begin{align*} T \models \forall x\bigl((\delta_1(x) \wedge \cdots \wedge \delta_m(x)) \rightarrow \varphi(x)\bigr). \end{align*} Define \begin{align*} \theta(x) := \delta_1(x) \wedge \cdots \wedge \delta_m(x), \end{align*} with $\theta(x) := \top$ if $m=0$. Since each $\delta_i(x)$ is a quantifier-free consequence of $\varphi(x)$ over $T$, we also have \begin{align*} T \models \forall x\bigl(\varphi(x) \rightarrow \theta(x)\bigr). \end{align*} Thus \begin{align*} T \models \forall x\bigl(\varphi(x) \leftrightarrow \theta(x)\bigr). \end{align*} The formula $\theta(x)$ is quantifier-free, so $\varphi(x)$ has been eliminated. Since $\varphi(x)$ was arbitrary, $T$ has quantifier elimination. [/guided] [/step] [step:Obtain existential elimination from quantifier elimination] Assume that $T$ has quantifier elimination. Let \begin{align*} \exists y_1 \cdots \exists y_m\,\psi(x_1,\dots,x_n,y_1,\dots,y_m) \end{align*} be an existential $L$-formula, where $\psi$ is quantifier-free. This is an $L$-formula in the free variables $x_1,\dots,x_n$. By quantifier elimination, there is a quantifier-free $L$-formula $\theta(x_1,\dots,x_n)$ such that \begin{align*} T \models \forall x_1 \cdots \forall x_n\left(\exists y_1 \cdots \exists y_m\,\psi(x_1,\dots,x_n,y_1,\dots,y_m) \leftrightarrow \theta(x_1,\dots,x_n)\right). \end{align*} Thus every existential formula is equivalent modulo $T$ to a quantifier-free formula. [/step] [step:Eliminate all formulas from existential elimination by induction] Assume that every existential $L$-formula is equivalent modulo $T$ to a quantifier-free $L$-formula. We prove by structural induction on $L$-formulas that every $L$-formula is equivalent modulo $T$ to a quantifier-free formula. Atomic formulas are already quantifier-free. If $\alpha(x)$ and $\beta(x)$ are equivalent modulo $T$ to quantifier-free formulas $\alpha_0(x)$ and $\beta_0(x)$, then $\neg\alpha(x)$, $\alpha(x)\wedge\beta(x)$, and $\alpha(x)\vee\beta(x)$ are equivalent modulo $T$ to the quantifier-free formulas $\neg\alpha_0(x)$, $\alpha_0(x)\wedge\beta_0(x)$, and $\alpha_0(x)\vee\beta_0(x)$, respectively. It remains to handle quantifiers. Suppose $\alpha(x,y)$ is equivalent modulo $T$ to a quantifier-free formula $\alpha_0(x,y)$. Then \begin{align*} T \models \forall x\,\forall y\bigl(\alpha(x,y) \leftrightarrow \alpha_0(x,y)\bigr), \end{align*} so \begin{align*} T \models \forall x\left(\exists y\,\alpha(x,y) \leftrightarrow \exists y\,\alpha_0(x,y)\right). \end{align*} The formula $\exists y\,\alpha_0(x,y)$ is existential with quantifier-free matrix, so by the hypothesis there is a quantifier-free formula $\theta(x)$ such that \begin{align*} T \models \forall x\left(\exists y\,\alpha_0(x,y) \leftrightarrow \theta(x)\right). \end{align*} Therefore $\exists y\,\alpha(x,y)$ is equivalent modulo $T$ to $\theta(x)$. For a universal quantifier, use the logical equivalence \begin{align*} \forall y\,\alpha(x,y) \leftrightarrow \neg\exists y\,\neg\alpha(x,y). \end{align*} The formula $\neg\alpha(x,y)$ is equivalent modulo $T$ to a quantifier-free formula by the Boolean step, and the preceding existential case eliminates $\exists y\,\neg\alpha(x,y)$. Negating the resulting quantifier-free formula gives a quantifier-free formula equivalent modulo $T$ to $\forall y\,\alpha(x,y)$. By structural induction, every $L$-formula is equivalent modulo $T$ to a quantifier-free $L$-formula. Hence $T$ has quantifier elimination. [/step] [step:Combine the implications] The first step proves condition 1 implies condition 2. The second step proves condition 2 implies condition 1. The third step proves condition 1 implies condition 3. The fourth step proves condition 3 implies condition 1. Therefore conditions 1, 2, and 3 are equivalent. [/step]