Constructive proof of existence of maximal ideal

Question

Let $R$ be a unital commutative ring. We know that the existence of a maximal ideal of any such $R$ is equivalent to the axiom of choice.

My question is, for what kind of $R$ is there a constructive proof that$R$ has a maximal ideal?

Answer 1

This problem is very hard, even for rings that we can list the elements effectively. For example, in $\mathbb Q[X]$, such a proof as you require will give a algorithm capable of calculating the factorization of every rational polynomial.

Answer 2

It is possible to give a different answer using results from Reverse Mathematics. In Reverse Mathematics there is a classification of theorems expressed in a countable language in proof systems of different strengths. The main ones are: $RCA_{0} < WKL_{0} < ACA_{0}$.

In $RCA_{0}$ it is possible to provide (essentially constructive) definitions (for example of Countable Commutative Rings and Ideals), and of elementary lemmas, but $RCA_{0}$ is usually not powerful enough to prove corresponding major theorems.

The following theorem, is provable in Reverse Mathematics (description from "Subsystems of Second Order Arithmetic", S.Simpson, 2010).

Theorem III.5.4. $ACA_{0}$ proves that every countable commutative ring has a maximal ideal.

This means, in effect, that "constructing" such a maximal ideal - in the general countable commutative ring case - would require solving the Halting problem.