Jump to content

Heyting field

From Wikipedia, the free encyclopedia

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

[edit]

A 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

[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.

Discussion

[edit]

An 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

[edit]

The prototypical Heyting field is the real numbers.

See also

[edit]

References

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