show/hide this revision's text 2 grammar

This is an answer to your parenthetical question:

Is there a first-order logic formula that is equivalent to UFD always, no matter whether the ring is Noetherian or not?

No. In fact, if T is any extension of the first-order theory of integral domains such that every model of T is a UFD, then every model of T is a field.

I think this is well known, but I couldn't think of a reference. I'll sketch a quick proof. First, let Let φn(x) be the standard first-order formula which says that x is a product of n irreducible elements (and φ0(x) says that x is a unit). We argue that for some fixed n,

T ⊦ ∀x (x ≠ 0 → φ0(x) ∨ ... ∨ φn(x)).

If not, by the Compactness Theorem, T has a model R with a distinguished nonzero element x such that R ⊧ ¬φn(x) for each n; so x does not have a factorization into irreducibles. To conclude, just show that every UFD which satisfies ∀x (x ≠ 0 → φ0(x) ∨ ... ∨ φn(x)) for some n must be a field.
show/hide this revision's text 1

This is an answer to your parenthetical question:

Is there a first-order logic formula that is equivalent to UFD always, no matter whether the ring is Noetherian or not?

No. In fact, if T is any extension of the first-order theory of domains such that every model of T is a UFD, then every model of T is a field.

I think this is well known, but I couldn't think of a reference. I'll sketch a quick proof. First, let φn(x) be the standard first-order formula which says that x is a product of n irreducible elements (and φ0(x) says that x is a unit). We argue that for some fixed n,

T ⊦ ∀x (x ≠ 0 → φ0(x) ∨ ... ∨ φn(x)).

If not, by the Compactness Theorem, T has a model R with a distinguished nonzero element x such that R ⊧ ¬φn(x) for each n; so x does not have a factorization into irreducibles. To conclude, just show that every UFD which satisfies ∀x (x ≠ 0 → φ0(x) ∨ ... ∨ φn(x)) for some n must be a field.