Also removed

It is not true that every weak Heyting field with decidable equality is Heyting. See this proof for details.

since decidable equality isn’t really all that important for constructive fields. Locality (in the sense of local ring) and decidable apartness are more important.

]]>Replaced

A Heyting field is a discrete field if and only if equality is decidable; it is in this sense that a discrete field is ‘discrete’

with

A Heyting field is a discrete field if and only if its apartness relation is a decidable relation.

This exact mistake was made and later corrected on the principle of omniscience page, where editors confused the analytic WLPO (reals have decidable equality) with the analytic LPO (reals have decidable apartness).

]]>I recently came back to this page and, after some thought, have demonstrated we cannot constructively prove all Heyting fields with decidable equality are discrete.

Theorem: if all Heyting fields with decidable equality are discrete, then excluded middle holds.

Proof: Fix any prime number $p \in \mathbb{N}$. Suppose $Q$ is a proposition. Then define $F_Q \subseteq \mathbb{Z}$ by $F_Q = \mathbb{Z} \setminus (p) \cup \{pn \mid n \neq 0 \wedge Q\}$. Then $F_Q$ is a prime filter, so $F_Q^{-1} \mathbb{Z}$ is a local ring. Let $k_Q$ be the corresponding Heyting field.

Note that $p = 0$ in $k_Q$ if and only if $p$ is not a unit in $F_Q^{-1} \mathbb{Z}$, if and only if $p \notin F_Q$, if and only if $\neg Q$. Thus, if $k_Q$ has decidable equality, then $\neg Q$ is decidable. Conversely, suppose $\neg Q$ is decidable. The ideal of nonunits in $F_Q^{-1} \mathbb{Z}$ is $\{x \in (p) \mid \neg Q\} \cup (0)$, which is a decidable subset of $\mathbb{Z}$, so $k_Q$ has decidable equality. Thus, $k_Q$ has decidable equality if and only if $\neg Q$ is decidable.

Note that $p$ is a unit in $k_Q$ if and only if $p$ is a unit in $F_Q^{-1} \mathbb{Z}$, iff $p \in F_Q$, iff $Q$. So if $k_Q$ is a discrete field, then $Q$ is decidable. Conversely, if $Q$ is decidable, then $k_Q$ is either $\mathbb{F}_p$ or $\mathbb{Q}$, and thus is a discrete field. So $k_Q$ is a discrete field if and only if $Q$ is decidable.

Now suppose all Heyting fields with decidable equality are discrete fields, and suppose $\neg \neg Q$. Then $\neg Q$ is decidable, so $k_Q$ is a Heyting field with decidable equality, so $k_Q$ is a discrete field. Because $k_Q$ is a discrete field, $Q$ is decidable. Since $Q$ is decidable and $\neg \neg Q$, we can conclude $Q$. We thus have double negation elimination, and hence full excluded middle. $\square$

If no one sees a flaw in this argument, then we should delete the portion of the page claiming “A Heyting field is a discrete field if and only if equality is decidable; it is in this sense that a discrete field is ‘discrete’.” Decidable equality is constructively weaker than decidable unithood.

]]>Added reference

- {#Richman20} Fred Richman,
*Laurent series over $\mathbb{R}$*. Communications in Algebra, Volume 48, Issue 5, 11 Jan 2020 Pages 1982-1984 [doi:10.1080/00927872.2019.1710166]

and used the more clear “weak Heyting field” over the ambiguous “residue field” throughout the page.

Anonymouse

]]>added Mark Saying’s proof that not every residue field with decidable equality is Heyting.

Anonymous

]]>There appears to be an error in the section on construction notions of a field. Specifically, the claim is that a residue field is discrete iff equality is decidable. But this seems not to be true.

In fact, the statement “A residue field with decidable equality is a Heyting field” is equivalent to excluded middle.

To see this, consider a proposition $p$. Consider the set $R_p = \mathbb{Z} \cup \{x \in \mathbb{Q} \mid p\}$, which is a subring of $\mathbb{Q}$. Since $R_p$ is a subset of $\mathbb{Q}$ and $\mathbb{Q}$ has decidable equality, $R_p$ also has decidable equality. And of course $0 \neq 1$ in $R_p$.

I claim that $R_p$ is a residue field iff $\neg \neg p$. For suppose $\neg \neg p$, and consider some $x \in R_p$. Suppose $x$ does not have a multiplicative inverse. Now suppose $x \neq 0$. Then we see that $x^{-1} \notin R_p$. If $p$ held, we would have $x^{-1} \in R_p$. So we know $\neg p$ holds. But this is a contradiction. Therefore, $x$ must be zero (using decidable equality).

Conversely, suppose $R$ is a residue field. Then $2 \neq 0$, so 2 does not fail to have an inverse. That is, $2^{-1}$ is not not in $R_p$. Then $\neg \neg p$.

I claim that $R_p$ is a Heyting field iff $p$ iff $R_p$ is a discrete field. For suppose $R$ is a Heyting field. Then either 2 or 3 has a multiplicative inverse, so either $2^{-1}$ or $3^{-1} \in R_p$. In either case, we see that $p$ holds. If $p$ holds, then $R_p = \mathbb{Q}$, which is a discrete field. And if $R_p$ is a discrete field, it is clearly a Heyting field.

With these facts in hand, we see that if every residue field with decidable equality is a Heyting field, then $p \iff \neg \neg p$ holds for all $p$. So we have full excluded middle.

Of course, assuming excluded middle, it is clear that all residue fields with decidable equality are discrete fields. $\square$

I have not yet determined whether all Heyting fields with decidable equality are discrete, but it seems very likely that this also cannot be proven.

If no one objects, I will change the page to say that a residue field is discrete if and only if unithood is decidable.

]]>added pointer to:

- Marc Bezem, Ulrik Buchholtz, Pierre Cagne, Bjørn Ian Dundas, Daniel R. Grayson: Chapter 8 of:
*Symmetry*(2021) $[$pdf$]$

I have taken the liberty of turning this comment from a sub-section into a remark (here). Also tried to adjust the wording a little, for readability.

]]>one pair of authors defined fields to be possibly trivial.

Anonymous

]]>cross-linked the discussion of weakly initial sets in the category of fields with the corresponding example at *multi-adjoint*

Change definition of denial field to actually match MRR87

]]>Clarify a sentence to say that the discrete field condition implies that $0\neq 1$.

Egbert Rijke

]]>Thanks! I’ve noticed that before, but always forget about it.

]]>I fixed up the DOI link for Johnstone’s paper (at field and at local ring), since the geniuses at Elsevier use parentheses in their DOIs, which break markdown syntax.

For reference, one needs to replace `(nn)`

in the DOI url by `%28nn%29`

.

I added to field a mention of some other constructive variants of the definition, with a couple more references.

]]>