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 dependant choice. Minor Questions: Does ZF + Countable Choice prove all PIDs are UFDs? Does ZF prove "If all PIDs are UFDs, then [some choice principle]"?