Philosophy Stack Exchange is a question and answer site for those interested in the study of the fundamental nature of knowledge, reality, and existence. It only takes a minute to sign up.
Sign up to join this community
The premises of the S5 system are:
□p → □□ p
◊p → □ ◊ p
(Note that □ is an actual square, not the missing-symbol placeholder).
What does the first one mean? If □p is what is necessary in all accessible worlds, how is there any difference between it and □□ p? Does the latter mean that p is necessary in all (accessible and not accessible) possible worlds?
In general □□ p and □ p are very different. Thinking in terms of Kripke frames, they only obviously coincide if the accessibility relation is transitive. This is true for Kripke frames validating S5, but not in general.
There are also important examples outside of the context of Kripke frames, provability logic being a huge example. In general, a theory can prove that it proves something without actually proving that thing: e.g. by Godel's incompleteness theorem, the theory T=ZFC+"ZFC is inconsistent" is consistent and hence does not prove 0=1 but it does prove that it proves 0=1. Interpreting "□" as "proves," we get that □□ p and □ p are not equivalent in the sense of T (the issue being that T is not Sigma1-sound). Indeed, Lob's theorem - which in provability logic is the scheme □(□p→p)→□p - is a very important example of this non-collapse even in the context of "nice" theories like ZFC.
To add to the existing answer, there's also epistemic logic, where □ is interpreted as knowledge (relative to a given subject).
Possible worlds in such a system are worlds that are consistent with the subject's current information. Since necessity is truth in all possible worlds, it means in epistemic logic that if something is necessary then it just follows from your information (its negation is inconsistent with your information). At least in an idealized sense, necessity is knowledge.
"□p" in epistemic logic means that you know that p, and "□□p" means that you know that you know that p. The two are not the same. For instance, if p is the statement that it's raining, then by knowing p you know something about the weather, but by knowing that you know p you know something about yourself. It's not obvious whether □□p follows from □p. The claim that it does is controversial in epistemology and is known as the KK principle.
