nLab Heyting field

Contents

 Definition

In constructive mathematics:

Definition

A Heyting field is a local ring where every non-invertible element is equal to zero. More specifically, it is a commutative ring RR such that

  1. RR is non-trivial (010 \neq 1);

  2. given elements aRa \in R and bRb \in R, if a+ba + b is invertible, then either aa is invertible or bb is invertible;

  3. given an element aRa \in R, if aa is non-invertible, then a=0a = 0.

Equivalently, a Heyting field is:

Remark

In Lombardi & Quitté (2010), the authors’ definition of Heyting field do not include the non-equational axiom 101 \neq 0. Instead, they define non-invertible to mean that if the element is invertible, then 1=01 = 0. With such a definition, the trivial ring counts as a Heyting field and constitutes the terminal object in the categories of Heyting fields.

 Properties

Stable and decidable equality.

Every Heyting field RR has stable equality, because it has a tight apartness relation defined as a#ba \# b if and only if aba - b is invertible. For all elements aRa \in R and bRb \in R, ¬¬¬(a#b)¬(a#b)\neg \neg \neg (a \# b) \iff \neg (a \# b), and because ¬(a#b)a=b\neg (a \# b) \iff a = b, ¬¬(a=b)a=b\neg \neg (a = b) \iff a = b, and thus RR has stable equality.

A Heyting field with decidable equality is a discrete field.

Weak Heyting fields

A weak Heyting field (cf. Richman (2020)) or Johnstone residue field is a commutative ring which only satisfy axioms 1 and 3 in Def. . Johnstone (1977) referred these as a residue field; however, this is not to be confused with the already existing notion of a residue field in algebraic geometry as the quotient field of a local ring.

If every weak Heyting field with decidable equality is a Heyting field, then excluded middle follows. The following proof is due to Mark Saving:

Definition

Let pp be a proposition. We define the set R pR_p to be the union of \mathbb{Z} and {x|p}\{x \in \mathbb{Q} \vert p\}

R pR_p is a subring of the rational numbers \mathbb{Q}.

Since R pR_p is a subset of \mathbb{Q} and \mathbb{Q} has decidable equality, R pR_p also has decidable equality. And of course 010\neq 1 in R pR_p.

Theorem

R pR_p is a weak Heyting field iff ¬¬p\neg \neg p.

Proof

Given a proposition pp, suppose its double negation ¬¬p\neg \neg p, and consider some xR px\in R_p. Suppose xx does not have a multiplicative inverse. Now suppose x0x\neq 0. Then we see that x 1x^{-1} is not in R pR_p. If pp held, we would have x1R px{-1} \in R_p. So we know ¬p\neg p holds. But this is a contradiction. Therefore, xx must be zero (using decidable equality).

Conversely, suppose R pR_p is a weak Heyting field. If ¬p\neg p held, we would have R p=R_p = \mathbb{Z}, which clearly is not a Johnstone residue field since 22 is neither invertible nor zero. So we must have ¬¬p\neg \neg p.

Theorem

R pR_p is a Heyting field iff it is the case that pp iff R pR_p is a discrete field.

Proof

Suppose R pR_p is a Heyting field. Then either 22 or 33 has a multiplicative inverse, so either 2 1R p2^{-1} \in R_p or 3 1R p3^{-1} \in R_p. In either case, we see that pp holds. If pp holds, then R p=R_p = \mathbb{Q}, which is a discrete field. And if R pR_p is a discrete field, it is clearly a Heyting field.

Theorem

If every weak Heyting field with discrete equality is Heyting, then excluded middle is valid.

Proof

From the lemmas above, if every weak Heyting field with decidable equality is a Heyting field, then p¬¬pp \iff \neg \neg p holds for all propositions pp. So we have full excluded middle.

See also

 References

Last revised on January 28, 2024 at 05:13:56. See the history of this page for a list of all contributions to it.