Do the real algebraic numbers satisfy a type of completeness axiom excluding free variables?

Question

Question: Do the real algebraic numbers satisfy a type of completeness axiom excluding free variables? (The specific axiom is given below.)

Attempt: Tarski gave a first-order axiomatization of Euclidean geometry which is equivalent to a first-order axiomatization of any real closed field. Tarski also gave an axiomatization of the real numbers which is second-order, and showed that the theory of real closed fields completely axiomatizes the first-order theory of the real numbers (at least according to Wikipedia).

The only axiom for Tarski's characterization of the real numbers which requires second-order logic (and which thus also must be that which distinguishes as the unique Dedekind-complete ordered field and thus from all other real closed fields) is the Dedekind-completeness axiom (which is equivalent to the least upper bound property, and/or being Cauchy complete):

For all $X,Y \subseteq \mathbb{R}$, if for all $x \in X$ and $y \in Y$, $x < y$, then there exists a $z$ such that for all $x \in X$ and $y \in Y$, if $z \not=x$ and $z \not=y$, then $x< z <y$.

However, there is a corresponding first-order axiom schema in Tarski's first-order characterization of Euclidean geometry which "is essentially the Dedekind cut construction, carried out in a way that avoids quantification over sets" /"plays the role of a Dedekind cut axiom expressed in first-order terms". The only difference between this axiom and the above (as far as I can tell) is that (1) it is technically an axiom schema, i.e. a compendium of infinitely many related axioms, and not as single axiom, (2) it explicitly excludes quantification with free variables. Specifically it reads:

Let $\phi(x)$ be a formula in which variables $z,y$ do not occur freely, and let $\psi(y)$ be a formula in which $z,x$ do not occur freely. Then $$(\forall x,y) (\phi(x) \land \psi(y) \implies x < y) \vdash (\exists z)(\forall x,y)(\phi(x) \land \psi(y) \implies x \le z \le y)$$

(I have tried to modify the axiom, given in terms of a betweenness relation for points on a line, to refer to the order property of a number system instead, see here and here for the original axiom.)

That the real algebraic numbers serve as a model for the first-order axiom schema excluding free variables but do not serve as a model for the second-order axiom (they aren't because they aren't Dedekind complete whereas Tarski's second-order axiomatization of the reals is unique up to isomorphism) seems to imply that the answer to my original question in the title is affirmative. On the other hand, I know little of mathematical logic, and barely understand the difference between free and bound variable, so I am hardly certain either way. Also it would seem kind of strange to me that any real closed field serves as a model for the real number system as long as one puts some arbitrary-looking restriction involving free variables on the Dedekind-completeness axiom.

I don't know if it's relevant that "real number is computable if and only if there is a computable Dedekind cut converging to it" and that all algebraic numbers are computable (e.g. Babylonian method). In particular, the use of an algorithm might preclude the use of free variables. If so, that might explain why computable transcendentals like $e$ ($\sum_{k=1}^{\infty} \frac{1}{k!}$) and $\pi$ can be defined in terms of power series which do not (seem to) involve free variables without there being a contradiction.

Note: This is a follow up to my previous question.

Answer 1

The first-order theory of real-closed fields is complete, which means that any first-order statement which is true in one real-closed field is true in any other real-closed field. In particular, this applies to each instance of your axiom schema. Since your axiom schema is true for $\mathbb{R}$, it follows that it is also true in any real-closed field.

To provide some counter to your intuition that this seems too strong, the restriction (which you did not explicitly state) that $\phi(x)$ and $\psi(y)$ must be first-order formulas in the language of ordered fields is huge. The strength of the completeness of $\mathbb{R}$ in analysis comes from the fact that every cut has a point. For instance, if you want to prove basic properties of continuous functions, you need to be able to refer to cuts defined in terms of an arbitary continuous function, and such a cut will only very rarely have any connection to the first-order language of ordered fields.

As a concrete example, you can't define $e$ in any obvious way, since in order to do so you would probably want $\phi(x)$ to be something like "$x=\sum_{k=1}^n\frac{1}{k!}$ for some natural number $n$". You can't say this in the first-order language of ordered fields: you can't refer to an indexed sum like $\sum_{k=1}^n\frac{1}{k!}$, nor can you even refer to natural numbers (you can only refer to variables that are elements of your field).

(The restriction on free variables here is totally irrelevant to your concern and is a distraction from what's going on. The reason that you restrict $\phi(x)$ to not use $y$ and $z$ as free variables is to make sure that $\phi(x)$ is only a statement about $x$, not about $y$ and $z$. For instance, if $\phi(x)$ were the statement $x<y$ which involves both $x$ and $y$, then it would be trivial that $\phi(x)\wedge\psi(y)$ implies $x<y$, but this does not mean that $\phi$ and $\psi$ define a cut.)