Adding to Carl Mummert's statements:
Notation: $\vdash$ means "provable in constructive logic", while $\vdash_{classical}$ means "provable in classical logic".
Suppose we have a multi-sorted vocabulary $V$. Note: this result can be generalised to dependently typed logics, but we won't get into that here.
We define the double-negation translation of a formula $\phi$ as follows:
- $translation(\top) = \top$, $translation(\bot) = \bot$
- If $a, b$ are terms of the same sort, $translation(a = b) = \neg \neg (a = b)$
- If $P$ is a predicate and $t_1, \ldots, t_n$ are terms of the appropriate sorts, $translation(P(t_1, \ldots, t_n)) = \neg \neg P(t_1, \ldots, t_n)$
- If $\phi$ and $\xi$ are statements, then $translation(\phi \lor \xi) = \neg \neg (translation(\phi) \lor translation(\xi))$, $translation(\phi \land \xi) = translation(\phi) \land translation(\xi)$, and $translation(\phi \to \xi) = translation(\phi) \to translation(\xi)$
- If $\phi(x)$ is a statement, then $translation(\forall x . \phi(x)) = \forall x . translation(\phi(x))$ and $translation(\exists x . \phi(x)) = \neg \neg \exists x . \phi(x)$.
Note here that $\neg \xi$ is taken as syntactic sugar for $\xi \to \bot$. So $translation(\neg \psi) = \neg translation(\psi)$.
I claim that for all sentences $\phi$, if $\vdash_{classical} \phi$ then $\vdash translation(\phi)$.
To prove this, we need to go through all the axioms in the classical Hilbert calculus one by one and, for each axiom $\xi$, prove $\vdash translation(\xi)$. This is a straightforward exercise, but a bit tedious.
Then, we need to prove the "modus ponens" rule as applied to translations.
Suppose we have $\vdash translation(a)$ and $\vdash translation(a \to b)$. Then we have $\vdash translation(a) \to translation(b)$. Then we have $\vdash translation(b)$.
This forms the base case and the inductive step for proving that for all derivations $\vdash_{classical} \psi$ in the Hilbert system, there is a derivation $\vdash \psi$.
It's also pretty easy to show that for all $\psi(x_1, \ldots, x_n)$, we have $\vdash_{classical} \forall x_1 \ldots \forall x_n . \psi(x_1, \ldots, x_n) \iff translation(\psi(x_1, \ldots, x_n))$. This follows from induction on $\psi$.
So in particular, for $\phi$ a sentence, we have $\vdash_{classical} \phi \iff translation(\phi)$. So if $\vdash \phi$, then $\vdash_{classical} \phi$, and thus $\vdash_{classical} translation(\phi)$.
Therefore, for all sentences $\phi$, we have $\vdash_{classical} \phi$ if and only if $\vdash translation(\phi)$.
Now consider a set $S$ of sentences over $V$. Let $translation(S) = \{translation(s) \mid s \in S\}$. I claim that $translation(S) \vdash translation(\psi)$ if and only if $S \vdash_{classical} \psi$.
For note that given any sentences $s_1, \ldots, s_n, \phi$, we have $\vdash translation(s_1) \land \cdots \land translation(s_2) \to translation(\phi)$ if and only if $\vdash translation(s_1 \cdots\ldots \land s_n \to \phi)$ if and only if $\vdash_{classical} s_1 \land \cdots \land s_n \to \phi$.
If $translation(S) \vdash translation(\psi)$, then there are $s_1, \ldots, s_n \in S$ such that $\vdash translation(s_1) \land \cdots \land translation(s_n) \vdash translation(\psi)$, and therefore $\vdash_{classical} s_1 \land \cdots \land s_n \to \psi$, and therefore $S \vdash_{classical} \phi$. And conversely, if $S \vdash_{classical} \phi$ then there are $s_1, \ldots, s_n \in S$ such that $\vdash_{classical} s_1 \land \cdots \land s_n \to \psi$, and therefore $\vdash translation(s_1) \land \cdots \land translation(s_n) \to translation(\psi)$, and therefore $translation(s) \vdash translation(\psi)$.
This gives us the following result:
Let $S$ be a set of sentences. Then $S$ is logically inconsistent in classical logic if and only if $translation(S)$ is logically consistent in intuitionist logic.
In other words, $S \vdash_{classical} \bot$ if and only if $S \vdash translation(\bot)$. But $translation(\bot) = \bot$.
Let's call a set $S$ of sentences "nice" if and only if $S \vdash translation(S)$. Then if $S$ is nice, we see that $S$ is logically inconsistent in classical logic if and only if $S$ is logically inconsistent in constructive logic.
There are quite a few nice theories which can be described this way. For example, let $V$ be the 1-sorted vocabulary $\{0, S, +, \cdot\}$, and let $S$ be the axioms of Peano Arithmetic. Then $S \vdash translation(S)$, as can be manually verified. Thus, classical Peano Arithmetic is equiconsistent with constructive Peano arithmetic (also known as Heyting arithmetic).
Unfortunately, not all theories can be approached in this way. For example, the axioms of ZF are not "nice" (if you use replacement and $\in$-induction, that is). However, using some more advanced techniques, we can prove that ZF is equiconsistent with intuitionist ZF formulated using collection. There are many other equiconsistency proofs applying to weaker versions of set theory such as ETCS.
So in this sense, classical logic can no more lead to contradiction than intuitionist logic can in most common cases.
If you don't believe the law of excluded middle, however, then classical logic proves something "wrong" just by accepting the law of excluded middle. This is more of a philosophical argument than a mathematical one.