Qiaochu, using the link I provided in my answer to this question, you find that this question is still open (or was, as of the mid 2000s, and I haven't heard of any recent results in this direction).
(According to the site's notation, the existence of algebraic closures is form 69, the ultrafilter theorem is form 14, uniqueness of the algebraic closure (in case they exist) is form 233; these numbers can be found by entering appropriate phrases in the last entry form in the page linked to above.)
It is known that uniqueness implies neither existence nor the ultrafilter theorem.
It is open whether existence implies uniqueness or the ultrafilter theorem, and also whether (existence and uniqueness) implies the ultrafilter theorem.
(Enter 14, 69, 233 in Table 1 in the link above for these implications/non-implications.)
Jech's book on the axiom of choice should provide the proofs of the known implications and references, and the book by Howard-Rubin (besides updates past the publication date of Jech's book) provides references for the known non-implications.
Here are some details on Banaschewski's paper:
1.
First, lets see that the ultrafilter theorem can be used to prove uniqueness of algebraic closures, in case they exist.
Let $K$ be a field, and let $E$ and $F$ be algebraic closures. We need to show that there is an isomorphism from $E$ onto $F$ fixing $K$ (pointwise).
Following Banaschewski, denote by $E_u$ (resp., $F_u$) the splitting field of $u\in K[x]$ inside $E$ (resp., $F$); we are not requiring that $u$ be irreducible. We then have that if $u|v$ then $E_u\subseteq E_v$ and $F_u\subseteq F_v$. Also, since $E$ is an algebraic closure of $K$, we have $E=\bigcup_u E_u$, and similarly for $F$.
Denote by $H_u$ the set of all isomorphisms from $E_u$ onto $F_u$ that fix $K$; it is standard that $H_u$ is finite and non-empty (no choice is needed here). If $u|v$, let $\varphi_{uv}:H_v\to H_u$ denote the restriction map; these maps are onto.
Now set $H=\prod_{u\in K[x]} H_u$ and for $v|w$, let
$$ H_{vw}=\{(h_u)\in H\mid h_v=h_w\upharpoonright E_v\}. $$
Then the Ultrafilter theorem ensures that $H$ and the sets $H_{vw}$ are non-empty. This is because, in fact, Tychonoff for compact Hausdorff spaces follows from the Ultrafilter theorem, see for example the exercises in Chapter 2 of Jech's "The axiom of choice." Also, the sets $H_{vw}$ have the finite intersection property. They are closed in the product topology of $H$, where each $H_u$ is discrete.
It then follows that the intersection of the $H_{vw}$ is non-empty. But each $(h_u)$ in this intersection determines a unique embedding $h:\bigcup_uE_u\to\bigcup_u F_u$, i.e., $h:E\to F$, which is onto and fixes $K$.
2.
Existence follows from modifying Artin's classical proof.
For each monic $u\in K[x]$ of degree $n\ge 2$, consider $n$ "indeterminates" $z_{u,1},\dots,z_{u,n}$ (distinct from each other, and for different values of $u$), let $Z$ be the set of all these indeterminates, and consider the polynomial ring $K[Z]$.
Let $J$ be the ideal generated by all polynomials of the form
$$ a_{n-k}-(-1)^k\sum_{i_1\lt\dots\lt i_k}z_{u,i_1}\dots z_{u,i_k} $$
for all $u=a_0+a_1x+\dots+a_{n-1}x^{n-1}+x^n$ and all $k$ with $1\le k\le n$.
The point is that any polynomial has a splitting field over $K$, and so for any finitely many polynomials there is a (finite) extension of $K$ where all admit zeroes. From this it follows by classical (and choice-free) arguments that $J$ is a proper ideal.
We can then invoke the ultrafilter theorem, and let $P$ be any prime ideal extending $J$. Then $K[Z]/P$ is an integral domain. Its field of quotients $\hat K$ is an extension of $K$, and we can verify that in fact, it is an algebraic closure. This requires to note that, obviously, $\hat K/K$ is algebraic, and that, by definition of $J$, every non-constant polynomial in $K[x]$ split into linear factors in $\hat K$. But this suffices to ensure that $\hat K$ is algebraically closed by classical arguments (see for example Theorem 8.1 in Garling's "A course in Galois theory").
3.
The paper closes with an observation that is worth making: It follows from the ultrafilter theorem, and it is strictly weaker than it, that countable unions of finite sets are countable. This suffices to prove uniqueness of algebraic closures of countable fields, in particular, to prove the uniqueness of $\bar{\mathbb Q}$.
I think Hahn-Banach can be eliminated from the usual proof, but
being a non-expert in set theory, I cannot guarantee that the proof
is completely independent of the axiom of choice.
Here is a sketch of a basic calculus proof. A function $U\to B$
from a region $U\subset C$ to a Banach space $B$ is called analytic if
every point has a neighborhood where it is represented by a
convergent Taylor series.
You can prove a weak form of Cauchy theorem which says that if a function
is analytic in
$| z | < R \leq \infty$
then its Taylor series
has radius of convergence at least $R$. It seems that this does not
use the axiom of choice.
Then you prove that Cauchy inequalities hold (there is a simple algebraic
proof of this, see my answer to Liouville's theorem with your bare hands), and derive the Liouville theorem for Banach-space-valued
functions.
Then again it is an elementary fact that if $a-\lambda_0 1$ has
has a bounded inverse then the resolvent is an analytic function (in the sense I defined above) in
a neighborhood of $\lambda_0$. Then you show that if the resolvent exists everywhere
then it tends to $0$ as $\lambda\to\infty$. Then it seems to me that you obtain a proof
without Hahn-Banach by applying the Liouville theorem to the resolvent.
Sorry if I missed something...
EDIT. The weak form of Cauchy's theorem that I mentioned uses only elementary manipulation with absolutely convergent series, no integral is involved, see
Liouville's theorem with your bare hands.
Best Answer
The ultrafilter theorem is the statement that any filter on a set can be extended to an ultrafilter. It is perhaps more common to see it sated as the (Boolean) Prime ideal theorem: Every Boolean algebra admits a prime ideal.
The Hahn-Banach theorem is actually equivalent to the statement that every Boolean algebra admits a real-valued measure, but this is not entirely straightforward (see Luxemburg, "Reduced powers of the real number system and equivalents of the Hahn-Banach extension theorem", Intern. Symp. on the applications of model theory, (1969) 123-127).
For a discussion of Hahn-Banach vs. Choice and some additional remarks and references, see Jech "The axiom of choice", North-Holland, 1973.
You may also be interested in the references I include in this answer.