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.

Weak Heyting fields

A weak Heyting field (cf. Richman (2020)) or Johnstone residue field is a commutative ring which only satisfy axioms 1 and 3 in Def. . Johnstone (1977) referred these as a residue field; however, this is not to be confused with the already existing notion of a residue field in algebraic geometry as the quotient field of a local ring.

If every weak Heyting 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 weak Heyting 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 weak Heyting 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 weak Heyting field with discrete equality is Heyting, then excluded middle is valid.


From the lemmas above, if every weak Heyting 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 28, 2024 at 05:13:56. See the history of this page for a list of all contributions to it.