My understand (from this question) is that we can construct a countable algebraic closure of $\mathbb{Q}$ without using the axiom of choice (i.e. we can construct $\overline{\mathbb{Q}} \subseteq \mathbb{C}$), although perhaps this oversimplifying thing.
What can we say about $\text{Gal}(\bar{\mathbb{Q}}/\mathbb{Q})$ without using the axiom of choice? I think the infinite Galois correspondence requires some form of choice, so maybe this the automorphism group of $\bar{\mathbb{Q}}$ doesn't deserve to be called a Galois group without choice. Can it be shown that it is uncountable? Or that it has more than $2$ elements?
Motivation: people often say that it is impossible to write down any non-trivial element of $\text{Gal}(\bar{\mathbb{Q}}/\mathbb{Q})$. If it is consistent with ZF that $\text{Gal}(\bar{\mathbb{Q}}/\mathbb{Q})$ has size $2$, then this would be a way to formalize that statement.
Best Answer
If $\overline{\mathbb{Q}}$ is a countable algebraic closure of $\mathbb{Q}$, the axiom of choice is hardly if ever needed to study $\text{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$. All of the usual arguments using the axiom of choice work without it, by just explicitly using an enumeration of $\overline{\mathbb{Q}}$ in place of the well-ordering that would be used via the axiom of choice. For instance, you can construct elements of $\text{Gal}(\overline{\mathbb{Q}}/\mathbb{Q})$ by one-by-one extending automorphisms of subfields of $\overline{\mathbb{Q}}$ which are finite and Galois over $\mathbb{Q}$ (no choice is ever needed since you have a well-ordering of $\overline{\mathbb{Q}}$ which you can use to make all your choices). The usual diagonalization argument goes through to show there are uncountably many such elements. Similarly, you can prove that any two countable algebraic closures of $\mathbb{Q}$ are isomorphic.
More generally, pretty much the same can be said for any algebraically closed field $K$ that is well-orderable. The only way the usual theory of algebraically closed fields (and more generally of infinite field extensions) uses the axiom of choice is to have a well-ordering on the field so that you can construct homomorphisms out of (and/or into) it by transfinite recursion. So, if you already know that such a well-ordering exists, you don't need the axiom of choice.