CatGloss
With these ideas in mind we move to the formal details of Kripke’s semantics. Let $ mathbf{P}=(P