Does the deduction theorem fail for modal logic?

Research output: Contribution to journalArticleScientificpeer-review

Abstract

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
JournalSynthese
Volume187
Issue number3
Pages (from-to)849-867
Number of pages19
ISSN0039-7857
DOIs
Publication statusPublished - 2012
MoE publication typeA1 Journal article-refereed

Bibliographical note

WOS:000309242100004
Volume:
Proceeding volume:

Fields of Science

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

Cite this

@article{35d458218cc6411da2fb93336f90372e,
title = "Does the deduction theorem fail for modal logic?",
abstract = "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.",
keywords = "611 Philosophy, Logic, Proof Theory, Modal logic, Sequent calculus",
author = "Raul Hakli and Sara Negri",
note = "WOS:000309242100004 Volume: Proceeding volume:",
year = "2012",
doi = "10.1007/s11229-011-9905-9",
language = "English",
volume = "187",
pages = "849--867",
journal = "Synthese",
issn = "0039-7857",
publisher = "Springer",
number = "3",

}

Does the deduction theorem fail for modal logic? / Hakli, Raul; Negri, Sara.

In: Synthese, Vol. 187, No. 3, 2012, p. 849-867.

Research output: Contribution to journalArticleScientificpeer-review

TY - JOUR

T1 - Does the deduction theorem fail for modal logic?

AU - Hakli, Raul

AU - Negri, Sara

N1 - WOS:000309242100004 Volume: Proceeding volume:

PY - 2012

Y1 - 2012

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

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

KW - 611 Philosophy

KW - Logic

KW - Proof Theory

KW - Modal logic

KW - Sequent calculus

U2 - 10.1007/s11229-011-9905-9

DO - 10.1007/s11229-011-9905-9

M3 - Article

VL - 187

SP - 849

EP - 867

JO - Synthese

JF - Synthese

SN - 0039-7857

IS - 3

ER -