Non-classical logics usually don't have a problem with the deduction theorem, as long as they have no relevancy based implication, i.e. if they are based on a residuate lattices. Many people on the other hand believe that the deduction theorem does not hold in modal logics, especially not in interesting logics such as temporal logic. A typical argument goes as follows. In modal logic we would have an inference rule: P ---- [] P And therefore if a deduction theorem would be available, we could proof P -> [] P, which is not desired. This argument is for example informally repeated in Temporal Logic, [The Lesser of Three Evils][1], Leslie Lamport, Microsoft Research, MSR-TR-2004-104. Fortunately matters are not that worse. A more detailed analysis is given by [Does the deduction theorem fail for modal logic?][2] Raul Hakli, Sara Negri, November 10, 2010. In a Hilbert Style calculus HK the above rule should be more precisely formulate as follows: |- A --------- G |- [] A The deduction theorem then holds. Since we cannot prove |- P in the first place, and therefore also not go to |- P -> [] P. Besides a Hilbert Style calculus, the paper also presents an equivalent Gentzen Style calculus which has the deduction theorem as an inference rule. Bye [1]: http://research.microsoft.com/en-us/events/lucacardellifest/ [2]: http://www.helsinki.fi/~negri/selected_pub/dedthm.pdf