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 residuated 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. And 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 already as an inference rule. It is the right implication introduction rule. Bye [1]: http://research.microsoft.com/en-us/events/lucacardellifest/ [2]: http://www.helsinki.fi/~negri/selected_pub/dedthm.pdf