pub fn negative_introspection(knows_p: bool) -> bool
Negative introspection (axiom 5, S5): ¬Kφ → K¬Kφ — not-knowing implies knowing one doesn’t.
¬Kφ → K¬Kφ