Edit. This solution is incorrect. As François pointed out in the comments, the ring $B$ I construct is definitely not a domain; indeed, no nontrivial Boolean ring is a domain. But Martin asked me not to delete it, so I am leaving it here.
The idea was to take the tree $T$ through which a branch is desired and turn it into a ring, so that the lack of a branch would mean that every ideal is principal. One way to turn any partial order into a ring is to look at the regular open algebra, the completion as a Boolean algebra, and then look upon the Boolean algebra as a Boolean ring.
I can prove a lower bound, showing that the statement implies at least a weakened version of DC.
The principle of Dependent Choice is the assertion that if $R$ is a binary relation on a set $X$ and every $x\in X$ has some $y$ with $x\mathrel{R}y$, then there is an infinite sequence $x_0,x_1,\ldots $ with $x_n\mathrel{R} x_{n+1}$. Thus, DC asserts that one can make countably many choices in succession.
Consider the weakened principle, call is DC-fin, where we make the conclusion of DC, but only for relations $R$ that are finitely-branching, so that every $x$ is $R$-related to at least one but at most finitely many $y$. This principle is closely related to Konig's Lemma, and is not provable in ZF, since it implies countable choice for finite sets, which is known not to be provable in ZF.
Theorem. If every PID is factorial, then DC-fin holds.
Proof. Suppose that $R$ is a finitely branching relation having no infinite choice sequence. Let $T$ be the tree of all finite choice sequences. Thus, $T$ is a finitely branching tree, with no leaves, but $T$ has no infinite branch. (Weird, yes, but this is the world where choice fails.) Note that every node in $T$ has incompatible extensions, since otherwise there would be an isolated branch in $T$, which would give a choice sequence for $R$.
There is a natural topology on the tree $T$, generated by the lower cones. That is, view $T$ as growing downwards, and use as the basic open sets the sets $U_t$ of all extensions of $t$ in $T$, for any $t\in T$. Let $B$ be the set of regular open subsets of $T$ (regular open = interior of its closure). This is a (complete) Boolean algebra, and is the completion of $T$ as a Boolean algebra (used commonly in forcing).
In particular, $B$ is a Boolean ring. The Boolean operations can be used to define the ring operations by $a\cdot b=a\wedge b$ and $a+b=a\triangle b$, the symmetric difference, and the concepts of ideal and filter translate from ring theory to the Boolean algebra context this way. The only unit in $B$ is $1$, which corresponds to the root of $T$. There are no irreducible elements of $B$, since it is non-atomic: if $a\neq 1$, then $\neg a$ is a nonzero element, which has incompatible nonzero elements $p,q\lt\neg a$, and so $a=(a\vee p)\cdot(a\vee q)$ is a nontrivial factorization.
But now, I argue under our assumption on $R$ that $B$ is a PID [Edit. This is wrong because it is not a domain]. Suppose that $I$ is an nonprincipal ideal in $B$. Let $F$ be the dual filter, which is therefore also not principal. So $1\in F$. Since the root $1$ is the join in $B$ of its immediate successors in $T$, it follows one and exactly one of them $x_0$ must be in $F$. Since $x_0$ is the join of its finitely many $R$-successors, again we get exactly one of these successors $x_1$ must be in $F$. And so on. The point is that the filter $F$ chooses exactly one successor at each level of the tree, and so defines a choice sequence through $R$. (Note, the filter cannot choose two different successors, since these are incompatible and hence meet to $0$ and so cannot both be in the filter, and it must choose something, or else $I$ is principal.) Since there is no such choice sequence, it must be that $F$ and hence $I$ is principal, and so $B$ is a PID that is not factorial. QED
The finite-branching assumption on $R$ was used in arguing that when an element of the tree is in $F$, then one of its successors is in $F$. I don't see how to make this part of the argument work if there are infinitely many $R$ successors.
I believe that the principle DC-fin, which is a special case of Konig's lemma, is strictly weaker than DC.
It appears that the solutions in the other direction (at the other question) really use DC and not just DC-fin. (Although if one has factorizations for every element, then part of the argument involves choosing among the finitely many factors, and this would seems to just use DC-fin. But choice arises in the other part of the argument, where one must choose the factorizations in the first place.)
If one could somehow improve those arguments to need to make only choices from finite sets, then one would get that the statement is equivalent to DC-fin.
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.
Best Answer
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}$.