Deduction theorem

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

-
Corollary 9.12 of Kohlenbach's Applied Proof Theory states that WE-HA$^\omega$ and hence WE-PA$^\omega$ fail to satisfy the deduction theorem. However, I must admit that I never fully understood what was going on there. –  François G. Dorais May 29 '13 at 20:08
Perhaps one should include "interesting" in front of "axiomatic system"? Even in an empty axiomatic system, A always follows from A, but in an empty axiomatic system, one cannot prove anything, much less A => A. By considering any set of axioms which do not allow the proof of A => A, the deduction theorem would still evidently not hold. –  abo May 29 '13 at 21:31
@abo: If you're willing to loosen the rules that much then "A always follows from A" is not even true: in a Hilbert system with just modus ponens and no axioms, A does not follow from A. –  François G. Dorais May 29 '13 at 22:14
I think for this question to make sense, we need a definition of "axiomatic system." For example, personally I would consider taking the deduction theorem as part of the definition of "axiomatic system;" I could in principle be talked out of it, but it seems like a reasonable requirement to make. –  Noah S May 29 '13 at 23:29
@François: How come? A is derivable from A by a one-line proof consisting of just A, even if your system has no logical axioms or rules. More generally, every Hilbert system defines a Tarski-style consequence relation, irrespective of the presence of any particular rules. –  Emil Jeřábek May 30 '13 at 11:57

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.

-
The link is broken; here is a pdf version –  Sniper Clown Jun 28 '13 at 1:24
@Mahmud: thank you. The link did work when I wrote the answer originally, so it must be an issue with the migration. –  Carl Mummert Jun 28 '13 at 2:40

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.

-
Bemvindo ao MO! –  Peter Arndt May 30 '13 at 17:42
Danke sehr, Peter! –  J Marcos May 30 '13 at 17:47
This is the answer. I’m sorry I can only upvote it once. –  Emil Jeřábek May 31 '13 at 12:43

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 first-order 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 3-valued 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).(x-1) (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.

Lukasiewicz-Wajsberg 3-valued logic, BCI, BCK, relevant calculi, Lukasiewicz infinite-valued logic, and equivalential calculi constitute some of the systems studied where the deduction theorem fails (or has a modified form).

-
It would help if you explained strings like CCCCqrCprsCCpqs - perhaps they are standard, but Octavio hasn't given any indication that s/he knows what that would mean. –  David Roberts Jun 28 '13 at 0:29
I agree with @David; meanwhile, there is this: en.wikipedia.org/wiki/Polish_notation –  Margaret Friedland Jun 28 '13 at 1:04
@DavidRoberts I'm not sure what you're looking for in terms of an explanation here. That said, I did add a small part on formation rules, if that helps. –  Doug Spoonwood Jun 28 '13 at 1:16
@DougSpoonwood That's great, thanks. –  David Roberts Jun 28 '13 at 1:18
I admire your insistence in voluntarily writing in a way which is essentially opaque to pretty much everyone else... :-/ –  Mariano Suárez-Alvarez Jun 28 '13 at 1:41