The field of algebraic numbers as a recursive structure

The field of algebraic numbers is a recursive structure. I give a brief sketch of the (ingredients of the) proof:

1. You can code each real algebraic number as a one-variable polynomial $p$ and a pair of rationals $l < u$ such that $p$ has exactly one root in the interval $[l,u]$.

2. The set of codes for one-variable polynomials with coefficients in $\mathbb{Q}$ is recursively enumerable by a standard argument, so you can encode the data $(p,l,u)$ recursively in a single natural number, and decode it into a triple of natural numbers.

3. By Sturm's theorem (Theorem 2.50 of R1) we can decide recursively which triples of natural numbers $(p,l,u)$ are valid representations of algebraic numbers in the sense that the polynomial represented by $p$ has exactly one root in $[l,u]$.

4. Using standard results on resultants (see R2) and separation bounds on roots of polynomials, we can obtain the following: given $(p_1,l_1,u_1)$ representing the algebraic number $\alpha$ and $(p_2,l_2,u_2)$ representing $\beta$, one can recursive derive some representation $(p,l,u)$ of $\alpha + \beta$ and similarly for $\alpha\beta$, and recursively decide whether $\alpha = \beta$ or not.

5. Now, using bullet point 3, we can fix an enumeration $E$ of all triples of natural numbers that represent algebraic numbers in the sense of bullet point 1. Using the equality test from bullet point 4, we can assume that $E$ is irredundant, in the sense that for each algebraic number $\alpha$ there is a unique $n$ such $E(n)$ represents $\alpha$.

6. Consider two algebraic numbers $(p_1,l_1,u_1)=E(n_\alpha)$ and $(p_2,l_2,u_2)=E(n_\beta)$ representing $\alpha$ and $\beta$ respectively. Using bullet point 4, we can recursively obtain some triple $(p,l,u)$ that represents $\alpha + \beta$. Define $n_\alpha \oplus n_\beta$ as "the least $n$ such that $E(n)$ represents the same number as $(p,l,u)$". This is a recursive definition. Similarly for $\odot$. Choose $c_1$ and $c_0$ appropriately.

7. It's immediate that $(\mathbb{N},\oplus,\odot,c_0,c_1)$ forms a field isomorphic to the field of real algebraic numbers. Since the real and imaginary parts of an algebraic number are themselves algebraic, it's easy to obtain the field of algebraic numbers at this point.

The best resources for the nitty-gritty details: Cyril Cohen's thesis (R2), which has a careful proof on the equality of algebraic Cauchy reals being decidable, and a computer-verified implementation of exact arithmetic with algebraic numbers; and the book Algorithms in Real Algebraic Geometry.

---

R1: Basu, Pollack, Roy: Algorithms in Real Algebraic Geometry

R2: Cohen: Formalization of real algebraic numbers