Heyting field

A Heyting field is one of the inequivalent ways in constructive mathematics to capture the classical notion of a field. It is essentially a field with an apartness relation. A commutative ring is a Heyting field if ¬${\displaystyle (0=1)}$, either ${\displaystyle a}$ or ${\displaystyle 1-a}$ is invertible for every ${\displaystyle a}$, and each noninvertible element is zero. The first two conditions say that the ring is local; the first and third conditions say that it is a field in the classical sense.

The apartness relation is defined by writing ${\displaystyle a}$ # ${\displaystyle b}$ if ${\displaystyle a-b}$ is invertible. This relation is often now written as ${\displaystyle a}$ ≠ ${\displaystyle b}$ with the warning that it is not equivalent to ¬${\displaystyle (a=b)}$. For example, the assumption ¬${\displaystyle (a=0)}$ is not generally sufficient to construct the inverse of ${\displaystyle a}$, but ${\displaystyle a}$ ≠ ${\displaystyle 0}$ is.

The prototypical Heyting field is the real numbers.

References

• Mines, Richman, Ruitenberg. A Course in Constructive Algebra. Springer, 1987.