Dedekind's theorem on an integrally closed algebra over a commutative ring without Axiom of Choice Motivation
This question came from my efforts to solve this problem presented by Andre Weil in 1951.
Can we prove the following theorem without Axiom of Choice?
If the answer is affirmative, by using this, we can get many examples of Dedekind domains without using Axiom of Choice.
This is a related question.
Theorem
Let $A$ be a commutative ring.
Let $B$ be an integrally closed $A$-algebra.
Suppose $B/fB$ has a composition series as an $A$-module for every non-zero element $f$ of $B$.
Then the following assertions hold.
(1) Every ideal of $B$ is finitely generated.
(2) Every non-zero prime ideal of $B$ is maximal.
(3) Every non-zero ideal of $B$ is invertible.
(4) Every non-zero ideal of $B$ has a unique factorization as a product of prime ideals.
EDIT
Why worry about the axiom of choice?
 A: We use the definitions of my answer to this question.
Definition 1
Let $A$ be a commutative ring.
Let $B$ be a commutative $A$-algebra.
Suppose $leng_A B$ is finite.
Then we say $B$ is an Artinian $A$-algebra.
Lemma 1
Let $A$ be a commutative ring.
Let $B$ be an Artinian $A$-algebra.
Let $\Lambda$ be nonempty set of ideals of $B$.
Then there exist a maximal element and a minimal element in $\Lambda$.
Proof:
We note that every ideal of $B$ can be regarded canonically as an A-module.
Let $r = sup$ {$leng_A I; I \in \Lambda$}.
Since $r$ is finite, there exists $I \in \Lambda$ such that $r = leng$ $I$.
By Lemma 4 of my answer to this, $I$ is a maximal element of $\Lambda$.
The existence of a minimal element is proved similarly.
QED
Lemma 2
Let $A$ be a commutative ring.
Let $B$ be an Artinian $A$-algebra.
Then $leng_B B$ is finite, namely $B$ is an Artinian ring as defined in Definition 1 in this.
Proof:
Let $\Lambda$ be the set of ideals $I$ of $B$ such that $leng_B I$ is finite.
Since $0 \in \Lambda$, $\Lambda$ is not empty.
By Lemma 1, there exists a maximal element $I \in \Lambda$.
Suppose $I \neq B$.
Then, by Lemma 1, there exists an ideal $J$ of $B$ such that $I \subset J$ and $J/I$ is a simple $B$-module.
Since $leng_B J = leng_B I + 1$, $J \in \Lambda$.
This is a contradiction.
Hence $B = I$.
QED
Definition 2
Let $A$ be a commutative ring.
Let $B$ be a commutative $A$-algebra.
Suppose $leng_A B/fB$ is finite of for every non-zero element $f \in B$.
Then we say $B$ is a weakly Artinian $A$-algebra.
By Lemma 2, $B$ is a weakly Artinian ring.
Proof of the title theorem
By Lemma 2, $B$ is a weakly Artinian ring.
Hence the assertions of the title theorem follow immediately from Lemma 2 and this.
QED
