In modal logics with a necessity modality , the rule of necessitation is a deductive rule that usually takes the form
That is: if is a theorem of the system (with no assumptions), then is also a theorem (with any assumptions). One must be particularly careful in handling assumptions here, otherwise the deduction theorem for the proof system will fail: see [Hakli and Negri 2012].
Modal logics that satisfy the rule of necessitation are called normal. When coupled with the usual conjunction, all these logics prove the axiom, namely
There are weaker systems of modal logic that do not satisfy necessitation.
Hakli, Raul, and Sara Negri. 2012. ‘Does the Deduction Theorem Fail for Modal Logic?’ Synthese 187 (3): 849–67. https://doi.org/10.1007/s11229-011-9905-9.
@article{hakli_2012,
title = {Does the deduction theorem fail for modal logic?},
volume = {187},
doi = {10.1007/s11229-011-9905-9},
number = {3},
journal = {Synthese},
author = {Hakli, Raul and Negri, Sara},
year = {2012},
keywords = {Deduction theorem, Modal logic, Sequent calculus},
pages = {849--867}
}