lo.logic - When can we prove constructively that a ring with unity has a maximal ideal?

I suspect that the most general reasonable answer is a ring endowed with a constructive replacement for what the axiom of choice would have given you.

How do you show in practice that a ring is Noetherian? Either explicitly or implicitly, you find an ordinal height for its ideals. Once you do that, an ideal of least height is a maximal ideal. This suffices to show fairly directly that any number field ring has a maximal ideal: The norms of elements serve as a Noetherian height.

The Nullstellensatz implies that any finitely generated ring over a field is constructively Noetherian in this sense.

Any Euclidean domain is also constructively Noetherian, I think. A Euclidean norm is an ordinal height, but not at first glance one with the property that $a|b$ implies that $h(a) le h(b)$ (with equality only when $a$ and $b$ are associates). However, you can make a new Euclidean height $h'(a)$ of $a$, defined as the minimum of $h(b)$ for all non-zero multiples $b$ of $a$. I think that this gives you a Noetherian height.

I'm not sure that a principal ideal domain is by itself a constructive structure, but again, usually there is an argument based on ordinals that it is a PID.

• Next fundamental astronomy - Calculating azimuth from equatorial coordinates
• Previous universe - Is time itself speeding up universally?