Modal logic isn’t “correct” or “wrong”. It is a formalism. An extension atop propositional and predicate logic, in order to be able to express so-called modes, chiefly possibility and necessity. There exist other modes, like “sometimes” and “always” (in future and in the past), “permitted” and “obligatory”, etc. Predicate logic already provided “all” and “some”.
The way possibility and necessity are achieved as modes is with an abstract construct called a “possible world”. In simple terms, a possible world is something quite like a “way things could have been” (were they not quite as they happen to be in the actual world). More formally, one could imagine a possible world as a set of all true propositions. Every proposition one can construct that is not in the list, would then be false in that world. So long as a combination of propositions being true (and the entailed falseness of all the other ones) is not internally contradictory, any such combination is definitionally a possible world.
The modes are then defined as such: Let P be a proposition.
- The statement \Diamond P (read “Possibly P”) means “There exists a possible world where P is true”. That is to say, there exists some combination of truth values for all constructible propositions which is internally consistent and wherein P happens to be assigned the value \texttt{TRUE}.
- The statement \Box P (read “Necessarily P”) means “For all possible worlds W, P is true in W”. That is to say, there exists no way of combining truth values without either contradicting oneself or assigning \texttt{TRUE} to P.
What one quickly finds with these very basic definitions is difficulty to prove or disprove certain statements that combine multiple instances of a mode. For example, it is intuitive to conjecture that that just because P (i.e. P is true in the actual world) it does not follow that P is true in every possible world. But what if P=\Box Q? In that case Q is true in every possible world, but is it also true in every possible world, that from that world’s perspective Q is true in every possible world? On the one hand, it is still P, so the answer should be no. But if that’s the case, then what on earth does “every” even mean anymore? To put it briefly, naive modal logic is insufficient to decide in the abstract, for all versions of P whether P entails \Box P, and that sort of destroys the entire enterprise of introducing the modes in the first place, and we’re back on square one. If we are to formalize modes at all, what we invent for this purpose must allow us to formalize statements like “It is possible that it is possible that P”. Therefore, we need to decide on just exactly what making a statement about a possible world other than one’s own means. We need to decide which worlds any given world gets to “see”.
This is what’s called the accessibility relation between possible worlds. And there is not one relation that is universally agreed upon, because it all depends on which inferences one wants to make valid or not. The accessibility relation properties are the same as for algebraic relations: Symmetry and antisymmetry, reflexivity, and transitivity, and they mean exactly what one would expect.
It is not the case that modal logic in general claims that a proposition that is possibly necessary is necessarily necessary.
If, for example, accessibility is not transitive and symmetrical, then \Diamond\Box P means that there exists some world W_1, and if one were to look out of that world, every world W_1' one would then see is one where P is true. But without transitivity and symmetry it is not guaranteed that W_1 can see all of the worlds visible out of the actual world W_0, or out of which ever other worlds are hence visible. So it may be the case that there exists a possible world W_2 where \Box P is false, and therefore in W_0 the statement \Box\Box P is false, eventhough \Diamond\Box P is true.
If, on the other hand, accessibility is symmetrical and transitive, then \Box P being true in all worlds visible out of W_1 means \Box P is true in W_0 (symmetry), and \Box P is true in every other possible world, since through a recursive web all of them are visible to W_1 (transitivity). In that case, indeed \Diamond\Box P\therefore\Box\Box P is a valid inference.