Is there an axiomatic system where the deduction theorem does not hold?

Failures of the deduction theorem are one of the more mysterious topics in logic, in my experience. The motto is that axioms are stronger than rules. Here is the simplest nontrivial example that I know. Start with propositional logic with two variables $A$ and $B$. Add the single new rule of inference $A \vdash B$ to the usual Hilbertstyle deductive system, with no new axioms. Note that this does not in any way change the collection of formulas that can be derived. (Proof: the first time you use the new rule, you already had to derive $A$ in the original system, but you cannot, because the original system only derives tautologies. So you can never use the new rule.) Thus the new system has the rule $A \vdash B$ but does not derive $A \to B$, and hence the deduction theorem fails. But this new system is not completely trivial. If we add $A$ as a new axiom, then we can derive $B$ in the expanded logic, which we cannot do in ordinary propositional logic. So there is an interplay between the rules of inference and the axioms of a given theory. The deduction theorem for first order logic shows that this interplay is very well behaved in that context: an arbitrary firstorder theory $\Delta$ with the usual deductive system has the derived rule $\phi \vdash \psi$ if and only if it has the derived rule $\vdash \phi \to \psi$. In retrospect, there is no reason to expect this to hold for arbitrary sets of deduction rules, because new axioms may give additional strength to the existing rules. As François G. Dorais has mentioned in the comments, more complicated examples are known in proof theory. They are similar to the above example in that they weaken an axiom by replacing it with a rule. The general idea is that an extensionality axiom of the form $x = y \to f(x) = f(y)$ might be replaced with a rule $x = y \vdash f(x) = f(y)$. This suggests immediately how the deduction theorem can fail: if $x$ and $y$ are terms that are not provably equal, but are equal in some interpretation, then the extensionality axiom might fail in that interpretation even if the rule of inference is satisfied in some sense. But this is just a heuristic sketch of the argument. For a short, rigorous explanation, see "A note on Spector’s quantifierfree rule of extensionality" by Ulrich Kohlenbach, Archive for Mathematical Logic 40:2 (2001), pp 8992. 


Abstract Algebraic Logic has studied the connections between various forms of the Deduction Theorem, for a given algebraizable logic, and universal algebraic notions such as the existence of definable principal congruence relations for its equivalent quasivariety. For a careful explanation of this, see "Abstract Algebraic Logic and the Deduction Theorem", by Blok and Pigozzi. Such tools help showing that the Deduction Theorem fails for some linear logics, or for orthomodular logic. 


Carl's answer is very good, but I will add something which I think may be useful from point of view of understanding the problem. As an example you may take as well some standard axiomatic formalization of firstorder logic with the rule of generalization: $$\frac{\varphi}{\forall x\varphi}$$ Then for any formula $\varphi(x)$ with $x$ free it is the case that $\varphi(x)\vdash\forall x\varphi(x)$, but in general it is not the case that $\vdash\varphi(x)\rightarrow\forall x\varphi(x)$. So deduction theorem does hold but in a slightly modified form: If $\varphi\vdash\forall x\varphi$, then $\vdash\varphi\rightarrow\forall x\varphi$, provided that the rule of generalization was not applied with respect to variables free in $\varphi$. Yet another example may be some systems of modal logic with the rule of necessitation: $$\frac{\varphi}{\square\varphi}$$ $\varphi\rightarrow\square\varphi$ usually is NOT a thesis of such systems. 


I use Polish notation here, where "C" indicates a conditional which is an operator of two arguments. The formation rules go: 1) all lower case letters with or without numerical subscripts are formulas. 2) If "x" and "y" are formulas, then Cxy is a formula. 3) For the present purpose, only strings which are formulas according to 1) and 2) are formulas. I'll assume that if the deduction theorem holds, then the system has CpCqp (Simp) and CCpCqrCCpqCpr (Frege) as theses ("theorems" in the object logic). If that assumption holds, you only need to find logical calculi where either Frege or Simp do not hold, and the deduction theorem will fail. Now let's concentrate our attention on axiomatic systems A where the axiom(s) are tautologies in classical propositional logic, and the only rule of inference of any system belonging to A is condensed detachment "D" (perhaps we could allow ordinary substitution of variables and ordinary modus ponens here and things will still work as follows). Consequently, we can generate as many (countable) systems where the deduction theorem fails as we want from a single thesis of classical propositional logic (though not necessarily any thesis of classical logic, since, for example, (CCNppp, D) has only one thesis). The axiom I choose here is CCpqCCqrCpr (Syll) (plenty of others will do also!). Syll holds for Lukasiewicz's 3valued logic, but Frege does not hold for such a system. Consequently, Frege fails for the entire system (Syll, D). But, since Frege fails for (Syll, D), Frege will also fail for (Syll', D) where Syll' is a thesis obtainable in (Syll, D). Thus, any system (Syll*, D) will not have the deduction theorem. How many systems (Syll', D) exist? Well, the variable "r" in Syll does not appear anywhere in Syll's antecedent Cpq (and every thesis of syll is of this type). Thus, given countably infinite variables, we can observe the sequence (Syll, CCCCqrCprsCCpqs, ...) where any thesis x after Syll is obtained from D(Syll).(x1) (if x=1, then we have D(Syll).Syll, if x=2, then we have D(Syll).(CCCCqrCprsCCpqs), and so on). Thus, (Syll, D) has countably infinite theses, which, with the above implies at least countably infinite systems where the deduction theorem fails. LukasiewiczWajsberg 3valued logic, BCI, BCK, relevant calculi, Lukasiewicz infinitevalued logic, and equivalential calculi constitute some of the systems studied where the deduction theorem fails (or has a modified form). 

