Polyonomial Functors

(under construction)

We use $\mathcal P$ for the powerset functor and $\mathcal H X=2^{2^X}$. In this section we indicate how to construct a modal logic for any functor $T$ built according to the following context-free grammar.

We describe functors $L:\BA\to\BA$ or $L:\BA\times\BA\to\BA$ by generators and relations as follows.

• $L_{K_C}(A)$ is the free $\BA$ given by generators $c\in C$ and satisfying $c_1\wedge c_2=\bot$ for all $c_1\not=c_2$ and $\bigvee_{c\in C} c = \top$.

• $L_+(A_1,A_2)$ is generated by $[\kappa_1]a_1$, $[\kappa_2]a_2$, $a_i\in A_i$ where the $[\kappa_i]$ preserve finite joins and binary meets and satisfy $[\kappa_1] a_1\wedge [\kappa_2]a_2=\bot$, $[\kappa_1]\top\vee [\kappa_2]\top=\top$, $\neg[\kappa_1]a_1=[\kappa_2]\top\vee[\kappa_1]\neg a_1$, $\neg[\kappa_2]a_2=[\kappa_1]\top\vee[\kappa_2]\neg a_2$.

• $L_\times(A_1,A_2)$ is generated by $[\pi_1]a_1$, $[\pi_2]a_2$, $a_i\in A_i$ where $[\pi_i]$ preserve Boolean operations.

• $L_\mathcal P(A)$ is generated by $\Box a$, $a \in A$, and $\Box$ preserves finite meets.

• $L_\mathcal H(A)$ is generated by $\Box a$, $a \in A$ (no equations).

For the semantics, we define Boolean algebra morphisms $\delta_T$

• $L_{K_C}\Pi X \to \Pi C$ by $c\mapsto \{c\}$,

• $L_+(\Pi X_1,\Pi X_2) \to \Pi(X_1+X_2)$ by $[\kappa_i]a_i\mapsto a_i$,

• $L_\times(\Pi X,\Pi Y) \to \Pi(X_1\times X_2)$ by $[\pi_1]a_1\mapsto a_1\times X_2$, $[\pi_2]a_2\mapsto X_1\times a_2$,

• $L_\mathcal P \Pi X\to \Pi\mathcal P X$ by $\Box a \mapsto \{b\subseteq X\mid b\subseteq a\}$,

• $L_\mathcal H \Pi X\to \Pi\mathcal H X$ by $\Box a \mapsto \{s\in \mathcal H X \mid a \in s \}$.

and extend them inductively to $\delta_T:L_T\Pi\to\Pi T$ for all $T$. Items (1)-(3) are slight variations of cases appearing in Abramsky (1991), (4) is in Abramsky (2005), and $\delta_X$ in (5) is given by the identity on $2^{2^{2^X}}$.