I am beginning to learn about constructive math on my own and am casually reading the paper Algebraic Numbers, a Constructive Development by W. Julian, R. Mines, and F. Richman (Pacific Journal of Mathematics, Vol. 74, No. 1, 1978). I am confused by some of their preliminary remarks they give. First, before they provide the field axioms they say the following
Inequality is to be thought of as a positive notion of distinctness rather than the denial of equality.
I take this to mean $a=b\iff\neg(a\neq b)$.
After providing the field axioms, which look like the standard axioms with the exception of this one:
- For each integer $n$, $a^{n}=0$ implies $a=0$,
they mention something called Heyting's axiom apart from their given list of field axioms and which says
If $x\neq y$ is impossible, then $x=y$,
and they mention that the funny axiom (6) is what is used to replace Heyting's axiom (whose invocation they recommend abstaining from). This confuses me, since Heyting's axiom seems to follow from the provided definition of distinctness. What am I misunderstanding?
You've taken the exact opposite meaning of what they intended with respect to inequality. What they are saying is that there is a binary relation $a\#b$, often called apartness, for which it is not necessarily the case that $a = b \iff \neg(a\#b)$. They are using $\neq$ for what I called $\#$, but what they are saying is exactly that $x\neq y$ does not necessarily mean $\neg(x=y)$. Instead $\neq$ should be treated as its own binary relation unrelated to equality. (Well, not completely unrelated. You will have things like $x\neq y\implies \neg(x=y)$ and $x=y\implies \neg(x\neq y)$, but these aren't equivalences in general.)
There are multiple distinct ways of formalizing the notion of a field in constructive mathematics. As mentioned by the paper, it is a weakening of the notion of a Heyting field. I don't believe it corresponds exactly to any of the definitions given on the nLab page, but I haven't thought about it too hard.