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.

Definition

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

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 ${\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.

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.