In modal logic, is $\lnot\square P\equiv\lozenge\lnot P$?

Question

"Possibly" and "necessarily" seem very much like "exists" and "for-all", but does the following hold true: $\neg \square P \equiv \lozenge \neg P$ in the same way as $\neg\forall P \equiv \exists\neg P$ ?

From the definition of "necessarily" in my book, being that $P$ should be true in all possible worlds, it seems to be so.

A corner case will be if there are no possible worlds. In this case, the "necessarily" is vacuously true, so its negation is false; at the same time, there are no possible worlds whatsoever, so there's no world where $\lnot P$ is possible, so the right-hand statement is false as well.

Is this so, or is my reasoning flawed?

Answer 1

Yes. There's a strong convention that $\Box$ and $\Diamond$ are always each other's duals, even in special-purpose modal logics. When the propositional substratum is classical, this implies that $\neg\Box\equiv \Diamond\neg$ and $\Box\neg\equiv\neg\Diamond$.

For example, when $\Box P \leftrightarrow \neg\Diamond\neg P$ is an axiom (or the definition of $\Box$ as an abbreviation), you get these laws by either negating both sides or letting $P$ be $\neg Q$, and then applying double-negation elimination.

If one wants to define a system with two unary modal connectives that are not related in this way, one had better choose a different symbol for one of them.

Answer 2

In classical modal logic, □ and ◊ are defined to be De Morgan duals, and so the relation necessarily holds for all classical modal logics, even non-normal modal logics.

In intuitionistic modal logic, the duality between the modalities is generally looser and the relation generally does not hold. Typically in intuitionistic modal logics, the meaning of one modality does not determine the other, but the two are stipulated to satisfy a relation, such as being in a Galois connection.

One can find an example of an intuitionistic modal formula that does satisfy this equation easily. Classical S5 is essentially equivalent to monadic predicate logic, and intuitionistic monadic predicate logic corresponds to an intuitionistic variant of S5, call it S5i. Then (¬□P)→◊¬P is a theorem of S5i iff (¬∀P)→∃¬P is a theorem of intuitionistic predicate logic, which it is not.