Does anyone know where I can look to find out what the generally categorical semantics of S5 is?

For S4, the answer is well-known: we want a Cartesian closed category with a product-preserving comonad to model $\Box$ and a monad strong with respect to the comonad to model $\Diamond$.

In Awodey's book on category theory, on page 235 he remarks in passing that this setup becomes S5 when the monad is left adjoint to the comonad. However, he doesn't give a reference.

  • $\begingroup$ Now you've peeked my curiosity: what is the point of having such a categorical semantics? Whenever I used S5 it felt like cutting corners. Its properties are really convenient but the implications of logical omniscience were hardly justifiable in the context of systems constrained by computational reality. $\endgroup$ – Kai Feb 19 '17 at 9:00
  • $\begingroup$ @Kai: I have worked out a natural deduction calculus for what I believe is S5. Since a categorical semantics gives a semantics for proofs, it's very convenient for checking whether this calculus can be interpreted the way I want it to. (For example, I want to make sure normalization is semantics-preserving.) The reason I'm interested in this is that the standard (McCain/Turner/Pearl) accounts of causal inference model causal entailment as $A \to \Box B$, and I'm curious if this can lead to any abstractions for imperative programming which differ from the common monadic abstractions. $\endgroup$ – Neel Krishnaswami Feb 19 '17 at 20:50
  • $\begingroup$ This situation has only degenerate set-theoretic models. I don't know if that's a bug or feature. Specificially, if $\Diamond \dashv \square$ are an adjoint pair of monad $\Diamond$ and a comonad $\square$ over $\mathbf{Set}$, then the following argument shows $\Diamond \cong - \times A$ and $\square \cong (-)^A$: Choose (of course) $A := \Diamond 1$ and calculate: $\Diamond X \cong \Diamond \sum_{x \in X} 1 \cong \sum_{x \in X} \Diamond 1 = \sum_{x \in X} A \cong X\times A$. You can probably repeat a similar argument when the category is sufficiently concrete and well-behaved. $\endgroup$ – Ohad Kammar Feb 21 '17 at 22:26
  • $\begingroup$ @OhadKammar: Now I think Awodey's semantics can't be right: if $\Diamond$ is left adjoint to $\Box$, then $\Box \Diamond A \to A$. I guess my question is still a question! $\endgroup$ – Neel Krishnaswami Feb 22 '17 at 9:53
  • $\begingroup$ I don't understand how you inferred that. Don't you mean $A \rightarrow \square\Diamond A$? $\endgroup$ – Ohad Kammar Feb 22 '17 at 13:56

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Browse other questions tagged or ask your own question.