Necessitation

In modal logics with a necessity modality \Box, the rule of necessitation is a deductive rule that usually takes the form

\frac{
  \vdash \phi
}{
  \Gamma \vdash \Box \phi
}

That is: if \phi is a theorem of the system (with no assumptions), then \Box \phi 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 \textsf{K} axiom, namely

  \Box(\phi \to \psi) \to \Box \phi \to \Box \psi

There are weaker systems of modal logic that do not satisfy necessitation.

References

@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}
}