Basis of field extension of rational number that is closed square root without axiom of choice Consider a field extension $F$ of the rational numbers. $F$ contains all numbers that can be constructed using square root. In this field, there are the regular rational numbers such as 1, 2, 3, $\frac{42}{13}$, etc. There are square roots such as $\sqrt{2}$, $\sqrt{3}$, $\sqrt{\frac{42}{13}}$, etc. It does not* contain cubic roots, i.e., $\sqrt[3]{2}$, $\sqrt[3]{3}$, $\sqrt[3]{\frac{42}{13}}$. The square root can be applied iteratively. This means that $\sqrt[4]{3} = \sqrt{\sqrt{3}}$ is in the set. The square root operation can only be applied a finite number of times, i.e., constructions that involve the limit of $a_i=\sqrt{42+a_{i-1}}$ or similar sequences are not considered.
(*I assume that F does not contain cubic roots. If one can show that a cubic root can somehow be written as combination of square roots then F would contain cubic roots. This would be valuable information to me, if my assumption is wrong here.)
Can somebody provide a constructive (i.e. no axiom of choice) construction of a basis of this field as rational vector space? If $F$ has no basis without axiom of choice would also be an interesting result.
My objective is to perform exact geometric computations that involve length computations in a computer. These computations may be very slow. The idea is to represent the numbers of $F$ by storing the coefficients of this basis. This is the reason why I do not want to use the axiom of choice. I need to know how the basis actually looks like to be able to perform computations on it. A statement of the form "if you believe the axiom of choice, then the basis exists but nobody knows how it looks" is not helpful. That is not something one can implement in a computer.
 A: There are two fine points here.

*

*There is always a canonical, countable, field which is the smallest subfield of $\Bbb C$ closed under $\sqrt\cdot$. Since this field is countable, simply enumerate it, and recursively construct a basis. Done and done.


*It is consistent with $\sf ZF$ that there is a field which is a closure of $\Bbb Q$ under $\sqrt\cdot$, but it is not well-orderable. I'm not sure if this field doesn't have a basis, but that stands to reason to expect that it doesn't. If it does, though, this basis is certainly not well-orderable. So working with it from a computational point of view is ... odd, at best.
Since you're saying "this field", it seems that you have in mind the first option. To see that it is countable more explicitly, note that every polynomial of the form $x^2-p=0$ has at most two roots and there are countably many such polynomials; using the fact that $\Bbb C$ can be linearly ordered (as a set!), this is a countable union of pairs; this defines a canonical enumeration of the smallest field in which $\sqrt q$ exists for each rational $q$. Now repeat this, using said canonical enumeration to kickstart the next step in the recursion.
After going through all the finite steps of the recursion, you are left with a countable sequence of countable sets that are equipped with canonical enumerations, and therefore their union is indeed countable.
