Can we prove that the ring of formal power series over a noetherian ring is noetherian without axiom of choice? Let $A$ be a commutative ring with an identity.
Suppose that every non-empty set of ideals of $A$ has a maximal element.
Let $A[[x]]$ be the formal power series ring over $A$.
Can we prove that every non-empty set of ideals of $A[[x]]$ has a maximal element without Axiom of Choice?
Remark
The same question was asked in MSE.
 A: I believe that the answer is yes.
Let $A$ be a commutative ring with $1$, such that any non-empty set of ideals has a maximal element.  For each ideal $I\leq A[[x]]$, and each $n\in \mathbb{N}$, define $I^{(n)}$ to be the set
$$\{0\}\cup\{a\in A\ :\ a\text{ is the leading non-zero coefficient, in degree $n$, of some }f\in A[[x]]\}.$$
This is an ideal of $A$.  Also define $I^{(\omega)}=\bigcup_{n\in \mathbb{N}}I^{(n)}$, which is also an ideal of $A$.
Now suppose $\{I_{\alpha}\}_{\alpha}$ is a set of ideals in $A[[x]]$.  The set of ideals $\{I_{\alpha}^{(\omega)}\}_{\alpha}$ has a maximal element, say $I^{(\omega)}_{\beta}$.  Further, it isn't hard to prove that the form of the noetherian hypothesis we are assuming implies finite generation of ideals (provable in ZF).  Thus, we may fix a generating set $a_1,a_2,\ldots, a_k$ for $I^{(\omega)}_{\beta}$.  This means that $I^{(\omega)}_{\beta}=I^{(n)}_{\beta}$ for some $n\in \mathbb{N}$, which we also fix.  (For instance, we can take the integer $n$ to be the lowest degree where each of $a_1,a_2,\ldots, a_k$ occurs as a leading coefficient.)
Now, restrict the set of $\alpha$ to only those for which $I_{\alpha}^{(n)}=I_{\beta}^{(n)}$.  (Note that if $I_{\alpha}^{(n)}\neq I_{\beta}^{(n)}$, then $I_{\alpha}$ does not contain $I_{\beta}$.  So this restriction costs us nothing.)  Next, we may as well also assume $\beta$ is chosen such that $I_{\beta}^{(n-1)}$ is a maximal element of $\{I_{\alpha}^{(n-1)}\}_{\alpha}$.  We then may assume $I_{\beta}^{(n-2)}$ is maximal in $\{I_{\alpha}^{(n-2)}\}_{\alpha}$, after restricting $\alpha$ again.  Recursively repeating this process (only finitely many times), the resulting $\beta$ is such that $I_{\beta}$ is maximal in $\{I_{\alpha}\}_{\alpha}$.
