No, you shouldn't need any choice for this, and it should still be true if you replace $\overline{\mathbb{Q}}$ with any other algebraic closure of $\mathbb{Q}$. Let $K$ be a field (which in our application will be $\overline{\mathbb{Q}}$) and let $G$ be a finite group of automorphisms of $K$. Then $K/K^G$ is always a degree $\#(G)$ extension. (See EG [Milne][1] Corollary 2.14 and Theorem 3.4.) The [Artin-Schreier][2] theorem says that $K/F$ is a finite degree extension and $K$ is algebraically closed, then $[K:F] \leq 2$. Combining the two statements, if $G$ is a finite subgroup of $\text{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$, then $\#(G) \leq 2$. There is no use of choice in the proof of either of the big tools that I'm using. [1]: https://www.jmilne.org/math/CourseNotes/FT.pdf [2]: https://kconrad.math.uconn.edu/blurbs/galoistheory/artinschreier.pdf