Main Question:


Does ZF (no axiom of choice) prove that every Principal Ideal Domain is a Unique Factorization Domain?


The proofs I've seen all use dependent choice.


Minor Questions:


Does ZF + Countable Choice prove all PIDs are UFDs?


Does ZF prove "If all PIDs are UFDs, then [some choice principle]"?


(If anyone knows how I could force line breaks to put the questions on their own lines, please tell me.)



Does ZF prove that all PIDs are UFDs?
ZF alone does not prove that every PID is a UFD, according to [this paper](http://journals.cambridge.org/action/displayAbstract?aid=2076124): Hodges, Wilfrid. *Läuchli's algebraic closure of $Q$.* Math. Proc. Cambridge Philos. Soc. 79 (1976), no. 2, 289--297. [MR 422022](http://www.ams.org/mathscinet-getitem?mr=422022).


One result in this paper is the following:
> COROLLARY 10. Neither (a) nor (b) is provable from ZF alone:  
> 
> (a) Every principal ideal domain is a unique factorization domain.  
> 
> (b) Every principal ideal domain has a maximal ideal.

 


By the way, I didn't know the answer to this question until today. To find the answer, I consulted Howard and Rubin's book *Consequences of the Axiom of Choice*. (Actually, I did a search for "principal ideal domain" of their book using [Google Books](http://books.google.co.uk/books?id=YXaVkHPQED4C&lpg=PP1&pg=PP1#v=onepage&q&f=false).)


