Coalgebraic Logic over Sets

--- tags: seminar, maths, blute, ottawa, Coalgebras over Lawvere metric spaces --- $\newcommand{\sem}[1]{[\![#1]\!]}$ [Part of a presentation on Coalgebras over Lawvere Metric Spaces](https://hackmd.io/@alexhkurz/HkzAdwlAF) # Coalgebraic Logic over Sets Is there a systematic way to associate with every functor $T$ a modal logic? ## Example **Paradigmatic Example:** For coalgebras for the powerset functor (Kripke frames in modal logic), we define the semantics of a 'modal operator' for a coalgebra $\xi: x\to\mathcal PX$, for a state $x\in X$, for a formula $\varphi$ via \begin{gather} x\Vdash \Box\varphi \quad \Longleftrightarrow \quad \forall y\in \xi(x)\,.\, y\Vdash\varphi \end{gather} **Fact:** Modal formulas are invariant under bisimulation. ## The Framework How can we generalise this to arbitrary functors $T:Set\to Set$? To capture classical propositional (Boolean) logic, we start from the adjunction $P\dashv S:Set^{op}\to BA$ where $BA$ is the category of Boolean algebras. ![](https://hackmd.io/_uploads/HJ2c4TO0t.png) - $P$ and $S$ are contravariant functors. $PX$ is the algebra of propositions over $X$. In our examples it is given by $PX=Set(X,2)$. $SB$ is the set (space, spectrum) of $B$ given by $SX=BA(B,2)$. In both cases, $2$ stands for a suitable object of two truth values. - $T$ represents the type of one-step transitions of coalgebras $X\to TX$ as before. - $L$ is a functor on BA, usually defined to be the dual of $T$. The category of $L$-algebras is the algebraic semantics of the modal logic induced by $T$. To explain the last item, given a coalgebra $X\stackrel \xi \longrightarrow TX$, a state (world) $x\in X$ and a formula $\varphi$ in the initial $L$-algebra, we need to define the semantics $$x\Vdash\varphi.$$ This is achieved by lifting the functor $P$ to (co)algebras $$Coalg(T) \stackrel {\bar P}\longrightarrow Alg(L)$$ Now let $I$ be the initial $L$-algebra and $\sem-_\xi:I\to \bar P(X,\xi)$ the unique arrow into the `complex algebra' of $(X,\xi)$. We then define $$x\Vdash \varphi \ \stackrel{\rm def} \Longleftrightarrow\ x\in\sem{\varphi}_\xi.$$ In order to lift $P$, we need a natural transformation $$\delta: LP\to PT,$$ which gives rise to the definition $$\bar P(X\to TX) = LPX\to PTX \to PX.$$ Intuitively, as we will see in the examples, $\delta$ is the one-step semantics of the logic. The extension to general formulas is taken care of by the induction implicit in the initial algebra morphism $\sem-_\xi:I\to \bar P(X,\xi)$. **Example:** In classical modal logic we take $T=\mathcal P$ and $LB$ to be the free Boolean algebra generated by $\{\Box b\mid b\in B\}$ and quotiented by the equations stipulating that $\Box$ preserves finite conjunctions. Since $LB$ is a free Boolean algebra it suffices to define $\delta$ on generators. To capture the idea that $\Box b$ holds if the set of successors $c$ is a subset of $b$, we define $$ \delta_X(\Box b)=\{ c\in \mathcal P X \mid c\subseteq b\}.$$ **Remark:** To verify that the definition of $\delta_X$ indeed captures the familiar semantics of modal logic, we calculate \begin{align} x\Vdash \Box\varphi & \Longleftrightarrow x\in\sem{\Box\varphi}_\xi & \textrm{def of $\Vdash$}\\ & \Longleftrightarrow x\in \bar P\xi(\Box\sem{\varphi}_\xi) &\textrm{$\sem{-}_\xi$ is an $L$-algebra morphism}\\ & \Longleftrightarrow x\in P\xi(\delta_X(\Box\sem{\varphi}_\xi)) &\textrm{def of $\bar P$} \\ & \Longleftrightarrow \xi(x)\in \delta_X(\Box\sem{\varphi}_\xi) &\textrm{$P\xi=\xi^{-1}$} \\ & \Longleftrightarrow \xi(x)\in \{ c \mid c\subseteq \sem{\varphi}_\xi\} &\textrm{def of $\delta$} \\ & \Longleftrightarrow \xi(x)\subseteq\sem\varphi_\xi, & \textrm{set comprehension} \end{align} which also amounts to `chasing' an element $\Box\phi$ from the top-left corner to the bottom-right in the diagram defining the unique morphism $\sem-_\xi$ from the intial algebra $LI\to I$ to the dual $\bar P(X,\xi)$ of the coalgebra $\xi:X\to TX$: ![](https://hackmd.io/_uploads/S1JAHTu0t.png =600x) Importantly, the above generalises to arbitrary functors $T$ on $Set$ in a uniform way. ## Summary and Outlook Here are some facts worth emphasizing. - For every $T$, one can define $L$ as the dual of $T$. - Such a functor $L$ has a presentation by operations and equations. - It follows that the category $Alg(L)$ of algebras for the functor $L$ is a variety in the sense of universal algebra. - In particular, $Alg(L)$ is the algebraic semantics of a propositional modal logic. - To summarize, every set-functor $T$ induces a modal logic $L_T$ in a canonical way. - $L_T$ is - invariant under behavioural equivalence - complete for $T$-coalgebras - expressive [^expressive] if $T$ is finitary. - Logics are closed under composition, that is, $L_{T_1T_2}=L_{T_1}\circ L_{T_2}$. **Remark:** There is some **beautiful category theory** hiding behind these items. Many classical topics play a role, such as distributive laws, sifted colimits, reflexive coequalizers, monadic functors that do (or don't) compose, locally finitely presentable and algebraic categories, presentations of functors by operations and equations, presheaf categories and completion of categories, Stone type dualities, relation lifting, ... and even more will come once we move to enriched category theory. ## References More references and details for the items discussed above can be found in the following publications. A. Kurz, J. Rosicky: <a href="http://arxiv.org/pdf/1207.2732">Strongly complete logics for coalgebras.</a> LMCS 8 (3:14) 2012. (The draft from July 2006 for reference: <a href="papers/KR/strcompl.ps">.ps</a>, <a href="papers/KR/strcompl.pdf">.pdf</a>, <a href="papers/KR/strcompl.dvi">.dvi</a>). A. Kurz, D. Petrisan: [Presenting functors on many-sorted varieties and applications](https://www.sciencedirect.com/science/article/pii/S0890540110000970). Information and Computation, Volume 208, Issue 12, December 2010, Pages 1421-1446. (<a href="papers/cmcs08-j.pdf">pdf</a>) C. Cirstea, A. Kurz, D. Pattinson, L. Schröder, Y. Venema: Modal Logics are Coalgebraic. <a href="http://www.bcs.org/visions">BCS Visions in Computer Science</a> 2008. (<a href="papers/BCS08/ModalCoalg.pdf">.pdf </a>) M. Bonsangue, A. Kurz: Presenting Functors by Operations and Equations. January 2006 (supersedes drafts from Feb and Oct 2005). (<a href="papers/Fossacs06/fossacs06.dvi">.dvi</a> <a href="papers/Fossacs06/fossacs06.ps">.ps</a> <a href="papers/Fossacs06/fossacs06.pdf">.pdf</a>). Fossacs 2006. M. Bonsangue, A. Kurz: Duality for Logics of Transition Systems. Fossacs 2005. (replaces a draft of October 2004 and extends an <a href="http://sierra.nmsu.edu/morandi/TbilisiConference/Kurz.ps">abstract</a> presented at <a href="http://sierra.nmsu.edu/morandi/TbilisiConference/Home.html">TANCL </a>, Tbilisi 7 - 11 July 2003) (<a href="papers/Fossacs05/fossacs05.dvi">.dvi</a>, <a href="papers/Fossacs05/fossacs05.pdf">.pdf</a>, <a href="papers/Fossacs05/fossacs05.ps">.ps</a>) C. Kupke, A. Kurz, D. Pattinson: Algebraic Semantics for Coalgebraic Modal Logic. CMCS 2004. (<a href="papers/KKP-cmcs04/cmcs2004.entcs.dvi">.dvi</a>, <a href="papers/KKP-cmcs04/cmcs2004.entcs.pdf">.pdf (recompiled with diagrams)</a>) [^expressive]: A logic is expressive if any two states that are not behaviourally equivalent are distinguished by some formula.