Separating points from closed convex sets over ordered fields and a metric for $\tilde {R}^n$

Abstract:

Let $R$ be an arbitrary ordered field, let $\bar R$ be a real closure, and let $\tilde R$ and ${\tilde R^n}$ denote the real spectra of $\bar R[X]$ and $\bar R[{X_1}, \ldots ,{X_n}]$. We prove that a closed convex subset in ${R^n}$ may be separated from a point not in it via a continuous "linear" functional taking values in $\tilde R$ and that there is a $\tilde R$-valued metric on ${\tilde R^n}$. The methods rely on the ultrafilter interpretation of points in ${\tilde R^n}$ and on the existence of suprema and infima of sets in $\tilde R$.