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?