Alethic modal logics for metaphysical possibility and necessity usually have the Necessitation Rule:

From ⊢P, infer ⊢□P.

Doesn’t this commit us to the meta-notion that logical necessity modulo some proof calculus implies metaphysical necessity? I can come up with a trivial consistent formal system that should invalidate this as an absolutely general principle. Take classical system K and add the axiom □(P&~P). This system cannot prove a contradiction since there is no T rule/axiom. Does that mean that falsehood is metaphysically necessary on this proof system? And if so, then how could such a system be logically possible?

  • K is too weak to fix □ as necessity rather than something else, obligation, for instance. According to SEP, □A→A "distinguishes logics for necessity from other logics in the modal family", so without it your system is not about necessity of any kind and with it it is inconsistent.
    – Conifold
    Jun 4, 2023 at 9:36
  • I’m not sure I agree with SEP, but I see what you’re saying.
    – PW_246
    Jun 4, 2023 at 14:53

1 Answer 1


Modal logics that include the necessitation rule are called normal. Not all modal systems are normal. Some of the non-normal logics are S1, S2 and S3, which are consistent with the necessitation rule, and S6, S7, S8 and S9, which are inconsistent with it.

The necessitation rule has the consequence ⊢¬◇⊥. In effect it excludes logically impossible worlds from being accessible to any world. You are correct to say that this has the consequence that logical necessity entails metaphysical necessity.

Your proposed system consisting of K + □(P & ¬P) would be consistent. In fact there is a modal system that Hughes and Cresswell call Ver that is simply K + □P so this would include the theorem □⊥ or □(P & ¬P) as a special case. As you say, without axiom T, □⊥ does not entail ⊥, so this system is not inconsistent. Its frame condition is a single world with no possible worlds accessible to it at all, not even itself. It is a normal modal logic though, since □P holds for all P, including theorems of the underlying logic, so the necessitation rule holds.

In the system Ver, □P holds for all P, even if P itself does not hold. Even □⊥ holds. This makes Ver rather weird. It would not be suitable for interpreting □ as 'necessarily'. Systems like Ver and Triv, which is K + (P → □P) + (□P → P), are not really meant to be useful modal logics. They are usually included in taxonomies of modal systems for the sake of completeness or for pedagogical purposes.

There are non-normal modal logics that allow for impossible worlds. These permit possibilities that lie beyond what is logically necessary. See, e.g. the SEP article on Impossible Worlds.

Hughes and Cresswell, A New Introduction to Modal Logic, 1996.

  • Thanks for your answer. I don’t think that K+(P → □P)+(◇P → P) is equivalent to Triv. Don’t you mean K+(P → □P)+(□P → P)?
    – PW_246
    Jun 4, 2023 at 18:54
  • 1
    You're right, that's better. Actually there are several equivalent ways to state Triv, e.g. D + (P → □P); or K + (P ↔ □P); or K + (P ↔ ◇P). Either way, P, ◇P and □P always have the same truth value.
    – Bumble
    Jun 4, 2023 at 19:42

You must log in to answer this question.

Not the answer you're looking for? Browse other questions tagged .