Heyting field

This article relies largely or entirely on a single source. Relevant discussion may be found on the talk page. Please help improve this article by introducing citations to additional sources. Find sources: "Heyting field" – news · newspapers · books · scholar · JSTOR (May 2024)

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.

This algebra-related article is a stub. You can help Wikipedia by expanding it.

• v
• t
• e