Due to a widely propagated historical error, it is commonly misbelieved that Euclid's proof was by contradiction. This is false. Euclid's proof was in fact presented in the obvious constructive fashion explained below. See Hardy and Woodgold's Intelligencer article [1] for a detailed analysis of the history (based in part on many sci.math discussions [2]).
The key idea is not that Euclid's sequence $\ f_1 = 2,\ \ \color{#0a0}{f_{n}} = \,\color{#a5f}{\bf 1}\, +\, f_1\cdot\cdot\cdot\cdot\, f_{n-1}$ is an infinite sequence of primes but, rather, that it's an infinite sequence of coprimes, i.e. $\,{\rm gcd}(f_k,f_n) = 1\,$ if $\,k<n,\,$ since then any common divisor of $\,\color{#c00}{f_k},\color{#0a0}{f_n}\,$ must also divide
$\, \color{#a5f}{\bf 1} = \color{#0a0}{f_n} - f_1\cdot\cdot\, \color{#c00}{f_k}\cdot\cdot\, f_{n-1}.$
Any infinite sequence of pairwise coprime $f_n > 1 \,$ yields an infinite sequence of distinct primes $\, p_n $ obtained by choosing $\,p_n$ to be any prime factor of $\,f_n,\,$ e.g. its least factor $> 1$.
A variant that deserves to be much better known is the following folklore one-line proof that there are infinitely many prime integers
$$n\:\! (n+1)\,\ \text{has a larger set of prime factors than does }\, n\qquad$$
because $\,n+1>1\,$ is coprime to $\,n\,$ so it has a prime factor which does not divide $\,n.\,$ Curiously, Ribenboim believes this proof to be of recent vintage, attributing it to Filip Saidak. But I recall seeing variants published long ago. Does anyone know its history?
For even further variety, here is a version of Euclid's proof reformulated into infinite descent form. If there are only finitely many primes, then given any prime $\,p\,$ there exists a smaller prime, namely the least factor $> 1\,$ of $\, 1 + $ product of all primes $\ge p\:.$
It deserves to be much better known that Euclid's constructive proof generalizes very widely - to any fewunit ring, i.e. any ring having fewer units than elements - see my proof here. $ $ The key idea is that Euclid's construction of a new prime generalizes from elements to ideals, i.e. given some maximal ideals $\rm\, P_1,\ldots,P_k,\, $
a simple pigeonhole argument employing CRT deduces that $\rm\, 1+P_1\:\cdots\:P_k\, $ contains a nonunit, which lies in some maximal ideal which, by construction,
is comaximal (so distinct) from the initial max ideals $\rm\,P_1,\ldots,P_k.$
[1] Michael Hardy; Catherine Woodgold. Prime Simplicity.
The Mathematical Intelligencer, Volume 31, Number 4, 44-52 (2009).
[2] Note: Although the article [1] makes no mention of such, it appears to have strong roots in frequent sci.math discussions - in which the first author briefly participated. A Google groups search in the usenet newsgroup sci.math for "Euclid plutonium" will turn up many long discussions on various misinterpretations of Euclid's proof.
Proof of negation and proof by contradiction are equivalent in classical logic. However there are not equivalent in constructive logic.
One would usually define $\neg \phi$ as $\phi \rightarrow \perp$, where $\perp$ stands for contradiction / absurdity / falsum. Then the proof of negation is nothing more than an instance of "implication introduction":
If $B$ follows from $A$, then $A\rightarrow B$. So in particular:
If $\perp$ follows from $\phi$, then $\phi \rightarrow \perp$ ($\neg \phi$).
The following rule is of course just a special case:
If $\perp$ follows from $\neg \phi$, then $\neg \neg \phi$.
But the rule $\neg \neg \phi \rightarrow \phi$ is not valid in constructive logic in general. It is equivalent to the law of excluded middle ($\phi\vee \neg \phi$). If you add this rule to your logic, you get classical logic.
Best Answer
There's no intuitionism/constructivism issue going on here at all.
First of all, as a general matter of practice you need to keep separate the notions of proof by contradiction and proof by negation. The latter is intuitionistically acceptable!
Specifically, let's say we interpret "$\neg p$" as shorthand for "$p\rightarrow\perp$" (this is pretty standard) and accept the inference rule $$(\mathsf{ded})\quad{A,p\vdash q\over A\vdash p\rightarrow q}$$ (= the deduction theorem) while rejecting double negation elimination. Then the proof by negation inference rule $$(\mathsf{nega})\quad{A,p\vdash\perp\over A\vdash\neg p}$$ is justifiable: from $A,p\vdash\perp$ we get $A\vdash p\rightarrow\perp$, which literally is the sequent $A\vdash\neg p$.
If we replace "$p$" by "$\neg p$" in the above we get $${A,\neg p\vdash \perp\over A\vdash\neg\neg p}$$ but the bottom sequent is not the same as $A\vdash p$ since we've rejected double negation elimination! Consequently the proof by contradiction inference rule $$(\mathsf{contra})\quad{A,\neg p\vdash \perp\over A\vdash p}$$ is not justified by our logical hypotheses so far.
This is all to say that a lot of the "elementary" examples of proof by contradiction are actually completely fine intuitionistically, since they're not proof by contradiction at all. Of course this is a distinction which doesn't exist classically, so is easy to miss at first.
But this is in fact only part of the story! We also need, when thinking nonclassically, to be more careful how we even phrase our goal. For example, consider the following statement:
There are no negations involved here whatsoever, and the obvious argument "$2$ divides $x$ and is strictly between $1$ and $x$" (once we've written out what "even" means) goes through perfectly. Things only become "negation-flavored" when we introduce unnecessary negations, a la "$\neg$ (there is an even number $x>2$ such that $\neg$ ($x$ is prime))." But the fact that we are allowed proof by negation means that such negation-introduction preserves intuitionistic provability.
As a toy example of this, consider the following proof that the sequent $$p\vdash\neg\neg p$$ is intuitionistically valid (unlike $\neg\neg p\vdash p$).
First, by modus ponens we have $p, \color{red}{p\rightarrow\perp}\vdash \perp.$
By $(\mathsf{ded})$ we have $p\vdash \color{red}{(p\rightarrow\perp)}\rightarrow\perp$.
But using our definition of $\neg$, this is literally the same sequent as $p\vdash \neg\neg p$.
A good exercise at this point is to intuitionistically prove triple negation elimination $$\neg\neg\neg p\dashv\vdash\neg p.$$