This article relies largely or entirely on a single source. (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
editA commutative ring is a Heyting field if it is a field in the sense that
- Each non-invertible element is zero
and if it is moreover local: Not only does the non-invertible not equal the invertible , but the following disjunctions are granted more generally
- Either or is invertible for every
The third axiom may also be formulated as the statement that the algebraic " " transfers invertibility to one of its inputs: If is invertible, then either or is as well.
Relation to classical logic
editThe 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
editAn apartness relation is defined by writing if is invertible. This relation is often now written as with the warning that it is not equivalent to .
The assumption is then generally not sufficient to construct the inverse of . However, is sufficient.
Example
editThe prototypical Heyting field is the real numbers.
See also
editReferences
edit- Mines, Richman, Ruitenberg. A Course in Constructive Algebra. Springer, 1987.