Proof. The implication $(b)\Rightarrow(c)$ is trivial, and $(c)\Rightarrow(a)$ is immediate from the definitions: If $N\preccurlyeq_\exists M^*\equiv_{\forall\exists} M$ and $\varphi\in{\rm Th}_{\forall\exists}(M)$, then without loss of generality φ is of the form $\forall\underline{x}\psi(\underline{x})$ with $\psi\in{\rm Form}_\exists(\mathfrak{L})$ (Remark 2.6). Now $M^*\equiv_{\forall\exists} M\models\varphi$ implies that $M^*\models\psi(\underline{a})$ for every $\underline{a}\in N^n$, and therefore $N\models\psi(\underline{a})$ by the assumption $N\preccurlyeq_\exists M^*$.

To prove (b) assuming (a), first note that we can assume without loss of generality that $M^*\equiv M$. Now [Reference Chang and Keisler10, Proposition 5.2.2] gives elementary extensions $M\preccurlyeq M'$ and $N\preccurlyeq N'$ such that $N\leq M'\leq N'$. By the Löwenheim–Skolem theorem, there exists $N\leq M^{\prime\prime}\preccurlyeq M'$ of cardinality $|M^{\prime\prime}|=\kappa:=\max\{|N|,|\mathfrak{L}|,\aleph_{0}\}$, in particular $N\preccurlyeq_\exists M^{\prime\prime}$. As the κ-saturated $M^*$ is $\kappa^+$-universal [Reference Hodges23, Theorem 8.1.6], there is an elementary embedding $M^{\prime\prime}\rightarrow M^*$.

Proof. $(a)\Rightarrow(b)$. Without loss of generality $N=N^{*}$. Let ${\underline{b}}\in N^n$ and let $\underline{x}$ denote the tuple of variables $(x_1,\dots,x_n)$. Write

\begin{equation*} p(\underline{x})=\{\forall y_1,\dots,y_m\;\psi(\underline{x},\underline{y})\mid m\in\mathbb{N},N\models\forall\underline{y}\;\psi(\underline{b},\underline{y}),\psi\in{\rm Form}_{\mathsf{F}_0}(\mathfrak{L})\}. \end{equation*}

This is the universal type of ${\underline{b}}$ in N. We claim that $p(\underline{x})\cup {\rm eldiag}(M)$ is finitely satisfiable: a conjunction of finitely many elements of $p(\underline{x})$ is logically equivalent to a universal formula in free variables $\underline{x}$, that is again in $p(\underline{x})$, say $\forall\underline{y}\;\psi(\underline{x},\underline{y})$. Since ${\underline{b}}\in N^n$, we have $N\models\exists\underline{x}\forall\underline{y}\;\psi(\underline{x},\underline{y})$. By (a), this implies $M\models\exists\underline{x}\forall\underline{y}\;\psi(\underline{x},\underline{y})$, which proves the claim. So by the compactness theorem there is an elementary extension $M_{\underline{b}}\succcurlyeq M$ and a tuple $\underline{a}_{\underline{b}}\in M_{\underline{b}}^n$ such that $M_{\underline{b}}\models p(\underline{a}_{\underline{b}})$.

We now consider the language $\mathfrak{L}'=\mathfrak{L}(\underline{c})$ where $\underline{c}=(c_1,\dots,c_n)$ is an n-tuple of new constant symbols, and the $\mathfrak{L}(\underline{c})$-structures $(M_{\underline{b}},\underline{a}_{\underline{b}})$ and $(N,\underline{b})$. The $\mathfrak{L}'(M_{\underline{b}}\cup N)$-theory $T=\mathrm{diag}(M_{\underline{b}},\underline{a}_{\underline{b}})\cup\mathrm{eldiag}(N,{\underline{b}})$ is finitely satisfiable: A conjunction of finitely many elements from $\mathrm{diag}(M_{\underline{b}},\underline{a}_{\underline{b}})$ is logically equivalent to a sentence of the form $\varphi(\underline{c},\underline{d})$ for a quantifier-free $\mathfrak{L}$-formula $\varphi(\underline{x},\underline{y})$ and $d_1,\dots,d_m\in M_{\underline{b}}$. Then $M_{\underline{b}}\not\models\forall\underline{y}\neg\varphi(\underline{a}_{\underline{b}},\underline{y})$ and therefore $N\models\exists\underline{y}\varphi(\underline{b},\underline{y})$, so $(N,\underline{b})$ can be expanded to a model of ${\rm eldiag}(N,\underline{b})\cup\{\varphi(\underline{c},\underline{d})\}$. So by the compactness theorem, T has a model $N_{\underline{b}}$, which is then an elementary extension of N, and the $\mathfrak{L}$-embedding $f_{\underline{b}}\colon M_{\underline{b}}\rightarrow N_{\underline{b}}$ with $f_{\underline{b}}(\underline{a}_{\underline{b}})=\underline{b}$ comes as usual from the method of diagrams.

$(b)\Rightarrow(c)$. For each $\underline{b}\in(N^*)^n$ fix $N_{\underline{b}}$, $M_{\underline{b}}$ and $f_{\underline{b}}$ as given by (b). Choose a cardinal number κ with $\kappa \gt |N_{\underline{b}}|$ for every $\underline{b}\in(N^*)^n$. Let $N^{**}\succcurlyeq N^{*}$ be κ-saturated, in particular $\kappa^+$-universal, so that for every $\underline{b}\in(N^*)^n$ there is an elementary $\mathfrak{L}(N^*)$-embedding $g_{\underline{b}}\colon N_{\underline{b}}\rightarrow N^{**}$. Then $g_{\underline{b}}\circ f_{\underline{b}}\colon M_{\underline{b}}\rightarrow N^{**}$ is as required for (c).

$(c)\Rightarrow(d)$. Write $M_{0}=M$ and $N_{0}=N$. We recursively construct an increasing elementary chain $(N_{i})_{i\in\omega}$, using (c), such that for each i and ${\underline{b}}\in(N_i)^n$ there exists $M_{\underline{b}}\succcurlyeq M$, $f_{\underline{b}}\colon M_{\underline{b}}\rightarrow N_{i+1}$ with $b_1,\dots,b_n\in f_{\underline{b}}(M_{\underline{b}})$. Then $N^*:=\varinjlim_i N_i$ satisfies the claim.

$(d)\Rightarrow(e)\Rightarrow(f)$. Trivial.

$(f)\Rightarrow(a)$. Let $\varphi\in {\rm Th}_{\forall_n\exists}(M)$. Without loss of generality, $\varphi=\forall x_1,\dots,x_n\exists\underline{y}\;\psi(\underline{x},\underline{y})$ with ψ quantifier-free (Remarks 2.2 and 2.6). Let $\underline{b}\in N^n$ and let $N_{\underline{b}}$, $M_{\underline{b}}$ and $f_{\underline{b}}\colon M_{\underline{b}}\rightarrow N_{\underline{b}}$ be given as in (f), in particular there exists $\underline{a}_{\underline{b}}\in (M_{\underline{b}})^n$ with $f_{\underline{b}}(\underline{a}_{\underline{b}})=\underline{b}$. Since $M_{\underline{b}}\equiv_{\forall_n\exists} M$ and $M\models\varphi$, also $M_{\underline{b}}\models\varphi$, so there exists $\underline{c}\in(M_{\underline{b}})^m$ such that $M_{\underline{b}}\models\psi(\underline{a}_{\underline{b}},\underline{c})$. Applying $f_{\underline{b}}$ we get $N_{\underline{b}}\models\psi(\underline{b},f_{\underline{b}}(\underline{c}))$, in particular $N_{\underline{b}}\models\exists\underline{y}\psi(\underline{b},\underline{y})$. Since $\underline{b}\in N^n$ and $N\preccurlyeq_{\exists}N_{\underline{b}}$, also $N\models\exists\underline{y}\psi(\underline{b},\underline{y})$. Thus, $N\models\varphi$.

Proof. $(a)\Rightarrow(b)$: By Lemma 3.3(d), we can construct an elementary chain $N=N_1\preccurlyeq N_2\preccurlyeq\cdots$ such that for each n and $B\subseteq N_n$ with $|B|\leq n$ there exists $M_B\succcurlyeq M$ and an $\mathfrak{L}$-embedding $f_B\colon M_B\rightarrow N_{n+1}$ with $B\subseteq f_B(M_B)$. Thus $N^*:=\varinjlim_n N_n$ satisfies (b).

$(b)\Rightarrow(a)$: Condition (b) implies Lemma 3.3(d) for every n, so $\mathrm{Th}_{\forall_{n}\exists}(M)\subseteq\mathrm{Th}_{\forall_{n}\exists}(N)$ for every n. Since every $\varphi\in{\rm Form}_{\forall\exists}(\mathfrak{L})$ is equivalent to ${\rm prnx}_{\exists,\mathfrak{L}}(\varphi)\in{\rm Form}_{\forall_n\exists}(\mathfrak{L})$ for some n, it follows that $\mathrm{Th}_{\forall\exists}(M)\subseteq\mathrm{Th}_{\forall\exists}(N)$.

Proof. Take $\chi_{p,n,0}=\top$ and $\chi_{p,n,1}=(x=y_1)$. Take $\chi_{p,n,2}$ to be

\begin{equation*} \exists \lambda_{0,\dots,0},\dots,\lambda_{p-1,\dots,p-1}\Bigg(x=\sum_{0\leq i_{1},\ldots,i_{n} \lt p}\lambda_{i_{1},\ldots,i_{n}}^{p}\prod_{j=1}^{n}z_j^{i_{j}}\wedge y_1=\lambda_{0,\dots,0}\wedge y_2=\lambda_{p-1,\dots,p-1}\Bigg) \end{equation*}

and inductively $\chi_{p,n,r+1}(x,y_1,\dots,y_{r+1},\underline{z})=\exists w(\chi_{p,n,r}(x,y_1,\dots,y_{r-1},w,\underline{z})\wedge\chi_{p,n,2}(w,y_r,y_{r+1},\underline{z}))$.

Proof. Let $\mathfrak{L}\supseteq\mathfrak{L}_{\rm ring}(\underline{c})$ and let $\varphi(\underline{u})\in\mathrm{Form}_{\forall\mathsf{F}}(\mathfrak{L})$. Then φ is equivalent to ${\rm prnx}_{\mathsf{F},\mathfrak{L}}(\varphi)=\forall x_{1},\ldots, x_{r}\psi(\underline{x},\underline{u})$ for some r, with $\psi(\underline{x},\underline{u})\in\mathrm{Form}_{\mathsf{F}}(\mathfrak{L})$, see Remark 2.6. Let $\tau_{\mathfrak{L}}\varphi$ be the formula

\begin{equation*} \forall w\exists\underline{x}(\chi_{p,n,r}(w,\underline{x},\underline{c})\wedge\psi(\underline{x},\underline{u})), \end{equation*}

with $\chi_{p,n,r}(w,\underline{x},\underline{c})\in\mathrm{Form}_{\exists}(\mathfrak{L}_{\mathrm{ring}}(\underline{c}))\subseteq\mathrm{Form}_{\mathsf{F}}(\mathfrak{L})$ as in Lemma 4.1. Then $\tau_{\mathfrak{L}}\varphi\in\mathrm{Form}_{\forall_{1}[\mathsf{F}]}(\mathfrak{L})$ is as required. This is uniform in $\mathfrak{L}$, since ${\rm prnx}_{\mathsf{F},\mathfrak{L}}$ is. If $\mathsf{F}$ is computable, then ${\rm prnx}_{\mathsf{F},\mathfrak{L}}$ is uniformly computable (Remark 2.6), which together with the computability of $\chi_{p,n,r}$ gives the uniform computability of $\tau_\mathfrak{L}$.

Proof. Take $\pi_{p,n}$ to be

\begin{equation*} \exists \lambda_{0,\dots,0},\dots,\lambda_{p-1,\dots,p-1}\Bigg(\sum_{0\leq i_{1},\ldots,i_{n} \lt p}\lambda_{i_{1},\ldots,i_{n}}^{p}\prod_{j=1}^{n}z_j^{i_{j}}=0\wedge \bigvee_{0\leq i_{1},\ldots,i_{n} \lt p}\neg \lambda_{i_{1},\ldots,i_{n}}=0\Bigg). \end{equation*}

Proof. Let $\mathfrak{L}\supseteq\mathfrak{L}_{\rm ring}$ and let $\varphi(\underline{u})\in\mathrm{Form}_{\forall\mathsf{F}}(\mathfrak{L})$. Again we may assume that $\varphi(\underline{u})$ is of the form $\forall x_{1},\ldots, x_{r}\psi(\underline{x},\underline{u})$ for some r, with $\psi(\underline{x},\underline{u})\in\mathrm{Form}_{\mathsf{F}}(\mathfrak{L})$ (Remark 2.6). Let $\tau_{\mathfrak{L}}\varphi$ be the formula

\begin{equation*} \forall w, z_{1},\ldots, z_{n}(\pi_{p,n}(\underline{z})\vee\exists \underline{x}(\chi_{p,n,r}(w,\underline{x},\underline{z})\wedge\psi(\underline{x},\underline{u}))), \end{equation*}

with $\chi_{p,n,r},\pi_{p,n}\in\mathrm{Form}_{\exists}(\mathfrak{L}_{\mathrm{ring}})\subseteq\mathrm{Form}_{\mathsf{F}}(\mathfrak{L})$ as in Lemmas 4.1 and 4.3. Then $\tau_{\mathfrak{L}}\varphi\in\mathrm{Form}_{\forall_{n+1}[\mathsf{F}]}(\mathfrak{L})$ is as required. Uniformity and uniform computability follow as in the proof of Proposition 4.2.

Proof. Let k and φ be as in the statement, and let $K=k(X)$. Without loss of generality, $\varphi(\underline{u})$ is of the form $\forall x_1,\dots, x_r\psi(\underline{x},\underline{u})$ with $\psi\in\mathrm{Form}_{\mathsf{F}}(\mathfrak{L}_{\rm ring})$ (Remark 2.6). For every $\nu\geq 1$,

\begin{equation*} K^{p^\nu}\;\cong\; K\;=\;\mathbb{F}_p(X)k\;\cong_k\;\mathbb{F}_p(X)^{p^\nu}k\;=\;(\mathbb{F}_p(X)k)^{p^\nu}k\;=\;K^{p^\nu}k \end{equation*}

and the degrees are as in the following diagram (cf. [Reference Bourbaki9, V.135 No. 6 Cor. 3]):

In particular, as $[K^{p^\nu}k:K^{p^\nu}]=p^{n\nu}$, the formula

\begin{equation*} \eta_\nu(x) := \exists y_1,\dots,y_{p^{n\nu}},z_1,\dots,z_{p^{n\nu}}\left(\bigwedge_{i=1}^{p^{n\nu}}\gamma(z_i) \wedge x = \sum_{i=1}^{p^{n\nu}}y_i^{p^\nu}z_i\right), \end{equation*}

defines $K^{p^\nu}k$ in K, and the formula $\pi'(\underline{z})$ given by

\begin{align*} \exists \lambda_{0,\dots,0},\dots,\lambda_{p-1,\dots,p-1}& \left( \bigwedge_{0\leq i_{1},\ldots,i_{d} \lt p}\eta_1(\lambda_{i_1,\dots,i_d})\wedge \sum_{0\leq i_{1},\ldots,i_{d} \lt p}\lambda_{i_{1},\ldots,i_{d}}\prod_{j=1}^{d}z_j^{i_{j}}=0 \right.\\ &\quad\left. \wedge \bigvee_{0\leq i_{1},\ldots,i_{d} \lt p}\neg \lambda_{i_{1},\ldots,i_{d}}=0\right) \end{align*}

defines the set d-tuples that are not p-bases of K over $K^{p}k$ (cf. proof of Lemma 4.3). Note that $\eta_\nu,\pi'\in{\rm Form}_{\exists}(\mathfrak{L}_{\rm ring})$. We write $\psi^{\eta_\nu}$ for ψ with all quantifiers relativized to η_ν, defined inductively by $(\exists x\alpha)^{\eta_\nu}=\exists x(\eta_\nu(x)\wedge\alpha^{\eta_\nu})$ and $(\forall x\alpha)^{\eta_\nu}=\forall x(\eta_\nu'(x)\vee\alpha^{\eta_\nu})$, where $\eta_\nu'={\rm prnx}(\neg\eta_\nu)\in\mathrm{Form}_{\forall}(\mathfrak{L}_{\rm ring})$, cf. Remark 2.6. Note that $\psi^{\eta_\nu}\in{\rm Form}_\mathsf{F}(\mathfrak{L}_{\rm ring})$, as $\exists=\exists\exists$, $\forall\exists=\forall\forall\exists$, etc. Now fix ν with $p^{\nu-1} \lt r\leq p^{\nu}$ and let

\begin{eqnarray*} \tau\varphi(\underline{u}) \;:=\; \forall w,z_1,\dots,z_d\exists \underline{\lambda} \Bigg(\pi'(\underline{z})&\vee&\bigg(w= \sum_{0\leq i_{1},\ldots,i_{d} \lt p^\nu}\lambda_{i_{1},\ldots,i_{d}}\prod_{j=1}^{d}z_j^{i_{j}}\\ &&\wedge\bigwedge_{0\leq i_1,\dots,i_d \lt p^\nu}\eta_\nu(\lambda_{i_1,\dots,i_d})\wedge\bigwedge_{j=1}^m\gamma(u_j) \\ &&\wedge\psi^{\eta_\nu} (\lambda_{0,\dots,0},\dots,\lambda_{r-1,0,\dots,0},\underline{u})\bigg)\Bigg). \end{eqnarray*}

Then $\tau\varphi\in\mathrm{Form}_{\forall_{d+1}[\mathsf{F}]}(\mathfrak{L}_{\rm ring})$, and $K\models\tau\varphi(\underline{a})$ if and only if $a_1,\dots,a_m\in k$ and $K^{p^\nu}k\models\varphi(\underline{a})$, which since $K^{p^\nu}k\cong_k K$ is equivalent to $K\models\varphi(\underline{a})$.

Proof. Let $\kappa=\max\{|k|,\aleph_0\}$ and let $l^{\mathcal{U}}$ be a $\kappa^+$-saturated ultrapower of l (so $\mathcal{U}$ is an ultrafilter on some index set I, and $l^{\mathcal{U}}=l^I/\mathcal{U}$). Then ${\rm Th}_\exists(k,k_0)\subseteq{\rm Th}_\exists(l,k_0)$ implies that there exists an $\mathfrak{L}_{\rm ring}(k_0)$-embedding $k\rightarrow l^{\mathcal{U}}$ [Reference Chang and Keisler10, Lemma 5.2.1], which extends uniquely to an $\mathfrak{L}_{\rm ring}(k_0(X))$-embedding $k(X)\rightarrow l^{\mathcal{U}}(X)$. The inclusion $l\rightarrow l(X)$ gives rise to an $\mathfrak{L}_{\rm ring}(l)$-embedding $l^{\mathcal{U}}\rightarrow l(X)^{\mathcal{U}}$, which extends uniquely to an $\mathfrak{L}_{\rm ring}(l(X))$-embedding $l^{\mathcal{U}}(X)\rightarrow l(X)^{\mathcal{U}}$. Therefore

\begin{equation*} {\rm Th}_\exists(k(X),k_0(X))\subseteq{\rm Th}_\exists(l^{\mathcal{U}}(X),k_0(X))\subseteq{\rm Th}_\exists(l(X)^{\mathcal{U}},k_0(X))={\rm Th}_\exists(l(X),k_0(X)). \end{equation*}

The ‘in particular’ part follows, since if $k,l$ are fields with ${\rm Th}_\exists(k)\subseteq{\rm Th}_\exists(l)$, then in particular ${\rm char}(k)={\rm char}(l)$, and so without loss of generality they have the same prime field k ₀, and we can apply the claim to the k ₀-variety $X=\mathbb{A}^1$.

Proof. Firstly, $k\preccurlyeq_\exists k'$ implies that $k(t)\preccurlyeq_\exists k'(t)$, see [Reference Daans, Dittmann and Fehm14, Lemma 7.2], from which it follows that $\mathrm{Th}_{\forall\exists}(k'(t))\subseteq\mathrm{Th}_{\forall\exists}(k(t))$ (Lemma 3.1), in particular $\mathrm{Th}_{\forall_1\exists}(k'(t))\subseteq\mathrm{Th}_{\forall_1\exists}(k(t))$. For the converse inclusion, we verify Lemma 3.3(f) for $N=k'(t)$, $M=k(t)$ and n = 1. So let $b\in k'(t)$. If $b\in k$, we extend the inclusion $\iota\colon k\rightarrow k'$ to $\iota'\colon k(t)\rightarrow k'(t)$ by $\iota'(t)=t$, and note that b is in the image. If $b\notin k$ then, as both $k'/k$ (by, e.g., [Reference Ershov18, Corollary 3.1.3]) and $k'(t)/k'$ are regular, b is transcendental over k, so we may extend ι to an embedding $\iota^{\prime\prime}\colon k(t)\rightarrow k'(t)$ with $\iota^{\prime\prime}(t)=b$. So (f) holds with $N_b=N$ and $M_b=M$. By $(f)\Rightarrow(a)$ of Lemma 3.3, we have $\mathrm{Th}_{\forall_{1}\exists}(k(t))\subseteq\mathrm{Th}_{\forall_{1}\exists}(k'(t))$.

Proof. From ${\rm Th}_{\forall_1\exists}(k)\subseteq{\rm Th}_{\forall_1\exists}(l)$ it follows by Lemma 3.3(d) that there exists $l^{*}\succcurlyeq l$ such that for every $b\in l^{*}$ there exist $k_{b}\succcurlyeq k$ and an embedding $f_{b}\colon k_{b}\rightarrow l^{*}$ with $b\in f_b(k_b)$. By Lemma 5.2, $\mathrm{Th}_{\forall_{1}\exists}(l^*(t))=\mathrm{Th}_{\forall_{1}\exists}(l(t))$.

To see that ${\rm Th}_{\forall_1\exists}(k(t))\subseteq{\rm Th}_{\forall_1\exists}(l^*(t))$, we verify Lemma 3.3(f) for $M=k(t)$, $N=l^*(t)$ and n = 1. So let $b\in l^{*}(t)$. If $b\in l^{*}$ then we extend f_b to an embedding $f_{b}'\colon k_{b}(t)\rightarrow l^{*}(t)$ by $f_b'(t)=t$. In this case, we choose $M_{b}=k_{b}(t)$ and $N_{b}=N$. If on the other hand $b\notin l^{*}$ then it is transcendental over $l^{*}$, in particular over $f_{1}(k_1)$. We extend f ₁ to an embedding $f_{1}^{\prime\prime}\colon k_{1}(t)\rightarrow l^{*}(t)$ by $f_1^{\prime\prime}(t)=b$. In this case, we choose $M_{b}=k_{1}(t)$ and $N_{b}=N$. Note that in both cases $M_{b}\equiv_{\forall_{1}\exists}M$ by Lemma 5.2. This verifies Lemma 3.3(f), and the result now follows from the implication $(f)\Rightarrow(a)$ of Lemma 3.3.

Proof. Every $\sigma\in{\rm End}(k(t)/k)$ is injective, so $\sigma^{-1}(k)=k$ and therefore $\sigma(t)\in k(t)\setminus k$. Conversely, every $s\in k(t)/k$ is transcendental over k, so $\sigma|_k={\rm id}_k$, $\sigma(t)=s$ defines an isomorphism $\sigma\colon k(t)\rightarrow k(s)$.

Proof. Let $\varphi=\forall x\psi$ with $\psi(x,\underline{u})\in{\rm Form}_\exists(\mathfrak{L}_{\rm ring})$. If $q=\infty$, define $\tau\varphi=(\psi(t,\underline{u}),\varphi)$, and if $q \lt \infty$ define $\tau\varphi=(\varphi_q,\top(\underline{u}))$, where

\begin{equation*} \varphi_q := \psi(t,\underline{u})\wedge\exists y_1,\dots,y_q\Big(\bigwedge_i y_i^q-y_i=0\wedge\bigwedge_{i\neq j}y_i\neq y_j\wedge\bigwedge_i\psi(y_i,\underline{u})\Big). \end{equation*}

To prove the claim, let k be a field with $q=\#k$, and let $\tau\varphi=(\psi_1,\psi_2)$. First let $\underline{a}\in\varphi(k(t))\cap k^n$, i.e. $\underline{a}\in k^n$ and for every $b\in k(t)$, $k(t)\models\psi(b,\underline{a})$. Then in particular $k(t)\models\psi(t,\underline{a})$, and if $q \lt \infty$, then also $k(t)\models\psi(b,\underline{a})$ for every $b\in k$, i.e. for the zeros of $Y^q-Y$. So $\underline{a}\in\psi_1((k(t),t))$ in all cases, and if $q=\infty$, then $k\preccurlyeq_\exists k(t)$, see, e.g., [Reference Ershov18, Example 3.1.2], and so $k(t)\models\varphi(\underline{a})$ implies $k\models\varphi(\underline{a})$ (Lemma 3.1), and therefore $\underline{a}\in\psi_2(k)$ in all cases.

Conversely, let $\underline{a}\in\psi_1((k(t),t))\cap\psi_2(k)$. Since $k(t)\models\psi(t,\underline{a})$, it follows that $k(t)\models\psi(b,\underline{a})$ for every $b\in k(t)\setminus k$: Indeed, by Lemma 5.5, there exists a $\sigma_b\in{\rm End}(k(t)/k)$ with $\sigma_b(t)=b$, hence $\sigma_b(k(t))\models\psi(b,\underline{a})$ and so, since $\sigma_b(k(t))\leq k(t)$ and ψ is an existential formula, $k(t)\models\psi(b,\underline{a})$. If $q \lt \infty$, then $k(t)\models\psi_1(\underline{a})$ also implies that $k(t)\models\psi(b,\underline{a})$ for every $b\in k$, and if $q=\infty$, then $k\models\psi_2(\underline{a})$ gives that $k\models\psi(b,\underline{a})$ for every $b\in k$, and so, since $k\leq k(t)$ and ψ is an existential formula, $k(t)\models\psi(b,\underline{a})$ for every $b\in k$. This shows that in all cases $k(t)\models\psi(b,\underline{a})$ for every $b\in k(t)$, i.e. $\underline{a}\in\varphi(k(t))$.

Proof. Write $\varphi(\underline{u})=\psi(\underline{u},t)$ with $\psi\in{\rm Form}_\exists(\mathfrak{L}_{\rm ring})$ and define $\tau\varphi:=\forall x(\psi(\underline{u},x)\vee\gamma(x))$. To see that this satisfies the claim, first let $\underline{a}\in\varphi((k(t),t))\cap k^n$, so $k(t)\models\psi(\underline{a},t)$. As in the previous proof, by Lemma 5.5, this implies that $k(t)\models\psi(\underline{a},b)$ for every $b\in k(t)\setminus k$. Since $k(t)\models\gamma(b)$ for every $b\in k$, it follows that $\underline{a}\in\tau\varphi(k(t))$. Conversely, if $\underline{a}\in\tau\varphi(k(t))\cap k^n$, then in particular $k(t)\models\psi(\underline{a},t)\vee\gamma(t)$, so $t\notin\gamma(k(t))$ shows that $\underline{a}\in\varphi((k(t),t))$.

Proof. It is known that ${\rm Th}_\exists(k(t),t)$ is undecidable whenever k is of positive characteristic not containing the algebraic closure of the prime field. For example, this is implicit in [Reference Eisenträger and Shlapentokh16]. By Proposition 5.7 and Example 5.8, if k is in addition perfect or large, it follows that also ${\rm Th}_{\forall_1\exists}(k(t))$ is undecidable.

Proof. For these k, k is existentially $\emptyset$-definable in k(t) by Example 5.8, and ${\rm Th}(k)$ is decidable (in particular so is ${\rm Th}_{\forall_1\exists}(k)$), so the claim follows from Propositions 5.6 and 5.7.

Proof. Assume that $k/k_0$ is an extension with $k\subseteq\gamma(k(C))\subseteq k(C)\setminus\{x\}$. Write $k(C)=k(x,y)$ and note that $f(x,y)=0$ and $x\notin k$. If $a,b\in k(C)\setminus k$ with $f(a,b)=0$, then $k(a,b)\cong_k k(C)$, and since $k(x,y)/k(a,b)$ is separable and $k(x,y)$ and $k(a,b)$ are function fields of the same genus greater one, the Riemann–Hurwitz formula [Reference Stichtenoth38, Theorem 3.4.13] implies that $k(a,b)=k(x,y)$. In particular, there is a unique $\sigma\in{\rm Aut}(k(C)/k)$ with $\sigma(x)=a$, $\sigma(y)=b$. Conversely, if $\sigma\in{\rm Aut}(k(C)/k)$, then $f(\sigma(x),\sigma(y))=0$ and $\sigma(x)\notin k$.

Given $\varphi(\underline{u})\in\mathrm{Form}_\mathsf{F}(\mathfrak{L}_{\rm ring}(k_0[\mathbf{x},\mathbf{y}]))$, express each constant c occurring in φ as $t(\mathbf{x},\mathbf{y})$ for an $\mathfrak{L}_{\rm ring}(k_0)$-term $t(v,w)$, and this way obtain $\varphi_0(\underline{u},v,w)\in{\rm Form}_\mathsf{F}(\mathfrak{L}_{\rm ring}(k_0))$ such that $k(C)\models(\varphi(\underline{u})\leftrightarrow\varphi_0(\underline{u},x,y))$, independent of k. Define

\begin{equation*} \tau\varphi := \forall a,b\big(f(a,b)\neq0\vee\gamma(a)\vee\varphi_0(\underline{u},a,b)\big). \end{equation*}

Then $\tau\varphi\in{\rm Form}_{\forall_2[\mathsf{F}]}(\mathfrak{L}_{\rm ring}(k_0))$ satisfies the claim: Indeed, if $\underline{c}\in\varphi(k(C))\cap k^n$, then $k(C)\models\varphi_0(\underline{c},x,y)$, and if $k(C)\models f(a,b)=0\wedge\neg\gamma(a)$, then, as explained above, there exists $\sigma\in{\rm Aut}(k(C)/k)$ with $\sigma(x)=a$, $\sigma(y)=b$, and therefore $\varphi_0(\sigma(\underline{c}),\sigma(x),\sigma(y)) = \varphi_0(\underline{c},a,b)$ holds in k(C), so $\underline{c}\in\tau\varphi(k(C))$. Conversely, if $\underline{c}\in\tau\varphi(k(C))\cap k^n$, then in particular $k(C)\models\varphi_0(\underline{c},x,y)$, and hence $\underline{c}\in\varphi(k(C))$.

Proof. As k ₀ is perfect and $k_0(C)$ is of genus at least two, $m:=|{\rm Aut}(k_0(C)/k_0)| \lt \infty$, see [Reference Rosenlicht35]. Since k ₀ is perfect, also the genus of $\overline{k_0}(C)$ is at least two, and so also ${\rm Aut}(\overline{k_0}(C)/\overline{k_0})$ is finite. It follows that ${\rm Aut}(\overline{k}(C)/\overline{k})={\rm Aut}(\overline{k_0}(C)/\overline{k_0})$, and therefore also ${\rm Aut}(k(C)/k)={\rm Aut}(k_0(C)/k_0)$ for every regular $k/k_0$.

Let $(a,b)\in k(C)^2\setminus k^2$ with $f(a,b)=0$. Then $k(C)/k(a,b)$ is finite, and $k(a,b)\cong_k k(C)$, so there exists $\sigma\in{\rm End}(k(C)/k)$ with $\sigma(x,y)=(a,b)$. If $k(C)/k(a,b)$ is separable, then in fact $k(C)=k(a,b)$ by the Riemann–Hurwitz formula, so $\sigma\in{\rm Aut}(k(C)/k)$. If on the other hand $k(C)/k(a,b)$ is inseparable, then, as $[k(C):k(C)^p]=p$ due to the assumption that k is perfect, $k(a,b)\subseteq k(C)^p$, and so in particular $a\in k(C)^p$.

Now let $\varphi(\underline{u})\in {\rm Form}_\exists(\mathfrak{L}_{\rm ring}(k_0[\mathbf{x},\mathbf{y}]))$, and again rewrite constants by $\mathfrak{L}_{\rm ring}(k_0)$-terms to obtain $\varphi_0(\underline{u},v,w)\in{\rm Form}_\exists(\mathfrak{L}_{\rm ring}(k_0))$ with $k(C)\models(\varphi(\underline{u})\leftrightarrow\varphi_0(\underline{u},x,y))$. As in the previous proof $\varphi_{0}(\underline{u},v,w)$ is independent of k. Define

\begin{eqnarray*} \tau\varphi&:=&\forall z \left( \exists w(w^p=z) \vee\eta(\underline{u},z) \right) \end{eqnarray*}

with

\begin{eqnarray*} \eta(\underline{u},z) &:=& \exists x_1,\dots,x_m,y_1,\dots,y_m \bigg(\bigwedge_{i\neq j}(x_i\neq x_j\vee y_i\neq y_j)\wedge \bigwedge_{i=1}^mf(x_i,y_i)=0 \\ &&\wedge \bigwedge_{i=1}^m\psi(\underline{u},z,x_i) \bigg) \end{eqnarray*}

and

\begin{eqnarray*} \psi(\underline{u},z,\xi) &:=& \exists \lambda_0,\dots,\lambda_{p-1} \bigg(z=\sum_{j=0}^{p-1}\lambda_j^p {\xi^j} \wedge \big(f(\lambda_0,\lambda_1)\neq 0 \vee \exists w(w^p=\lambda_0)\\ && \vee\varphi_0(\underline{u},\lambda_0,\lambda_1)\big) \bigg) . \end{eqnarray*}

Then $\tau\varphi\in{\rm Form}_{\forall_1[\exists]}(\mathfrak{L}_{\rm ring}(k_0))$ satisfies the claim:

Indeed, if $\underline{d}\in\tau\varphi(k(C))\cap k^n$ then in particular $k(C)\models\eta(\underline{d},c_0)$ for $c_0:=x^p+xy^p$, as the separability of f in y implies that $x\notin k(C)^p$ and therefore $c_0\notin k(C)^p$. Thus there exist pairwise distinct $(x_1,y_1),\dots,(x_m,y_m)$ with $f(x_i,y_i)=0$ such that $\psi(\underline{d},c_0,x_i)$ holds for every i. In particular, $\sum_{j=0}^{p-1} \lambda_j^px_i^j=c_0\notin k(C)^p$, so in particular $x_i\notin k(C)^p$, especially $x_i\notin k$. Therefore $(x_i,y_i)=\sigma(x,y)$ for some $\sigma\in{\rm Aut}(k(C)/k)$, so since $m=|{\rm Aut}(k(C)/k)|$ there exists i ₀ with $(x_{i_0},y_{i_0})=(x,y)$. From $\psi(\underline{d},c_0,x_{i_0})$ we get $\lambda_0,\dots,\lambda_{p-1}$ with

\begin{equation*} \sum_{j=0}^{p-1} \lambda_j^px^j=c_0=x^px^0+y^px^1, \end{equation*}

which since x is a p-basis for k(C) implies that $\lambda_0=x$ and $\lambda_1=y$, so since $f(\lambda_0,\lambda_1)=f(x,y)=0$ and $\lambda_0=x\notin k(C)^p$ we conclude that $\varphi_0(\underline{d},x,y)$ holds, i.e. $\underline{d}\in\varphi(k(C))$.

Conversely, suppose that $\underline{d}\in\varphi(k(C))\cap k^n$, in particular $k(C)\models\varphi_0(\underline{d},x,y)$. Then also $\varphi_0(\underline{d},a,b)$ holds in k(C) for all $(a,b)\in k(C)^2\setminus k^2$ with $f(a,b)=0$, as it holds in $k(a,b)$ by the isomorphism above, and therefore it holds in $k(C)\supseteq k(a,b)$ due to the fact that φ ₀ is existential. Now take any $c\in k(C)\setminus k(C)^p$, let ${\rm Aut}(k(C)/k)=\{\sigma_1,\dots,\sigma_m\}$ and define $(x_i,y_i)=\sigma_i(x,y)$. Then $(x_1,y_1),\dots,(x_m,y_m)$ are pairwise distinct as $x,y$ generate k(C) over k, and $f(x_i,y_i)=0$ for each i. We claim that $k(C)\models\psi(\underline{d},c,x_i)$ for every i. Indeed, write $c=\sum_{j=0}^{p-1} \lambda_j^p x_i^j$, which is possible since $x_i\notin k(C)^p$, so x_i is a p-basis of k(C). Whenever $f(\lambda_0,\lambda_1)= 0$ and $\lambda_0\notin k(C)^p$, in particular $\lambda_0\notin k$, so $\varphi_0(\underline{d},\lambda_0,\lambda_1)$ holds.

If k ₀ is presented and has a splitting algorithm, then $\tau$ is computable uniformly in f, since ${\rm Aut}(k_0(C)/k_0)$ and in particular m is computable, see [Reference Hess22].

Proof. With k also k(C) is presented, and [Reference Eisenträger and Shlapentokh16, Theorem 1.1] gives that ${\rm Th}_{\exists}(k(C),k(C))$ is undecidable. By choosing a plane affine curve $C':f(X,Y)=0$ birationally equivalent to C, Proposition 5.13 then immediately implies that ${\rm Th}_{\forall_1\exists}(k(C),k)$ is undecidable.

Proof of Theorem 1.3

Part (a) is the ‘in particular’ part of Proposition 5.1. Part (b) is Proposition 5.3. Part (c) follows from Proposition 5.6. Part (d) follows from Proposition 5.7. Part (e) follows from the case n = 1 of Propositions 4.2 and 4.5.

Proof. Part (a) is [Reference Anscombe and Fehm5, Proposition 3.25]. Part (b) is [Reference Anscombe and Fehm5, Corollary 3.19(c)]. Part (c) is an immediate consequence of the classical Ax–Kochen/Ershov principle for equicharacteristic zero henselian valued fields; the map $\tau$ can be obtained for example from [Reference Anscombe and Fehm5, Corollary 2.23].

Proof. This follows from the fact that the satisfaction of existential sentences (in this case with parameters from the residue field sort and from C) is preserved under embeddings.

Proof. We treat (a) and (b) simultaneously, where we use that the assumption of (b) implies that Kv and Lw are of characteristic zero so that (R4) holds when restricted to extensions of these (see [Reference Anscombe, Dittmann and Fehm2, Remarks 2.4, 4.18]). By [Reference Anscombe, Dittmann and Fehm2, Proposition 4.5], we can replace (K, v) by an elementary extension to assume without loss of generality that there is a section $\zeta_{K}\colon Kv\rightarrow K$ of the residue map of v. Similarly, we can assume that there is a section $\zeta_{L}\colon Lw\rightarrow L$ of the residue map of w. Replacing further the structure $(K,v,\zeta_K)$ by an elementary extension, we can assume that in addition it is $\max\{|Lw|,\aleph_0\}$-saturated, and then so is Kv, hence the assumption $\mathrm{Th}_{\forall\exists}(Kv)\subseteq\mathrm{Th}_{\forall\exists}(Lw)$ gives an existentially closed embedding $\varphi_{k}\colon Lw\rightarrow Kv$ by Lemma 3.1.

By mapping $t\mapsto\pi_{K}$, and using the universal property of the henselization, we extend ζ_K to an embedding of valued fields with distinguished uniformizers ${\zeta}_{K}'\colon (Kv(t)^{h},v_{t},t)\rightarrow(K,v,\pi_{K})$, where $Kv(t)^{h}$ denotes the henselization, as introduced above. By [Reference Anscombe, Dittmann and Fehm2, Corollary 4.14], (R4) implies that ${\zeta}_{K}'$ is existentially closed. Similarly, by mapping $t\mapsto\pi_{L}$, we extend ζ_L to an embedding of valued fields with distinguished element ${\zeta}_{L}'\colon(Lw(t)^{h},v_{t},t)\rightarrow(L,w,\pi_{L})$. Note that ${\zeta}_{L}'$ induces an isomorphism on the residue fields. Finally, by mapping $t\mapsto t$, we extend φ_k to an embedding of valued fields with distinguished uniformizers $\varphi\colon(Lw(t)^{h},v_{t},t)\rightarrow(Kv(t)^{h},v_{t},t)$. Again by [Reference Anscombe, Dittmann and Fehm2, Corollary 4.14], (R4) implies that φ is existentially closed. The situation looks as follows:

By Lemma 3.1,

\begin{equation*} \mathrm{Th}_{\forall^{}\exists}(K,v,\pi_{K}) \subseteq \mathrm{Th}_{\forall^{}\exists}(Kv(t)^{h},v_{t},t) \subseteq \mathrm{Th}_{\forall^{}\exists}(Lw(t)^{h},v_{t},t). \end{equation*}

In particular, $\mathrm{Th}_{\forall^{\mathbf{k}}\exists}(K,v,\pi_{K}) \subseteq\mathrm{Th}_{\forall^{\mathbf{k}}\exists}(Lw(t)^{h},v_{t},t) $ and we also have $\mathrm{Th}_{\forall^{\mathbf{k}}\exists}(Lw(t)^{h},v_{t},t) \subseteq\mathrm{Th}_{\forall^{\mathbf{k}}\exists}(L,w,\pi_{L})$ by Lemma 6.3 applied to $\zeta_L'$ with $C=\{t\}$, which concludes case (a). In case (b), by the usual Ax–Kochen/Ershov principle for residue characteristic zero, $\zeta_L'$ is an elementary embedding (it is an isomorphism on residue fields, and the embedding of value groups $\mathbb{Z}=v_tLw(t)^h\rightarrow wL$ is elementary since the theory of $\mathbb{Z}$-groups is model complete in the language of ordered abelian groups with a constant symbol for the smallest positive element [Reference Prestel and Delzell34, Theorem 4.1.3]), and so in particular ${\rm Th}_{\forall\exists}(Lw(t)^h,v_t,t)={\rm Th}_{\forall\exists}(L,w,\pi_L)$.

Question 6.5.

Does Proposition 6.4(b) hold similarly for all the ‘standard’ fragments $\exists,\forall\exists,\exists\forall\exists,\dots$? Can this be extended to a full Ax–Kochen/Ershov-principle of the following form: If (K, v) and (L, w) are equicharacteristic zero henselian non-trivially valued fields with ${\rm Th}_{\forall\exists}(Kv)\subseteq{\rm Th}_{\forall\exists}(Lw)$ and ${\rm Th}_{\forall\exists}(vK)\subseteq{\rm Th}_{\forall\exists}(wL)$, then ${\rm Th}_{\forall\exists}(K,v)\subseteq{\rm Th}_{\forall\exists}(L,w)$, and similarly for the other standard fragments?

Proof. There exists an extension $(K',v')\supseteq(K,v)$ and $\pi_{K}\in K'$ such that $(K',v',\pi_{K})\models\mathrm{H}^{e,\varpi}$ and the induced embedding $Kv\rightarrow K'v'$ is an isomorphism, see, for example, the first sentence in the proof of [Reference Anscombe, Dittmann and Fehm2, Corollary 4.16]. Lemma 6.3 with $C=\emptyset$ gives that $\mathrm{Th}_{\forall^{\mathbf{k}}\exists}(K,v)\subseteq \mathrm{Th}_{\forall^{\mathbf{k}}\exists}(K',v')$. Choose any $\pi_L\in L^\times$ with $w(\pi_L) \gt 0$. As ${\rm Th}_{\forall\exists}(K'v')={\rm Th}_{\forall\exists}(Kv)\subseteq{\rm Th}_{\forall\exists}(Lw)$, Proposition 6.4(a) implies $\mathrm{Th}_{\forall^{\mathbf{k}}\exists}(K',v',\pi_K)\subseteq\mathrm{Th}_{\forall^{\mathbf{k}}\exists}(L,w,\pi_L)$, so in particular $\mathrm{Th}_{\forall^{\mathbf{k}}\exists}(K',v')\subseteq\mathrm{Th}_{\forall^{\mathbf{k}}\exists}(L,w)$.

Proof. Parts (a) and (b) are consequences of (a) and (b) of Proposition 6.4, and part (c) is a consequence of Corollary 6.6, where in each case the map $\tau$ can be obtained using [Reference Anscombe and Fehm5, Corollary 2.23].

Proof. Since $(k(t)^{h},v_{t},t)\preccurlyeq_{\exists}(k(\!(t)\!),v_{t},t)$, there exists an elementary extension $(K,v,\pi_{v})\succcurlyeq(k(t)^{h},v_{t},t)$ and an $\mathfrak{L}_{\mathrm{val}}(\varpi)$-embedding $(k(\!(t)\!),v_{t},t)\rightarrow(K,v,\pi_{v})$. By [Reference Anscombe, Dittmann and Fehm2, Corollary 4.14], since $k[\![t]\!]$ is excellent, this embedding is existentially closed. Thus $\mathrm{Th}_{\forall\exists}(k(t)^{h},v_{t},t)\supseteq\mathrm{Th}_{\forall\exists}(k(\!(t)\!),v_{t},t)\supseteq \mathrm{Th}_{\forall\exists}(K,v,\pi_v)=\mathrm{Th}_{\forall\exists}(k(t)^{h},v_{t},t)$ by Lemma 3.1.

Proof. By the Keisler–Shelah theorem [Reference Hodges23, Theorem 8.5.10], it suffices to show that $(k(t)^{h},v_{t},t)\equiv_{\forall\exists}(k^{\mathcal{U}}(t)^{h},v_{t},t)$ for every ultrapower $k^{\mathcal{U}}$ of k. The embedding $k\rightarrow k^{\mathcal{U}}$ extends uniquely to an embedding $(k(t)^h,v_t,t)\rightarrow(k^{\mathcal{U}}(t)^h,v_t,t)$. The inclusion $k\rightarrow k(t)^h$ on the other hand extends to an embedding $k^{\mathcal{U}}\rightarrow (k(t)^h)^{\mathcal{U}}$ and then further to an embedding $f\colon(k^{\mathcal{U}}(t)^h,v_t,t)\rightarrow ((k(t)^h)^{\mathcal{U}},v_t^{\mathcal{U}},t^{\mathcal{U}})=(k(t)^h,v_t,t)^{\mathcal{U}}$ over $k(t)^h$, which immediately shows that $(k(t)^{h},v_t)\preccurlyeq_{\exists}(k^{\mathcal{U}}(t)^{h},v_t)$, hence ${\rm Th}_{\forall\exists}(k^{\mathcal{U}}(t)^{h},v_{t},t)\subseteq{\rm Th}_{\forall\exists}(k(t)^{h},v_{t},t)$ by Lemma 3.1. Moreover, the embedding f induces an isomorphism of residue fields $k^{\mathcal{U}}(t)^hv_t=k^{\mathcal{U}}= (k(t)^h)^{\mathcal{U}}v_t^{\mathcal{U}}$, hence f is existentially closed by [Reference Anscombe, Dittmann and Fehm2, Corollary 4.14], and therefore also ${\rm Th}_{\forall\exists}(k^{\mathcal{U}}(t)^{h},v_{t},t)\supseteq{\rm Th}_{\forall\exists}(k(t)^{h},v_{t},t)$, again by Lemma 3.1.

Proof. By Corollary 3.4, there exists $l\preccurlyeq l^*$ such that for every finite $B\subseteq l^*$ there exists $k_B\succcurlyeq k$ and an $\mathfrak{L}_{\rm ring}$-embedding $f_B\colon k_B\rightarrow l^*$ with $B\subseteq f_B(k_B)$. By Lemma 6.10, $(l^{*}(t)^h,v_t,t)\equiv_{\forall\exists}(l(t)^h,v_t,t)$, so it suffices to verify Lemma 3.3(e) for $M=(k(t)^h,v_t,t)$, $N=(l^*(t)^h,v_t,t)$, and $N^*=N$. So let $b_1,\dots,b_n\in l^{*}(t)^{h}$. As $l^*(t)^h$ is the direct limit of $l'(t)^h$ for l ^ʹ running over finitely generated subfields of $l^*$, there exists a finite $B\subseteq l^*$ such that $b_1,\dots,b_n\in \mathbb{F}(B)(t)^h$, where $\mathbb{F}$ is the prime field of l. The map f_B extends to an $\mathfrak{L}_{\rm val}(\varpi)$-embedding $f\colon(k_{B}(t)^h,v_{t},t)\rightarrow(l^*(t)^h,v_{t},t)$, and $b_1,\dots,b_n\in f(k_{B}(t)^h)$. So since $(k_{B}(t)^{h},v_{t},t)\equiv_{\forall\exists}(k(t)^{h},v_{t},t)=M$ by Lemma 6.10, $M_{\underline{b}}:=(k_{B}(t)^h,v_t,t)$ satisfies Lemma 3.3(e).

Proof. Let k = Kv and l = Lw. By [Reference Anscombe, Dittmann and Fehm2, Proposition 4.5], replacing $(K,v,\pi_K)$ by an elementary extension, there exists a section $k\rightarrow K$ of the residue map of v, which extends to an $\mathfrak{L}_{\mathrm{val}}(\varpi)$-embedding $(k(t)^{h},v_{t},t)\rightarrow(K,v,\pi_{K})$. By [Reference Anscombe, Dittmann and Fehm2, Corollary 4.14], since $\mathcal{O}_{v_t}$ is excellent, this embedding is existentially closed. Therefore, $\mathrm{Th}_{\forall\exists}(K,v,\pi_{K})\subseteq\mathrm{Th}_{\forall\exists}(k(t)^{h},v_{t},t)$ by Lemma 3.1. By Lemmas 6.11 and 6.9,

\begin{equation*} \mathrm{Th}_{\forall\exists}(k(t)^{h},v_{t},t)\subseteq\mathrm{Th}_{\forall\exists}(l(t)^{h},v_{t},t)=\mathrm{Th}_{\forall\exists}(l(\!(t)\!),v_{t},t). \end{equation*}

Since $wL\cong\mathbb{Z}$, there is also an $\mathfrak{L}_{\mathrm{val}}(\varpi)$-embedding $(L,w,\pi_{L})\rightarrow(l(\!(t)\!),v_{t},t)$, obtained by completing, see [Reference Anscombe, Dittmann and Fehm2, Propositions 4.2 and 4.3]. By [Reference Anscombe, Dittmann and Fehm2, Corollary 4.14], since $\mathcal{O}_w$ is excellent, this embedding is existentially closed. Therefore $\mathrm{Th}_{\forall\exists}(l(\!(t)\!),v_{t},t)\subseteq\mathrm{Th}_{\forall\exists}(L,w,\pi_{L})$, again by Lemma 3.1.

Proof. By Lemma 3.3(d), there exists $l^{*}\succcurlyeq l$ such that for every $b\in l^{*}$ there exists $k_{b}\succcurlyeq k$, $a_b\in k_b$ and an $\mathfrak{L}_{\mathrm{ring}}$-embedding $f_{b}\colon k_{b}\rightarrow l^{*}$ with $f_b(a_b)=b$. By Lemma 6.10, $(l^{*}(t)^h,v_t)\equiv_{\forall\exists}(l(t)^h,v_t)$, so it suffices to verify Lemma 3.3(e) for $M=(k(t)^h,v_t)$, $N=(l^*(t)^h,v_t)$ and n = 1, with $N^*:=N$.

So let $c\in l^{*}(t)^{h}$. Without loss of generality, $v_t(c)\geq0$, so $c=b+u$ for $b\in l^{*}$ and $v_t(u) \gt 0$. If u = 0, then $c=b\in l^{*}$, so f_b may be extended to an $\mathfrak{L}_{\mathrm{val}}(\varpi)$-embedding $f_b'\colon(k_{b}(t)^{h},v_{t},t)\rightarrow(l^{*}(t)^{h},v_{t},t)$, and $f_b'(a_b)=f_b(a_b)=b=c$. Otherwise, if u ≠ 0, then u is transcendental over $l^*$ and $v_t|_{l^*(u)}$ is the u-adic valuation on $l^*(u)$, so we may extend f_b to an $\mathfrak{L}_{\mathrm{val}}$-embedding $f_{b}^{\prime\prime}\colon(k_{b}(t)^{h},v_{t})\rightarrow(l^{*}(t)^{h},v_{t})$ with $f_b^{\prime\prime}(t)=u$. Then $f_{b}^{\prime\prime}(a_{b}+t)=f_{b}(a_{b})+f_{b}(t)=b+u=c$.

In both cases, $(k_{b}(t)^{h},v_{t})\equiv_{\forall\exists}(k(t)^{h},v_{t})$ by Lemma 6.10, in particular $(k_{b}(t)^{h},v_{t})\equiv_{\forall_{1}\exists}(k(t)^{h},v_{t})$. Therefore, $M_b:=(k_b(t)^h,v_t)$ satisfies Lemma 3.3(e).

Proof. Let $(K,v),(L,w)\models\mathrm{H}^{e,\mathrm{disc}}$ and suppose that $\mathrm{Th}_{\forall_{1}\exists}(k)\subseteq\mathrm{Th}_{\forall_{1}\exists}(l)$, where k = Kv and l = Lw. Let π_K be any uniformizer of v, so that $(K,v,\pi_{K})\models\mathrm{H}^{e,\varpi}$. As above (for example, apply Proposition 6.12), $\mathrm{Th}_{\forall\exists}(K,v,\pi_{K})\subseteq\mathrm{Th}_{\forall\exists}(k(t)^{h},v_{t},t)$, in particular $\mathrm{Th}_{\forall_{1}\exists}(K,v)\subseteq\mathrm{Th}_{\forall_{1}\exists}(k(t)^{h},v_{t})$. By Lemma 6.14, $\mathrm{Th}_{\forall_{1}\exists}(k(t)^{h},v_{t})\subseteq\mathrm{Th}_{\forall_{1}\exists}(l(t)^{h},v_{t})$.

By [Reference Anscombe, Dittmann and Fehm2, Proposition 4.5], replacing (L, w) by an elementary extension, there exists a section $f\colon l\rightarrow L$ of the residue map of w. For every $s\in L^\times$ with $w(s) \gt 0$, f extends uniquely to an embedding $f_s\colon(l(t)^h,v_t,t)\rightarrow (L,w,s)$, as in the proof of Lemma 6.14. By Lemma 3.3(e) (applied with n = 1), in order to show that $\mathrm{Th}_{\forall_{1}\exists}(l(t)^{h},v_{t})\subseteq \mathrm{Th}_{\forall_{1}\exists}(L,w)$, it suffices to find for every $c\in L$ an $\mathfrak{L}_{\mathrm{val}}$-embedding $g\colon(l(t)^{h},v_{t})\rightarrow(L,w)$ with $c\in g(l(t)^{h})$. Replacing c by c ⁻¹ if necessary, we may assume that $w(c)\geq0$, and then we may write $c=f(b)+u$ with $b\in l$ and $w(u) \gt 0$. If u = 0, then $c=f(b)$, and we let $g=f_s$ where $s\in L^\times$ with $w(s) \gt 0$ is arbitrary, and then $c=g(b)$. Otherwise we let $g=f_u$, and then $c=g(b+t)$

Proof. The map $\tau$ can again be obtained from Proposition 6.15 by [Reference Anscombe and Fehm5, Corollary 2.23].

Proof. The claim that each $\sigma\in{\rm Aut}(K/k)$ preserves v_t is contained in [Reference Schilling36] and also follows from [Reference Ax6]. By [Reference Schilling36, Theorem 1], $\sigma\mapsto\sigma(t)/t$ gives a bijection ${\rm Aut}(K/k)\rightarrow\mathcal{O}_v^\times$, which implies that $\{\sigma(t):\sigma\in{\rm Aut}(K/k)\}$ is the set of uniformizers. For each $0\neq s\in\mathfrak{m}_t$, $\sum_ia_it^i\mapsto\sum_ia_is^i$ defines a $\sigma\in{\rm End}(K/k)$ with $\sigma(t)=s$. Conversely, if $\sigma\in{\rm End}(K/k)$, then $L:=\sigma(K)$ carries the henselian valuation $w:=v_t\circ\sigma^{-1}$, whose extension to $F:=\overline{L}\cap K$ must be equivalent to $v_t|_F$ by F. K. Schmidt’s theorem [Reference Engler and Prestel17, Theorem 4.4.1], so since $v_t(t) \gt 0$ also $w(t) \gt 0$ and therefore $v_t(\sigma(t)) \gt 0$. This also shows that $\sigma\in{\rm End}(K,v_t)$.

Proof. Let $\nu(x)$ be $\forall z( v(x) \gt 0 \wedge (v(z)\geq v(x)\vee v(z)\leq 0))$.

Proof. We write K for the $\mathfrak{L}_{\rm val}$-structure $(k(\!(t)\!),v_t)$. Write the formula ν from Lemma 6.20 as $\nu(x)=\forall z\eta(x,z)$ with $\eta\in{\rm Form}(\mathfrak{L}_{\rm val})$ quantifier-free. Given $\varphi(\underline{u})\in{\rm Form}_{\forall_n[\exists_1[\mathsf{F}]]}(\mathfrak{L}_{\rm val}(t))$, write $\varphi=\forall y_1,\dots,y_n\exists z\psi(\underline{u},t,\underline{y},z)$ with $\psi(\underline{u},w,\underline{y},z)\in{\rm Form}_{\mathsf{F}}(\mathfrak{L}_{\rm val})$, and define

\begin{equation*} \tau\varphi \;:=\; \forall x\forall y_1,\dots,y_n \exists z (\neg\eta(x,z)\vee\psi(\underline{u},x,\underline{y},z)). \end{equation*}

Then $\tau\varphi\in{\rm Form}_{\forall_{n+1}[\exists_1[\mathsf{F}]]}(\mathfrak{L}_{\rm val})$, as $\neg\eta\in{\rm Form}_{\mathsf{F}_0}(\mathfrak{L}_{\rm val})\subseteq{\rm Form}_{\mathsf{F}}(\mathfrak{L}_{\rm val}) $ and $\psi\in{\rm Form}_{\mathsf{F}}(\mathfrak{L}_{\rm val})$. If $\underline{a}\in \tau\varphi(K)\cap k^m$, then in particular $K\models\forall\underline{y}\exists z(\neg\eta(t,z)\vee\psi(\underline{a},t,\underline{y},z))$, and since t is a uniformizer and therefore $K\models\forall z\eta(t,z)$ we get that $K\models\forall\underline{y}\exists z\psi(\underline{a},t,\underline{y},z)$, hence $\underline{a}\in\varphi(K)$. Conversely, if $\underline{a}\in\varphi(K)$, then $K\models\forall\underline{y}\exists z\psi(\underline{a},t,\underline{y},z)$. Given any $x\in k(\!(t)\!)$, either x is a uniformizer, in which case there is $\sigma\in{\rm Aut}(K)$ with $\sigma(t)=x$ and $\sigma|_k={\rm id}_k$ (Lemma 6.19) and therefore $K\models\forall\underline{y}\exists z\psi(\underline{a},x,\underline{y},z)$, or x is not a uniformizer, in which case there exists $z\in k(\!(t)\!)$ with $K\models\neg\eta(x,z)$. Thus $K\models\forall x\forall\underline{y}\exists z(\neg\eta(x,z)\vee\psi(\underline{a},x,\underline{y},z))$, i.e. $\underline{a}\in\tau\varphi(K)$.