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

<p>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$. </p>

<p>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. </p>

CC BY-SA 3.0
2017-02-19T09:00:17.510Z
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.
Kai
CC BY-SA 3.0
2017-02-19T20:50:05.303Z
@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.
Neel Krishnaswami
CC BY-SA 3.0
2017-02-21T22:26:01.603Z
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.
Ohad Kammar
CC BY-SA 3.0
2017-02-22T09:53:00.997Z
@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!
Neel Krishnaswami
CC BY-SA 3.0
2017-02-22T13:56:49.327Z
I don't understand how you inferred that. Don't you mean $A \rightarrow \square\Diamond A$?
Ohad Kammar
CC BY-SA 3.0
2017-02-22T15:39:22.760Z
The unit of the adjunction (what you wrote) is indeed what distinguishes S4 from S5. However, I actually meant to write $\Diamond\Box A \to A$ (the counit of the adjunction), which is not AFAICT derivable from the standard axioms of S5.
Neel Krishnaswami
CC BY-SA 3.0
2017-02-22T18:03:43.403Z
I see. Perhaps you can instrument the following data into a counter-example over $\mathbf{Set}$. Choose $\Diamond A := A + 1$ and $\square B := B$. We then have $A \rightarrow A+1$, but not $\Diamond \square A \rightarrow A$ (take $A = \emptyset$).
Ohad Kammar
CC BY-SA 4.0
2023-01-08T22:45:37.077Z
@NeelKrishnaswami I think $\Diamond \Box A\rightarrow A$ *is* S5-derivable. The semantic argument is that S5 corresponds to frames where the accessibility relation is an equivalence relation, and in such a frame if some world that $w$ sees sees only worlds where $A$ holds then $A$ must hold at $w$. Am I missing something?
Noah Schweber
<reference-request><lo.logic><ct.category-theory><proof-theory>
Categorical semantics for S5 modal logic?
Neel Krishnaswami
# Categorical semantics for S5 modal logic?

(Asked by: username_0 on 2017-02-18)

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.

**Tags:** reference-request, lo.logic, ct.category-theory, proof-theory

> **Comments:**
> **username_1**: 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.  
> **username_0**: @username_1: 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.  
> **username_2**: 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.  
> **username_0**: @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!  
> **username_2**: I don't understand how you inferred that. Don't you mean $A \rightarrow \square\Diamond A$?  
> **username_0**: The unit of the adjunction (what you wrote) is indeed what distinguishes S4 from S5. However, I actually meant to write $\Diamond\Box A \to A$ (the counit of the adjunction), which is not AFAICT derivable from the standard axioms of S5.  
> **username_2**: I see. Perhaps you can instrument the following data into a counter-example over $\mathbf{Set}$. Choose $\Diamond A := A + 1$ and $\square B := B$. We then have $A \rightarrow A+1$, but not $\Diamond \square A \rightarrow A$ (take $A = \emptyset$).  
> **username_3**: @NeelKrishnaswami I think $\Diamond \Box A\rightarrow A$ *is* S5-derivable. The semantic argument is that S5 corresponds to frames where the accessibility relation is an equivalence relation, and in such a frame if some world that $w$ sees sees only worlds where $A$ holds then $A$ must hold at $w$. Am I missing something?  

---

## 0 answers

