Let me expand on my comments. Suppose we have a structure with two constants $0$ and $1$, one unary operation $-$ and two binary operations $+$ and $\times$ satisfying
- $0 + x = x + 0 = x$
- $x + (y + z) = (x + y) + z$
- $x + (-x) = (-x) + x = 0$
- $x + y = y + x$
- $1 \times x = x \times 1 = x$
- $x \times (y \times z) = (x \times y) \times z$
- $x \times y = y \times x$
- $x \times (y + z) = x \times y + x \times z$
- $(x + y) \times z = x \times z + y \times z$
- $0 \ne 1$
- $(x = 0) \lor \exists y . (x \times y = 1)$
A model of this theory is what some people call a discrete field. It is easy enough to prove that discrete fields have no non-trivial zero divisors: indeed, if $x \times y = 0$, then by (11) either $y = 0$ or there is a $z$ such that $y \times z = 1$; but if there is such a $z$, then $0 = 0 \times z = x \times y \times z = x \times 1 = x$, so $(x \times y = 0) \implies ((x = 0) \lor (y = 0))$ as required. This deduction does not make use of the law of excluded middle and is valid intuitionistically.
Unfortunately, the theory of discrete fields is somewhat unsatisfactory. Firstly, axiom 10 is somewhat unnatural: the usual axiom is $(x \ne 0) \implies \exists y. (x \times y = 1)$ which is intuitionistically strictly weaker than axiom 11. (Morally, this is because intuitionistic logic has the disjunction property.) If we had adopted this axiom instead, it would not be possible to prove the non-existence of non-trivial zero divisors.
Secondly, I think you will agree with me that however we axiomatise the theory of fields, we had better axiomatise it in such a way that a model of the Dedekind real numbers is a model for the theory of fields. However, one can easily produce models of the intuitionistic theory of Dedekind real numbers which are not discrete fields, by the following theorem:
Theorem. Let $X$ be a topological space. A model of the theory of Dedekind real numbers in the internal logic of the sheaf topos $\textrm{Sh}(X)$ is isomorphic to the sheaf of continuous real-valued functions on $X$.
Proof. See Sheaves in Geometry and Logic [Ch. VI, §8, Theorem 2].
So let us consider the space $X = [-1, 1]$. Let $\mathscr{O}_X$ be the sheaf of continuous real-valued functions on $X$. We have a continuous map $i : \{ 0 \} \hookrightarrow X$, and by general sheaf theory we know that the inverse image sheaf $i^* \mathscr{O}_X$ is just the local ring of germs of continuous functions at $0$ in $X$. The inverse image functor $i^* : \textrm{Sh}(X) \to \textrm{Sh}(\{ 0 \})$ preserves the interpretation of geometric formulae, and the theory of discrete fields is geometric, so if $\mathscr{O}_X$ were a discrete field, so would $i^* \mathscr{O}_X$. But a sheaf on a point is just a set, so the internal logic of $\textrm{Sh}(\{ 0 \})$ is classical, and $i^* \mathscr{O}_X$ is not a field: the germ of, say, $x \mapsto x^2$ is not invertible in $i^* \mathscr{O}_X$, yet is not zero either. So $\mathscr{O}_X$ could not have been a discrete field to begin with.
So is there an intuitionistic theory of fields which does admit the Dedekind real numbers as a model? It turns out we should add a binary relation $\newcommand{\hash}{\mathrel{\#}}$ $\hash$, called a tight apartness relation, satisfying the axioms one would expect for inequality $\ne$:
- $\lnot (x \hash x)$
- $(x \hash y) \implies (y \hash x)$
- $(x \hash z) \implies (x \hash y \lor y \hash z)$
- $\lnot (x \hash y) \implies (x = y)$
Then, if we replace axioms 10 and 11 above by the axioms
- $(x \hash y) \Longleftrightarrow \exists z . (x \times z = y \times z + 1)$
we obtain the theory of Heyting fields. In words, $x \hash y$ precisely when $x - y$ is invertible. It turns out that a model of the Dedekind real numbers is indeed a Heyting field, and the intuition here is that $x \hash y$ when $x$ and $y$ are functions such that $x - y$ is nowhere zero: thus, the graphs of $x$ and $y$ do not intersect anywhere if $x \hash y$. (Hence the name ‘apartness relation’.) (One may object that just because $x - y$ is somewhere zero doesn't mean $x = y$, but the interpretation of $\lnot$ is quite subtle in this context and $\lnot (x \hash y)$ turns out to mean exactly that $x = y$.)
Specialising the Heyting field axiom above, we obtain $(x \hash 0) \Longleftrightarrow \exists y . (x \times y = 1)$ and so by contraposition we have $\nexists y . (x \times y = 1) \implies \lnot (x \hash 0)$ but $\lnot (x \hash 0) \implies x = 0$, so $\nexists y . (x \times y = 1) \implies x = 0$ exactly as in the classical theory of fields. Moreover, since $1 \times 1 = 0 \times 1 + 1$ we must have $1 \hash 0$.
Now, let us turn our attention to zero divisors. It seems there is an unavoidable tradeoff: now that we've allowed the Dedekind real numbers to be a field, we must allow fields to have zero divisors. Indeed, consider the function $f : [-1, 1] \to \mathbb{R}$ $f(x) = \begin{cases} 0 & x \le 0 \\ \exp (-1 / x^2) & x > 0 \end{cases}$ This is continuous (and even smooth!), but if we set $g(x) = f(-x)$, then $f(x) g(x) = 0$ for all $x$. Yet, for all open covers $\{ U_i \}$ of $X = [-1, 1]$, there must be a neighbourhood $U$ of $0$ such that $f|_U \ne 0 \text{ and } g|_U \ne 0$ so thus $X \not\Vdash (f = 0) \lor (g = 0)$ (in the sense of sheaf semantics) and therefore $X \not\Vdash (f \times g = 0) \Rightarrow ((f = 0) \lor (g = 0))$ but sheaf semantics validates intuitionistic logic, so this implies $(x \times y = 0) \implies ((x = 0) \lor (y = 0))$ cannot be proven in intuitionistic logic.