Hi I am trying to prove that ACF has quantifier elimination.
A. Background:
It uses the follow theory:
First order theory $\mathcal{T}=\left<\mathcal{L}_\mathcal{A},\mathbb{L}_\mathcal{A},T,T^*\right>$ that is consistent, then for any $\phi(x_1,...,x_n)\in\mathcal{L}_\mathcal{A}$ the following statements are equivalent:
there exists $\psi(x_1,...,x_n)\in\mathcal{L}_\mathcal{A}$ without quantifier that satisfy $T\vdash(\phi\leftrightarrow\phi)$
Any $\mathcal{M}=\left<M,I\right>,\mathcal{N}=\left<N,J\right>$ are models of $\mathcal{T}$ if there are sub-struct $\mathcal{M}'=\left<M',I'\right>,\mathcal{N}' =\left<N',J'\right>$ that is isomorphic ($e$ as the mapping), then for any $\left<a_1,...,a_n\right>\in (M')^n$, $\mathcal{M}\vDash\phi[a_1,...,a_n]$ is equivalent to $\mathcal{N}\vDash\phi[e(a_1),...,e(a_n)]$
During the proof, it assumes that if ACF $\mathcal{M},\mathcal{N}$ has a subfield $\mathcal{M}',\mathcal{N}' $ are isomorphic, then following some properties of field to prove that.
B. My question:
The theory states that for any sub-struct, which means that may be $\mathcal{M}',\mathcal{N}' $ are isomorphic but not sub-field, since field requires $(\forall x_1(\exists x_2(f_+(x_1,x_2)\hat{=}c_0)))$ and $(\forall x_1((\lnot(x_1\hat{=}c_0))\to(\exists x_2(f_\times(x_1,x_2)\hat{ =}c_1))))$
Thus, I would like to ask how to handle the above situation??