Is Dependent Choice equivalent to the statement that every PID is factorial?

In this question, it was asked if AC is needed in the proof of the well-known fact that every principal ideal domain is factorial. As KConrad and Joel David Hamkins have pointed out, only DC, the axiom of dependent choice, is needed, and in the comment box the question was raised if the statement is actually equivalent to DC. But this was not answered so far.

So I ask it here, is the statement equivalent to DC? It would not surprise me since there are already many algebraic equivalents of AC (existence of vector bases, existence of maximal ideals). Also note that the requirement of ideals being principal is somewhat analoguous to the assumption of entireness of the relation in DC, and the representation as a product of irreducibles is somewhat analoguous to the conclusion of DC.

If the statements turns out to be weaker, I would be also interested in a proof which is the set-theoretical equivalent (perhaps it's DC-fin as in Joel's answer?).

PS: Of course, this question takes place in ZF ;).

-
I suggest the set-theory tag and possibly also axiom-of-choice. – Joel David Hamkins Sep 24 '10 at 17:35

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.

-
But $B$ is not a domain. – François G. Dorais Sep 24 '10 at 20:51
François, you are completely right! My solution attempt appears to be fundamentally flawed. I'll delete it, but perhaps leave it up leave it up for a day or so, in case anyone has some insightful remarks. – Joel David Hamkins Sep 24 '10 at 22:11
Please don't delete it. Just mention Francois' comment in your answer. Perhaps the ideas can be used. – Martin Brandenburg Sep 25 '10 at 8:54
DC-fin is more commonly known as König's lemma: en.wikipedia.org/wiki/K%C3%B6nig%27s_lemma – Colin Reid Sep 25 '10 at 10:02
Colin, yes, of course they are equivalent. – Joel David Hamkins Sep 25 '10 at 10:14