Every normal modal logic Σ contains ¬♢⊥.

The following proposition comes from this PDF: http://builds.openlogicproject.org/content/normal-modal-logic/normal-modal-logic.pdf (p.31)

It says: Every normal modal logic Σ contains ¬♢⊥.

The problem beneath it says to prove this. I don't really know how I would e able to prove this. Can someone help me?

The definition of a normal modal logic can be found under definition 3.5 it says:

A modal logic Σ is normal if it contains

□(p → q) → (□p → □q), (K)

♢p ↔ ¬□¬p (dual)

and is closed under necessitation, i.e., if φ ∈ Σ, then □φ ∈ Σ. Observe that while tautological implication is “fine-grained” enough to preserve truth at a world, the rule nec only preserves truth in a model (and hence also validity in a frame or in a class of frames).

Thank you!


Clue: you want to rewrite what you want to prove with a box. How?

Clue: what is the logical status of $\neg\bot$?

If the answer to the second doesn’t hit you immediately then perhaps it is propositional logic you first need to get clearer about!