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
¬ ( 0 = 1 ) {\displaystyle \neg (0=1)}
Each non-invertible element is zero and if it is moreover local: Not only does the non-invertible 0 {\displaystyle 0} not equal the invertible 1 {\displaystyle 1} , but the following disjunctions are granted more generally
Either a {\displaystyle a} or 1 − a {\displaystyle 1-a} is invertible for every a {\displaystyle a}
The third axiom may also be formulated as the statement that the algebraic " + {\displaystyle +} " transfers invertibility to one of its inputs: If a + b {\displaystyle a+b} is invertible, then either a {\displaystyle a} or b {\displaystyle b} 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 a # b {\displaystyle a\#b} if a − b {\displaystyle a-b} is invertible. This relation is often now written as a ≠ b {\displaystyle a\neq b} with the warning that it is not equivalent to ¬ ( a = b ) {\displaystyle \neg (a=b)} . The assumption ¬ ( a = 0 ) {\displaystyle \neg (a=0)} is then generally not sufficient to construct the inverse of a {\displaystyle a} . However, a # 0 {\displaystyle a\#0} 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.