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 it is a field in the sense that and if it is moreover local: Not only does the non-invertible
, but the following disjunctions are granted more generally The third axiom may also be formulated as the statement that the algebraic "
" transfers invertibility to one of its inputs: If
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.
An apartness relation is defined by writing
is then generally not sufficient to construct the inverse of
The prototypical Heyting field is the real numbers.