[Math] intuitionistic interpretation of classical logic

Question

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.

Answer 1

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.