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 ¬formula_1, either formula_2 or formula_3 is invertible for every formula_2, 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 formula_2 # formula_6 if formula_7 is invertible. This relation is often now written as formula_2 ≠ formula_6 with the warning that it is not equivalent to ¬formula_10. For example, the assumption ¬formula_11 is not generally sufficient to construct the inverse of formula_2, but formula_2 ≠ formula_14 is.
The prototypical Heyting field is the real numbers.