Misplaced Pages

Heyting field

Article snapshot taken from Wikipedia with creative commons attribution-sharealike license. Give it a read and then ask your questions in the chat. We can research this topic together.
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

  • ¬ ( 0 = 1 ) {\displaystyle \neg (0=1)}
  • Each non-invertible element is zero

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

  • Either a {\displaystyle a} or 1 a {\displaystyle 1-a} is invertible for every a {\displaystyle a}

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

The assumption ¬ ( a = 0 ) {\displaystyle \neg (a=0)} is then generally not sufficient to construct the inverse of a {\displaystyle a} . However, a # 0 {\displaystyle a\#0} is sufficient.

Example

The prototypical Heyting field is the real numbers.

See also

References

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


Stub icon

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

Categories: