Side-stepping contradiction in the proof of ; ab = 0 then a or b is 0. Suppose we need to show a field has no zero divisors - that is prove the title - then we head off exactly like the one common argument in the reals (unsurprisingly as they themselves are a field).
What I want to know is; how do we prove this not by contradiction?
I was talking to some philosophers about - again not so surprising - logic and they seemed to have an issue with argument by contradiction. I admit I'm not a huge fan (of it) myself, though the gist of it was that classical logic (where contradiction / law of excluded middle is valid) is a really, really, really strong form of logic; a much weaker type of logic is something called intuitist (?) logic (I only caught the name) but they said it did not hold here.
Now, if we take something like the field axioms - or the reals (e.g. order in the bag...) - how can we prove in this new logic that there are no zero divisors. Or, more precisely how can we avoid contradiction?
 A: 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.
A: Let's prove the contrapositive: if $a\neq0$ and $b\neq0$ then $ab\neq0$.
Since we're in a field, any nonzero element has an inverse: $aa'=1$, $bb'=1$. Then $(ab)(a'b')=(aa')(bb')=1\cdot1=1$. This implies that $ab\ne0$ because $0$ times anything is $0$. 
For this last step, I've used: $xy\ne0$ for some $y$ $\implies x\ne0$, which is the contrapositive of $0y=0$ for all $y$.
A: A way to prove that a field has no zero divisors without using a contradiction method : Suppose $ab = 0$. Then there is two possibilities : either $a = 0$ (in which case we are done) or $a \neq 0$ and $a$ is a unit, therefore $b = a^{-1}ab = a^{-1}0 = 0$. I have never used any form of contradiction hypothesis. I've only dealt with cases. This also works in non-commutative fields.
Hope that helps,
A: You could approach this case by case:
$a$ and $b$ are either positive, negative, or zero.


*

*$a>0$, $b>0$ then $ab>0$ (positive times positive is positive). Thus $ab \not=0$.

*$a>0$, $b<0$ then $ab<0$ (positive times negative is negative). Thus $ab \not=0$.

*$a>0$, $b=0$ then $ab=0$.


etc.
Therefore, the only way we get $ab=0$ is if $a=0$ or $b=0$.
Edit: Admittedly, I guess I'm still using the law of excluded middle (and thus contradiction) here :(
For any field: 
Suppose $ab=0$. Then if $a=0$, we are done. If $a \not=0$, then $a^{-1}$ exists and so, $a^{-1}ab=0$ thus $1b=0$ and so $b=0$. Therefore, either $a=0$ or $b=0$.
A: Let $m,n\in\mathbb{N}$ such that $m,n>0$ (I subscribe to $0\in\mathbb{N}$ but it really doesn't matter here). It can be shown by induction that $mn\neq 0$. That is, that $mn>0$.
Now, let $a,b\in\mathbb{Z}$. If $ab=0$, then $|ab|=|0|=0$. Therefore $|ab|>0$ implies $ab\neq 0$.
Suppose $a,b\neq 0$. Then $|a|=m>0$ and $|b|=n>0$. By the above, $|a|\,|b|=|ab|=mn>0$. Hence $ab\neq 0$. Then if $ab=0$, we have $a=0$ or $b=0$.
