intuitionistic interpretation of classical logic 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 formula C* such that C and C* are classically equivalent and C* is intuitionistically derivable if C is 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.
 A: Note that the statements are classically equivalent; the intuitionistically derivable statement may be intuitionistically weaker.
For example, the classical ‘law of the excluded middle’ $\lnot A \vee A$ is classically equivalent to $\top$, which is certainly intuitionistically derivable, even though the law of the excluded middle is not.
Does that help to understand the meaning of the statement?
EDIT:  fqpc points out that the symbol $\top$ might be non-standard in this context.  It probably comes from too much recent reading of the computer-science literature, where it's used for ‘top’ (the type of which all other types are a subtype; as opposed to ‘bottom’, $\bot$, which is a subtype of all other types)—and, indeed, that's the TeX code for it.
I thought it was common usage as a sort of visual pun on ‘true’ or ‘tautology’—an abbreviation for the empty statement.
A: There exists a translation, T, applicable to both propositions and proofs with the property that:
If $P$ is a classical proof of $\phi$ then $P^T$ is an intuitionistic proof of $\phi^T$.
(Trivially, any intuitionistic proof is also a perfectly good classical one.)
The details of some versions of the translation of the proof can be found in computer science texts under the name "CPS translation", though with different notation. Surprisingly this translation has an alter-ego as one of the stages when compiling certain programming languages.
Update: Adding (1) more detail and (2) something on the CPS translation.
(1) These translations don't allow you to completely remove double-negation elimination from classical proofs. But they do allow you to pull all of the double negation eliminations all the way out of the body of the proof to the very last line. So starting with a classical proof of $\phi$ we can translate it into an intuitionistic proof of $\neg\neg\phi$ and then we can tack one double negation elimination step onto the end to turn this back into a classical proof of $\phi$.
(2) According to the Curry-Howard isomorphism, a proof $P$ of a theorem $\phi$ can be interpreted as a program $P$ that produces a result of type $\phi$. When we convert a program to "continuation passing style", instead of just accepting a result of type $\phi$ back from our program, we instead write a program that accepts an extra argument (known as a continuation) that tells the program what it should do with its result. Ie. instead of writing a program of type $\phi$ we write a program of type $(\phi\rightarrow k)\rightarrow k$. The continuation is the extra argument of type $\phi\rightarrow k$ and we now get a final result of type $k$. The CPS translation takes an already existing program of type $\phi$ and converts it to one of type $(\phi\rightarrow k)\rightarrow k$. It's a bit fiddly but you can get a translation by following your nose, so to speak. Every function that your program calls also has to be modified so that it too uses the continuation and you thread the continuation all the way through the code.
But by the Curry-Howard isomorphism, this means you're translating a proof of the proposition $\phi$ into a proof of $(\phi\rightarrow k)\rightarrow k$. This is basically a version of the Godel-Gentzen translation as described in Constructivism in Mathematics: an Introduction Studies in Logic and the Foundations of Mathematics (by A. S. Troelstra and D. van Dalen.) A nice result of this is that you can now interpret classical proofs as computer programs.
I think it is a pretty amazing fact that you can take some esoteric mathematics comparing two systems of logic and turn it directly into code that can be used in a compiler.
A: The translation you refer to is just the double-negative. That is, C is classically derivable if and only if not-not-C is intuitionistically derivable. 
What this fact shows is that the use of the law of excluded middle in classical logic can be contained entirely in the proof that C and not-not-C are equivalent.
Edit. Here is a reference to the Gödel–Gentzen negative translation, which explains the translation. The situation is that in propositional logic, one can just use the double negation, but in first order logic, one must perform double negation hereditarily, applying the translation to the subformulas fo the formula. The basic idea is that classical laws of deduction become intuitionistically valid for the double negated forms.
A: The translations into INT are derivable iff the classical expressions so translated are derivable. 
For instance, A v ¬ A is not intuitionistically derivable. A v ~ A is classically derivable. Now, one of the available translations from classical to intuitionistic is the Gödel translation, such that:
g(A v ~ A) = ¬ (¬ g(A) & ¬ g(~ A)) = ¬ (¬ ¬ ¬ A & ¬ ¬ g(A)) = ¬ (¬ ¬ ¬ A & ¬ ¬ ¬ ¬ A). This should be intuitionistically derivable then although [A v ¬ A] is not.
