Am I right to assume that in no modal logic, whether in K or in a logic where the accessibility relation is specified as either reflexive, symmetrical or transitive, does ”p implies necessarily p” hold? In what (if any) ways does the accessibility relation between worlds have to be qualified in order for this inference to be provable?

  • Temporal modal logic, like Aristotle's ship-battle discussion uses, presumes p implies necessarily p as an axiom -- which means it is provable. Only the future (even if it is the immediate future, or the immediate past to be known only in the future) has possibilities and requires arguments about necessity. Later modal logics often take a more abstract version of necessary. But this one is not dead.
    – user9166
    Jan 7, 2019 at 16:37
  • Very interesting! You mean that if we are speaking about the past, the inference could be provable?
    – simulacra
    Jan 11, 2019 at 15:49
  • The answer below makes sense, and renders this comment irrelevant, for this case. You aren't filtering p for temporal references. If you know the past and can totally predict the future, because it is all necessarily determined to be the same as the original world, you no longer have an interesting modality of necessity left to talk about. (So Scholastics who wanted primarily to talk about 'eternal' things then needed a different way of looking at necessity -- they pulled 'necessary' back to what could not have been otherwise rather than Aristotle's can no longer be otherwise)
    – user9166
    Jan 11, 2019 at 18:17
  • For materialists, if we are talking about the past, this is not just provable, it is an axiom, right? We cannot change the facts from which we must start. Things are as they are and have the histories they already have. So that is then uninteresting again.
    – user9166
    Jan 11, 2019 at 18:25

2 Answers 2


You are right.

If the equation p→☐p is provable, then the only world that is allowed to be accessible from world w is w itself. One could describe that as all worlds being isolated. More formally, this axiom forces the accessibility relation R to satisfy:

If wRv, then v=w.

The whole idea of having other worlds breaks down...

If R is also reflexive (i.e. if ☐p→p is an axiom), you can derive p↔☐p, and the logic behaves exactly as the usual propositional logic with an uninteresting additional symbol.


Your question is more interesting than it may seem at first.

Almost every modal logic includes an inference rule called "Necessitation" which was originally proposed by Goedel. This rule states:

"If p is a theorem, then ☐p is also a theorem"

So it's also interesting to ask why modal logic should include the Goedel inference rule, but not p→☐p as an axiom.

It is not true that a logic with the axiom p→☐p cannot allow for any world to be accessible other than to itself. For an example, consider a modal frame where the domain of possible worlds is a power set P(D) of some simple non-empty domain D. Then for accessibility take the subset containment relation w⊃v, (read as "greater or equal to") as the accessibility relation. This is a partial order, meaning it is reflexive, transitive, and anti-symmetric. This last property means:

  "If w⊃v and v⊃w then w=v"

In a frame like this, p→☐p is valid. It cannot be proven from any other axioms, but it's true in every frame whose accessibility relation is a partial order. So it could be an axiom.

What's even more interesting (to me, at least) is that nowhere in the literature is there any discussion at all of any such logic, or any such frame. If anyone knows of an exception, please share it in the comments!

It's perhaps understandable that such frames would be omitted, because in these frames necessity "disappears" into ordinary truth. For every possible world where p is true, ☐p is also true. And vice versa. So modality has almost no interest in such frames.

I take this as a justification for adopting the Goedel rule of Necessitation, instead of an axiom such as p→☐p. I only wish there were more discussion in the literature.

  • Isn't modal collapse the explanation of why not to include p→☐p as an axiom? Necessitation only applies to theorems, so it just reflects that 'analytic' truths are necessary. But p→☐p would not have any restrictions on p, so p can be any contingent truth, and that's the problem. If p is restricted to theorems ⊢ p→☐p just rephrases necessitation.
    – Conifold
    May 29, 2023 at 19:13
  • @Conifold. I think you have it right. Hughes and Cresswell use the name Triv for the modal system that includes p → ☐p and ◇p → p as axioms. It is a system of modal collapse, since it follows that ◇p, p and ☐p always have the same truth value. The necessitation rule is quite different: it entails ⊢¬◇⊥ so one might say that its role is to enforce that no impossible worlds are accessible. It leaves open exactly what counts as impossible.
    – Bumble
    May 30, 2023 at 1:39

You must log in to answer this question.

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