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 ¬[math]\displaystyle{ (0=1) }[/math], either [math]\displaystyle{ a }[/math] or [math]\displaystyle{ 1-a }[/math] is invertible for every [math]\displaystyle{ a }[/math], 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 [math]\displaystyle{ a }[/math] # [math]\displaystyle{ b }[/math] if [math]\displaystyle{ a-b }[/math] is invertible. This relation is often now written as [math]\displaystyle{ a }[/math] ≠ [math]\displaystyle{ b }[/math] with the warning that it is not equivalent to ¬[math]\displaystyle{ (a=b) }[/math]. For example, the assumption ¬[math]\displaystyle{ (a=0) }[/math] is not generally sufficient to construct the inverse of [math]\displaystyle{ a }[/math], but [math]\displaystyle{ a }[/math] ≠ [math]\displaystyle{ 0 }[/math] is.
Example
The prototypical Heyting field is the real numbers.
See also
References
- Mines, Richman, Ruitenberg. A Course in Constructive Algebra. Springer, 1987.
 |  |
