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 Hilbert-style 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 first-order 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 quantifier-free rule of extensionality" by Ulrich Kohlenbach, Archive for Mathematical Logic 40:2 (2001), pp 89-92.

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 Hilbert-style 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 first-order 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 quantifier-free rule of extensionality" by Ulrich Kohlenbach, Archive for Mathematical Logic 40:2 (2001), pp 89-92.

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 Hilbert-style 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 first-order 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, 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 heuristic; look at "A note on Spector’s quantifier-free rule of extensionality" by Kohlenbach for a short and rigorous explanation.

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 Hilbert-style 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 first-order 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 quantifier-free rule of extensionality" by Ulrich Kohlenbach, Archive for Mathematical Logic 40:2 (2001), pp 89-92.