A commutative ring is a Heyting field if it is a field in the sense that

• ${\displaystyle \neg (0=1)}$ 
• Each non-invertible element is zero

and if it is moreover local: Not only does the non-invertible ${\displaystyle 0}$  not equal the invertible ${\displaystyle 1}$ , but the following disjunctions are granted more generally

• Either ${\displaystyle a}$  or ${\displaystyle 1-a}$  is invertible for every ${\displaystyle a}$ 

The third axiom may also be formulated as the statement that the algebraic "${\displaystyle +}$ " transfers invertibility to one of its inputs: If ${\displaystyle a+b}$  is invertible, then either ${\displaystyle a}$  or ${\displaystyle b}$  is as well.

Relation to classical logic edit

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.

An apartness relation is defined by writing ${\displaystyle a\#b}$  if ${\displaystyle a-b}$  is invertible. This relation is often now written as ${\displaystyle a\neq b}$  with the warning that it is not equivalent to ${\displaystyle \neg (a=b)}$ .

The assumption ${\displaystyle \neg (a=0)}$  is then generally not sufficient to construct the inverse of ${\displaystyle a}$ . However, ${\displaystyle a\#0}$  is sufficient.

The prototypical Heyting field is the real numbers.

• Constructive analysis
• Pseudo-order
• Markov's principle

• Mines, Richman, Ruitenberg. A Course in Constructive Algebra. Springer, 1987.