nLab Heyting field



In constructive mathematics:


A Heyting field is a local ring where every non-invertible element is equal to zero. More specifically, it is a commutative ring RR such that

  1. RR is non-trivial (010 \neq 1);

  2. given elements aRa \in R and bRb \in R, if a+ba + b is invertible, then either aa is invertible or bb is invertible;

  3. given an element aRa \in R, if aa is non-invertible, then a=0a = 0.

Equivalently, a Heyting field is:


In Lombardi & Quitté (2010), the authors’ definition of Heyting field do not include the non-equational axiom 101 \neq 0. Instead, they define non-invertible to mean that if the element is invertible, then 1=01 = 0. With such a definition, the trivial ring counts as a Heyting field and constitutes the terminal object in the categories of Heyting fields.


Stable and decidable equality.

Every Heyting field RR has stable equality, because it has a tight apartness relation defined as a#ba \# b if and only if aba - b is invertible. For all elements aRa \in R and bRb \in R, ¬¬¬(a#b)¬(a#b)\neg \neg \neg (a \# b) \iff \neg (a \# b), and because ¬(a#b)a=b\neg (a \# b) \iff a = b, ¬¬(a=b)a=b\neg \neg (a = b) \iff a = b, and thus RR has stable equality.

A Heyting field with decidable equality is a discrete field.

Relation to Johnstone residue fields

Johnstone (1977) defined a residue field to be a commutative ring which only satisfy axioms 1 and 3 in Def. ; we shall call these Johnstone residue fields in this article to not confuse them with the notion of residue field in algebraic geometry.

If every Johnstone residue field with decidable equality is a Heyting field, then excluded middle follows. The following proof is due to Mark Saving:


Let pp be a proposition. We define the set R pR_p to be the union of \mathbb{Z} and {x|p}\{x \in \mathbb{Q} \vert p\}

R pR_p is a subring of the rational numbers \mathbb{Q}.

Since R pR_p is a subset of \mathbb{Q} and \mathbb{Q} has decidable equality, R pR_p also has decidable equality. And of course 010\neq 1 in R pR_p.


R pR_p is a Johnstone residue field iff ¬¬p\neg \neg p.


Given a proposition pp, suppose its double negation ¬¬p\neg \neg p, and consider some xR px\in R_p. Suppose xx does not have a multiplicative inverse. Now suppose x0x\neq 0. Then we see that x 1x^{-1} is not in R pR_p. If pp held, we would have x1R px{-1} \in R_p. So we know ¬p\neg p holds. But this is a contradiction. Therefore, xx must be zero (using decidable equality).

Conversely, suppose R pR_p is a Johnstone residue field. If ¬p\neg p held, we would have R p=R_p = \mathbb{Z}, which clearly is not a Johnstone residue field since 22 is neither invertible nor zero. So we must have ¬¬p\neg \neg p.


R pR_p is a Heyting field iff it is the case that pp iff R pR_p is a discrete field.


Suppose R pR_p is a Heyting field. Then either 22 or 33 has a multiplicative inverse, so either 2 1R p2^{-1} \in R_p or 3 1R p3^{-1} \in R_p. In either case, we see that pp holds. If pp holds, then R p=R_p = \mathbb{Q}, which is a discrete field. And if R pR_p is a discrete field, it is clearly a Heyting field.


If every Johnstone residue field with discrete equality is Heyting, then excluded middle is valid.


From the lemmas above, if every Johnstone residue field with decidable equality is a Heyting field, then p¬¬pp \iff \neg \neg p holds for all propositions pp. So we have full excluded middle.

See also


Last revised on January 12, 2023 at 18:20:49. See the history of this page for a list of all contributions to it.