Heyting field explained

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