Does the deduction theorem fail for modal logic?

Research output: Contribution to journalArticleScientificpeer-review


Various sources in the literature claim that the deduction theorem does not hold for normal modal or epistemic logic, whereas others present versions of the deduction theorem for several normal modal systems. It is shown here that the appar- ent problem arises from an objectionable notion of derivability from assumptions in an axiomatic system. When a traditional Hilbert-type system of axiomatic logic is generalized into a system for derivations from assumptions, the necessitation rule has to be modified in a way that restricts its use to cases in which the premiss does not depend on assumptions. This restriction is entirely analogous to the restriction of the rule of universal generalization of first-order logic. A necessitation rule with this restriction permits a proof of the deduction theorem in its usual formulation. Other suggestions presented in the literature to deal with the problem are reviewed, and the present solution is argued to be preferable to the other alternatives. A contraction- and cut-free sequent calculus equivalent to the Hilbert system for basic modal logic shows the standard failure argument untenable by proving the underivability of Box A from A.
Original languageEnglish
Issue number3
Pages (from-to)849-867
Number of pages19
Publication statusPublished - 2012
MoE publication typeA1 Journal article-refereed

Bibliographical note


Fields of Science

  • 611 Philosophy
  • Logic
  • Proof Theory
  • Modal logic
  • Sequent calculus

Cite this