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.

Definition

A commutative ring is a Heyting field if ¬$(0=1)$, either $a$ or $1-a$ is invertible for every $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 $a$ # $b$ if $a-b$ is invertible. This relation is often now written as $a$ ≠ $b$ with the warning that it is not equivalent to ¬$(a=b)$. For example, the assumption ¬$(a=0)$ is not generally sufficient to construct the inverse of $a$, but $a$ ≠ $0$ is.

Example

The prototypical Heyting field is the real numbers.

See also

• Constructive analysis
• Pseudo-order

References

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