\documentclass[12pt,titlepage]{article}

\usepackage{amsmath}
\usepackage{mathrsfs}
\usepackage{amsfonts}
\usepackage{amssymb}
\usepackage{amsthm}
\usepackage{mathtools}
\usepackage{graphicx}
\usepackage{color}
\usepackage{ucs}
\usepackage[utf8x]{inputenc}
\usepackage{xparse}
\usepackage{hyperref}

%----Macros----------
%
% Unresolved issues:
%
%  \righttoleftarrow
%  \lefttorightarrow
%
%  \color{} with HTML colorspec
%  \bgcolor
%  \array with options (without options, it's equivalent to the matrix environment)

% Of the standard HTML named colors, white, black, red, green, blue and yellow
% are predefined in the color package. Here are the rest.
\definecolor{aqua}{rgb}{0, 1.0, 1.0}
\definecolor{fuschia}{rgb}{1.0, 0, 1.0}
\definecolor{gray}{rgb}{0.502, 0.502, 0.502}
\definecolor{lime}{rgb}{0, 1.0, 0}
\definecolor{maroon}{rgb}{0.502, 0, 0}
\definecolor{navy}{rgb}{0, 0, 0.502}
\definecolor{olive}{rgb}{0.502, 0.502, 0}
\definecolor{purple}{rgb}{0.502, 0, 0.502}
\definecolor{silver}{rgb}{0.753, 0.753, 0.753}
\definecolor{teal}{rgb}{0, 0.502, 0.502}

% Because of conflicts, \space and \mathop are converted to
% \itexspace and \operatorname during preprocessing.

% itex: \space{ht}{dp}{wd}
%
% Height and baseline depth measurements are in units of tenths of an ex while
% the width is measured in tenths of an em.
\makeatletter
\newdimen\itex@wd%
\newdimen\itex@dp%
\newdimen\itex@thd%
\def\itexspace#1#2#3{\itex@wd=#3em%
\itex@wd=0.1\itex@wd%
\itex@dp=#2ex%
\itex@dp=0.1\itex@dp%
\itex@thd=#1ex%
\itex@thd=0.1\itex@thd%
\advance\itex@thd\the\itex@dp%
\makebox[\the\itex@wd]{\rule[-\the\itex@dp]{0cm}{\the\itex@thd}}}
\makeatother

% \tensor and \multiscript
\makeatletter
\newif\if@sup
\newtoks\@sups
\def\append@sup#1{\edef\act{\noexpand\@sups={\the\@sups #1}}\act}%
\def\reset@sup{\@supfalse\@sups={}}%
\def\mk@scripts#1#2{\if #2/ \if@sup ^{\the\@sups}\fi \else%
  \ifx #1_ \if@sup ^{\the\@sups}\reset@sup \fi {}_{#2}%
  \else \append@sup#2 \@suptrue \fi%
  \expandafter\mk@scripts\fi}
\def\tensor#1#2{\reset@sup#1\mk@scripts#2_/}
\def\multiscripts#1#2#3{\reset@sup{}\mk@scripts#1_/#2%
  \reset@sup\mk@scripts#3_/}
\makeatother

% \slash
\makeatletter
\newbox\slashbox \setbox\slashbox=\hbox{$/$}
\def\itex@pslash#1{\setbox\@tempboxa=\hbox{$#1$}
  \@tempdima=0.5\wd\slashbox \advance\@tempdima 0.5\wd\@tempboxa
  \copy\slashbox \kern-\@tempdima \box\@tempboxa}
\def\slash{\protect\itex@pslash}
\makeatother

% math-mode versions of \rlap, etc
% from Alexander Perlis, "A complement to \smash, \llap, and lap"
%   http://math.arizona.edu/~aprl/publications/mathclap/
\def\clap#1{\hbox to 0pt{\hss#1\hss}}
\def\mathllap{\mathpalette\mathllapinternal}
\def\mathrlap{\mathpalette\mathrlapinternal}
\def\mathclap{\mathpalette\mathclapinternal}
\def\mathllapinternal#1#2{\llap{$\mathsurround=0pt#1{#2}$}}
\def\mathrlapinternal#1#2{\rlap{$\mathsurround=0pt#1{#2}$}}
\def\mathclapinternal#1#2{\clap{$\mathsurround=0pt#1{#2}$}}

% Renames \sqrt as \oldsqrt and redefine root to result in \sqrt[#1]{#2}
\let\oldroot\root
\def\root#1#2{\oldroot #1 \of{#2}}
\renewcommand{\sqrt}[2][]{\oldroot #1 \of{#2}}

% Manually declare the txfonts symbolsC font
\DeclareSymbolFont{symbolsC}{U}{txsyc}{m}{n}
\SetSymbolFont{symbolsC}{bold}{U}{txsyc}{bx}{n}
\DeclareFontSubstitution{U}{txsyc}{m}{n}

% Manually declare the stmaryrd font
\DeclareSymbolFont{stmry}{U}{stmry}{m}{n}
\SetSymbolFont{stmry}{bold}{U}{stmry}{b}{n}

% Manually declare the MnSymbolE font
\DeclareFontFamily{OMX}{MnSymbolE}{}
\DeclareSymbolFont{mnomx}{OMX}{MnSymbolE}{m}{n}
\SetSymbolFont{mnomx}{bold}{OMX}{MnSymbolE}{b}{n}
\DeclareFontShape{OMX}{MnSymbolE}{m}{n}{
    <-6>  MnSymbolE5
   <6-7>  MnSymbolE6
   <7-8>  MnSymbolE7
   <8-9>  MnSymbolE8
   <9-10> MnSymbolE9
  <10-12> MnSymbolE10
  <12->   MnSymbolE12}{}

% Declare specific arrows from txfonts without loading the full package
\makeatletter
\def\re@DeclareMathSymbol#1#2#3#4{%
    \let#1=\undefined
    \DeclareMathSymbol{#1}{#2}{#3}{#4}}
\re@DeclareMathSymbol{\neArrow}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\neArr}{\mathrel}{symbolsC}{116}
\re@DeclareMathSymbol{\seArrow}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\seArr}{\mathrel}{symbolsC}{117}
\re@DeclareMathSymbol{\nwArrow}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\nwArr}{\mathrel}{symbolsC}{118}
\re@DeclareMathSymbol{\swArrow}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\swArr}{\mathrel}{symbolsC}{119}
\re@DeclareMathSymbol{\nequiv}{\mathrel}{symbolsC}{46}
\re@DeclareMathSymbol{\Perp}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\Vbar}{\mathrel}{symbolsC}{121}
\re@DeclareMathSymbol{\sslash}{\mathrel}{stmry}{12}
\re@DeclareMathSymbol{\bigsqcap}{\mathop}{stmry}{"64}
\re@DeclareMathSymbol{\biginterleave}{\mathop}{stmry}{"6}
\re@DeclareMathSymbol{\invamp}{\mathrel}{symbolsC}{77}
\re@DeclareMathSymbol{\parr}{\mathrel}{symbolsC}{77}
\makeatother

% \llangle, \rrangle, \lmoustache and \rmoustache from MnSymbolE
\makeatletter
\def\Decl@Mn@Delim#1#2#3#4{%
  \if\relax\noexpand#1%
    \let#1\undefined
  \fi
  \DeclareMathDelimiter{#1}{#2}{#3}{#4}{#3}{#4}}
\def\Decl@Mn@Open#1#2#3{\Decl@Mn@Delim{#1}{\mathopen}{#2}{#3}}
\def\Decl@Mn@Close#1#2#3{\Decl@Mn@Delim{#1}{\mathclose}{#2}{#3}}
\Decl@Mn@Open{\llangle}{mnomx}{'164}
\Decl@Mn@Close{\rrangle}{mnomx}{'171}
\Decl@Mn@Open{\lmoustache}{mnomx}{'245}
\Decl@Mn@Close{\rmoustache}{mnomx}{'244}
\makeatother

% Widecheck
\makeatletter
\DeclareRobustCommand\widecheck[1]{{\mathpalette\@widecheck{#1}}}
\def\@widecheck#1#2{%
    \setbox\z@\hbox{\m@th$#1#2$}%
    \setbox\tw@\hbox{\m@th$#1%
       \widehat{%
          \vrule\@width\z@\@height\ht\z@
          \vrule\@height\z@\@width\wd\z@}$}%
    \dp\tw@-\ht\z@
    \@tempdima\ht\z@ \advance\@tempdima2\ht\tw@ \divide\@tempdima\thr@@
    \setbox\tw@\hbox{%
       \raise\@tempdima\hbox{\scalebox{1}[-1]{\lower\@tempdima\box
\tw@}}}%
    {\ooalign{\box\tw@ \cr \box\z@}}}
\makeatother

% \mathraisebox{voffset}[height][depth]{something}
\makeatletter
\NewDocumentCommand\mathraisebox{moom}{%
\IfNoValueTF{#2}{\def\@temp##1##2{\raisebox{#1}{$\m@th##1##2$}}}{%
\IfNoValueTF{#3}{\def\@temp##1##2{\raisebox{#1}[#2]{$\m@th##1##2$}}%
}{\def\@temp##1##2{\raisebox{#1}[#2][#3]{$\m@th##1##2$}}}}%
\mathpalette\@temp{#4}}
\makeatletter

% udots (taken from yhmath)
\makeatletter
\def\udots{\mathinner{\mkern2mu\raise\p@\hbox{.}
\mkern2mu\raise4\p@\hbox{.}\mkern1mu
\raise7\p@\vbox{\kern7\p@\hbox{.}}\mkern1mu}}
\makeatother

%% Fix array
\newcommand{\itexarray}[1]{\begin{matrix}#1\end{matrix}}
%% \itexnum is a noop
\newcommand{\itexnum}[1]{#1}

%% Renaming existing commands
\newcommand{\underoverset}[3]{\underset{#1}{\overset{#2}{#3}}}
\newcommand{\widevec}{\overrightarrow}
\newcommand{\darr}{\downarrow}
\newcommand{\nearr}{\nearrow}
\newcommand{\nwarr}{\nwarrow}
\newcommand{\searr}{\searrow}
\newcommand{\swarr}{\swarrow}
\newcommand{\curvearrowbotright}{\curvearrowright}
\newcommand{\uparr}{\uparrow}
\newcommand{\downuparrow}{\updownarrow}
\newcommand{\duparr}{\updownarrow}
\newcommand{\updarr}{\updownarrow}
\newcommand{\gt}{>}
\newcommand{\lt}{<}
\newcommand{\map}{\mapsto}
\newcommand{\embedsin}{\hookrightarrow}
\newcommand{\Alpha}{A}
\newcommand{\Beta}{B}
\newcommand{\Zeta}{Z}
\newcommand{\Eta}{H}
\newcommand{\Iota}{I}
\newcommand{\Kappa}{K}
\newcommand{\Mu}{M}
\newcommand{\Nu}{N}
\newcommand{\Rho}{P}
\newcommand{\Tau}{T}
\newcommand{\Upsi}{\Upsilon}
\newcommand{\omicron}{o}
\newcommand{\lang}{\langle}
\newcommand{\rang}{\rangle}
\newcommand{\Union}{\bigcup}
\newcommand{\Intersection}{\bigcap}
\newcommand{\Oplus}{\bigoplus}
\newcommand{\Otimes}{\bigotimes}
\newcommand{\Wedge}{\bigwedge}
\newcommand{\Vee}{\bigvee}
\newcommand{\coproduct}{\coprod}
\newcommand{\product}{\prod}
\newcommand{\closure}{\overline}
\newcommand{\integral}{\int}
\newcommand{\doubleintegral}{\iint}
\newcommand{\tripleintegral}{\iiint}
\newcommand{\quadrupleintegral}{\iiiint}
\newcommand{\conint}{\oint}
\newcommand{\contourintegral}{\oint}
\newcommand{\infinity}{\infty}
\newcommand{\bottom}{\bot}
\newcommand{\minusb}{\boxminus}
\newcommand{\plusb}{\boxplus}
\newcommand{\timesb}{\boxtimes}
\newcommand{\intersection}{\cap}
\newcommand{\union}{\cup}
\newcommand{\Del}{\nabla}
\newcommand{\odash}{\circleddash}
\newcommand{\negspace}{\!}
\newcommand{\widebar}{\overline}
\newcommand{\textsize}{\normalsize}
\renewcommand{\scriptsize}{\scriptstyle}
\newcommand{\scriptscriptsize}{\scriptscriptstyle}
\newcommand{\mathfr}{\mathfrak}
\newcommand{\statusline}[2]{#2}
\newcommand{\tooltip}[2]{#2}
\newcommand{\toggle}[2]{#2}

% Theorem Environments
\theoremstyle{plain}
\newtheorem{theorem}{Theorem}
\newtheorem{lemma}{Lemma}
\newtheorem{prop}{Proposition}
\newtheorem{cor}{Corollary}
\newtheorem*{utheorem}{Theorem}
\newtheorem*{ulemma}{Lemma}
\newtheorem*{uprop}{Proposition}
\newtheorem*{ucor}{Corollary}
\theoremstyle{definition}
\newtheorem{defn}{Definition}
\newtheorem{example}{Example}
\newtheorem*{udefn}{Definition}
\newtheorem*{uexample}{Example}
\theoremstyle{remark}
\newtheorem{remark}{Remark}
\newtheorem{note}{Note}
\newtheorem*{uremark}{Remark}
\newtheorem*{unote}{Note}

%-------------------------------------------------------------------

\begin{document}

%-------------------------------------------------------------------


\section*{algebraic- and coalgebraic semantics of modal logic}

This entry is about

\begin{itemize}%
\item Yde Venema, Algebras and Coalgebras, §6 (p.332-426)in Blackburn, van Benthem, Wolter, Handbook of modal logic, Elsevier, 2007.

\end{itemize}
The bibliography lists many articles of Robert Goldblatt and Bart Jacobs on modal logic.

\hypertarget{1_introduction}{}\subsection*{{1 Introduction}}\label{1_introduction}

(p.332)

(\ldots{})

An important difference of the coalgebraic approach compared to the algebraic one is that coalgebras \emph{generalize} rather than \emph{dualize} the model theory of modal logic. One may generalize the concept of modal logic from Kripke frames to arbitrary coalgebras. In fact the link between modal logic and coalgebra is so strong that one may claim that modal logic is the natural logic for coalgebras (just like equational logic is that for algebra)

\hypertarget{9_coalgebras_an_introduction}{}\subsection*{{9 Coalgebras: an introduction}}\label{9_coalgebras_an_introduction}

(p.389)

The notion of \emph{coalgebra} was formed in the sixties but the topic attracted a wider attention only when was realized that coalgebras can be seen as a general uniform theory of dynamic systems.

We list some applications (or examples) of the theory of coalgebras.

\begin{itemize}%
\item The main examples for coalgebras are \emph{Kripke frames}.


\item Aczel in [non-well founded sets] models transition systems and non-well founded sets as coalgebras.


\item Barwise-Moss in [Vicious Circles] discuss notions of circularity and self-reference (and many (other) applications).


\item Rutten [Automata and coinduction] on coalgebras and deterministic automata.



\end{itemize}
(Definition 146, p.392) A \emph{[[nLab:polynomial functor]]} is a $Set$-valued functor inductively defined by

\begin{displaymath}
K::=I | C | K_0 + K_1 | K_0\times K_1 | K^D
\end{displaymath}
where $I$ denotes the identity functor, $C$ denotes the constant functor on an object $C$, $K_0 +K_1$ denotes the coproduct functor of two polynomial functors, and likewise for the product functor, $K^D$ denotes the exponent functor $X\mapsto K(X)^D$.

A \emph{Kripke polynomial functor} is inductively defined by

\begin{displaymath}
K::=I | C | K_0 + K_1 | K_0\times K_1 | K^D | P K
\end{displaymath}
where $P K$ denotes the composition of a polynomial functor $K$ with the power set functor $P$.

(\ldots{})

(p.392) Kripke frames are $PI$-coalgebras, and Kripke models are coalgebras for the functor $PProp\times PI$.

Explanation: see [[modal logic]]

\hypertarget{13_modal_logic_and_coalgebras}{}\subsection*{{13 Modal logic and coalgebras}}\label{13_modal_logic_and_coalgebras}

(p.406)

The initial ideas in this section are attributed to L. Moss:

\begin{itemize}%
\item Coalgebraic logic. Annals of Pure and Applied Logic, 96:277–317, 1999. (Erratum published Ann.P.Appl.Log. 99:241–259, 1999).


\item J. Barwise and L. Moss. Vicious Circles, volume 60 of CSLI Lecture Notes. CSLI Publications, 1996.



\end{itemize}
\hypertarget{introduction}{}\subsubsection*{{Introduction}}\label{introduction}

Let $\phi$ be a set of formulas.

\begin{displaymath}
\nabla \phi:=\Box\bigvee \phi \wedge \bigwedge \diamond\phi
\end{displaymath}
where $\diamond \phi:=\{\diamond \varphi|\varphi\in \phi\}$ and likewise $\Box\phi$. Then we have

\begin{displaymath}
\diamond\varphi \simeq \nabla\{\varphi,\top\}
\end{displaymath}
\begin{displaymath}
\Box \varphi\simeq\nabla\varnothing\vee\nabla\{\varphi\}
\end{displaymath}
Let $\mathbb{S}:=\langle S,\lambda,R[\cdot]\rangle$ be a \emph{modal model in coalgebraic shape}(§9 Example 143). Then $\mathbb{S},s\Vdash\nabla \phi$ iff $(R[s],\phi)$ belongs to the \emph{relation lifting} (§11) $\overline{\mathcal{P}}(\Vdash_{\mathbb{S}})$ of the satisfaction relation $\Vdash_{\mathbb{S}}\subseteq S\times \phi$: Every $\varphi\in \Phi$ must hold at some successor $t\in R[s]$, and at every successor $t$ of some $\varphi\in \phi$ must hold.

The previous lines are the founding insights to \emph{coalgebraic logic} in which the same principle is applied to an arbitrary set functor $\Omega$ and the basic idea is to have

\begin{displaymath}
\mathbb{S},s\Vdash_{\mathbb{S}}\nabla P\;\text{iff}\; (P,\sigma(s))\in \overline{\Omega}(\Vdash_{\mathbb{S}}).
\end{displaymath}
In this situation, the satisfaction relation is much like a [[nLab:bisimulation]] between a language and a coalgebra; for this see

\begin{itemize}%
\item A. Baltag. A logic for coalgebraic simulation. In

\begin{itemize}%
\item H. Reichel, editor. Coalgebraic Methods in Computer Science (CMCS’00), volume 33 of Electronic Notes in Theoretical Computer Science. Elsevier, 2000.

\end{itemize}


\end{itemize}
\hypertarget{definition}{}\subsubsection*{{Definition}}\label{definition}

For the existence of the \emph{language of coalgebraic formulas for $\Omega$} it is necessary to allow class based algebras. This may be accomplished by letting $\Omega^+$ be the unique extension of $\Omega$ to a set based functor on the category $SET$ having classes as objects and set-continuous (standard) set functors as morphisms. In examples these functors are often [[polynomial functor]]s; e.g. Kripke functors are of this kind.

\begin{udefn}
The initial algebra of the functor $(P+\Omega)^+$ is called the \emph{language of coalgebraic formulas for $\Omega$} and is denoted by

\begin{displaymath}
\langle\mathcal{L}_\Omega, \bigwedge,\nabla\rangle.
\end{displaymath}
\end{udefn}
Unwinding this definition yields the following equivalent characterization.

\begin{udefn}
Let $\Omega:Set\to Set$ be (for convenience) be a set functor sending inlusions to inclusions (call this a \emph{standard set functor}). Then the \emph{language of coalgebraic formulas} denoted by $\mathcal{L}_\Omega$ is defined to be the least class $C$ such that

(1) $\phi\in \mathcal{L}_\Omega$ implies $\bigwedge\phi\in \mathcal{L}_\Omega$.

(2) $P\in \Omega^+(\mathcal{L}_\Omega)$ implies $\nabla P\in \mathcal{L}_\Omega$.Let $\Omega^+$ is the unique extension of $\Omega$ to a set based functor on the category $SET$ having classes as objects and set-continuous (standard) set functors as morphisms.

\end{udefn}
\begin{udefn}
Let $\Omega:\Set\to Set$ be a functor, let $\nu:\Omega\to Prop$ be some natural transformation, let $\bigwedge$ be some collection of natural transformations $\Omega\to \mathcal{P}$. then $\mathcal{L}_{\nu,\bigwedge}$ is the standard modal language obtained by taking $Prop$ as the collection off propositional variables, and $\tau_\bigwedge:=\{\diamond_\lambda|\lambda\in \bigwedge\}$ as the modal similarity type.

\end{udefn}
Predicate liftings (from $\mathcal{P} S\to \mathcal{P}\Omega S$ can be used to obtain modal operators.

\begin{udefn}
A \emph{predicate lifting for a set functor $\Omega$} is a natural transformation $\mu:\check{\mathcal{P}}\to \check{\mathcal{P}} \Omega$ where $\check{P}$ denotes the contravariant power set functor. Which each predicate lifting we can associate a modal operator $\diamond_\mu$ with the following semantics:

\begin{displaymath}
\mathbb{S},s\Vdash \diamond_\lambda \varphi\;\text{iff}\;\sigma(s)\in \mu_S([[\varphi]]).
\end{displaymath}
\end{udefn}
\hypertarget{references}{}\subsection*{{References}}\label{references}

For polynomial functors see also the references at [[nLab:polynomial functor]]. In particular

\begin{itemize}%
\item (Joachim) Kock, Joyal, Batanin, Mascari, Polynomial functors and opetopes, \href{http://arxiv.org/abs/0706.1033}{arXiv:0706.1033}


\item Joachim Kock. Polynomial functors and trees. Preprint, \href{http://arxiv.org/abs/0807.2874}{arXiv:0807.2874}


\item Nicola Gambino and Joachim Kock (2009); Polynomial functors and [[polynomial monad]]s; \href{http://arxiv.org/abs/0906.4931}{arXiv}.



\end{itemize}


\end{document}