I am actually not reading the original paper "Diophantine problems over local fields, I (1965)" by Ax and Kochen but the revised version " The model theory of local fields (1975) " by Kochen which is simpler. 



> 
> Side question: Are the ideas in this two papers significantly different from one another?
> 
> 
> 


The central result of the paper is the isomorphism theorem:


Let $V$ and $V'$ be unramified $\omega$-pseudo-complete Hensel fields of cardinality $\aleph\_1$ with normalized cross section ($x$-section). Then there is a x-analytic isomorphis $\varphi: V \rightarrow V'$ if and only if $ \bar{V} \simeq \bar{V'}$ and $\text{ord}\ V \simeq \text{ord}\ V'$.


Here unramified means the characteristic of the residue field is 0 or the characteristic of the residue field is $p$, and the absolute ramification index is 1 i.e. p is the element of least positive value. $\bar{V}$ denotes the residue field of $V$ and $\text{ord}\ V$ denotes the valuation group of $V$. An x-isomorphism is and isomorphism that send the cross section in $V$ to the cross section in $V'$.


I have read that in "One Definable subsets of p-adic fields ", MacIntyre proved that in the case of p-adic fields, the x-section can be replaced with the quantifier $P\_n$.



> 
> Is it possible to get rid of the x-section in the above isomorphism theorem in general?
> 
> 
> 


The motivation is that the x-section is not among the usual functions. ( There is certain discussion on the same paper by Kochen about removing the x-section, but it appears not what I want).



Can the cross-section (x-section) be removed from the Ax-Kochen proof in "Diophantine problems over local fields"?
It is not necessary to assume the existence of a cross-section to conclude the relative completeness part of the Ax-Kochen-Ershov theorem, but for the more refined relative quantifier elimination is not true in general without the cross section.


Let me explain.


First of all, we should make a slight correction to your statement of the Ax-Kochen theorem. The existence of an isomorphism between V and V' requires the continuum hypothesis. [See Shelah, Saharon, Vive la différence. II. The Ax-Kochen isomorphism theorem,  

Israel J. Math. 85 (1994), no. 1-3, 351--390, in which Shelah shows that there models of ZFC in which there are nonprincipal ultrafilters ${\mathcal U}$ on the primes for which $\prod\_{\mathcal U} {\mathbb F}\_p((t))$ and $\prod\_{\mathcal U} {\mathbb Q}\_p$ are
 not isomorphic.]


What Matthew Morrow says about completeness relative to $RV(F)$ is correct (mathematically, though not historically --- these structures have been studied under different names, by for example, Franz-Viktor Kuhlmann and Serban Basarab, in connection with quantifier elimination and relative completeness and by the founders of the theory of valued fields already in the 1930s. I discuss these structures in detail in my paper published in the proceedings of the 1999 workshop on valuation theory in Saskatoon). There are many suitable languages for understanding RV, but the following might be the most straight forward. 


We give ourselves four sorts: VF for the valued field, RV for the residue-valuation sort, $\Gamma$ for the value group, and $k$ for the residue field. On VF and k we have the language of rings, on RV the language of multiplicative groups and on $\Gamma$ the language of ordered abelian groups. These sorts are connected by the natural quotient map $r:K^\times \to RV(K) = K^\times/(1 + {\mathfrak m})$, the valuation map $v:K^\times \to \Gamma$, the induced valuation map (still denoted by $v$) $v:RV \to \Gamma$, the reduction map $\pi:{\mathcal O} \to k$, and the natural inclusion $\iota:k^\times \to RV$. 


It should be clear that $k$ and $\Gamma$ are interpretable in RV with its full induced structure. That is, if we would prefer to work with a two-sorted language, then we should treat RV as a structure with multiplication, a predicate for the image of $\iota$, a three place predicate for addition on the image of $\iota$ and a two-place relation $V(x,y)$ to be interpreted as $v(x) \leq v(y)$. 


In this language it is now the case that if $K$ and $L$ are unramified henselian fields (so either $k(K)$ and $k(L)$ have residue characteristic zero or the residue characteristic is $p > 0$ and $v(p)$ is the least positive element of the value group), then $K$ and $L$ are elementarily equivalent (in the two-sorted language described above) if and only if $RV(K)$ and $RV(L)$ are elementarily equivalent. 


Moreover, the theory of unramified henselian fields eliminates quantifiers relative to RV in the sense that for any formula $\phi$ there is another formula $\psi$ for which the quantifiers only range over RV for which the theory of unramified henselian fields proves that $\phi$ is equivalent to $\psi$.


Now, one may deduce the relative completeness theorem for the residue field and value group from the corresponding relative completeness theorem for RV. The point is that $RV(K)$ and $RV(L)$ are elementarily equivalent if and only if $k(K)$ and $k(L)$ are elementarily equivalent as fields and $\Gamma(K)$ and $\Gamma(L)$ are elementarily equivalent as ordered groups. Why? The question is absolute, so we may prove the result under the assumption of the continuum hypothesis. We can replace $K$ and $L$ with elementarily equivalent saturated models of size $\aleph\_1$, $K^\ast$ and $L^\ast$, respectively. From the saturation hypothesis, cross-sections $\chi\_K:\Gamma(K^\ast) \to RV(K^\ast)$ and $\chi\_L:\Gamma(L^\ast) \to RV(L^\ast)$ exist as do isomorphisms $k(K^\ast) \cong k(L^\ast)$ and $\Gamma(K^\ast) \cong \Gamma(L^\ast)$. Since with $\chi$, RV splits as a product, we conclude that $RV(K^\ast) \cong RV(L^\ast)$. In particular, $RV(K) \equiv RV(K^\ast) \equiv RV(L^\ast) \equiv RV(L)$ so that $K$ and $L$ are elementarily equivalent by the weak form AKE for RV.


Quantifier elimination simply relative to the residue field and value group is not true. For example, in ${\mathbb Q}((t))$ the elements $t^2$ and $5 t^2$ have the same [relative to the residue field and value group] quantifier-free type (ie they agree on all formulas in which only quantification over $k$ and $\Gamma$ are allowed) but they do not have the same type as the first is a square and the second is not.


Generalizing the RV construction to include sorts $RV\_n$ to be interpreted as $RV\_n(K) = K^\times/(1 + n {\mathfrak m})$ one may obtain a relative quantifier elimination and completeness theorem for all henselian fields of characteristic zero. That is, without any restriction on ramification.


