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

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

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

• Either $a$ or $1-a$ is invertible for every $a$

The third axiom may also be formulated as the statement that the algebraic "$+$" transfers invertibility to one of its inputs: If $a+b$ is invertible, then either $a$ or $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$ if $a-b$ is invertible. This relation is often now written as $a\neq b$ with the warning that it is not equivalent to $\neg (a=b)$.

The assumption $\neg (a=0)$ is then generally not sufficient to construct the inverse of $a$. However, $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.