Deduction theorem

Question

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

Answer 1

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.

Answer 2

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.

Answer 3

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.

Answer 4

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

Answer 5

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.

Answer 6

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).