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.)