# 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 Schweber 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
I am probably late, but consider the first system you described. Say you assume $A$ and you want to prove $B$. You could easily do it by your rule $A \vdash B$. However, this proof is not ok since $B$ does not have to be true. Hence, this system is unsound. Am I maybe misinterpreting your text? –  bellpeace Aug 24 '14 at 2:10
@bellpeace: the original system is sound for a particular class of models, namely those in which $A \to B$ holds. Whenever we add new rules of inference, we have to restrict the set of models to those for which the new rules are sound. Of course the system I described, with the additional inference rule, is not complete, and no example that answers the question can be complete in that sense. –  Carl Mummert Aug 24 '14 at 2:14

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.

-

Non-classical logics, such as paraconsistent logic etc.., 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 and don't try to avoid the positive paradox.

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, 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? Raul Hakli, Sara Negri, November 10, 2010. In a Hilbert Style calculus HK the above rule should be more precisely formulated 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

-
I don’t know why is it that many people believe otherwise, but modal logics do have a perfectly simple deduction theorem: $\Gamma,A\vdash B$ iff $\Gamma\vdash\Box^{\le n}A\to B$ for some $n$. While this is only a parametrized deduction theorem in the AAL sense, this is no different from the form of deduction theorem needed for most other nonclassical logics (in particular, noncontractive). –  Emil Jeřábek Sep 12 '14 at 21:12
+1. The solution of Negri and Hakli is elegant - they redefine the meaning of $\vdash$ so that what they have is not quite the standard Hilbert system (because they have changed the N rule to a weaker rule), but which does have a deduction theorem. Of course the original Hilbert system, with the full N rule, does not satisfy the deduction theorem, in that it admits $A \vdash \Box A$ as a derived rule but not $\vdash A \to \Box A$. Presumably one could apply a similar method to certain systems for first order logic as well. –  Carl Mummert Sep 14 '14 at 19:14

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
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
@Mariano, why don't you represent just yourself, and don't worry about your imagined pretty much everyone else. –  Włodzimierz Holsztyński Sep 13 '14 at 2:29

As it seems that on the research level notation is the biggest problem for some of people, I will share a link to classical notation of Łukasiewicz L3 system, where deductive theorem i classical meaning does not hohold ( but modified version - holds) - just take a look here: L3 Łukasiewicz logic and here: Łukasiewicz L3 system and reference:

Bergmann, Merrie (2008). An introduction to many-valued and fuzzy logic: semantics, algebras, and derivation systems. Cambridge University Press. p. 114. ISBN 978-0-521-88128-9.

-