Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
The entry for constructive fields contains a discussion about different options to define a field constructively, but the most obvious definitions is not among the options. One could simply say that a constructive field is a commutative ring $R$ such that
$(x\neq 0)\Leftrightarrow\mathsf{isinvertible}(x)$.
for all $x\in R$. Strangely, in several of the definitions on the nlab page it is proposed to replace this condition, but it is never said why this is necessary.
On the other hand, the definition of a residue field is included. Here the condition is
$(x=0)\Leftrightarrow\neg\mathsf{isinvertible}(x)$
for all $x\in R$. This condition implies that the predicate $x=0$ is double-negation stable, which seems to reduce the applicability of the definition more than the more natural condition which seems to be dismissed.
So I was wondering why the condition $(x\neq 0)\Leftrightarrow\mathsf{isinvertible}(x)$ is not considered as an option for a definition of constructive field. Perhaps there is something obviously wrong with it, that I’m missing.
Well, a main example we want is the real numbers, which form a Heyting field, whose apartness is not the denial inequality. The condition you write is like MRR87’s denial field, but without the requirement that the denial inequality be tight (so = not nec. stable), and without the requirement that (0) be a prime ideal. What’s a good example of such a field with non-stable equality?
1 to 2 of 2