关于模型论论证应用于代数闭域/实闭域的困惑

我正在上模型论的入门课，讲师反复用一种论证思路，但我怎么都绕不过弯来。

示例：希尔伯特第17问题的模型论证明 #

希尔伯特第17问题的结论是：每个实系数半正定多项式都可以表示为有理函数的平方和。

我转述了David Marker《Model Theory: An Introduction》里的一个证明过程：
我们用逆否命题来推导：设$F$是$\mathbb{R}$上关于变量$x_1,\dots,x_n$的有理函数域，$f\in\mathbb{R}[x_1,\dots,x_n]$是一个无法表示为$F$中平方和的实多项式。根据佐恩引理，存在一个序关系让$F$成为有序域，并且在这个序下$f<0$。接下来把$F$嵌入到它（本质上唯一的）保序实闭包$R$中——这部分我都能理解。

但接下来的步骤我就卡壳了：因为在$R$中$f<0$，所以有$R\models\exists\bar{v}.f(\bar{v})<0$。而所有实闭域都是初等等价的，因此$\mathbb{R}\models\exists\bar{v}.f(\bar{v})<0$，至此证明完成。

我的核心困惑 #

我们使用的是有序域的语言，签名为$(0,1,+,\times,<)$。我觉得这里的问题在于，$f(\bar{x})$是$R$中的元素，但证明似乎把“域变量”$\bar{x}$和“模型论变量”$\bar{v}$混为一谈了。在有序域的语言中，$f(\bar{v})$（这里$\bar{v}$是模型论变量）通常不是一个合法的项——毕竟这个语言里的项只能是整系数多项式。这么一来，$\exists\bar{v}.f(\bar{v})<0$根本不是这个语言中的句子，说$R\models\exists\bar{v}.f(\bar{v})<0$就完全说不通了。我一开始尝试把$f$的系数换成模型论变量，再额外加几个量词，但还是没法让这个证明变得严谨。

我的问题 #

我已经好几次看到这种“把多项式假装成项”的策略了（比如用模型论证明希尔伯特零点定理和Chevalley定理的时候），但就是搞不懂背后的逻辑。我想请教两个问题：

• 怎么严谨地证明这种论证思路是合理的？
• 我对Marker的证明理解得正确吗？

备注：内容来源于stack exchange，提问作者Hernán Ibarra Mejia