Main Question: Does
Does ZF (no axiom of choice) prove that every Principal Ideal Domain is a Unique Factorization Domain?
The proofs I've seen all use dependantdependent choice.
Minor Questions: Does
Does ZF + Countable Choice prove all PIDs are UFDs? Does
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.)