Basically intuitionistic logic is classical logic minus the law of the excluded middle, i.e. $\neg A\vee A$ is not necessarily valid for all formulas. So I would take this to mean that classical logic allows one to prove more theorems but apparently this view is too naive because yesterday I read the following in a book on proof theory:

Given a formula

C, there is a translation giving a formulaC* such thatCandC* are classically equivalent andC* is intuitionistically derivable ifCis classically derivable. … The translation gives an interpretation of classical logic in intuitionistic logic.

How am I supposed to understand the above statement? Is it saying that every theorem that uses the law of excluded middle in its proof can be done without the law of excluded middle or is it saying something more subtle?

Edit: Thanks to the answers I received the interpretation of the quote is in fact much more subtle than I was thinking. The double negation translation allows us to prove $\neg\neg C=C^*$ if we can classically prove $C$ but in intuitionistic logic $\neg\neg C$ and $C$ are not necessarily equivalent. I think intuitively this means that there is a subtle semantic difference between $C$ and $\neg\neg C$. In intuitionistic logic a single classical theorem is potentially two intuitionistic theorems since knowing $\neg\neg C$ does not tell us much about $C$. So my naive interpretation was quite wrong. There are potentially more theorems in intuitionistic logic than there are in classical logic.

Edit 2: The last sentence is not precise and Reid Barton has an excellent comment on what I was actually thinking.

modallogic using the Godel translation. Basically you introduce a modality "provable", and view intuitionistic $A \to B$ as classical $provable(A) \to B$. So intuitionistic implications are weaker than classical ones, since their assumptions are stronger, but its conclusions are stronger than classical ones, since you get actual existence proofs. This contravariance makes comparing it to classical logic hard, and show why there are constructively legit principles that are false classically. (E.g., all functions are continuous.) $\endgroup$ – Neel Krishnaswami Dec 9 '09 at 16:18infinitelymany intuitionistically nonequivalent formulas in just one propositional variable. Search for Rieger–Nishimura lattice. $\endgroup$ – Emil Jeřábek supports Monica Dec 4 '14 at 15:29