Modal Logic Question: In S5 modal logic is p and □◊¬p a contradiction?

Question

In S5 modal logic is p and □◊¬p a contradiction?

Intuitively, I feel like it is because if it is possible that ¬p then we can't already have p.

If my intuition is correct, how do I show this? If not could someone show me why my intuition is wrong?

Answer 1

No. Consider the Kripke frame with two worlds, both accessible to themselves and each other. And let one world have $p$ true, and the other false. The world where $p$ is true has $p\land\square\lozenge\lnot p$ true.

As for the intuition, I would say that just cause something is definitely possibly not the case doesn’t imply it’s not the case. “p” does not intuitively translate to “we already have $p$”… this way of thinking seems suited to Kripke semantics for intuitionistic logic, but not S5.