I was working on proving the following classic result for non-zero commutative rings in constructive logic:

$I \subseteq R$ is a maximal ideal iff $R / I$ is a field.

The definition of maximal ideals that I started with was the following:

$I$ is maximal if for any other ideal $J \supseteq I$ we have either $J \subseteq I$ or $J = R$.

And regarding fields I used the following:

A non-zero commutative ring $S$ is a field iff for every element $x \in S$ either $x = 0$ or $x$ has an inverse.

But when trying to proof their equivalence I hit some roadblocks. I have given the details below, but to summarise, it seems that to make the equivalence work constructively, the definitions can be changed in at least two different ways. The following will work:

(1.1) $I \subseteq R$ is maximal if for any ideal $J \supseteq I$ with $\exists x \in J : \, x \notin I$ we have $J = R$.

(1.2) $S$ is a field if for any $x \in S$ we have $x \neq 0$ implies that $x$ is invertible.

or alternatively:

(2.1) $I \subseteq R$ is maximal if for any $x \in R$ either $x \in I$ or $1 \in I + (x)$.

(2.2) $S$ in a field if for any $x \in S$ either $x = 0$ or $x$ has an inverse.

So in either case one of the definitions has to be altered. This leaves me with two questions:

  • Is this what really happens when we consider maximal ideals constructively? Or is one of the two a property that has a different name?
  • Which one of the two definitions is the right constructive notion for field?

Here are the details on one of the proofs, which motivates the changes in the definition. I will present the proof as done in classical logic, and then discuss what to change in order to make it work constructively.

Proof. $(\Leftarrow)$ Assume that $R / I$ is a field and let $J \supseteq I$ be an ideal. We need to show that either $J \subseteq I$ or $J = R$. Make use of $A \lor B \iff \neg A \to B$ which allows us to furthermore assume $\neg J \subseteq I$ with the goal to prove $J = R$. Note that we have: $$ \neg J \subseteq I \iff \neg (\forall x: \; x \in J \to x \in I) \iff \exists x \in J : x \notin I $$ So let $x$ be the element given by this existence and let $\overline x$ be its remainder in $R / I$. Since $x \notin I$ we must have $\overline x \neq 0$, so we conclude that it has in inverse $\overline y \in R / I$. There exist $u_1, u_2, u \in I$ such that $$ \overline x = x + u_1 ~\land~ \overline y = y + u_2 ~\land~ \overline 1 = 1 + u $$ Which gives us $$ 1 = (x + u_1)(y + u_2) - u = {xy} + (xu_2 + yu_1 + u_1 u_2 - u) $$ Since $xy \in J$ and the last summand is in $I \subseteq J$, this shows $1 \in J$ and therefore $J = R$. $\Box$

Constructively this proof breaks down at the following points:

  • The equivalence $A \lor B \iff \neg A \to B$ does not hold.
  • We cannot get an existence $\exists x: \neg \varphi(x)$ from $\neg \forall x : \varphi(x)$.

To resolve (or rather skip) these issues, the definition of a maximal ideal can simply be taken to be:

$I$ is maximal if for every ideal $J \supseteq I$ with $\exists x \in J : \, x \notin I$ we have $J = R$.

i.e. every proper ideal which includes $I$ must already be the full ring. The proof then just works out as previously. When going through the proof of the $(\Rightarrow)$ direction however, we can now only show $$ \overline x \neq 0 \to \overline x \text{ invertible} $$ which is not equivalent to $\overline x = 0 \lor \overline x \text{ invertible}$ constructively. So the definition of field also needs to be changed in the above mentioned way (1.2).

  • 2
    $\begingroup$ There is no right constructive notion for fields. Fields that satisfy (2.2) are often called discrete fields in a constructive context, whereas fields that satisfy (1.2) may be called weak Heyting fields. The notion of discrete field is sometimes excessively strong (e.g. the reals fail to form a discrete field), whereas the notion of weak Heyting field is often too weak, so many intermediate notions (Kock field, Heyting field) are considered. In any case, (2.2) implies (1.2) straightforwardly, so discrete fields are also weak Heyting fields. $\endgroup$
    – Z. A. K.
    Commented Jun 11 at 9:34
  • 2
    $\begingroup$ As you found out, if we try to naively transcribe commutative algebra into constructive mathematics, we run into trouble fairly quickly: the traditional approach to the subject lacks constructive content. You could survey e.g. Lombardi-Quitté, or the dynamical method more generally, and that's before even touching upon the less developed (but no less important) approaches to algebra based on apartness relations. $\endgroup$
    – Z. A. K.
    Commented Jun 11 at 9:51
  • 1
    $\begingroup$ @Z.A.K. Ok this makes a lot of sense. So it's one of the common cases where a notion really splits up once it is viewed constructively. Also thanks a lot for these references! $\endgroup$
    – Léreau
    Commented Jun 11 at 10:25


You must log in to answer this question.