# The UP-Isomorphism Theorems for UP-algebras111This work was financially
supported by the University of Phayao.

Aiyared Iampan222Corresponding author.
Department of Mathematics, School of Science
University of Phayao, Phayao 56000, Thailand
Email<EMAIL_ADDRESS>
###### Abstract

In this paper, we construct the fundamental theorem of UP-homomorphisms in UP-
algebras. We also give an application of the theorem to the first, second,
third and fourth UP-isomorphism theorems in UP-algebras.

Mathematics Subject Classification: 03G25

Keywords: UP-algebra, fundamental theorem of UP-homomorphisms, first, second,
third and fourth UP-isomorphism theorems

##  1 Introduction and Preliminaries

Among many algebraic structures, algebras of logic form important class of
algebras. Examples of these are BCK-algebras [5], BCI-algebras [6], BCH-
algebras [3], KU-algebras [13], SU-algebras [8] and others. They are strongly
connected with logic. For example, BCI-algebras introduced by Iséki [6] in
1966 have connections with BCI-logic being the BCI-system in combinatory logic
which has application in the language of functional programming. BCK and BCI-
algebras are two classes of logical algebras. They were introduced by Imai and
Iséki [5, 6] in 1966 and have been extensively investigated by many
researchers. It is known that the class of BCK-algebras is a proper subclass
of the class of BCI-algebras.

The isomorphism theorems play an important role in a general logical algebra,
which were studied by several researches such as: In 1998, Jun, Hong, Xin and
Roh [7] proved isomorphism theorems by using Chinese Remainder Theorem in BCI-
algebras. In 2001, Park, Shim and Roh [12] proved isomorphism theorems of IS-
algebras. In 2004, Hao and Li [2] introduced the concept of ideals of an ideal
in a BCI-algebra and some isomorphism theorems are obtained by using this
concept. They obtained several isomorphism theorems of BG-algebras and related
properties. In 2006, Kim [10] introduced the notion of KS-semigroups. He
characterized ideals of a KS-semigroup and proved the first isomorphism
theorem for KS-semigroups. In 2008, Kim and Kim [9] introduced the notion of
BG-algebras which is a generalization of B-algebras. They obtained several
isomorphism theorems of BG-algebras and related properties. In 2009, Paradero-
Vilela and Cawi [11] characterized KS-semigroup homomorphisms and proved the
isomorphism theorems for KS-semigroups. In 2011, Keawrahun and Leerawat [8]
introduced the notion of SU-semigroups and proved the isomorphism theorems for
SU-semigroups. In 2012, Asawasamrit [1] introduced the notion of KK-algebras
and studied isomorphism theorems of KK-algebras.

Iampan [4] now introduced a new algebraic structure, called a UP-algebra and a
concept of UP-ideals, congruences and UP-homomorphisms in UP-algebras, and
defined a congruence relation on a UP-algebra and a quotient UP-algebra. In
this paper, we construct the fundamental theorem of UP-homomorphisms in UP-
algebras. We also give an application of the theorem to the first, second,
third and fourth UP-isomorphism theorems in UP-algebras.

Before we begin our study, we will introduce to the definition of a UP-
algebra.

######  Definition 1.1.

[4] An algebra $A=(A,\cdot,0)$ of type $(2,0)$ is called a UP-algebra, where
$A$ is a nonempty set, $\cdot$ is a binary operation on $A$, and $0$ is a
fixed element of $A$ (i.e., a nullary operation) if it satisfies the following
axioms: for any $x,y,z\in A$,

(UP-1)

$(y\cdot z)\cdot((x\cdot y)\cdot(x\cdot z))=0$,

(UP-2)

$0\cdot x=x$,

(UP-3)

$x\cdot 0=0$, and

(UP-4)

$x\cdot y=y\cdot x=0$ implies $x=y$.

######  Example 1.2.

[4] Let $X$ be a universal set. Define a binary operation $\cdot$ on the power
set of $X$ by putting $A\cdot B=B\cap A^{\prime}=A^{\prime}\cap B=B-A$ for all
$A,B\in\mathcal{P}(X)$. Then $(\mathcal{P}(X),\cdot,\emptyset)$ is a UP-
algebra and we shall call it the power UP-algebra of type 1.

######  Example 1.3.

[4] Let $X$ be a universal set. Define a binary operation $\ast$ on the power
set of $X$ by putting $A\ast B=B\cup A^{\prime}=A^{\prime}\cup B$ for all
$A,B\in\mathcal{P}(X)$. Then $(\mathcal{P}(X),\ast,X)$ is a UP-algebra and we
shall call it the power UP-algebra of type 2.

######  Example 1.4.

[4] Let $A=\\{0,a,b,c\\}$ be a set with a binary operation $\cdot$ defined by
the following Cayley table:

$\begin{array}[]{c|cccc}\cdot&0&a&b&c\\\ \hline\cr 0&0&a&b&c\\\ a&0&0&0&0\\\
b&0&a&0&c\\\ c&0&a&b&0\end{array}$ (1.1)

Then $(A,\cdot,0)$ is a UP-algebra.

The following proposition is very important for the study of UP-algebras.

######  Proposition 1.5.

[4] In a UP-algebra $A$, the following properties hold: for any $x,y,z\in A$,

  1. (1)

$x\cdot x=0$,

  2. (2)

$x\cdot y=0$ and $y\cdot z=0$ implies $x\cdot z=0$,

  3. (3)

$x\cdot y=0$ implies $(z\cdot x)\cdot(z\cdot y)=0$,

  4. (4)

$x\cdot y=0$ implies $(y\cdot z)\cdot(x\cdot z)=0$,

  5. (5)

$x\cdot(y\cdot x)=0$,

  6. (6)

$(y\cdot x)\cdot x=0$ if and only if $x=y\cdot x$, and

  7. (7)

$x\cdot(y\cdot y)=0$.

######  Theorem 1.6.

[4] An algebra $A=(A,\cdot,0)$ of type $(2,0)$ is a UP-algebra if and only if
it satisfies the following conditions: for all $x,y,z\in A$,

  1. (1)

_(UP-1):_ $(y\cdot z)\cdot((x\cdot y)\cdot(x\cdot z))=0$,

  2. (2)

$(y\cdot 0)\cdot x=x$, and

  3. (3)

_(UP-4):_ $x\cdot y=y\cdot x=0$ implies $x=y$.

######  Definition 1.7.

[4] Let $A$ be a UP-algebra. A nonempty subset $B$ of $A$ is called a UP-ideal
of $A$ if it satisfies the following properties:

  1. (1)

the constant $0$ of $A$ is in $B$, and

  2. (2)

for any $x,y,z\in A,x\cdot(y\cdot z)\in B$ and $y\in B$ implies $x\cdot z\in
B$.

Clearly, $A$ and $\\{0\\}$ are UP-ideals of $A$.

We can easily show the following example.

######  Example 1.8.

[4] Let $A=\\{0,a,b,c,d\\}$ be a set with a binary operation $\cdot$ defined
by the following Cayley table:

$\begin{array}[]{c|ccccc}\cdot&0&a&b&c&d\\\ \hline\cr 0&0&a&b&c&d\\\
a&0&0&b&c&d\\\ b&0&0&0&c&d\\\ c&0&0&b&0&d\\\ d&0&0&0&0&0\end{array}$ (1.2)

Then $(A,\cdot,0)$ is a UP-algebra and $\\{0,a,b\\}$ and $\\{0,a,c\\}$ are UP-
ideals of $A$.

######  Theorem 1.9.

[4] Let $A$ be a UP-algebra and $B$ a UP-ideal of $A$. Then the following
statements hold: for any $x,a,b\in A$,

  1. (1)

if $b\cdot x\in B$ and $b\in B$, then $x\in B$. Moreover, if $b\cdot
X\subseteq B$ and $b\in B$, then $X\subseteq B$,

  2. (2)

if $b\in B$, then $x\cdot b\in B$. Moreover, if $b\in B$, then $X\cdot
b\subseteq B$, and

  3. (3)

if $a,b\in B$, then $(b\cdot(a\cdot x))\cdot x\in B$.

######  Theorem 1.10.

[4] Let $A$ be a UP-algebra and $\\{B_{i}\\}_{i\in I}$ a family of UP-ideals
of $A$. Then $\bigcap_{i\in I}B_{i}$ is a UP-ideal of $A$.

From Theorem 1.10, the intersection of all UP-ideals of a UP-algebra $A$
containing a subset $X$ of $A$ is the UP-ideal of $A$ generated by $X$. For
$X=\\{a\\}$, let $I(a)$ denote the UP-ideal of $A$ generated by $\\{a\\}$. We
see that the UP-ideal of $A$ generated by $\emptyset$ and $\\{0\\}$ is
$\\{0\\}$, and the UP-ideal of $A$ generated by $A$ is $A$.

######  Definition 1.11.

[4] Let $A=(A,\cdot,0)$ be a UP-algebra. A subset $S$ of $A$ is called a UP-
subalgebra of $A$ if the constant $0$ of $A$ is in $S$, and $(S,\cdot,0)$
itself forms a UP-algebra. Clearly, $A$ and $\\{0\\}$ are UP-subalgebras of
$A$.

Applying Proposition 1.5 (1), we can then easily prove the following
Proposition.

######  Proposition 1.12.

[4] A nonempty subset $S$ of a UP-algebra $A=(A,\cdot,0)$ is a UP-subalgebra
of $A$ if and only if $S$ is closed under the $\cdot$ multiplication on $A$.

######  Theorem 1.13.

[4] Let $A$ be a UP-algebra and $\\{B_{i}\\}_{i\in I}$ a family of UP-
subalgebras of $A$. Then $\bigcap_{i\in I}B_{i}$ is a UP-subalgebra of $A$.

######  Theorem 1.14.

[4] Let $A$ be a UP-algebra and $B$ a UP-ideal of $A$. Then $A\cdot B\subseteq
B$. In particular, $B$ is a UP-subalgebra of $A$.

######  Theorem 1.15.

[4] Let $A$ be a UP-algebra and $B$ a UP-subalgebra of $A$. If $S$ is a subset
of $B$ that is satisfies the following properties:

  1. (1)

the constant $0$ of $A$ is in $S$, and

  2. (2)

for any $x,a,b\in B$, if $a,b\in S$, then $(b\cdot(a\cdot x))\cdot x\in S$.

Then $S$ is a UP-ideal of $B$.

######  Definition 1.16.

[4] Let $A$ be a UP-algebra and $B$ a UP-ideal of $A$. Define the binary
relation $\sim_{B}$ on $A$ as follows: for all $x,y\in A$,

$x\sim_{B}y\textrm{ if and only if }x\cdot y\in B\textrm{ and }y\cdot x\in B.$
(1.3)

######  Definition 1.17.

[4] Let $A$ be a UP-algebra. An equivalence relation $\rho$ on $A$ is called a
congruence if for any $x,y,z\in A$,

$x\rho y\textrm{ implies }x\cdot z\rho y\cdot z\textrm{ and }z\cdot x\rho
z\cdot y.$

######  Proposition 1.18.

[4] Let $A$ be a UP-algebra and $B$ a UP-ideal of $A$ with a binary relation
$\sim_{B}$ defined by (1.3). Then $\sim_{B}$ is a congruence on $A$.

Let $A$ be a UP-algebra and $\rho$ a congruence on $A$. If $x\in A$, then the
$\rho$-class of $x$ is the $(x)_{\rho}$ defined as follows:

$(x)_{\rho}=\\{y\in A\mid y\rho x\\}.$

Then the set of all $\rho$-classes is called the quotient set of $A$ by
$\rho$, and is denoted by $A/\rho$. That is,

$A/\rho=\\{(x)_{\rho}\mid x\in A\\}.$

######  Theorem 1.19.

[4] Let $A$ be a UP-algebra and $\rho$ a congruence on $A$. Then the following
statements hold:

  1. (1)

the $\rho$-class $(0)_{\rho}$ is a UP-ideal and a UP-subalgebra of $A$,

  2. (2)

a $\rho$-class $(x)_{\rho}$ is a UP-ideal of $A$ if and only if $x\rho 0$, and

  3. (3)

a $\rho$-class $(x)_{\rho}$ is a UP-subalgebra of $A$ if and only if $x\rho
0$.

######  Theorem 1.20.

[4] Let $A$ be a UP-algebra and $B$ a UP-ideal of $A$. Then the following
statements hold:

  1. (1)

the $\sim_{B}$-class $(0)_{\sim_{B}}$ is a UP-ideal and a UP-subalgebra of $A$
which $B=(0)_{\sim_{B}}$,

  2. (2)

a $\sim_{B}$-class $(x)_{\sim_{B}}$ is a UP-ideal of $A$ if and only if $x\in
B$,

  3. (3)

a $\sim_{B}$-class $(x)_{\sim_{B}}$ is a UP-subalgebra of $A$ if and only if
$x\in B$, and

  4. (4)

$(A/\sim_{B},\ast,(0)_{\sim_{B}})$ is a UP-algebra under the $\ast$
multiplication defined by $(x)_{\sim_{B}}\ast(y)_{\sim_{B}}=(x\cdot
y)_{\sim_{B}}$ for all $x,y\in A$, called the quotient UP-algebra of $A$
induced by the congruence $\sim_{B}$.

######  Definition 1.21.

[4] Let $(A,\cdot,0)$ and $(A^{\prime},\cdot^{\prime},0^{\prime})$ be UP-
algebras. A mapping $f$ from $A$ to $A^{\prime}$ is called a UP-homomorphism
if

$f(x\cdot y)=f(x)\cdot^{\prime}f(y)\textrm{ for all }x,y\in A.$

A UP-homomorphism $f\colon A\to A^{\prime}$ is called a

  1. (1)

UP-epimorphism if $f$ is surjective,

  2. (2)

UP-monomorphism if $f$ is injective,

  3. (3)

UP-isomorphism if $f$ is bijective. Moreover, we say $A$ is UP-isomorphic to
$A^{\prime}$, symbolically, $A\cong A^{\prime}$, if there is a UP-isomorphism
from $A$ to $A^{\prime}$.

Let $f$ be a mapping from $A$ to $A^{\prime}$, and let $B$ be a nonempty
subset of $A$, and $B^{\prime}$ of $A^{\prime}$. The set $\\{f(x)\mid x\in
B\\}$ is called the image of $B$ under $f$, denoted by $f(B)$. In particular,
$f(A)$ is called the image of $f$, denoted by $\mathrm{Im}(f)$. Dually, the
set $\\{x\in A\mid f(x)\in B^{\prime}\\}$ is said the inverse image of
$B^{\prime}$ under $f$, symbolically, $f^{-1}(B^{\prime})$. Especially, we say
$f^{-1}(\\{0^{\prime}\\})$ is the kernel of $f$, written by $\mathrm{Ker}(f)$.
That is,

$\mathrm{Im}(f)=\\{f(x)\in A^{\prime}\mid x\in A\\}$

and

$\mathrm{Ker}(f)=\\{x\in A\mid f(x)=0^{\prime}\\}.$

In fact it is easy to show the following theorem.

######  Theorem 1.22.

[4] Let $A,B$ and $C$ be UP-algebras. Then the following statements hold:

  1. (1)

the identity mapping $I_{A}\colon A\to A$ is a UP-isomorphism,

  2. (2)

if $f\colon A\to B$ is a UP-isomorphism, then $f^{-1}\colon B\to A$ is a UP-
isomorphism, and

  3. (3)

if $f\colon A\to B$ and $g\colon B\to C$ are UP-isomorphisms, then $g\circ
f\colon A\to C$ is a UP-isomorphism.

######  Theorem 1.23.

[4] Let $A$ be a UP-algebra and $B$ a UP-ideal of $A$. Then the mapping
$\pi_{B}\colon A\to A/\sim_{B}$ defined by $\pi_{B}(x)=(x)_{\sim_{B}}$ for all
$x\in A$ is a UP-epimorphism, called the natural projection from $A$ to
$A/\sim_{B}$.

On a UP-algebra $A=(A,\cdot,0)$, we define a binary relation $\leq$ on $A$ as
follows: for all $x,y\in A$,

$x\leq y\textrm{ if and only if }x\cdot y=0.$ (1.4)

######  Proposition 1.24.

[4] Let $A$ be a UP-algebra with a binary relation $\leq$ defined by (1.4).
Then $(A,\leq)$ is a partially ordered set with $0$ as the greatest element.

We often call the partial ordering $\leq$ defined by (1.4) the UP-ordering on
$A$. From now on, the symbol $\leq$ will be used to denote the UP-ordering,
unless specified otherwise.

######  Theorem 1.25.

[4] Let $(A,\cdot,0_{A})$ and $(B,\ast,0_{B})$ be UP-algebras and let $f\colon
A\to B$ be a UP-homomorphism. Then the following statements hold:

  1. (1)

$f(0_{A})=0_{B}$,

  2. (2)

for any $x,y\in A$, if $x\leq y$, then $f(x)\leq f(y)$,

  3. (3)

if $C$ is a UP-subalgebra of $A$, then the image $f(C)$ is a UP-subalgebra of
$B$. In particular, $\mathrm{Im}(f)$ is a UP-subalgebra of $B$,

  4. (4)

if $D$ is a UP-subalgebra of $B$, then the inverse image $f^{-1}(D)$ is a UP-
subalgebra of $A$. In particular, $\mathrm{Ker}(f)$ is a UP-subalgebra of $A$,

  5. (5)

if $C$ is a UP-ideal of $A$ such that $\mathrm{Ker}(f)\subseteq C$, then the
image $f(C)$ is a UP-ideal of $f(A)$,

  6. (6)

if $D$ is a UP-ideal of $B$, then the inverse image $f^{-1}(D)$ is a UP-ideal
of $A$. In particular, $\mathrm{Ker}(f)$ is a UP-ideal of $A$, and

  7. (7)

$\mathrm{Ker}(f)=\\{0_{A}\\}$ if and only if $f$ is injective.

##  2 Main Results

In this section, we construct the fundamental theorem of UP-homomorphisms in
UP-algebras. We also give an application of the theorem to the first, second,
third and fourth UP-isomorphism theorems in UP-algebras.

######  Theorem 2.1.

(Fundamental Theorem of UP-homomorphisms) Let $(A,\cdot,0_{A})$ and
$(B,\bullet,0_{B})$ be UP-algebras, and $f\colon A\to B$ a UP-homomorphism.
Then there exists uniquely a UP-homomorphism $\varphi$ from
$A/\sim_{\mathrm{Ker}(f)}$ to $B$ such that
$f=\varphi\circ\pi_{\mathrm{Ker}(f)}$. Moreover,

  1. (1)

$\pi_{\mathrm{Ker}(f)}$ is a UP-epimorphism and $\varphi$ a UP-monomorphism,
and

  2. (2)

$f$ is a UP-epimorphism if and only if $\varphi$ is a UP-isomorphism.

As $f$ makes the following diagram commute,

$\textstyle{A\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{f}$$\scriptstyle{\pi_{\mathrm{Ker}(f)}}$$\textstyle{B}$$\textstyle{A/\sim_{\mathrm{Ker}(f)}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\varphi}$

###### Proof.

Put $K=\mathrm{Ker}(f)$. By Theorem 1.25 (6), we have $K$ is a UP-ideal of
$A$. It follows from Theorem 1.20 (4) that
$(A/\sim_{K},\ast,(0_{A})_{\sim_{K}})$ is a UP-algebra. Define

$\varphi\colon A/\sim_{K}\to B,(x)_{\sim_{K}}\mapsto f(x).$ (2.1)

Let $(x)_{\sim_{K}},(y)_{\sim_{K}}\in A/\sim_{K}$ be such that
$(x)_{\sim_{K}}=(y)_{\sim_{K}}$. Then $x\sim_{K}y$, so $x\cdot y\in K$ and
$y\cdot x\in K$. Thus

$f(x)\bullet f(y)=f(x\cdot y)=0_{B}\textrm{ and }f(y)\bullet f(x)=f(y\cdot
x)=0_{B}.$

By (UP-4), we have $f(x)=f(y)$ and so
$\varphi((x)_{\sim_{K}})=\varphi((y)_{\sim_{K}})$. Thus $\varphi$ is a
mapping. For any $x,y\in A$, we see that

$\varphi((x)_{\sim_{K}}\ast(y)_{\sim_{K}})=\varphi((x\cdot
y)_{\sim_{K}})=f(x\cdot y)=f(x)\bullet
f(y)=\varphi((x)_{\sim_{K}})\bullet\varphi((y)_{\sim_{K}}).$

Thus $\varphi$ is a UP-homomorphism. Also, since

$(\varphi\circ\pi_{K})(x)=\varphi(\pi_{K}(x))=\varphi((x)_{\sim_{K}})=f(x)\textrm{
for all }x\in A,$

we obtain $f=\varphi\circ\pi_{K}$. We have shown the existence. Let
$\varphi^{\prime}$ be a mapping from $A/\sim_{K}$ to $B$ such that
$f=\varphi^{\prime}\circ\pi_{K}$. Then for any $(x)_{\sim_{K}}\in A/\sim_{K}$,
we have

$\varphi^{\prime}((x)_{\sim_{K}})=\varphi^{\prime}(\pi_{K}(x))=(\varphi^{\prime}\circ\pi_{K})(x)=f(x)=(\varphi\circ\pi_{K})(x)=\varphi(\pi_{K}(x))=\varphi((x)_{\sim_{K}}).$

Hence, $\varphi=\varphi^{\prime}$, showing the uniqueness.

(1) By Theorem 1.23, we have $\pi_{K}$ is a UP-epimorphism. Also, let
$(x)_{\sim_{K}},(y)_{\sim_{K}}\in A/\sim_{K}$ be such that
$\varphi((x)_{\sim_{K}})=\varphi((y)_{\sim_{K}})$. Then $f(x)=f(y)$, and it
follows from Proposition 1.5 (1) that

$f(x\cdot y)=f(x)\bullet f(y)=f(y)\bullet f(y)=0_{B},$

that is, $x\cdot y\in K$. Similarly, $y\cdot x\in K$. Hence, $x\sim_{K}y$ and
$(x)_{\sim_{K}}=(y)_{\sim_{K}}$. Therefore, $\varphi$ a UP-monomorphism.

(2) Assume that $f$ is a UP-epimorphism. By (1), it suffices to prove
$\varphi$ is surjective. Let $y\in B$. Then there exists $x\in A$ such that
$f(x)=y$. Thus $y=f(x)=\varphi((x)_{\sim_{K}})$, so $\varphi$ is surjective.
Hence, $\varphi$ is a UP-isomorphism.

Conversely, assume that $\varphi$ is a UP-isomorphism. Then $\varphi$ is
surjective. Let $y\in B$. Then there exists $(x)_{\sim_{K}}\in A/\sim_{K}$
such that $\varphi((x)_{\sim_{K}})=y$. Thus $f(x)=\varphi((x)_{\sim_{K}})=y$,
so $f$ is surjective. Hence, $f$ is a UP-epimorphism. ∎

######  Theorem 2.2.

(First UP-isomorphism Theorem) Let $(A,\cdot,0_{A})$ and $(B,\bullet,0_{B})$
be UP-algebras, and $f\colon A\to B$ a UP-homomorphism. Then

$A/\sim_{\mathrm{Ker}(f)}\cong\mathrm{Im}(f).$

###### Proof.

By Theorem 1.25 (3), we have $\mathrm{Im}(f)$ is a UP-subalgebra of $B$. Thus
$f\colon A\to\mathrm{Im}(f)$ is a UP-epimorphism. Applying Theorem 2.1 (2), we
obtain $A/\sim_{\mathrm{Ker}(f)}\cong\mathrm{Im}(f)$. ∎

######  Lemma 2.3.

Let $(A,\cdot,0)$ be a UP-algebra, $H$ a UP-subalgebra of $A$, and $K$ a UP-
ideal of $A$. Denote $HK=\bigcup_{h\in H}(h)_{\sim_{K}}$. Then $HK$ is a UP-
subalgebra of $A$.

###### Proof.

Clearly, $\emptyset\neq HK\subseteq A$. Let $a,b\in HK$. Then
$a\in(x)_{\sim_{K}}$ and $b\in(y)_{\sim_{K}}$ for some $x,y\in H$, so
$(a)_{\sim_{K}}=(x)_{\sim_{K}}$ and $(b)_{\sim_{K}}=(y)_{\sim_{K}}$. Thus

$(a\cdot
b)_{\sim_{K}}=(a)_{\sim_{K}}\ast(b)_{\sim_{K}}=(x)_{\sim_{K}}\ast(y)_{\sim_{K}}=(x\cdot
y)_{\sim_{K}},$

so $a\cdot b\in(x\cdot y)_{\sim_{K}}$. Since $x,y\in H$, it follows from
Proposition 1.12 that $x\cdot y\in H$. Thus $a\cdot b\in(x\cdot
y)_{\sim_{K}}\subseteq HK$. Hence, $HK$ is a UP-subalgebra of $A$. ∎

######  Theorem 2.4.

(Second UP-isomorphism Theorem) Let $(A,\cdot,0)$ be a UP-algebra, $H$ a UP-
subalgebra of $A$, and $K$ a UP-ideal of $A$. Denote
$HK/\sim_{K}=\\{(x)_{\sim_{K}}\mid x\in HK\\}$. Then

$H/\sim_{H\cap K}\cong HK/\sim_{K}.$

###### Proof.

By Lemma 2.3, we have $HK$ is a UP-subalgebra of $A$. Then it is easy to check
that $HK/\sim_{K}$ is a UP-subalgebra of $A/\sim_{K}$, thus
$(HK/\sim_{K},\ast,(0)_{\sim_{K}})$ itself is a UP-algebra. Also, it is
obvious that $H\subseteq HK$, then

$f\colon H\to HK/\sim_{K},x\mapsto(x)_{\sim_{K}},$ (2.2)

is a mapping. For any $x,y\in H$, we have

$f(x\cdot y)=(x\cdot y)_{\sim_{K}}=(x)_{\sim_{K}}\ast(y)_{\sim_{K}}=f(x)\ast
f(y).$

Thus $f$ is a UP-homomorphism. We shall show that $f$ is a UP-epimorphism with
$\mathrm{Ker}(f)=H\cap K$. For any $(x)_{\sim_{K}}\in HK/\sim_{K}$, we have
$x\in HK=\bigcup_{h\in H}(h)_{\sim_{K}}$. Then there exists $h\in H$ such that
$x\in(h)_{\sim_{K}}$ and so $(x)_{\sim_{K}}=(h)_{\sim_{K}}$. Thus
$f(h)=(h)_{\sim_{K}}=(x)_{\sim_{K}}$. Therefore, $f$ is a UP-epimorphism.
Also, for any $h\in H$, if $h\in\mathrm{Ker}(f)$, then $f(h)=(0)_{\sim_{K}}$.
Since $f(h)=(h)_{\sim_{K}}$, we obtain $(h)_{\sim_{K}}=(0)_{\sim_{K}}$. By
(UP-2) and (1.3), we have $h=0\cdot h\in K$. Thus $h\in H\cap K$, that is,
$\mathrm{Ker}(f)\subseteq H\cap K$. On the other hand, if $h\in H\cap K$, by
$h\in H$, $f(h)$ is well-defined, by $h\in K$ and $0\in K$, $h\cdot 0\in K$
and $0\cdot h\in K$. By (1.3), we have $h\sim_{K}0$ and so
$(h)_{\sim_{K}}=(0)_{\sim_{K}}$. Thus $f(h)=(h)_{\sim_{K}}=(0)_{\sim_{K}}$.
So, $h\in\mathrm{Ker}(f)$, that is, $H\cap K\subseteq\mathrm{Ker}(f)$.
Therefore, $\mathrm{Ker}(f)=H\cap K$. Now, Theorem 2.2 gives $H/\sim_{H\cap
K}\cong HK/\sim_{K}$. ∎

######  Theorem 2.5.

(Third UP-isomorphism Theorem) Let $(A,\cdot,0)$ be a UP-algebra, and $H$ and
$K$ UP-ideals of $A$ with $H\subseteq K$. Then

$(A/\sim_{H})/\sim_{(K/\sim_{H})}\cong A/\sim_{K}.$

###### Proof.

By Theorem 1.20 (4), we obtain $(A/\sim_{K},\ast,(0)_{\sim_{K}})$ and
$(A/\sim_{H},\ast^{\prime},(0)_{\sim_{H}})$ are UP-algebras. Define

$f\colon A/\sim_{H}\to A/\sim_{K},(x)_{\sim_{H}}\mapsto(x)_{\sim_{K}}.$ (2.3)

For any $x,y\in A$, if $(x)_{\sim_{H}}=(y)_{\sim_{H}}$, then $x\cdot y,y\cdot
x\in H$. Since $H\subseteq K$, we obtain $x\cdot y,y\cdot x\in K$. Thus
$(x)_{\sim_{K}}=(y)_{\sim_{K}}$, so $f((x)_{\sim_{H}})=f((y)_{\sim_{H}})$.
Thus $f$ is a mapping. Also, for any $x,y\in A$, we see that

$f((x)_{\sim_{H}}\ast^{\prime}(y)_{\sim_{H}})=f((x\cdot y)_{\sim_{H}})=(x\cdot
y)_{\sim_{K}}=(x)_{\sim_{K}}\ast(y)_{\sim_{K}}=f((x)_{\sim_{H}})\ast
f((y)_{\sim_{H}}).$

Thus $f$ is a UP-homomorphism. Clearly, $f$ is surjective. Hence, $f$ is a UP-
epimorphism. We shall show that $\mathrm{Ker}(f)=K/\sim_{H}$. In fact,

$\displaystyle\mathrm{Ker}(f)$ $\displaystyle=\\{(x)_{\sim_{H}}\in
A/\sim_{H}\mid f((x)_{\sim_{H}})=(0)_{\sim_{K}}\\}$
$\displaystyle=\\{(x)_{\sim_{H}}\in
A/\sim_{H}\mid(x)_{\sim_{K}}=(0)_{\sim_{K}}\\}$
$\displaystyle=\\{(x)_{\sim_{H}}\in A/\sim_{H}\mid x=0\cdot x\in K\\}$ (By
(UP-2)) $\displaystyle=K/\sim_{H}.$

Now, Theorem 2.2 gives $(A/\sim_{H})/\sim_{(K/\sim_{H})}\cong A/\sim_{K}$. ∎

######  Theorem 2.6.

(Fourth UP-isomorphism Theorem) Let $(A,\cdot,0_{A})$ and $(B,\bullet,0_{B})$
be UP-algebras, and $f\colon A\to B$ a UP-epimorphism. Denote
$\mathcal{A}=\\{X\mid X$ is a UP-ideal of $A$ containing $\mathrm{Ker}(f)\\}$
and $\mathcal{B}=\\{Y\mid Y$ is a UP-ideal of $B\\}$. Then the following
statements hold:

  1. (1)

there is an inclusion preserving bijection

$\varphi\colon\mathcal{A}\to\mathcal{B},X\mapsto f(X),$ (2.4)

with inverse given by $Y\mapsto f^{-1}(Y)$, and

  2. (2)

for any $X\in\mathcal{A}$,

$A/\sim_{X}\cong B/\sim_{f(X)}.$

###### Proof.

(1) For any $X\in\mathcal{A}$, it follows from Theorem 1.25 (5) that $f(X)$ is
a unique UP-ideal of $B$ such that $\varphi(X)=f(X)$. Thus $\varphi$ is a
mapping. For any $X_{1},X_{2}\in\mathcal{A}$, if
$\varphi(X_{1})=\varphi(X_{2})$, then $f(X_{1})=f(X_{2})$. Since
$\mathrm{Ker}(f)\subseteq X_{1}$, we obtain $X_{1}=f^{-1}(f(X_{1}))$. Indeed,
let $x\in f^{-1}(f(X_{1}))$. Then $f(x)\in f(X_{1})$, so $f(x)=f(x_{1})$ for
some $x_{1}\in X_{1}$. Applying Proposition 1.5 (1), we have $f(x_{1}\cdot
x)=f(x_{1})\bullet f(x)=f(x_{1})\bullet f(x_{1})=0_{B}$. Thus $x_{1}\cdot
x\in\mathrm{Ker}(f)\subseteq X_{1}$, it follows from Theorem 1.9 (1) that
$x\in X_{1}$. So, $f^{-1}(f(X_{1}))\subseteq X_{1}$. Clearly, $X_{1}\subseteq
f^{-1}(f(X_{1}))$. Similarly, since $\mathrm{Ker}(f)\subseteq X_{2}$, we
obtain $X_{2}=f^{-1}(f(X_{2}))$. Thus
$X_{1}=f^{-1}(f(X_{1}))=f^{-1}(f(X_{2}))=X_{2}$. Hence, $\varphi$ is
injective. Also, for any $Y\in\mathcal{B}$, we obtain $Y=f(f^{-1}(Y))$ because
$f$ is surjective. Applying Theorem 1.25 (6), we have $f^{-1}(Y)$ is a UP-
ideal of $A$ with $\mathrm{Ker}(f)\subseteq f^{-1}(Y)$. Thus
$f^{-1}(Y)\in\mathcal{A}$ is such that $\varphi(f^{-1}(Y))=f(f^{-1}(Y))=Y$.
Hence, $\varphi$ is surjective. Therefore, $\varphi$ is bijective. Finally,
for any $Y\in\mathcal{B}$, we get that $Y=\varphi(f^{-1}(Y))$. Hence,
$\varphi^{-1}(Y)=f^{-1}(Y)$.

(2) By Theorem 1.25 (5) and Theorem 1.20 (4), we have $f(X)$ is a UP-ideal of
$B$ and $(B/\sim_{f(X)},\ast,(0_{B})_{\sim_{f(X)}})$ is a UP-algebra. It
follows from Theorem 1.23 that $\pi_{f(X)}\colon B\to B/\sim_{f(X)}$ is a UP-
epimorphism. Thus $\pi_{f(X)}\circ f\colon A\to B/\sim_{f(X)}$ is a UP-
epimorphism. We shall show that $\mathrm{Ker}(\pi_{f(X)}\circ f)=X$. In fact,

$\displaystyle\mathrm{Ker}(\pi_{f(X)}\circ f)$ $\displaystyle=\\{a\in
A\mid(\pi_{f(X)}\circ f)(a)=(0_{B})_{\sim_{f(X)}}\\}$ $\displaystyle=\\{a\in
A\mid\pi_{f(X)}(f(a))=(0_{B})_{\sim_{f(X)}}\\}$ $\displaystyle=\\{a\in
A\mid(f(a))_{\sim_{f(X)}}=(0_{B})_{\sim_{f(X)}}\\}$ $\displaystyle=\\{a\in
A\mid f(a)=0_{B}\bullet f(a)\in f(X)\\}$ (By (UP-2))
$\displaystyle=f^{-1}(f(X))$ $\displaystyle=X.$

Applying Theorem 2.2, we have $A/\sim_{X}\cong B/\sim_{f(X)}$. ∎

## Acknowledgment

The author wish to express their sincere thanks to the referees for the
valuable suggestions which lead to an improvement of this paper.

## References

  * [1] S. Asawasamrit, _KK-isomorphism and its properties_ , Int. J. Pure Appl. Math. 78 (2012), no. 1, 65–73.
  * [2] J. Hao and C. X. Li, _On ideals of an ideal in a BCI-algebra_ , Sci. Math. Jpn. (in Editione Electronica) 10 (2004), no. 16, 493–500.
  * [3] Q. P. Hu and X. Li, _On BCH-algebras_ , Math. Semin. Notes, Kobe Univ. 11 (1983), 313–320.
  * [4] A. Iampan, _A new branch of the logical algebra: UP-algebras_ , J. Algebra Relat. Top. 5 (2017), no. 1, 35–54.
  * [5] Y. Imai and K. Iséki, _On axiom system of propositional calculi, XIV_ , Proc. Japan Acad. 42 (1966), no. 1, 19–22.
  * [6] K. Iséki, _An algebra related with a propositional calculus_ , Proc. Japan Acad. 42 (1966), no. 1, 26–29.
  * [7] Y. B. Jun, S. M. Hong, X. L. Xin, and E. H. Roh, _Chinese remainder theorems in BCI-algebras_ , Soochow J. Math. 24 (1998), no. 3, 219–230.
  * [8] S. Keawrahun and U. Leerawat, _On isomorphisms of SU-algebras_ , Sci. Magna 7 (2011), no. 2, 39–44.
  * [9] C. B. Kim and H. S. Kim, _On BG-algebras_ , Demonstr. Math. 41 (2008), no. 3, 497–505.
  * [10] K. H. Kim, _On structure of KS-semigroup_ , Int. Math. Forum 1 (2006), no. 2, 67–76.
  * [11] J. S. Paradero-Vilela and M. Cawi, _On KS-semigroup homomorphism_ , Int. Math. Forum 4 (2009), no. 23, 1129–1138.
  * [12] J. K. Park, W. H. Shim, and E. H. Roh, _On isomorphism theorems in IS-algebras_ , Soochow J. Math. 27 (2001), no. 2, 153–160.
  * [13] C. Prabpayak and U. Leerawat, _On ideals and congruences in KU-algebras_ , Sci. Magna 5 (2009), no. 1, 54–57.

Received:


$p\subseteq q$ | $\nu x.(p\to q)\land\underline{\Box}x$
$\lambda(p,q_{1},\dots,q_{n})$ | $\nu x.(p\to\heartsuit_{\lambda}(q_{1},\dots,q_{n}))\land\underline{\Box}x$
$\alpha\vee\beta$ | $t(\alpha)\vee t(\beta)$
$\neg\alpha$ | $\neg t(\alpha)$
$\exists p.\alpha$ | $\widetilde{\exists}p.t(\alpha)$

where the map
$\widetilde{\exists}p:\mu\mathtt{ML}_{\Lambda}(\mathtt{X}p)\to\mu\mathtt{ML}_{\Lambda}(\mathtt{X})$
is defined precisely as in Section 6. We can now prove the equivalence (13) by
induction on the complexity of formulas of $\mathtt{MSO}_{\Lambda}$. The first
three atomic cases for $\mathsf{sr}(p)$, $p\subseteq q$ and
$\lambda(p,q_{1},\dots,q_{n})$ can be checked by routine verification, where
the proofs for the first two cases uses the fact that the map $f_{\mathbb{S}}$
maps the points of $\mathbb{S}_{*}$ surjectively onto the points in
$\mathbb{S}$, the second case additionally uses the fact that $\mathbb{S}_{*}$
is constructed so that its supporting Kripke frame is a tree rooted at $s_{*}$
(see [9] for details), and the case for $\lambda(p,q_{1},\dots,q_{n})$ uses
the fact that $f_{\mathbb{S}}$ is a $\mathsf{T}$-model homomorphism. The
induction steps for boolean connectives are trivial. Finally, the proof for
the crucial case of $\exists p.\varphi$ closely follows that of Proposition
19, so we omit the details. ∎

##  8\. Disjunctive bases for combined modal logics

An important topic in modal logic concerns methods to construct complex logics
from simpler ones, in such a way that desirable metalogical properties
transfer to a combined logic from its components. For an overview of this
field, see [23]. This thread has also been picked up in coalgebraic modal
logic: in a particularly interesting paper [5], Cîrstea & Pattinson provide
generic methods to obtain, from modal signatures for two set functors
$\mathsf{T}_{1}$ and $\mathsf{T}_{2}$, modal signatures for the coproduct,
product, and composition of $\mathsf{T}_{1}$ and $\mathsf{T}_{2}$. Since the
verification that a particular modal logic has a disjunctive basis can be
quite non-trivial — as witnessed here by the case of graded modal logic — it
will be useful to have some methods available that guarantee the existence of
a disjunctive basis being preserved by Cîrstea & Pattinson’s modular
constructions of signatures. In fact, we will show that disjunctive bases can
be constructed in a modular fashion as well: in each of the cases of
coproduct, product and composition we will give an explicit construction of a
disjunctive basis for the combined signature, based on disjunctive bases for
the composing functors.

###  8.1. Coproduct

Let $\mathsf{T}=\mathsf{T}_{1}+\mathsf{T}_{2}$ be the coproduct of the set
functors $\mathsf{T}_{1}$ and $\mathsf{T}_{2}$. For $i=1,2$ we will use
$\kappa_{i}$ to denote the natural transformation
$\kappa_{i}:\mathsf{T}_{i}\Rightarrow\mathsf{T}$ that instantiates to the
coproduct insertion map ${(\kappa_{i})}_{S}:\mathsf{T}_{i}S\to\mathsf{T}S$,
for every set $S$. Now suppose that we have been given signatures for
$\mathsf{T}_{1}$ and $\mathsf{T}_{2}$, respectively. Following Cîrstea &
Pattinson [5], we define the combined signature $\Lambda_{1}\oplus\Lambda_{2}$
for $\mathsf{T}$ as follows.

######  Definition 8.1.

Where $\Lambda_{1}$ and $\Lambda_{2}$ are monotone modal signatures for
$\mathsf{T}_{1}$ and $\mathsf{T}_{2}$ respectively, we define

$\Lambda_{1}\oplus\Lambda_{2}\mathrel{:=}\\{\kappa_{i}\circ\lambda\mid\lambda\in\Lambda_{i}\\}.$

In the syntax we shall write
$\raisebox{1.29167pt}{$\scriptstyle\bigcirc$}_{i,\lambda}$ rather than
$\heartsuit_{\kappa_{i}\circ\lambda}$.

We leave it for the reader to check that $\Lambda_{1}\oplus\Lambda_{2}$ is
indeed a collection of monotone predicate liftings for $\mathsf{T}$. The
meaning of the $\Lambda_{1}\oplus\Lambda_{2}$-modalities in an arbitrary
$\mathsf{T}$-coalgebra $\mathbb{S}$ is given as follows:

$\mathbb{S},s\Vdash\raisebox{1.29167pt}{$\scriptstyle\bigcirc$}_{i,\lambda}(\varphi_{1},\ldots,\varphi_{n})\text{
iff }\begin{array}[]{l}\sigma(s)={(\kappa_{i})}_{S}(\sigma^{i})\text{ for some
}\sigma^{i}\in\mathsf{T}_{i}S\\\ \text{with
}\sigma^{i}\in\lambda_{S}([\\![\varphi_{1}]\\!]^{\mathbb{S}},\ldots,[\\![\varphi_{n}]\\!]^{\mathbb{S}}).\end{array}$
(14)

Note that the subscript $i$ in
$\raisebox{1.29167pt}{$\scriptstyle\bigcirc$}_{i,\lambda}$ works as a _tag_
indicating to which part of the coproduct
$\mathsf{T}S=\mathsf{T}_{1}S+\mathsf{T}_{2}S$ the unfolding $\sigma(s)$ of the
state $s$ is situated.

The result on the existence of disjunctive bases that we want to prove is the
following.

######  Theorem 24.

Suppose both signatures $\Lambda_{1}$ and $\Lambda_{2}$ admit a disjunctive
basis. Then so does $\Lambda_{1}\oplus\Lambda_{2}$.

We start with giving a disjunctive basis for the combined signature.

######  Definition 8.2.

Fix a set $A=\\{a_{1},\ldots,a_{n}\\}$. Given a one-step formula $\alpha$ in
the language $\mathtt{1ML}_{\Lambda_{i}}(A)$, we let
$\alpha^{i}\in\mathtt{1ML}_{\Lambda_{1}\oplus\Lambda_{2}}(A)$ denote the
result of replacing every occurrence of a modality $\heartsuit_{\lambda}$ with
$\raisebox{1.29167pt}{$\scriptstyle\bigcirc$}_{i,\lambda}$. Define

$(\mathtt{D}_{1}\oplus\mathtt{D}_{2})(A)\mathrel{:=}\\{\delta_{1}^{1}\lor\delta_{2}^{2}\in\mathtt{1ML}_{\Lambda_{1}\oplus\Lambda_{2}}(A)\mid\delta_{i}\in\mathtt{D}_{i}(A)\\}.$

where $\mathtt{D}_{1}$ and $\mathtt{D}_{2}$ are disjunctive bases for
$\Lambda_{1}$ and $\Lambda_{2}$, respectively.

It remains to show that $\mathtt{D}_{1}\oplus\mathtt{D}_{2}$ is a disjunctive
basis for the signature $\Lambda_{1}\oplus\Lambda_{2}$.

  * Proof of Theorem 24.

We first show that $\mathtt{D}_{1}\oplus\mathtt{D}_{2}(A)$ consists of
disjunctive formulas. For this purpose we fix a set $A$ and an arbitrary
formula in $\mathtt{D}_{1}\oplus\mathtt{D}_{2}(A)$, say, $\delta^{1}$ such
that $\delta\in\mathtt{D}_{1}(A)$. Let $(S,\sigma,m)$ be an arbitrary one-step
$\mathsf{T}$-model such that $S,\sigma,m\Vdash^{1}\delta^{1}$, and make a case
distinction. If $\sigma={(\kappa_{2})}_{S}(\sigma^{2})$ for some
$\sigma^{2}\in\mathsf{T}_{2}S$ then a straightforward induction will show that
$S,\sigma,m^{\prime}\Vdash^{1}\delta^{1}$, where
$m^{\prime}(s)\mathrel{:=}\varnothing$ for every $s\in S$.

If, on the other hand, $\sigma={(\kappa_{1})}_{S}(\sigma^{1})$ for some
$\sigma^{1}\in\mathsf{T}_{1}S$ then a routine inductive proof will reveal that
the one-step $\mathsf{T}_{1}$-model $(S,\sigma^{1},m)$ satisfies $\delta$. By
disjunctiveness of $\mathtt{D}_{1}$ we then obtain a separating cover for
$(S,\sigma^{1},m)$, consisting of a one-step $\mathsf{T}_{1}$-model
$(S^{\prime},\sigma^{\prime},m^{\prime})$ and a map $f:S^{\prime}\to S$. It is
then easy to verify that the one-step $\mathsf{T}$-model
$(S^{\prime},\kappa_{1}(\sigma^{\prime}),m^{\prime})$, together with the same
map $f$, is a separating cover for the one-step $\mathsf{T}$-model
$(S,\sigma,m)$.

It is left to check that $\mathtt{D}_{1}\oplus\mathtt{D}_{2}(A)$ satisfies the
closure conditions of disjunctive bases. We leave it to the reader to verify
that (modulo equivalence) the set $\mathtt{D}_{1}\oplus\mathtt{D}_{2}(A)$ is
closed under taking disjunctions, and contains the formula $\top$. For
condition (2), take a formula of the form
$\raisebox{1.29167pt}{$\scriptstyle\bigcirc$}_{i,\lambda}\overline{\pi}$,
where $\lambda$ is a predicate lifting in $\Lambda_{i}$; without loss of
generality assume $i=1$. Then by assumption there is a formula
$\delta\in\mathtt{D}_{1}(\mathsf{P}A)$ such that
$\heartsuit_{\lambda}\overline{\pi}\equiv^{1}\delta[\wedge_{A}]$. It is
straightforward to verify that $\alpha\equiv^{1}\beta$ implies
$\alpha^{j}\equiv^{1}\beta^{j}$, for any pair of formulas
$\alpha,\beta\in\mathtt{1ML}_{\Lambda_{j}}^{+}(A)$. But then it is immediate
that
$\raisebox{1.29167pt}{$\scriptstyle\bigcirc$}_{1,\lambda}\overline{\pi}\equiv^{1}\delta^{1}[\wedge_{A}]\equiv^{1}(\delta^{1}\lor\bot)[\wedge_{A}]$;
clearly this suffices, since
$\delta^{1}\lor\bot\in\mathtt{D}_{1}\oplus\mathtt{D}_{2}(\mathsf{P}A)$.

Finally, for condition (3), consider the conjunction of two formulas in the
sets $\mathtt{D}_{1}\oplus\mathtt{D}_{2}(A)$ and
$\mathtt{D}_{1}\oplus\mathtt{D}_{2}(B)$, respectively. Using the distributive
law of conjunctions over disjunctions, we may rewrite this conjunction into an
equivalent disjunction of formulas of the form $\alpha^{i}\land\beta^{j}$,
where $\alpha\in\mathtt{D}_{i}(A)$ and $\beta\in\mathtt{D}_{j}(B)$ for some
$\\{i,j\\}\subseteq\\{1,2\\}$. Clearly then it suffices to show that each
conjunction of the latter form can be rewritten into the required shape. We
distinguish two cases.

If $i=j$, then since $\mathtt{D}_{i}$ is a disjunctive basis for
$\Lambda_{i}$, there is a formula
$\gamma^{i}\in\mathtt{D}_{i}(A\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}B)$ such that
$\alpha\land\beta\equiv^{1}\gamma^{i}[\theta_{A,B}]$. It is then
straightforward to verify that
$\alpha^{i}\land\beta^{i}\equiv^{1}\gamma^{i}[\theta_{A,B}]\equiv^{1}(\gamma^{i}\lor\bot)[\theta_{A,B}]$.

If, on the other hand, $i$ and $j$ are distinct, then we may without loss of
generality assume that $i=1$ and $j=2$. We claim that in fact for _any_ pair
of formulas $\alpha\in\mathtt{1ML}^{+}_{\Lambda_{1}}(A)$ and
$\mathtt{1ML}^{+}_{\Lambda_{2}}(B)$ (i.e, we do not need to assume that
$\alpha\in\mathtt{D}_{1}(A)$ or $\beta\in\mathtt{D}_{2}(B)$), the conjunction
$\alpha^{1}\land\beta^{2}$ is equivalent to a formula from the set
$\\{\top,\bot,\alpha^{1},\beta^{2}\\}$. The key observation in the proof of
this claim is that if $\alpha=\heartsuit_{\lambda}\overline{\pi}$ and
$\beta=\heartsuit_{\eta}\overline{\rho}$, then
$\alpha^{1}\land\beta^{2}\equiv\bot$ — this easily follows from the
observation about tagging that we made just after (14). Finally, note that
$\\{\top,\bot,\alpha^{1},\beta^{2}\\}\subseteq\mathtt{D}_{1}\oplus\mathtt{D}_{2}(A\cup
B)$. This means that every formula $\gamma$ in this set belongs to
$\mathtt{D}_{1}\oplus\mathtt{D}_{2}(A\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}B)$, and in addition
satisfies that $\gamma[\theta_{A,B}]=\gamma$. But then clearly the claim
suffices to find a formula
$\gamma\in\mathtt{D}_{1}\oplus\mathtt{D}_{2}(A\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}B)$ such that
$\alpha^{1}\land\beta^{2}\equiv^{1}\gamma[\theta_{A,B}]$, as required. ∎

###  8.2. Product

Given two functors $\mathsf{T}_{1},\mathsf{T}_{2}$ and modal signatures
$\Lambda_{1},\Lambda_{2}$ for these functors respectively, we construct a new
modal signature $\Lambda_{1}\otimes\Lambda_{2}$ that contains the modalities
of both $\Lambda_{1}$ and $\Lambda_{2}$. We want to interpret this combined
language on coalgebras that can be seen simultaneously as both
$\mathsf{T}_{1}$\- and $\mathsf{T}_{2}$-coalgebras, and the natural choice is
to form the product of the two functors and consider
$\mathsf{T}_{1}\times\mathsf{T}_{2}$-coalgebras.

######  Definition 8.3.

Suppose $\Lambda_{1},\Lambda_{2}$ are modal signatures for functors
$\mathsf{T}_{1},\mathsf{T}_{2}$ respectively. Then the modal signature
$\Lambda_{1}\otimes\Lambda_{2}$ for $\mathsf{T}_{1}\times\mathsf{T}_{2}$ is
defined by:

$=\Lambda_{1}\otimes\Lambda_{2}=\\{\breve{\mathsf{P}}\pi_{i}\circ\lambda\mid\lambda\in\Lambda_{i},\;i\in\\{1,2\\}\\}$

where $\pi_{1}:\mathsf{T}_{1}\times\mathsf{T}_{2}\to\mathsf{T}_{1}$ and
$\pi_{2}:\mathsf{T}_{1}\times\mathsf{T}_{2}\to\mathsf{T}_{2}$ are the natural
projection maps.

For simplicity of notation we will allow a small bit of imprecision and just
use the symbol $\lambda$ to denote the predicate lifting
$\breve{\mathsf{P}}\pi_{i}\circ\lambda$, given a lifting $\lambda$ for
$\mathsf{T}_{i}$. This means that we can view the languages
$\mathtt{1ML}_{\Lambda_{1}}(A)$ and $\mathtt{1ML}_{\Lambda_{2}}(A)$ as
fragments of $\mathtt{1ML}_{\Lambda_{1}\otimes\Lambda_{2}}(A)$. Our goal is to
prove the following.

######  Theorem 25.

Suppose both signatures $\Lambda_{1}$ and $\Lambda_{2}$ admit a disjunctive
basis. Then so does $\Lambda_{1}\otimes\Lambda_{2}$.

The disjunctive basis for the combined signature is defined as follows.

######  Definition 8.4.

Let $\mathtt{D}_{1},\mathtt{D}_{2}$ be disjunctive bases for
$\Lambda_{1},\Lambda_{2}$ respectively. Given a set of variables $A$ we define
the set of one-step formulas $(\mathtt{D}_{1}\otimes\mathtt{D}_{2})(A)$ to be
all finite disjunctions of formulas of the form $\delta_{1}\wedge\delta_{2}$,
where $\delta_{1}\in\mathtt{D}_{1}(A)$ and $\delta_{2}\in\mathtt{D}_{2}(A)$.

Note that $\top\in(\mathtt{D}_{1}\otimes\mathtt{D}_{2})(A)$, since it is in
$\mathtt{D}_{1}(A)$ and $\mathtt{D}_{2}(A)$, given that we allow a slight
abuse of notation and identify the conjunction $\top\wedge\top$ with $\top$.

We will show that $\mathtt{D}_{1}\otimes\mathtt{D}_{2}$ is a disjunctive basis
for $\Lambda_{1}\otimes\Lambda_{2}$ indeed. The first thing we need to check
is that these formulas are indeed disjunctive.

######  Proposition 26.

Let $\delta_{1}\in\mathtt{D}_{1}(A)$ and $\delta_{2}\in\mathtt{D}_{2}(A)$.
Then the formula $\delta_{1}\wedge\delta_{2}$ is disjunctive.

######  Proof 8.5.

Let $(X,(\xi_{1},\xi_{2}),m)$ be a one-step
$\mathsf{T}_{1}\times\mathsf{T}_{2}$-model satisfying the formula
$\delta_{1}\wedge\delta_{2}$. Then $X,\xi_{1},m\Vdash^{1}\delta_{1}$ and
$X,\xi_{2},m\Vdash^{1}\delta_{2}$. Since $\delta_{1},\delta_{2}$ are
disjunctive there exist two covering one-step frames
$h_{1}:(Y_{1},\rho_{1})\to(X,\xi_{1})$ and
$h_{2}:(Y_{2},\rho_{2})\to(X,\xi_{2})$ together with markings
$m_{1}:Y_{1}\to\mathsf{P}\mathtt{X}$ and $m_{1}:Y_{2}\to\mathsf{P}\mathtt{X}$
such that for each $i\in\\{1,2\\}$:

  * •

$Y_{i},\rho_{i},m_{i}\Vdash^{1}\delta_{i}$,

  * •

$m_{i}(u)\subseteq m(h_{i}(u))$ for all $u\in Y_{i}$,

  * •

$|m_{i}(u)|\leq 1$ for all $u\in Y_{i}$.

We shall construct a covering one-step
$\mathsf{T}_{1}\times\mathsf{T}_{2}$-frame based on the co-product
$Y_{1}+Y_{2}$ of the sets $Y_{1},Y_{2}$, with the covering map given by the
co-tuple of the maps $h_{1},h_{2}$, as shown in Figure 2.

$\textstyle{Y_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{i_{1}}$$\scriptstyle{h_{1}}$$\textstyle{Y_{1}+Y_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{[h_{1},h_{2}]}$$\textstyle{Y_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{h_{2}}$$\scriptstyle{i_{2}}$$\textstyle{X}$
Figure 2. The covering map $[h_{1},h_{2}]$

We define the covering one-step frame to be
$(Y_{1}+Y_{2},((\mathsf{T}_{1}i_{1})\rho_{1},(\mathsf{T}_{2}i_{2})\rho_{2}))$,
where $i_{1},i_{2}$ are the insertions of the co-product, so that
$[h_{1},h_{2}]\circ i_{1}=h_{1}$ and $[h_{1},h_{2}]\circ i_{2}=h_{2}$. That
the co-tuple $[h_{1},h_{2}]$ is in fact a one-step frame morphism is shown by
a straightforward calculation:

$\displaystyle(\mathsf{T}_{1}\times\mathsf{T}_{2})[h_{1},h_{2}](\mathsf{T}_{1}i_{1}\rho_{1},\mathsf{T}_{2}i_{2}\rho_{2})$
$\displaystyle=$
$\displaystyle(\mathsf{T}_{1}[h_{1},h_{2}]\circ\mathsf{T}_{1}i_{1}(\rho_{1}),\mathsf{T}_{2}[h_{1},h_{2}]\circ\mathsf{T}_{2}i_{2}(\rho_{2}))$
$\displaystyle=$ $\displaystyle(\mathsf{T}_{1}([h_{1},h_{2}]\circ
i_{1})(\rho_{1}),\mathsf{T}_{2}([h_{1},h_{2}]\circ i_{2})(\rho_{2}))$
$\displaystyle=$
$\displaystyle(\mathsf{T}_{1}h_{1}(\rho_{1}),\mathsf{T}_{2}h_{2}(\rho_{2}))$
$\displaystyle=$ $\displaystyle(\xi_{1},\xi_{2})$

The commutative diagram shown in Figure 3 may help to give an overview of the
construction, in which the top middle entry shows the type of the covering
one-step frame we have constructed.

|
---|---
$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\mathsf{T}_{1}(Y_{1}+Y_{2})}$$\scriptstyle{\mathsf{T}_{1}[h_{1},h_{2}]}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces(\mathsf{T}_{1}\times\mathsf{T}_{2})(Y_{1}+Y_{2})\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{(\mathsf{T}_{1}\times\mathsf{T}_{2})[h_{1},h_{2}]}$$\textstyle{\mathsf{T}_{2}(Y_{1}+Y_{2})\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{T}_{2}[h_{1},h_{2}]}$$\textstyle{\mathsf{T}_{1}Y_{1}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{T}_{1}i_{1}}$$\scriptstyle{\mathsf{T}_{1}h_{1}}$$\textstyle{\mathsf{T}_{2}Y_{2}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\mathsf{T}_{2}i_{2}}$$\scriptstyle{\mathsf{T}_{2}h_{2}}$$\textstyle{\mathsf{T}_{1}X}$$\textstyle{\ignorespaces\ignorespaces\ignorespaces\ignorespaces(\mathsf{T}_{1}\times\mathsf{T}_{2})X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\textstyle{\mathsf{T}_{2}X}$
Figure 3. The map $[h_{1},h_{2}]$ is a one-step frame morphism

The construction is completed by defining a marking on the covering one-step
$\mathsf{T}_{1}\times\mathsf{T}_{2}$-frame by co-tupling the markings for each
covering $\mathsf{T}_{i}$-frame, to obtain the marking $[m_{1},m_{2}]$. Since
each of the markings $m_{1},m_{2}$ factor through the co-tuple $[m_{1},m_{2}]$
via the insertions, we have $[m_{1},m_{2}](u)\subseteq m([h_{1},h_{2}](u))$
for each $u\in Y_{1}+Y_{2}$, and also $|[m_{1},m_{2}](u)|\leq 1$ for each
$u\in Y_{1}+Y_{2}$.

By naturality of one-step formulas, and again since the markings $m_{1},m_{2}$
factor through the co-tuple $[m_{1},m_{2}]$ via the insertions, we have

$Y_{1}+Y_{2},\mathsf{T}_{1}i_{1}(\rho_{1}),[m_{1},m_{2}]\Vdash^{1}\delta_{1}$

and

$Y_{1}+Y_{2},\mathsf{T}_{2}i_{2}(\rho_{2}),[m_{1},m_{2}]\Vdash^{1}\delta_{2}$

It easily follows that:

$Y_{1}+Y_{2},(\mathsf{T}_{1}i_{1}(\rho_{1}),\mathsf{T}_{2}i_{2}(\rho_{2})),[m_{1},m_{2}]\Vdash^{1}\delta_{1}\wedge\delta_{2}$

as required. So $\delta_{1}\wedge\delta_{2}$ is disjunctive.

  * Proof of Theorem 25.

Since we know the formulas in $(\mathtt{D}_{1}\otimes\mathtt{D}_{2})(A)$ are
disjunctive, we only need to check conditions (1) – (3) of Definition 3.2 one
by one: condition (1) just requires the formulas in a disjunctive bases to
contain $\top$ and be closed under disjunctions, which holds by definition of
$\mathtt{D}_{1}\otimes\mathtt{D}_{2}$. For condition (2), consider a one-step
formula in $\mathtt{1ML}_{\Lambda_{1}\otimes\Lambda_{2}}(A)$ of the form
$\heartsuit_{\lambda}\overline{\pi}$ where $\lambda\in\Lambda_{1}$ or
$\lambda\in\Lambda_{2}$. Suppose the former is the case. Then there is a
formula $\delta\in\mathtt{D}_{1}(\mathsf{P}A)$ such that such that
$\heartsuit_{\lambda}\overline{\pi}\equiv^{1}\delta[\land_{A}]$. But then
$\delta\wedge\top\in(\mathtt{D}_{1}\otimes\mathtt{D}_{2})(A)$, and this
formula is also one-step equivalent to $\heartsuit_{\lambda}\overline{\pi}$.

Finally, for condition (3), by rewriting positive one-step formulas into
disjunctive normal form (treating modalities as atomic) we only need to
consider conjunctions of the form:

$(\delta_{1}\wedge\delta_{2})\wedge(\delta_{1}^{\prime}\wedge\delta_{2}^{\prime})$

where $\delta_{1}\in\mathtt{D}_{1}(A)$, $\delta_{2}\in\mathtt{D}_{2}(A)$,
$\delta_{1}^{\prime}\in\mathtt{D}_{1}(B)$,
$\delta_{2}^{\prime}\in\mathtt{D}_{2}(B)$. Apply the distributive law of
$\mathtt{D}_{1}$ to $\delta_{1}\wedge\delta_{1}^{\prime}$ and that of
$\mathtt{D}_{2}$ to $\delta_{2}\wedge\delta_{2}^{\prime}$ to find formulas
$\gamma_{1}\in\mathtt{D}_{1}(A\times B)$ and
$\gamma_{2}\in\mathtt{D}_{2}(A\times B)$ such that
$\delta_{1}\wedge\delta_{1}^{\prime}\equiv^{1}\gamma_{1}[\theta_{A,B}]$ and
$\delta_{2}\wedge\delta_{2}^{\prime}\equiv^{1}\gamma_{2}[\theta_{A,B}]$. The
conjunction $\gamma_{1}\wedge\gamma_{2}$ is in
$(\mathtt{D}_{1}\otimes\mathtt{D}_{2})(A\times B)$ and we have:

$(\delta_{1}\wedge\delta_{2})\wedge(\delta_{1}^{\prime}\wedge\delta_{2}^{\prime})\equiv^{1}(\gamma_{1}\wedge\gamma_{2})[\theta_{A,B}]$

as required. ∎

###  8.3. Composition

The third and final example that we consider involves the _composition_
$\mathsf{T}=\mathsf{T}_{1}\circ\mathsf{T}_{2}$ of two set functors
$\mathsf{T}_{1}$ and $\mathsf{T}_{2}$. We first recall Cîrstea & Pattinson’s
definition of the combined signature in the case of composition [5].

######  Definition 8.6.

Let $\lambda\in\Lambda_{1}$ be an $m$-ary predicate lifting, and let
$\alpha_{1},\ldots,\alpha_{m}$ be one-step formulas in
$\mathtt{1ML}_{\Lambda_{2}}(A)$ for some set $A=\\{a_{1},\ldots,a_{n}\\}$.
Then we define the $n$-ary predicate lifting

$\underline{\lambda\langle\alpha_{1},\ldots,\alpha_{m}\rangle}:\breve{\mathsf{P}}^{n}\Rightarrow\breve{\mathsf{P}}\mathsf{T}$

in the obvious way:

$\underline{\lambda\langle\alpha_{1},\ldots,\alpha_{m}\rangle}_{S}:(U_{1},\ldots,U_{n})\mapsto\lambda_{\mathsf{T}_{2}S}\Big{(}\widehat{\alpha_{1}}_{S}(U_{1},\ldots,U_{n}),\ldots,\widehat{\alpha_{m}}_{S}(U_{1},\ldots,U_{n})\Big{)}.$

We let $\Lambda_{1}\circledcirc\Lambda_{2}$ denote the set of all (finitary)
predicate liftings that can be obtained in this way.

In the sequel we will often abbreviate $\Lambda_{1}\circledcirc\Lambda_{2}$ as
$\Lambda$.

######  Theorem 27.

Suppose both signatures $\Lambda_{1}$ and $\Lambda_{2}$ admit a disjunctive
basis. Then so does $\Lambda_{1}\circledcirc\Lambda_{2}$.

For the definition of the disjunctive basis of the combined signature, fix a
set $A=\\{a_{1},\ldots,a_{n}\\}$ and consider the one-step language
$\mathtt{1ML}_{\Lambda_{1}}(\mathtt{1ML}_{\Lambda_{2}}(A))$. Given a formula
$\alpha$ in this language, every occurrence of an $m$-ary
$\Lambda_{1}$-modality $\heartsuit_{\lambda}$ is of the form
$\heartsuit_{\lambda}(\gamma_{1},\ldots,\gamma_{m})$ with each
$\gamma_{i}\in\mathtt{1ML}_{\Lambda_{2}}(A)$. If we now replace each such
subformula $\heartsuit_{\lambda}(\gamma_{1},\ldots,\gamma_{m})$ with the
formula
$\heartsuit_{\underline{\lambda\langle\gamma_{1},\ldots,\gamma_{m}\rangle}}(a_{1},\ldots,a_{n})$,
we have associated with $\alpha$ a unique formula
$\alpha^{\prime}\in\mathtt{1ML}_{\Lambda}(A)$.

######  Definition 8.7.

Define

$(\mathtt{D}_{1}\circledcirc\mathtt{D}_{2})(A)\mathrel{:=}\\{\delta^{\prime}\in\mathtt{1ML}_{\Lambda}(A)\mid\delta\in\mathtt{D}_{1}(\mathtt{D}_{2}(A))\\}.$

where $\mathtt{D}_{1}$ and $\mathtt{D}_{2}$ are disjunctive bases for
$\Lambda_{1}$ and $\Lambda_{2}$, respectively.

To prove that $\mathtt{D}_{1}\circledcirc\mathtt{D}_{2}$ is a disjunctive
basis for the signature $\Lambda_{1}\circledcirc\Lambda_{2}$ we first show
that $\mathtt{D}_{1}\circledcirc\mathtt{D}_{2}(A)$ consists of disjunctive
formulas, for any set $A$.

######  Proposition 28.

Every formula in $\mathtt{D}_{1}\circledcirc\mathtt{D}_{2}(A)$ is disjunctive.

######  Proof 8.8.

It suffices to show that for an arbitrary but fixed formula
$\delta\in\mathtt{D}_{1}(\mathtt{D}_{2}(A))$, the formula
$\delta^{\prime}\in(\mathtt{D}_{1}\circledcirc\mathtt{D}_{2})(A)$ is
disjunctive.

Let $(S,\sigma,m)$ be an arbitrary one-step $\mathsf{T}$-model such that
$S,\sigma,m\Vdash^{1}\delta^{1}$, and let $\delta\in\mathtt{D}_{1}(B)$ and
$\eta:B\to\mathtt{D}_{2}(A)$ be such that $\delta=\delta_{1}[\eta]$. Consider
the one-step $\mathsf{T}_{1}$-model $(\mathsf{T}_{2}S,\sigma,m_{\eta})$ where
$m_{\eta}:\mathsf{T}_{2}S\to\mathsf{P}B$ is given by

$m_{\eta}(\rho)\mathrel{:=}\\{b\in B\mid(S,\rho,m)\Vdash^{1}\eta(b)\\}.$

Unravelling the definitions, it is not hard to show that for any formula
$\alpha_{1}\in\mathtt{1ML}_{{\Lambda}_{1}}(B)$ we have

$(S,\sigma,m)\Vdash^{1}\alpha_{1}[\eta]\text{ iff
}(\mathsf{T}_{2}S,\sigma,m_{\eta})\Vdash^{1}\alpha_{1},$ (15)

and as an immediate consequence of this we find that

$(\mathsf{T}_{2},\sigma,m_{\eta})\Vdash^{1}\delta_{1}.$

Then by disjunctiveness of $\mathtt{D}_{1}$ there is a one-step
$\mathsf{T}_{1}$-model $(Z,\zeta,n)$, where $\zeta\in\mathsf{T}_{1}Z$ and
$n:Z\to\mathsf{P}(B)$, together with a map $f:Z\to\mathsf{T}_{2}S$ such that
$(\mathsf{T}_{1}f)\zeta=\sigma$; $|n(z)|\leq 1$ and $n(z)\subseteq
m_{\eta}(f(z))$, for all $z\in Z$; and $(Z,\zeta,n)\Vdash^{1}\delta_{1}$.

Define, for $z\in Z$, $\eta_{z}\in\mathtt{D}(A)$ to be the formula $\eta(b)$
in case $b\in B$ is the unique element of $n(z)$; and set
$\eta_{z}\mathrel{:=}\top$ if $n(z)=\varnothing$. Observe that for any $z\in
Z$, the triple $(S,f(z),m)$ constitutes a $\mathsf{T}_{2}$-model; we claim
that

$(S,f(z),m)\Vdash^{1}\eta_{z}.$ (16)

To see this, clearly we only have to pay attention to the case where
$n(z)=\\{b\\}$ for some $b\in B$. But here it is immediate from $n(z)\subseteq
m_{\eta}(f(z))$ that $b\in m_{\eta}(f(z))$, and so we obtain (16) by
definition of $m_{\eta}$.

Given (16), we now use the disjunctiveness of $\mathtt{D}_{2}$ to obtain, for
each $z\in Z$, a one-step $\mathsf{T}_{2}$-model $(S_{z},\rho_{z},m_{z})$,
with $\rho_{z}\in\mathsf{T}_{2}S_{z}$ and $m_{z}:S_{z}\to\mathsf{P}(A)$,
together with a map $g_{z}:S_{z}\to S$, such that
$(T_{2}g_{z})(\rho_{z})=f(z)$; $|m_{z}|\leq 1$ and $m_{z}(t)\subseteq
m(f(t))$, for all $t\in S_{z}$; and
$(S_{z},\rho_{z},m_{z})\Vdash^{1}\eta_{z}$.

We are now ready to define the required separating cover for $(S,\sigma,m)$.
As its domain we will take the coproduct $\coprod_{z\in Z}S_{z}$, and where
for $z\in Z$ we let $i_{z}:S_{z}\to S^{\prime}$ denote the insertion map, we
define the maps $m^{\prime}:S^{\prime}\to\mathsf{P}A$ and $g:S^{\prime}\to S$
via co-tupling; in particular, we require $m\circ i_{z}=m_{z}$ and $g\circ
i_{z}=g_{z}$ for all $z\in Z$. For the definition of the distinguished element
$\sigma^{\prime}\in\mathsf{T}S^{\prime}$, we first define the map
$\rho^{\prime}:Z\to\mathsf{T}_{2}S^{\prime}$ by setting
$\rho^{\prime}(z)\mathrel{:=}(\mathsf{T}_{2}i_{z})\rho_{z}$. We then put
$\sigma^{\prime}\mathrel{:=}(\mathsf{T}_{1}\rho^{\prime})\zeta$.

It is obvious that $(S^{\prime},\sigma^{\prime},m)$ is a one-step
$\mathsf{T}$-model; we now check that together with the map $g:S^{\prime}\to
S$ is indeed a separating cover for $(S,\sigma,m)$. First of all, it is
obvious that $|m^{\prime}(s^{\prime})|\leq 1$ and $m^{\prime}(z)\subseteq
m(g(z))$, for all $s^{\prime}\in S^{\prime}$. Second, to check that

$(\mathsf{T}g)\sigma^{\prime}=\sigma$ (17)

we first observe that $(\mathsf{T}_{2}g)\circ\rho^{\prime}=f$, as can easily
verified:
$((\mathsf{T}_{2}g)\circ\rho^{\prime})(z)=(\mathsf{T}_{2}g)(\rho^{\prime}(z))=(\mathsf{T}_{2}g)((\mathsf{T}_{2}i_{z})\rho_{z})=(\mathsf{T}_{2}(g\circ
i_{z}))(\rho_{z})=(\mathsf{T}_{2}g_{z})(\rho_{z})=f(z)$. We then continue with
the following calculation:

$(\mathsf{T}g)\sigma^{\prime}=(\mathsf{T}_{1}\mathsf{T}_{2}g)((\mathsf{T}_{1}\rho^{\prime})\zeta)=((\mathsf{T}_{1}\mathsf{T}_{2}g)\circ(\mathsf{T}_{1}\rho^{\prime}))(\zeta)=(\mathsf{T}_{1}((\mathsf{T}_{2}g)\circ\rho^{\prime}))(\zeta)=(\mathsf{T}_{1}f)(\zeta)=\sigma.$

Finally, we need to prove that

$(S^{\prime},\sigma^{\prime},m^{\prime})\Vdash^{1}\delta^{\prime}.$ (18)

To see this, let $m^{\prime}_{\eta}:\mathsf{T}_{2}S^{\prime}\to\mathsf{P}B$ be
the marking given by

$m^{\prime}_{\eta}(\rho^{\prime})\mathrel{:=}\\{b\in
B\mid(S^{\prime},\rho^{\prime},m^{\prime})\Vdash^{1}\eta(b)\\},$

and consider the marking $n^{\prime}:Z\to\mathsf{P}B$ defined by
$n^{\prime}(z)\mathrel{:=}m^{\prime}_{\eta}(\rho^{\prime}_{z})$. Our key claim
is now that $n\subseteq n^{\prime}$, and we prove this as follows. In case
$n(z)=\varnothing$ there is nothing to prove; in case $n(z)\neq\varnothing$,
let $b\in B$ be the unique element of $n(z)$. Then we have

$\displaystyle b\in n(z)$ $\displaystyle\Rightarrow b\in m_{\eta}(f(z))$
(assumptions on $f$ and $n$)
$\displaystyle\Rightarrow(S,f(z),m)\Vdash^{1}\eta(b)$ (definition $m_{\eta}$)
$\displaystyle\Rightarrow(S_{z},\rho_{z},m_{z})\Vdash^{1}\eta(b)$
($(S_{z},\rho_{z},m_{z})$ is cover)
$\displaystyle\Rightarrow(S^{\prime},\rho^{\prime}_{z},m^{\prime})\Vdash^{1}\eta(b)$
(invariance under $i_{z}$, Prop. 1) $\displaystyle\Rightarrow b\in
m^{\prime}_{\eta}(\rho^{\prime}_{z})$ (definition $m^{\prime}_{\eta}$)
$\displaystyle\Rightarrow b\in n^{\prime}(z)$ (definition $n^{\prime}$)

But by the monotonicity of disjunctive formulas, it follows from $n\subseteq
n^{\prime}$ and $(Z,\zeta,n)\Vdash^{1}\delta_{1}$ that
$(Z,\zeta,n^{\prime})\Vdash^{1}\delta_{1}$. Then by invariance (Proposition 1)
we find that $(\mathsf{T}_{2}S,\sigma,m^{\prime}_{\eta})\Vdash^{1}\delta_{1}$,
and from this we may derive (18), using an analogous claim to (15).

  * Proof of Theorem 27.

Since we have verified the disjunctivity of all formulas in
$\mathtt{D}_{1}\circledcirc\mathtt{D}_{2}(A)$, it remains to check that
$\mathtt{D}_{1}\circledcirc\mathtt{D}_{2}(A)$ satisfies the closure conditions
of disjunctive bases. For condition (1) this is an immediate consequence of
the definitions. It is in fact not very hard to see that
$\mathtt{D}_{1}\circledcirc\mathtt{D}_{2}$ meets the other two closure
conditions as well, but full proofs are very tedious. In order to avoid
convoluted syntax we confine ourselves to somewhat sketchy arguments here.

For condition (2), consider a formula of the form
$\heartsuit_{\underline{\lambda\langle\alpha_{1},\ldots,\alpha_{m}\rangle}}(b_{1},\ldots,b_{n})[\pi]$,
where $\lambda\in\Lambda_{1}$, each
$\alpha_{i}\in\mathtt{1ML}_{\Lambda_{2}}(B)$ and $\pi:B\to\mathtt{Latt}(A)$.
Since $\mathtt{D}_{1}$ is a disjunctive basis for $\Lambda_{1}$, we may find
formulas $\delta_{1}\in\mathtt{D}_{1}(\\{1,\ldots,k\\})$ and
$\beta_{1},\ldots,\beta_{k}\in\mathtt{1ML}_{\Lambda_{2}}(A)$ such that
$\heartsuit_{\lambda}(\alpha_{1}[\pi],\ldots,\alpha_{m}[\pi])\equiv^{1}\delta_{1}(\beta_{1},\ldots,\beta_{k})$.
But, now using the fact that $\mathtt{D}_{2}$ is a disjunctive basis for
$\Lambda_{2}$, we may derive from Proposition 4 that each formula $\beta_{i}$
is equivalent to a formula $\gamma_{i}[\wedge_{A}]$, where
$\gamma_{i}\in\mathtt{D}_{2}(\mathsf{P}A)$. It is then a tedious but
straightforward exercise to show that
$\heartsuit_{\underline{\lambda\langle\alpha_{1},\ldots,\alpha_{m}\rangle}}(b_{1},\ldots,b_{n})[\pi]\equiv^{1}\delta^{\prime}$,
where we define $\delta\mathrel{:=}\delta_{1}(\gamma_{1},\ldots,\gamma_{k})$.

Finally, for condition (3), consider two disjunctive formulas
$\gamma^{\prime}\in\mathtt{D}_{1}\circledcirc\mathtt{D}_{2}(A)$ and
$\delta^{\prime}\in\mathtt{D}_{1}\circledcirc\mathtt{D}_{2}(B)$, where
$\gamma=\gamma_{1}[\sigma]$ and $\delta=\delta_{1}[\tau]$ for
$\gamma_{1}\in\mathtt{D}_{1}(A^{\prime})$,
$\delta_{1}\in\mathtt{D}_{1}(B^{\prime})$, and
$\sigma:A^{\prime}\to\mathtt{D}_{2}(A)$, $\tau:B^{\prime}\to\mathtt{D}_{2}(B)$
for some sets $A^{\prime}$ and $B^{\prime}$ that without loss of generality we
may take to be disjoint. $\mathtt{D}_{1}$ being a disjunctive basis yields a
formula
$\beta_{1}\in\mathtt{D}(A^{\prime}\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}B^{\prime})$ such that
$\gamma_{1}\land\delta_{1}\equiv^{1}\beta_{1}[\theta_{A^{\prime},B^{\prime}}]$.
By the disjointness of $A^{\prime}$ and $B^{\prime}$ we then have

$\gamma^{\prime}\land\delta^{\prime}\equiv^{1}\beta_{1}[\theta_{A^{\prime},B^{\prime}}][\sigma][\tau].$
(19)

Now consider an arbitrary pair $(a^{\prime},b^{\prime})\in A^{\prime}\times
B^{\prime}$; since $\mathtt{D}_{2}$ is a disjunctive basis there is a formula
$\alpha_{a^{\prime},b^{\prime}}\in\mathtt{D}_{2}(A\times B)$ such that
$\sigma_{a^{\prime}}\land\tau_{b^{\prime}}\equiv^{1}\alpha_{a^{\prime},b^{\prime}}[\theta_{A,B}]$.
Define the following substitution
$\sigma\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}\tau:A^{\prime}\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}B^{\prime}\to\
D_{2}(A^{\prime}\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}B^{\prime})$:

$\sigma\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}\tau(d)\mathrel{:=}\begin{cases}\sigma(d)&\text{
if }d\in A^{\prime}\\\ \tau(d)&\text{ if }d\in B^{\prime}\\\
\alpha_{a^{\prime},b^{\prime}}&\text{ if }d=(a^{\prime},b^{\prime})\in
A^{\prime}\times B^{\prime}\end{cases}$

It then follows from the definitions that the substitutions
$[\theta_{A^{\prime},B^{\prime}}][\sigma][\tau]$ and
$[\sigma\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}\tau][\theta_{A,B}]$
produce one-step equivalent formulas, so that combining this with (19) we
obtain that

$\gamma^{\prime}\land\delta^{\prime}\equiv^{1}\beta_{1}[\sigma\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}\tau][\theta_{A,B}].$

This suffices, since obviously we have that
$\beta_{1}[\sigma\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}\tau]\in\mathtt{D}_{1}\circledcirc\mathtt{D}_{2}(A\mathbin{\ooalign{$\cup$\cr\hfil\raise
1.80832pt\hbox{$\scriptscriptstyle\times$}\hfil\cr}}B)$. ∎

##  9\. Yoneda representation of disjunctive liftings

It is a well known fact in coalgebraic modal logic that predicate liftings
have a neat representation via an application of the Yoneda lemma. This was
explored by Schröder in [32], where it was used among other things to prove a
characterization theorem for the monotone predicate liftings. Here, we apply
the same idea to disjunctive liftings. We shall be working with a slightly
generalized notion of predicate lifting here, taking a predicate lifting over
a finite set of variables $A$ to be a natural transformation
$\lambda:\breve{\mathsf{P}}^{A}\to\breve{\mathsf{P}}\circ\mathsf{T}$. Clearly,
one-step formulas in $\mathtt{1ML}_{\Lambda}(A)$ can then be viewed as
predicate liftings over $A$.

######  Definition 9.1.

Let $\lambda:\breve{\mathsf{P}}^{A}\to\breve{\mathsf{P}}\circ\mathsf{T}$ be a
predicate lifting over variables $A=\\{a_{1},\dots,a_{n}\\}$. The _Yoneda
representation_ $y(\lambda)$ of $\lambda$ is the subset

$\lambda_{\mathsf{P}A}(\mathsf{true}_{a_{1}},\dots,\mathsf{true}_{a_{n}})\in\mathsf{P}\mathsf{T}\mathsf{P}A$

where $\mathsf{true}_{a_{i}}=\\{B\subseteq A\mid a_{i}\in B\\}$. We shall
write simply $\lambda\subseteq\mathsf{T}\mathsf{P}A$ instead of $y(\lambda)$.

######  Definition 9.2.

Given a set $A$, let $A^{\top}$ be the set $A\cup\\{\top\\}$. Let
$\epsilon_{A}\subseteq A^{\top}\times\mathsf{P}A$ be the relation defined by
$a\epsilon_{A}B$ iff $a\in B$, and $\top\epsilon_{A}B$ for all $B\subseteq A$.
Let $\eta_{A}:A^{\top}\to\mathsf{P}A$ be defined by $\eta_{A}(a)=\\{a\\}$, and
$\eta_{A}(\top)=\varnothing$.

In the remainder of this section we assume familiarity with the Barr relation
lifting $\overline{\mathsf{T}}$ associated with a functor $\mathsf{T}$; see
[21] for the definition and some basic properties.

######  Definition 9.3.

A predicate lifting $\lambda\subseteq\mathsf{T}\mathsf{P}A$ is said to be
_divisible_ if, for all $\alpha\in\lambda$ there is some
$\beta\in\mathsf{T}A^{\top}$ such that
$(\beta,\alpha)\in\overline{\mathsf{T}}(\epsilon_{A})$ and
$\mathsf{T}\eta_{A}(\beta)\in\lambda$.

######  Proposition 29.

Any disjunctive lifting over $A$ is divisible, and if $\mathsf{T}$ preserves
weak pullbacks the disjunctive liftings over $A$ are precisely the divisible
ones.

######  Proof 9.4.

Suppose $\lambda\subseteq\mathsf{T}\mathsf{P}A$ is disjunctive, and pick
$\alpha\in\lambda$. Then
$\mathsf{P}A,\alpha,\mathsf{id}_{\mathsf{P}A}\Vdash^{1}\lambda$, so since
$\lambda$ is disjunctive there are some one-step model $(X,\xi,m)$ and map
$f:X\to\mathsf{P}A$ with $m:X\to\mathsf{P}A$, $m(u)\subseteq f(u)$ for all
$u\in X$, $\mathsf{T}f(\xi)=\alpha$, and $|m(u)|\leq 1$ for all $u\in X$. We
define a map $g:X\to A^{\top}$ by setting $g:u\mapsto\top$ if
$m(u)=\varnothing$, $g:u\mapsto a$ if $m(u)=\\{a\\}$. We tuple the maps $f,g$
to get a map $\langle f,g\rangle:X\to A^{\top}\times\mathsf{P}A$. In fact,
since $m(u)\subseteq f(u)$ for all $u\in X$, we have $\langle
f,g\rangle:X\to\epsilon_{A}$. Let $\pi_{1}:\epsilon_{A}\to A^{\top}$ and
$\pi_{2}:\epsilon_{A}\to\mathsf{P}A$ be the projection maps. We have the
following diagram, in which the two triangles and the outer edges commute
(i.e., $m=\eta_{A}\circ g$).

$\textstyle{\mathsf{P}A}$$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\scriptstyle{f}$$\scriptstyle{g}$$\scriptstyle{\langle
f,g\rangle}$$\textstyle{\epsilon_{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{2}}$$\scriptstyle{\pi_{1}}$$\textstyle{A^{\top}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{A}}$

Now apply $\mathsf{T}$ to this diagram and define $\beta\in\mathsf{T}A^{\top}$
to be $\mathsf{T}(\pi_{1}\circ\langle f,g\rangle)(\xi)=\mathsf{T}g(\xi)$.
First, we have $(\beta,\alpha)\in\overline{\mathsf{T}}(\epsilon_{A})$,
witnessed by $\mathsf{T}(\langle f,g\rangle)(\xi)\in\mathsf{T}\epsilon_{A}$.
We claim that $\mathsf{T}\eta_{A}(\beta)\in\lambda$. But since
$X,\xi,m\Vdash^{1}\lambda$ and $m=\eta_{A}\circ g$, naturality of $\lambda$
applied to the map $g:X\to A^{\top}$, gives
$A^{\top},\beta,\eta_{A}\Vdash^{1}\lambda$. Another naturality argument,
applied to
$\eta_{A}:(A^{\top},\beta,\eta_{A})\to(\mathsf{P}A,\mathsf{T}\eta_{A}(\beta),\mathsf{id}_{\mathsf{P}A})$
gives
$\mathsf{P}A,\mathsf{T}\eta_{A}(\beta),\mathsf{id}_{\mathsf{P}A}\Vdash^{1}\lambda$,
i.e., $\mathsf{T}\eta_{A}(\beta)\in\lambda$.

For the converse direction, under the assumption that $\mathsf{T}$ preserves
weak pullbacks, suppose that $\lambda$ is divisible, and suppose
$X,\xi,m\Vdash^{1}\lambda$. We get $\mathsf{T}m(\xi)\in\lambda$ and so we find
some $\beta\in\mathsf{T}A^{\top}$ with
$\beta(\overline{\mathsf{T}}\epsilon_{A})\mathsf{T}m(\xi)$ and
$\mathsf{T}\eta_{A}(\beta)\in\lambda$. Pick some
$\beta^{\prime}\in\mathsf{T}\epsilon_{A}$ with
$\mathsf{T}\pi_{2}(\beta^{\prime})=\mathsf{T}m(\xi)$ and
$\mathsf{T}\pi_{1}(\beta^{\prime})=\beta$. Let $R,g_{1},g_{2}$ be the pullback
of the diagram $X\rightarrow\mathsf{P}A\leftarrow\epsilon_{A}$, shown in the
diagram:

$\textstyle{X\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{m}$$\textstyle{\mathsf{P}A}$$\textstyle{R\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{g_{1}}$$\scriptstyle{g_{2}}$$\textstyle{\epsilon_{A}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\pi_{2}}$$\scriptstyle{\pi_{1}}$$\textstyle{A^{\top}\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces\ignorespaces}$$\scriptstyle{\eta_{A}}$

By weak pullback preservation there is $\rho\in\mathsf{T}R$ with
$\mathsf{T}g_{1}(\rho)=\xi$ and $\mathsf{T}g_{2}(\rho)=\beta^{\prime}$. The
map $g_{1}:(R,\rho)\to(X,\xi)$ is thus a cover, and we have a marking
$m^{\prime}$ on $R$ defined by $\eta_{A}\circ\pi_{1}\circ g_{2}$ (follow the
bottom-right path in the previous diagram). It is now routine to check that
$R,\rho,m^{\prime}\Vdash^{1}\lambda$, and $|m^{\prime}(u)|\leq 1$ and
$m^{\prime}(u)\subseteq m(g_{1}(u))$ for all $u\in R$, so we are done.

For the moment, we leave the question open, whether a similar characterization
of disjunctive predicate liftings can be proved without weak pullback
preservation. We also leave it as an open problem to characterize the functors
that admit a disjunctive basis.

#### Acknowledgement

We thank the two anonymous referees for their detailed and helpful comments.

## References

  * [1] R. Alur, T.A. Henzinger, and O. Kupferman.  Alternating-time temporal logic.  Journal of the ACM (JACM), 49(5):672–713, 2002.
  * [2] J. Bergfeld.  Moss’s coalgebraic logic: Examples and completeness results.  Master’s thesis, Institute for Logic, Language and Computation, University of Amsterdam, 2009.
  * [3] C. Cîrstea, C. Kupke, and D. Pattinson.  EXPTIME tableaux for the coalgebraic $\mu$-calculus.  In E. Grädel and R. Kahle, editors, Computer Science Logic (CSL 2009), volume 5771 of Lecture Notes in Computer Science, pages 179–193. Springer, 2009.
  * [4] C. Cîrstea and D. Pattinson.  Modular construction of modal logics.  In Ph. Gardner and N. Yoshida, editors, Proceedings of the 15th International Conference on Concurrency Theory (CONCUR 2004), volume 3170 of LNCS, pages 258–275. Springer, 2004.
  * [5] C. Cîrstea and D. Pattinson.  Modular construction of complete coalgebraic logics.  Theoretical Computer Science, 388(1):83 – 108, 2007.
  * [6] G. D’Agostino and M. Hollenberg.  Logical questions concerning the $\mu$-calculus.  Journal of Symbolic Logic, 65:310–332, 2000.
  * [7] E.A. Emerson and C.S. Jutla.  Tree automata, mu-calculus and determinacy (extended abstract).  In Proceedings of the 32nd Symposium on the Foundations of Computer Science, pages 368–377. IEEE Computer Society Press, 1991.
  * [8] S. Enqvist, F. Seifan, and Y. Venema.  Completeness for $\mu$-calculi: a coalgebraic approach.  Technical Report PP-2017-04, Institute for Logic, Language and Computation, Universiteit van Amsterdam.  _Annals of Pure and Applied Logic_ , to appear.
  * [9] S. Enqvist, F. Seifan, and Y. Venema.  An expressive completeness theorem for coalgebraic modal mu-calculi.  Logical Methods in Computer Science, Volume 13, Issue 2.  An earlier version of this paper appeared in LICS (2015).
  * [10] S. Enqvist, F. Seifan, and Y. Venema.  Monadic second-order logic and bisimulation invariance for coalgebras.  In Proceedings of the 30th Annual ACM/IEEE Symposium on Logic in Computer Science, (LICS 2015), pages 353–365, 2015.
  * [11] S. Enqvist, F. Seifan, and Y. Venema.  Completeness for coalgebraic fixpoint logic.  In Proceedings of the 25th EACSL Annual Conference on Computer Science Logic (CSL 2016), volume 62 of LIPIcs, pages 7:1–7:19, 2016\.
  * [12] S. Enqvist and Y. Venema.  Disjunctive bases: Normal forms for modal logics.  In F. Bonchi and B. König, editors, Proceedings of the 7th Conference on Algebra and Coalgebra in Computer Science (CALCO 2017), volume 72 of Leibniz International Proceedings in Informatics (LIPIcs), pages 11:1–11:16, 2017.
  * [13] G. Fontaine, R. Leal, and Y. Venema.  Automata for coalgebras: An approach using predicate liftings.  In Automata, Languages and Programming: 37th International Colloquium ICALP’10, volume 6199 of LNCS, pages 381–392. Springer, 2010\.
  * [14] G. Fontaine and T. Place.  Frame definability for classes of trees in the mu-calculus.  In Proceedings of the 35th International Symposium on Mathematical Foundations of Computer Science (MFCS 2010), pages 381–392. Springer, 2010.
  * [15] E. Grädel, W. Thomas, and T. Wilke, editors.  Automata, Logic, and Infinite Games, volume 2500 of LNCS.  Springer, 2002.
  * [16] H.P. Gumm.  From T-coalgebras to filter structures and transition systems.  In J. L. Fiadeiro, editor, Algebra and Coalgebra in Computer Science (CALCO 2005), volume 3629 of LNCS, pages 194–212, 2005.
  * [17] D. Janin and G. Lenzi.  Relating levels of the mu-calculus hierarchy and levels of the monadic hierarchy.  In Proceedings of the 16th Annual IEEE Symposium on Logic in Computer Science (LICS 2001), pages 347–356, 2001.
  * [18] D. Janin and I. Walukiewicz.  Automata for the modal $\mu$-calculus and related results.  In J. Wiedermann and P. Hájek, editors, Mathematical Foundations of Computer Science 1995, 20th International Symposium (MFCS’95), volume 969 of LNCS, pages 552–562. Springer, 1995.
  * [19] D. Janin and I. Walukiewicz.  On the expressive completeness of the propositional $\mu$-calculus w.r.t. monadic second-order logic.  In Proceedings CONCUR ’96, 1996.
  * [20] D. Kozen.  Results on the propositional $\mu$-calculus.  Theoretical Computer Science, 27:333–354, 1983.
  * [21] C. Kupke, A. Kurz, and Y. Venema.  Completeness for the coalgebraic cover modality.  Logical Methods in Computer Science, 8(3), 2010.
  * [22] C. Kupke and Y. Venema.  Coalgebraic automata theory: basic results.  Logical Methods in Computer Science, 4, 2008.  (An earlier version of this paper appeared in LICS 2005.).
  * [23] A. Kurucz.  Combining modal logics.  In J. van Benthem, P. Blackburn, and F. Wolter, editors, Handbook of Modal Logic, pages 721–756. Elsevier, 2006.
  * [24] A. Kurz and R. Leal.  Modalities in the stone age: a comparison of coalgebraic logics.  Theoretical Computer Science, 430:88–116, 2012.
  * [25] R.A. Leal.  Predicate liftings versus nabla modalities.  Electronic Notes in Theoretical Computer Science, 203:195–220, 06 2008.
  * [26] J. Marti, F. Seifan, and Y. Venema.  Uniform interpolation for coalgebraic fixpoint logic.  In L.S. Moss and P. Sobocinski, editors, Proceedings of the Sixth Conference on Algebra and Coalgebra in Computer Science (CALCO 2015), volume 35 of LIPIcs, pages 238–252. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2015.
  * [27] L. Moss.  Coalgebraic logic.  Annals of Pure and Applied Logic, 96:277–317, 1999.  (Erratum published APAL 99:241–259, 1999).
  * [28] A.M. Mostowski.  Games with forbidden positions.  Technical Report 78, Instytut Matematyki, Uniwersytet Gdański, Poland, 1991.
  * [29] E. Pacuit and S. Salame.  Majority logic.  In Proceedings of the Ninth International Conference on Principles of Knowledge Representation and Reasoning (KR2004), pages 598–605, 2004.
  * [30] R. Parikh.  The logic of games and its applications.  Annals of Discrete Mathematics, 24:111–139, 1985.
  * [31] D. Pattinson.  Coalgebraic modal logic: soundness, completeness and decidability of local consequence.  Theoretical Computer Science, 309(1–3):177–193, 2003.
  * [32] L. Schröder.  Expressivity of coalgebraic modal logic: the limits and beyond.  Theoretical Computer Science, pages 230–247, 2008.
  * [33] L. Schröder and D. Pattinson.  Pspace bounds for rank-1 modal logics.  ACM Transactions on Computational Logic (TOCL), 10(2):13, 2009.
  * [34] L. Schröder and D. Pattinson.  Rank-1 modal logics are coalgebraic.  Journal of Logic and Computation, 20(5):1113–1147, 2010.
  * [35] Y. Venema.  Automata and fixed point logic: a coalgebraic perspective.  Information and Computation, 204:637–678, 2006.
  * [36] Y. Venema.  Lectures on the modal $\mu$-calculus.  Lecture Notes, ILLC, University of Amsterdam, 2012.
  * [37] I. Walukiewicz.  Completeness of Kozen’s axiomatisation of the propositional $\mu$-calculus.  Information and Computation, 157:142–182, 2000.