Proving existence of $\overline{\Bbb Q_p}$ without AC The proof that every field has an algebraic closure is known to require at least a weak form of AC, the boolean prime ideal theorem. But I recall reading somewhere that for concrete, sufficiently small (say, countable) fields, it is not necessary to invoke choice. Now $\Bbb Q_p$ is not countable, but $2^{\aleph_0}$ is at least manageably small and I'm told that $\overline{\Bbb Q_p}$ should be no larger than this, so perhaps it is possible to show the existence of an algebraically closed field extension to $\Bbb Q_p$.
On a related note, is it possible to define the algebraically closed field extension to $\Bbb Q_p$? That is, is there some definable class and operations that form an appropriate extension of $\Bbb Q_p$? The usual (ZFC) proof shows that there exists a field extension, but this extension is not defined uniquely in the set-theoretic sense but is only unique up to some isomorphism fixed on $\Bbb Q_p$. But perhaps it is possible to collect all these extensions up into a set and work with the equivalence classes instead to get a single object that acts like an extension.
Note that you don't need proper classes or unbounded cardinalities in the above because when extending a field $F$ you can work within the "universe" $\Bbb N\times F^{<\omega}$ since every algebraic extension should have all its elements algebraic over $F$ and hence be of the form "root $k$ of the polynomial $\sum_n^da_nx^n$" where $k\in\Bbb N$ and $(a_1,\dots,a_d)\in F^{<\omega}$.
 A: user8268 has supplied the proof (in Algebraic Number Theory, Remark 7.65) that there are finitely many extensions $(K_{n,i}/\Bbb Q_p)_{i=1,\dots,d_n}$ with degree $n$. From this, you can prove the existence of $\overline{\Bbb Q_p}$: Consider the subset relation on finite extensions of $\Bbb Q_p$. This is a directed set, because we can take the union of two finite extensions to get another finite extension. Then the union of all extensions of a given degree $K_n=\bigcup_iK_{n,i}$ is also a finite extension, which contains all roots of $n$-degree polynomials over $\Bbb Q_p$, and $\bigcup_nK_n:=\overline{\Bbb Q_p}$ then contains all roots of polynomials over $\Bbb Q_p$ (and I believe that a theorem then gives that it must also contain roots of polynomials over $\overline{\Bbb Q_p}$.)
This relies on $K_{n,i}$ being a definable set, or at least $\{K_{n,i}:i=1,\dots,d_n\}$ being a definable finite set. Otherwise you need countable choice to finish this one.
But now let's analyze the proof of Remark 7.65 (A local field $K$ of characteristic 0, such as $\Bbb Q_p$ or its finite extensions, has finitely many extensions of degree $n$.) The statement follows from


*

*(Example 7.54) There is a unique unramified extension $K_m$ of $K$ for any $m$, and this extension is definable as $K(\sigma)$ where $\sigma$ is the Frobenius element defined by $\sigma\beta\equiv\beta^q\pmod{\frak p}$ for all $\beta\in B$, the discrete valuation ring in $K_n$, where $\frak p$ is the nonzero prime ideal in $B$. (Not sure I understand all that, but I'll take it as given for now.)

*(Proposition 7.61, Krasner's lemma) If $f\in K[X]$ is a monic irreducible polynomial, then for any monic $g$ sufficiently close to $f$ any root $\beta$ of $g$ is close to some root $\alpha$ of $f$, and for that root $K(\alpha)=K(\beta)$.

*(Proposition 7.64) The space $(a_1,\dots,a_n)\in{\frak p\times p}\times\dots\times A^\times\pi$ (where $A$ is the ring of integers in $K$) generates the coefficients of the Eisenstein polynomials $X^n+a_1X^{n-1}+\dots+a_n$, which together generate all the totally ramified extensions of $K$.

*(Proposition 7.46) The space $A$ ($\supseteq A^\times,\frak p$) is compact because it is complete and totally bounded.

*Every extension factors into an unramified extension and a totally ramified extension.


We want to make these statements more constructive in order to extract a definable set of candidate extensions. Now (1) is already definable, and (2) does not involve choice but invokes the existence of a neighborhood of $f$. (4) is a straight application of generalized Heine-Borel and thus involves countable choice, but if we carefully trace the linkage from (4) to (3) to (2) we can eliminate the compactness argument.

Define $T_m=\{\sum_{i=0}^ms_i\pi^i:s_0,\dots,s_m\in S\}^n\cap V$, where $V={\frak p\times p}\times\dots\times A^\times\pi$. This is the $\epsilon$-net (for $\epsilon_m=|\pi^{m+1}|$) used in the proof of Proposition 7.46, except here it is in an $n$-fold cartesian product and restricted to the subset $V\subseteq A^n$ of interest. For the same reasons as detailed there, this is a  $\epsilon_m$-net of $V$ in the supremum norm. Furthermore, $T_m\subseteq T_{m+1}$ for each $m$. Now each $x\in V$ is associated with a neighborhood $U_x$ of all functions that are close enough to $X^n+a_0X^{n-1}+\dots+a_n$ to satisfy the conditions of (2).
Now we can mirror the proof of compactness of a closed interval in $\Bbb R$. Suppose $V$ is not compact (w.r.t the $U_x$ collection). Then one of the $T_0$ balls is not compact, and one of the $T_1$ balls inside that ball is not compact, and so on. There is a simple definable order on $T_m$ given an order on $S$ (which we can fix once and for all), so we can pick the first one in each case to get a sequence of points that converges to a constant sequence at some $y$ and thus $y$ is a point in one of the $T_m$ sets, which is a contradiction since it is covered by $U_y$. Therefore there is a finite subcovering of $\{U_x\}_x$ that covers $V$, and we can reduce this to say that for some $m$, $B(\epsilon_m,x)\subseteq U_x$ for each $x\in T_m$.
Thus there is a smallest such $m$, and we can define the set $\{K_{n,i}\}_i$ to be the set of all extensions $K(\sigma_d)(e_{x,k})$ where $d\mid n$, $\sigma_d$ is the Frobenius element for $K_d$ as defined in (1), and $e_{x,k}$ is the $k$-th root of the Eisenstein polynomial defined by $x\in T_m$ for that smallest $m$ (using $n/d$ instead of $n$ in the definition of $T_m$). (Do all of the roots need to be added? I feel like they would all be isomorphic assuming the root is not already in the field.)
This yields a definable $K_n$ field (from the first paragraph), and thus a definable field that is isomorphic to $\overline{\Bbb Q_p}$.
