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 it is a field in the sense that
Each non-invertible element is zero and if it is moreover local: Not only does the non-invertible not equal the invertible , but the following disjunctions are granted more generally Either or is invertible for every
The third axiom may also be formulated as the statement that the algebraic "" transfers invertibility to one of its inputs: If is invertible, then either or is as well.
Relation to classical logic The structure defined without the third axiom may be called a weak Heyting field. Every such structure with decidable equality being a Heyting field is equivalent to excluded middle. Indeed, classically all fields are already local.
Discussion An apartness relation is defined by writing if is invertible. This relation is often now written as with the warning that it is not equivalent to .
The assumption is then generally not sufficient to construct the inverse of . However, is sufficient.
Example The prototypical Heyting field is the real numbers.
See also Constructive analysis Pseudo-order Markov's principle
References Mines, Richman, Ruitenberg. A Course in Constructive Algebra. Springer, 1987.