Dedekind's theorem on a weakly Artinian integrally closed domain without Axiom of Choice Let $A$ be a commutative ring.
Let $f$ be any non-zero element of $A$.
Suppose that $A/fA$ has a composition series as an $A$-module.
Then we say $A$ is a weakly Artinian ring (this may not be a standard terminology).
Can we prove the following theorem without Axiom of Choice?
Theorem
Let $A$ be a weakly Artinian integrally closed domain.
Then the following assertions hold.
(1) Every ideal of $A$ is finitely generated.
(2) Every non-zero prime ideal is maximal.
(3) Every non-zero ideal of $A$ is invertible.
(4) Every non-zero ideal of $A$ has a unique factorization as a product of prime ideals.
EDIT
May I ask the reason for the downvotes?
Is this the reason?
EDIT
What's wrong with trying to prove it without using AC?
A proof without AC is constructive.
When you are looking for a computer algorithm for solving a mathematical problem, this type of a proof may provide a hint. At least, you can be sure that there is a constructive proof.
EDIT
why-worry-about-the-axiom-of-choice. 
 A: We assume tacitly the definitions in my answer to this question.
Definition 1
Let $A$ be a commutative ring.
Suppose $A$ has a composition series as an $A$-module.
Then we say $A$ is an Artinian ring.
Lemma 1
Let $A$ be an Artinian ring.
Let $I$ be an ideal of $A$.
Then $A/I$ is an Artinian ring.
Proof:
This follows from Lemma 2 of my answer to this question.
Lemma 2
An Artinian ring is weakly Artinian.
Proof:
This follows from Lemma 1.
Lemma 3
Let $A$ be a weakly Artinian ring.
Let $I$ be a non-zero ideal of A.
Then $A/I$ is Artinian.
Proof:
Since $I$ is non-zero, $I$ contains a non-zero element $f$.
Since $A/fA$ is Artinian, $A/I$ is Artinian by Lemma 1.
QED
Lemma 4
Let $A$ be a weakly Artinian ring.
Let $I$ be an ideal of $A$.
Then $A/I$ is a weakly Artinian ring.
Proof:
Clear.
Lemma 5
Let $A$ be a weakly Artinian ring.
Then every ideal of $A$ is finitely generated.
Proof:
Let $I$ be a non-zero ideal of $A$.
Let $f \in I$ be a non-zero element.
By Lemma 7 of my answer to this question, $I/fA$ is a finite $A$-module.
Since $fA$ is a finite $A$-module, $I$ is also a finite $A$-module.
QED
Lemma 6
Let $A$ be a (not necessarily commutative) ring.
Let $M$ be a left $A$-module.
Suppose that $M$ has a composition series.
Let $f:M \rightarrow M$ be an injective $A$-homomorphism.
Then $f$ is surjective.
Proof:
Since $f$ is injective, $leng$ $M = leng$ $f(M)$.
By Lemma 4 of my answer to this question, $f(M) = M$.
QED
Lemma 7
Let $A$ be an Artinian integral domain.
Then $A$ is a field.
Proof:
Let $a$ be a non-zero element of $A$.
Let $f: A \rightarrow A$ be the map defined by $f(x) = ax$.
Since $f$ is injective, it is surjective by Lemma 6.
Hence $a$ is invertible.
Hence $A$ is a field.
QED
Lemma 8
Let $A$ be an Artinian ring.
Let $P$ be a prime ideal of $A$.
Then $P$ is maximal.
Proof:
This follows immediately from Lemma 1 and Lemma 7.
Lemma 9
Let $A$ be a weakly Artinian ring.
Let $P$ be a non-zero prime ideal.
Then $P$ is maximal.
Proof:
By Lemma 3, $A/P$ is an Artinian ring.
Since $A/P$ is an integral domain, $A/P$ is a field by Lemma 7.
Hence $P$ is maximal.
QED
Lemma 10
Let $A$ be a (not necessarily commutative) ring.
Let $M$ be a left $A$-module.
Suppose that $M$ has a composition series.
Let $N$ be an $A$-submodule of $M$.
Then $leng$ $M = leng$ $N + leng$ $M/N$.
Proof:
By Lemma 2 of my answer to this question, $leng$ $M/N$ is finite.
By Lemma 3 of my answer to this question, $leng$ $N$ is finite.
Hence $leng$ $M = leng$ $N + leng$ $M/N$.
QED
Lemma 11
Let $A$ be a (not necessarily commutative) ring.
Let $M$ be a left $A$-module.
Let $N_0 \supset N_1 \supset ... \supset N_r$ be a descending sequence of $A$-submodules of $M$.
Suppose that $N_i \neq N_{i+1}$ for $i = 0, 1, ..., r - 1$.
Then $r \leq leng$ $M$.
Proof:
This follows from Lemma 10.
Lemma 12
Let $A$ be an Artinian ring.
Then Spec($A$) is finite.
Proof:
This follows from Lemma 2 of my answer to this question and Lemma 8 and  Lemma 11.
Lemma 13
Let $A$ be an Artinian ring.
By Lemma 12, Spec($A$) is finite.
Let Spec($A$) = {$P_1, ..., P_r$}.
Let $I = P_1 \cap ..., \cap P_r$.
Then $I$ is nilpotent.
Proof:
This follows from Lemma 8 and the proposition of my answer to this question.
Lemma 14
Let $A$ be a weakly Artinian ring.
Let $I$ be a non-zero proper ideal of $A$.
Then there exist maximal ideals $P_1, ..., P_r$ such that $P_1...P_r \subset I$.
Proof:
By Lemma 3, $A/I$ is Artinian.
By Lemma 13, Spec($A/I$) is finite.
Let Spec($A/I$) = {$Q_1, ..., Q_s$}.
Let $J = Q_1 \cap ... \cap Q_s$.
Since each $Q_i$ is maximal, $J = Q_1...Q_s$.
By Lemma 13, $J^k = 0$ for some integer $k \geq 1$.
Let $P_i$ be the inverse image of $Q_i$ by the canonical morphism $A \rightarrow A/I$.
Then $(P_1...P_s)^k \subset I$.
QED
Lemma 15
Let $A$ be a weakly Artinian integrally closed domain.
Then every non-zero prime ideal of $A$ is invertible.
Proof:
Let $P$ be a non-zero prime ideal of $A$.
We claim that $P^{-1} \neq A$.
Let $a \in P$ be non-zero.
By Lemma 14, there exist maximal ideals $P_1, ..., P_r$ such that $P_1...P_r \subset aA$.
Choose $r$ such that $r$ is minimal.
Since $P_1...P_r \subset P$, one of $P_i = P$.
Without loss of generality, we can assume $P_1 = P$.
By the minimality of r, $P_2...P_r$ is not contained in $aA$.
Hence there exits $b \in P_2...P_r$ such that $b$ is not contained in $aA$.
Since $bP \subset aA$, $ba^{-1}P \subset A$.
Hence $ba^{-1} \in P^{-1}$.
Since $ba^{-1}$ is not contained in $A$, $P^{-1} \neq A$.
Since $P$ is maximal and $P \subset PP^{-1} \subset A$, $P = PP^{-1}$ or $PP^{-1} = A$.
Suppose $P = PP^{-1}$.
Since $P$ is finitely generated by Lemma 5, every element of $P^{-1}$ is integral over $A$.
Since $A$ is integrally closed $P^{-1} \subset A$.
This is a contradiction.
QED
Lemma 16
Let $A$ be a weakly Artinian integrally closed domain.
Then every non-zero ideal is invertible.
Proof.
Let $\Lambda$ be the set of non-zero ideals which are not invertible.
Suppose $\Lambda$ is not empty.
By Lemma 5 of my answer to this question, there exists a maximal element $I$ in $\Lambda$.
Since $A \neq I$, by Lemma 5 of my answer to this question, there exists a maximal ideal $P$ such that $I \subset P$.
$I \subset IP^{-1} \subset II^{-1} \subset A$.
If $I = IP^{-1}$, since $P$ is finitely generated by Lemma 5, every element of $P^{-1}$ is integral over $A$.
Since $A$ is integrally closed, this cannot happen by the proof of Lemma 15.
Hence $I \neq IP^{-1}$.
Since $I$ is a maximal element in $\Lambda$, $IP^{-1}$ is invertible.
Hence $I$ is invertible.
This is a contradiction.
QED
Lemma 17
Let $A$ be a weakly Artinian integrally closed domain.
Then every non-zero ideal is a product of prime ideals.
Proof:
Let $\Lambda$ be the set of non-zero ideals which are not a product of prime ideals.
Suppose $\Lambda$ is not empty.
By Lemma 5 of my answer to this question, there exists a maximal element $I \in \Lambda$.
Since $I$ is not a maximal ideal, By Lemma 5 of my answer to this question, there exists a prime ideal $P$ such that $I \subset P$.
Then $IP^{-1} \subset A$ and $IP^{-1} \neq A$.
Suppose $I = IP^{-1}$. Since I is finitely generated by Lemma 5, every element of $P^{-1}$ is integral over $A$. Since $A$ is integrally closed, this cannot happen by the proof of Lemma 15. Hence $I \neq IP^{-1}$.
Since $I \subset IP^{-1}$, $IP^{-1}$ is a product of prime ideals.
Then $I$ is a product of prime ideals.
This is a contradiction.
QED
Proposition
Let $A$ be a weakly Artinian integrally closed domain.
Then every non-zero ideal has a unique factorization as a product of prime ideals.
Proof:
This follows immediately from Lemma 16 and Lemma 17.
