Without excluded middle: simple example of field with nilpotents?

Question

I would like to verify I'm not making a mistake.

Does the statement "fields do not have non-zero nilpotents" depend on the law of excluded middle?

All proofs of this fact I can conjure rely on the dichotomy $a=0\vee a\neq 0$ along with the implication (for fields) that $a\neq 0\implies a$ invertbile. Moreover, in algebraic geometry it's possible to show the generic ring of Zariski topoi is internally a field (has the implication $a\neq 0\implies a$ invertible, but not necessarily excluded middle).

Is there some super simple example of a (commutative unitary) ring which is internally a field and has nilpotents?

Added. What about the statement "in a field, the only nilpotent is zero"?

Remark. The implication ($\neg (a=0)\implies a$ is invertible) is not of my invention; it is taken as the definition of a "ring of fractions" in section 2 of this paper by Kock. Fields are defined analogously.

Answer 1

If $F$ is a field, I would interpret "No non-zero element is nilpotent" to mean simply that $(\forall x\in F)(x\ne 0 \implies (\forall n\in\mathbb{N})(x^n \ne 0)).$ The usual proof of this from the field axioms assumes $x\ne 0$ and proves that no power of $x$ is $0,$ which is constructive.

(The sentence $(\forall x\in F)(x=0 \,\lor\, (\forall n\in\mathbb{N})(x^n \ne 0))$ might be problematic, but that's a different sentence.)

---

As for the statement "In a field, the only nilpotent is zero," I think this depends how it's interpreted constructively.

(1) $\;(\forall x)\Big( \big((\exists n)(x^n=0)\big) \implies x=0 \Big)$ means that for every $x,$ if we have a witness $n$ that $x^n=0,$ then we can prove constructively that $x=0.$

(2) $\;\lnot (\exists x) \Big(\big((\exists n)(x^n=0)\big) \,\wedge\, x\ne0 \Big)$ means that we can derive a contradiction from the existence of a non-zero nilpotent.

(3) $\;(\forall x)\Big(x\ne 0 \implies \big((\forall n)(x^n \ne 0)\big) \Big)$ means that if we have a constructive proof that $x\ne 0,$ then, for every $n,$ we can produce constructively a constructive proof that $x^n\ne 0.$

(4) $\;(\forall x)\Big(x\ne 0 \implies \big(\lnot(\exists n)(x^n =0)\big) \Big)$ means the same thing as (2).

This is assuming I've unravelled everything correctly; it's tricky. If one thinks through the proofs very carefully, one should be able to see which of these are always true constructively.

Answer 2

You don't need the excluded middle to get a contradiction from a nilpotent in a field:

Suppose $a\ne 0$ but $a^n=0$ for some $n>1$. Then

$$ a = (a^{-1})^{n-1} \cdot a^n = (a^{-1})^{n-1} \cdot 0 = 0 $$ contradicting $a\ne 0$.

Answer 3

I think the intuitionistic definition of field you assume has to be disputed: First, you have $$(\ddagger):\qquad\forall s: \neg(s=0)\Rightarrow (s\text{ invertible})\quad\Longleftrightarrow\quad \forall s: \neg(s=0)\Leftrightarrow (s\text{ invertible}).$$ There, since $\neg\neg\neg\Phi\Leftrightarrow\neg\Phi$ is intuitionistically valid for any proposition $\Phi$, you get that $$(\star)\qquad\left[\neg(s=0)\Leftrightarrow (s\text{ invertible})\right]\quad\Longrightarrow\quad \left[\neg\neg(s\text{ invertible})\Leftrightarrow (s\text{ invertible})\right].$$ It's questionable you want to impose this restriction, because e.g. it does not hold when interpreting the domain of $s$ as the structure sheaf ${\mathscr O}_X$ of a reduced scheme $X$, which internally you might want to think of as a field.

The reason the R.H.S. of $(\star)$ does not hold in this case is that the truth value of $(s\text{ invertible})$ is the (scheme-theoretic) non-vanishing locus $\{x\in X\ |\ s(x)\neq 0\text{ in }k(x)\}$ of $s$, so $\neg\neg(s\text{ invertible})$ holds iff the latter is dense in $X$, which is the case iff $s$ is regular.

On the other hand, the alternative implication/equivalence defining intuitionistic fields $$(\dagger):\qquad\forall s: \neg(s\text{ invertible})\Rightarrow (s=0)\quad\Longleftrightarrow\quad \forall s: \neg(s\text{ invertible})\Leftrightarrow (s=0)$$ does hold for reduced schemes. Also, with this definition you can quickly prove that $$s\text{ nilpotent}\quad\Longrightarrow\quad s=0$$ since $s\text{ nilpotent}\Rightarrow\neg(s\text{ invertible})$.

Source: Ingo Blechschmidt's paper is a very interesting and pleasant read on all of this.

Answer 4

Here is a model of a field in which it is not true that every nilpotent is zero. The model will be the presheaf of commutative rings: $$\mathbb{Z} / 4\mathbb{Z} \overset{\pi}{\rightarrow} \mathbb{Z} / 2\mathbb{Z}.$$

To see this satisfies the field axiom $\forall x, x \ne 0 \rightarrow \exists y, xy = 1$: first, it clearly holds at the level of $\mathbb{Z} / 2 \mathbb{Z}$. As for the level of $\mathbb{Z} / 4 \mathbb{Z}$, if $x \in \mathbb{Z} / 4 \mathbb{Z}$, suppose $x \ne 0$ evaluates to true at that level. Then by definition of the interpretation of a negation, that implies $\pi(x) \ne 0$, so $x = 1 + 4\mathbb{Z}$ or $x = 3 + 4\mathbb{Z}$. In either case, $x$ has an inverse at the level of $\mathbb{Z} / 4 \mathbb{Z}$.

However, $x = 2 + 4 \mathbb{Z}$ is nilpotent, whereas $x = 0$ does not evaluate to true at the level of $\mathbb{Z} / 4 \mathbb{Z}$. (Note, though, that $\lnot(x \ne 0)$ does evaluate to true, as we would expect from the usual argument -- valid intuitionistically -- that in a field, products of nonzero elements are nonzero.)