A Heyting field is a local ring where every non-invertible element is equal to zero. More specifically, it is a commutative ring such that
is non-trivial ();
given elements and , if is invertible, then either is invertible or is invertible;
given an element , if is non-invertible, then .
Equivalently, a Heyting field is:
a local ring whose quotient ring by the ideal of non-invertible elements is isomorphic to ;
a local ring such that the canonical apartness relation — defined as if and only if is invertible — is a tight apartness relation.
a local ring which is both reduced and Artinian.
a local ring which is a semiprimitive ring.
In Lombardi & Quitté (2010), the authors’ definition of Heyting field do not include the non-equational axiom . Instead, they define non-invertible to mean that if the element is invertible, then . With such a definition, the trivial ring counts as a Heyting field and constitutes the terminal object in the categories of Heyting fields.
Every Heyting field has stable equality, because it has a tight apartness relation defined as if and only if is invertible. For all elements and , , and because , , and thus has stable equality.
A Heyting field with decidable tight apartness is a discrete field.
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:
Let be a proposition. We define the set to be the union of and
is a subring of the rational numbers .
Since is a subset of and has decidable equality, also has decidable equality. And of course in .
is a weak Heyting field iff .
Given a proposition , suppose its double negation , and consider some . Suppose does not have a multiplicative inverse. Now suppose . Then we see that is not in . If held, we would have . So we know holds. But this is a contradiction. Therefore, must be zero (using decidable equality).
Conversely, suppose is a weak Heyting field. If held, we would have , which clearly is not a Johnstone residue field since is neither invertible nor zero. So we must have .
is a Heyting field iff it is the case that iff is a discrete field.
Suppose is a Heyting field. Then either or has a multiplicative inverse, so either or . In either case, we see that holds. If holds, then , which is a discrete field. And if is a discrete field, it is clearly a Heyting field.
If every weak Heyting field with discrete equality is Heyting, then excluded middle is valid.
From the lemmas above, if every weak Heyting field with decidable equality is a Heyting field, then holds for all propositions . So we have full excluded middle.
Peter Johnstone, Rings, Fields, and Spectra, Journal of Algebra 49 (1977) 238-260 [doi:10.1016/0021-8693(77)90284-8]
Henri Lombardi, Claude Quitté (2010): Commutative algebra: Constructive methods (Finite projective modules) Translated by Tania K. Roblo, Springer (2015) [doi:10.1007/978-94-017-9944-7, pdf]
Fred Richman, Laurent series over . Communications in Algebra, Volume 48, Issue 5, 11 Jan 2020 Pages 1982-1984 [doi:10.1080/00927872.2019.1710166]
Last revised on September 5, 2024 at 13:34:40. See the history of this page for a list of all contributions to it.