Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Hansen, Helle Hvid; Poiger, Wolfgang

doi:10.4230/LIPIcs.CALCO.2025.9

Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Helle Hvid Hansen

Bernoulli Institute of Maths, CS and AI, University of Groningen, The Netherlands Wolfgang Poiger

Institute of Computer Science of the Czech Academy of Sciences, Prague, Czech Republic

Abstract

We present a coalgebraic framework for studying generalisations of dynamic modal logics such as PDL and game logic in which both the propositions and the semantic structures can take values in an algebra $\mathbf{A}$ of truth-degrees. More precisely, we work with coalgebraic modal logic via $\mathbf{A}$ -valued predicate liftings where $\mathbf{A}$ is an $\mathsf{FL}_{\mathrm{ew}}$ -algebra, and interpret actions (abstracting programs and games) as $\mathsf{F}$ -coalgebras where the functor $\mathsf{F}$ represents some type of $\mathbf{A}$ -weighted system. We also allow combinations of crisp propositions with $\mathbf{A}$ -weighted systems and vice versa. We introduce coalgebra operations and tests, with a focus on operations which are reducible in the sense that modalities for composed actions can be reduced to compositions of modalities for the constituent actions. We prove that reducible operations are safe for bisimulation and behavioural equivalence, and prove a general strong completeness result, from which we obtain new strong completeness results for $\mathbf{2}$ -valued iteration-free PDL with $\mathbf{A}$ -valued accessibility relations when $\mathbf{A}$ is a finite chain, and for many-valued iteration-free game logic with many-valued strategies based on finite Łukasiewicz logic.

Keywords and phrases:

dynamic logic, many-valued coalgebraic logic, safety, strong completeness

Funding:

Wolfgang Poiger: Received financial support from the European Union under the project no. CZ.02.01.01/00/23_025/0008724 via the Operational Programme Jan Amos Komenský, and from the University of Groningen.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Modal and temporal logics ; Theory of computation

\rightarrow

Program reasoning

DOI:

10.4230/LIPIcs.CALCO.2025.9

Event:

11th Conference on Algebra and Coalgebra in Computer Science (CALCO 2025)

Editors:

Corina Cîrstea and Alexander Knapp

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Propositional dynamic logic (PDL) [10, 19] is a well-known modal logic for reasoning about non-deterministic programs. In PDL, programs are an explicit part of the syntax, and PDL thus combines modal reasoning with a programming language. Parikh’s game logic [30, 34] can be seen as a generalisation of PDL from programs to 2-player games, which allows for reasoning about program correctness in a distributed setting where the environment is viewed as an opponent. A variant of game logic has been applied to reason about hybrid systems [35] and neural networks [46]. Both PDL and game logic combine modal reasoning with an algebra of operations on their semantic structures. This view was abstracted into a coalgebraic framework, called coalgebraic dynamic logic [17, 16], which extends the approach to coalgebraic modal logic via predicate liftings. Coalgebraic modal logic [31, 22] allows for a uniform treatment of modal logics over a wide range of state-based structures including Kripke models, neighbourhood models, multigraphs, weighted automata and probabilistic transition systems by modelling these structures as $\mathsf{F}$ -coalgebras for some $\mathsf{Set}$ -endofunctor $\mathsf{F}$ .

In this paper, we generalise the coalgebraic dynamic framework and results from [17] to the many-valued setting. Many-valued logic, where Boolean truth-values are replaced by an algebra $\mathbf{A}$ of truth-degrees, is more suitable than classical logic when reasoning about uncertainty, vagueness, and fuzzy systems, where propositions cannot be determined as being either true or false. There are numerous approaches to many-valued modal logic, each with their own motivations [11, 12, 5, 18]. These approaches can generally be parametrised in the algebra $\mathbf{A}$ (which determines the propositional base) and whether the semantics is given by crisp relations or $\mathbf{A}$ -labelled (fuzzy) relations. Our framework is also parametric in $\mathbf{A}$ , which we assume to be (at least) an $\mathsf{FL}_{\mathrm{ew}}$ -algebra, i.e., a certain kind of residuated lattice prevalent in many-valued/fuzzy logic (Definition 1). The choice between crisp or fuzzy relations is subsumed and generalised by the choice of functor $\mathsf{F}$ . The dynamic coalgebraic setting further adds a choice of modalities (predicate liftings) and a choice of operations on $\mathsf{F}$ -coalgebras. These parameters allow us to cover a wide range of many-valued dynamic logics in a single framework, and facilitate uniform proofs which eliminates the need to reprove concrete results for each new combination of parameters. The abstract setting also helps to identify which conditions ensure that certain results hold. Our framework accommodates iteration constructs and they are included in Sections 3 & 4. However, we exclude iteration when proving (strong) completeness in Section 6. As different techniques are needed to prove (weak) completeness including iteration, this is left for future work.

As our main contributions, we (i) define a notion of reducibility for coalgebra operations and tests which entails the soundness of certain reduction axioms (Propositions 25 and 34); (ii) prove that reducible coalgebra operations and tests are safe for bisimulation and behavioural equivalence (Propositions 26 and 35); (iii) prove for finite $\mathbf{A}$ that one-step completeness of the underlying coalgebraic modal logic implies strong completeness of its dynamic version under certain conditions (Theorem 42). We note that (i) generalises [17] already in the Boolean setting, e.g., we do not require $\mathsf{F}$ to be a monad in order to axiomatise sequential composition, which allows us to include Instantial PDL [48] in our framework. By instantiating (iii) for concrete $\mathsf{F}$ , we obtain for any finite, linear $\mathsf{FL}_{\mathrm{ew}}$ -algebra $\mathbf{A}$ , strong completeness for 2-valued iteration-free PDL with $\mathbf{A}$ -labelled accessibility relations (Example 45), and if furthermore negation is an involution on $\mathbf{A}$ (e.g., Łukasiewicz logic), we obtain strong completeness for an $\mathbf{A}$ -valued version of iteration-free game logic (Example 46). To our knowledge, both of these results are new.

Related work.

Our work can be seen as a coalgebraic generalisation of the iteration-free part of the axiomatisation for many-valued PDL with many-valued relations (for any finite $\mathsf{FL}_{\mathrm{ew}}$ -algebra $\mathbf{A}$ ) in [44], and as a dynamic generalisation of the completeness theorems (via one-step completeness) for many-valued coalgebraic modal logics in [27, Theorem 23] (where $\mathbf{A}$ is a finite $\mathsf{FL}_{\mathrm{ew}}$ -algebra) and [24] (where $\mathbf{A}$ is a semi-primal algebra). Completeness and decidability for variants of many-valued PDL with crisp relations was proved in [43, 45]. Expressivity of many-valued coalgebraic logics has been studied in [2, 3] and in connection with behavioural distances in, e.g., [1].

Omitted proofs and further details can be found in Appendix A.

2 Preliminaries

Setting the scene, we recall some basics of $\mathsf{FL}_{\mathrm{ew}}$ -algebras and many-valued modal logic (Subsection 2.1) as well as coalgebraic logic via predicate liftings (Subsection 2.2).

2.1 Many-valued modal logic

The basic idea of many-valued modal logic is to replace the two-element Boolean algebra by another algebra $\mathbf{A}$ of truth-values (or truth-degrees), which is (an expansion of) a $\mathsf{FL}_{\mathrm{ew}}$ -algebra (synonymously a commutative integral residuated lattice, e.g. see [13, Section 2.2]. The name “ $\mathsf{FL}_{\mathrm{ew}}$ -algebra” stems from the fact that these algebras correspond to the Full Lambek Calculus with exchange and weakening).

Definition 1 ( $\mathsf{FL}_{\mathrm{ew}}$ -algebra).

An algebra $\mathbf{A}=\langle A,\wedge,\vee,\odot,\rightarrow,0,1\rangle$ is a (complete) $\mathsf{FL}_{\mathrm{ew}}$ -algebra if $\langle A,\wedge,\vee,0,1\rangle$ is a (complete) bounded lattice, $\langle A,\odot,1\rangle$ is a commutative monoid and $\mathbf{A}$ satisfies the residuation law $x\odot y\leq z\Leftrightarrow x\leq y\rightarrow z$ , where $\leq$ is the lattice-order.

The choice of $\mathbf{A}$ determines the underlying many-valued propositional logic. Negation is defined by $\neg x:=x\rightarrow 0$ . In particular, different choices of $\odot$ on $[0,1]\subseteq\mathbb{R}$ with its usual order ( $\wedge=\mathrm{min}$ , $\vee=\mathrm{max}$ ) give rise to different fuzzy logics [14] in (3)-(5) below.

Example 2.

The following are examples of $\mathsf{FL}_{\mathrm{ew}}$ -algebras.

(1)

Heyting algebras are $\mathsf{FL}_{\mathrm{ew}}$ -algebras with $\odot=\wedge$ , including the next two examples.
(2)

The two-element Boolean algebra $\mathbf{2}$ yields classical propositional logic.
(3)

The standard Gödel chain $\mathbf{[0,1]_{G}}$ with $\odot=\wedge$ yields infinite Gödel logic and its finite subalgebras $\mathbf{G}_{n}$ yield finite Gödel logics (see, e.g., [36]).
(4)

The standard $\mathsf{MV}$ -chain $\mathbf{[0,1]_{\text{\bf\L }}}$ with $x\odot y=\mathrm{max}\{0,(x+y)-1\}$ , $x\rightarrow y=\mathrm{min}\{1,1-x+y\}$ and its subalgebras $\text{\bf\L }_{n}=\{0,\tfrac{1}{n},\dots,\tfrac{n-1}{n},1\}$ yield Łukasiewicz logics (see, e.g., [6]).
(5)

The standard product chain $\mathbf{[0,1]_{P}}$ , with $\odot$ the usual product of reals and $x\rightarrow y=\mathrm{min}\{\tfrac{y}{x},1\}$ (with $\tfrac{y}{0}:=1$ ), yields product logic (see, e.g., [15]).

$\blacktriangleright$ Remark 3 (Semi-primal $\mathsf{FL}_{\mathrm{ew}}$ -algebras).

The algebras $\text{\bf\L }_{n}$ of Example 2(4) are examples of $\mathsf{FL}_{\mathrm{ew}}$ -algebras which are semi-primal, meaning that they satisfy a term-expressivity property generalizing the well-known functional completeness (primality) of the Boolean algebra $\mathbf{2}$ (i.e., every map $2^{n}\to 2$ is term-definable). A $\mathsf{FL}_{\mathrm{ew}}$ -algebra $\mathbf{A}$ is semi-primal if and only if for all $P\subseteq A$ , the characteristic function $\chi_{P}\colon A\to\{0,1\}$ is term-definable in $\mathbf{A}$ , i.e., there exists a unary term-function $t_{P}(x)\colon A\to A$ with $t_{P}(a)=1$ if $a\in P$ else $t_{P}(a)=0$ [25, Proposition 2.8]. Any finite $\mathsf{FL}_{\mathrm{ew}}$ -algebra has a semi-primal expansion by introducing a term for each subset. Semi-primality is the key property in the study of many-valued coalgebraic logics of [24, 23]. In the present paper, the algebra $\mathbf{A}$ is not required to be semi-primal. However, semi-primality will sometimes be convenient to find reduction axioms (e.g., Example 36(1)) or to ensure one-step completeness of coalgebraic logics (e.g., Example 43).

Let $\mathbf{A}$ be a complete $\mathsf{FL}_{\mathrm{ew}}$ -algebra. Formulas of $\mathbf{A}$ -valued modal logic are inductively defined from a countable set $\mathsf{Prop}$ of propositional variables, the algebraic signature of $\mathbf{A}$ and modalities $\Box,\Diamond$ . A crisp Kripke model is a Kripke frame $(X,R)$ together with a propositional valuation map $[\![{\cdot}]\!]\colon\mathsf{Prop}\to A^{X}$ , which is inductively extended to all formulas via

[\![{\Box\varphi}]\!](x)=\bigwedge_{xRx^{\prime}}[\![{\varphi}]\!](x^{\prime})% \quad\text{ and }\quad[\![{\Diamond\varphi}]\!](x)=\bigvee_{xRx^{\prime}}[\![{% \varphi}]\!](x^{\prime}).

(1)

More generally, in an $\mathbf{A}$ -labelled Kripke model with $\mathbf{A}$ -labelled accessibility relation $R\colon X^{2}\to A$ the semantics of modalities is given by

[\![{\Box\varphi}]\!](x)=\bigwedge_{x^{\prime}\in X}R(x,x^{\prime})\rightarrow% [\![{\varphi}]\!](x^{\prime})\quad\text{ and }\quad[\![{\Diamond\varphi}]\!](x% )=\bigvee_{x^{\prime}\in X}R(x,x^{\prime})\odot[\![{\varphi}]\!](x^{\prime}).

(2)

Strong completeness results for Gödel modal logic are found in [5] for crisp and [37] for labelled accessibility relations. For Łukasiewicz modal logics such results are found in [18] for crisp and [4] for labelled relations. The latter also includes strong completeness results for $\mathbf{A}$ -valued modal logic (crisp and labelled) for any finite $\mathsf{FL}_{\mathrm{ew}}$ -algebra expanded with truth-constants (the crisp case also requires a unique coatom). Lastly, many-valued neighbourhood semantics over arbitrary $\mathsf{FL}_{\mathrm{ew}}$ -algebras was studied in [7].

2.2 Coalgebraic logic via predicate liftings

We assume familiarity with basic category theory and coalgebra, and only briefly recall relevant definitions and fix notation. For more details, we refer to, e.g., [26, 38]. Unless stated otherwise, $\mathbf{A}$ is an arbitrary $\mathsf{FL}_{\mathrm{ew}}$ -algebra.

Definition 4 (Coalgebra).

Let $\mathsf{F}$ be a $\mathsf{Set}$ -endofunctor. An $\mathsf{F}$ -coalgebra is a map $\gamma\colon X\to\mathsf{F}X$ . A map $f\colon X\to Y$ is a coalgebra morphism from $\gamma\colon X\to\mathsf{F}X$ to $\gamma^{\prime}\colon Y\to\mathsf{F}Y$ , denoted $f\colon\gamma\to\gamma^{\prime}$ , if $\mathsf{F}f\circ\gamma=\gamma^{\prime}\circ f$ . The category of $\mathsf{F}$ -coalgebras thus defined is denoted $\mathsf{Coalg}({\mathsf{F}})$ .

Example 5.

The following are examples of (categories of) coalgebras.

(1)

It is well-known that $\mathsf{Coalg}({\mathcal{P}})$ for the covariant powerset functor $\mathcal{P}$ is isomorphic to the category of Kripke frames (with bounded morphisms).
(2)

More generally, if $\mathbf{A}$ is a complete $\mathsf{FL}_{\mathrm{ew}}$ -algebra, define the covariant $\mathbf{A}$ -powerset functor $\mathcal{P}_{\mathbf{A}}$ by $\mathcal{P}_{\mathbf{A}}X=A^{X}$ , and for $f\colon X\to Y$ , $(\mathcal{P}_{\mathbf{A}}f)(\sigma)\colon y\mapsto\bigvee\{\sigma(x)\mid f(x)=y\}$ . Coalgebras for $\mathcal{P}_{\mathbf{A}}$ are Kripke frames with $\mathbf{A}$ -labelled accessibility relations as in Subsection 2.1.
(3)

The $\mathbf{A}$ -neighbourhood functor $\mathcal{N}_{\mathbf{A}}$ is defined as $\mathcal{N}_{\mathbf{A}}:=A^{\mathrm{(-)}}\circ A^{\mathrm{(-)}}$ , where $A^{\mathrm{(-)}}$ is the contravariant hom-functor $\mathsf{Set}(-,A)$ . The monotone $\mathbf{A}$ -neighbourhood functor $\mathcal{M}_{\mathbf{A}}$ is the subfunctor of $\mathcal{N}_{\mathbf{A}}$ obtained by $\mathcal{M}_{\mathbf{A}}X=\{N\in\mathcal{N}_{\mathbf{A}}X\mid\forall\sigma_{1}% ,\sigma_{2}\in A^{X}\colon\sigma_{1}\leq\sigma_{2}\Rightarrow N(\sigma_{1})% \leq N(\sigma_{2})\}$ . With $\mathbf{A}=\mathbf{2}$ , their coalgebras are (monotone) neighbourhood frames (see, e.g., [29]), $\mathcal{N}_{\mathbf{A}}$ -coalgebras are the $\mathbf{A}$ -neighbourhood frames of [7].
(4)

The instantial neighbourhood functor is the double (covariant) powerset functor $\mathcal{P}\circ\mathcal{P}$ and the corresponding coalgebras are instantial neighbourhood frames considered in [49, 48].

Formal reasoning about classes of coalgebras is the subject of coalgebraic logic. We follow the predicate lifting approach (see, e.g., [31]; for an overview of all approaches [22]), that is, our modalities correspond to certain natural transformations. The following generalization of Boolean-valued predicate liftings is, for example, also used in [3, 27].

Definition 6 (Predicate lifting).

A $k$ -ary $A$ -predicate lifting for $\mathsf{F}$ (where $k\geq 1$ ) is a natural transformation $\lambda\colon(A^{\mathrm{(-)}})^{k}\Rightarrow A^{\mathrm{(-)}}\circ\mathsf{F}$ .

From a coalgebra $\gamma\colon X\to\mathsf{F}X$ and $A$ -predicates $[\![{\varphi_{1}}]\!],\dots,[\![{\varphi_{k}}]\!]\in A^{X}$ , with $\lambda$ as above one obtains semantics of modal formulas as $[\![{\heartsuit^{\lambda}(\varphi_{1},\dots,\varphi_{k})}]\!]=\lambda_{X}([\![% {\varphi_{1}}]\!],\dots,[\![{\varphi_{k}}]\!])\circ\gamma$ .

For all $X$ , via transposition, $\lambda_{X}\colon(A^{X})^{k}\rightarrow A^{\mathsf{F}X}$ corresponds to $\widehat{\lambda}_{X}\colon\mathsf{F}X\rightarrow A^{(A^{X})^{k}}$ . Hence $\lambda$ corresponds to a natural transformation $\widehat{\lambda}\colon\mathsf{F}\Rightarrow k\mathcal{N}_{\mathbf{A}}$ , where $k\mathcal{N}_{\mathbf{A}}$ is defined by $X\mapsto A^{(A^{X})^{k}}$ and similarly to $\mathcal{N}_{\mathbf{A}}$ on morphisms. We frequently employ this correspondence throughout the paper.

A key feature of coalgebraic logic is that modal truth is invariant under coalgebra morphisms, in particular under behavioural equivalence (cf. [22, Definition 4.1 & Corollary 4.4]). In order to have an expressive (see, e.g., [41]) modal language, i.e., where modal equivalence implies behavioural equivalence, the collection of predicate liftings needs to be able to distinguish elements in $\mathsf{F}X$ . This separation property is also required to obtain quasi-canonical models in [39] (which we will need in Section 6).

Definition 7 (Separating).

A collection $\Lambda$ of predicate liftings is separating if $\{\widehat{\lambda}\mid\lambda\in\Lambda\}$ is jointly monic, that is, $t_{1}\neq t_{2}$ in $\mathsf{F}X$ implies $\widehat{\lambda}_{X}(t_{1})\neq\widehat{\lambda}_{X}(t_{2})$ for some $\lambda\in\Lambda$ .

Example 8.

The following are predicate liftings. In (1)-(3), $\mathbf{A}$ is required to be complete.

(1)

$\mathcal{P}$ -coalgebras are crisp Kripke frames and the $\mathbf{A}$ -valued $\Box$ and $\Diamond$ modalities (Eq. (1)) correspond to unary $A$ -predicate liftings defined for $\sigma\in A^{X}$ , $Z\in\mathcal{P}(X)$ by $\lambda_{X}^{\Box}(\sigma)\colon Z\mapsto\bigwedge\sigma(Z)$ and $\lambda_{X}^{\Diamond}(\sigma)\colon Z\mapsto\bigvee\sigma(Z)$ . It can be checked that $\{\lambda^{\Box}\}$ are $\{\lambda^{\Diamond}\}$ separating.
(2)

For $\mathcal{P}_{\mathbf{A}}$ , the $\mathbf{A}$ -valued $\Box$ and $\Diamond$ modalities on $\mathbf{A}$ -labelled frames (Eq. (2)) correspond to the unary $A$ -predicate liftings defined for $\sigma\in A^{X}$ and $\rho\in\mathcal{P}_{\mathbf{A}}X$ by

$\lambda_{X}^{\Box}(\sigma)\colon\rho\mapsto\bigwedge_{x\in X}\rho(x)% \rightarrow\sigma(x)\quad\text{and}\quad\lambda_{X}^{\Diamond}(\sigma)\colon% \rho\mapsto\bigvee_{x\in X}\rho(x)\odot\sigma(x).$

Again, it can be checked that $\{\lambda^{\Box}\}$ and $\{\lambda^{\Diamond}\}$ are separating.
(3)

For $\mathcal{P}_{\mathbf{A}}$ , we obtain a Boolean-valued logic over $\mathbf{A}$ -labelled frames by considering for any $r\in\mathbf{A}$ , the unary $2$ -predicate lifting $\lambda^{r}_{X}\colon 2^{X}\to 2^{A^{X}}$ defined by $\lambda^{r}_{X}(S)=\{\rho\in A^{X}\mid\bigvee\rho(S)\geq r\}$ . The collection $\{\lambda^{r}\}_{r\in A}$ is separating (for $\mathbf{A}$ linear it suffices to let $r$ range over an order-dense subset $D\subseteq A$ ).
(4)

For $\mathcal{N}_{\mathbf{A}}$ and $\mathcal{M}_{\mathbf{A}}$ , the unary $A$ -predicate lifting $\lambda^{\mathsf{ev}}$ taking evaluations, defined by $\lambda^{\mathsf{ev}}_{X}(\sigma)=\mathsf{ev}_{\sigma}\colon N\mapsto N(\sigma)$ , corresponds to $\mathbf{A}$ -valued neighbourhood semantics [7]. One easily checks that $\{\lambda^{\mathsf{ev}}\}$ is separating for both $\mathcal{N}_{\mathbf{A}}$ and $\mathcal{M}_{\mathbf{A}}$ .
(5)

For $\mathcal{P}\circ\mathcal{P}$ and any $k\in\mathbb{N}$ , we define the $(k+1)$ -ary $2$ -predicate lifting $\lambda^{k+1}$ by $\lambda^{k+1}_{X}(S_{1},\dots,S_{k},S)=\{N\subseteq\mathcal{P}X\mid\exists Z% \in N\colon Z\subseteq S\wedge(\forall i\colon Z\cap S_{i}\neq\varnothing)\}$ . The collection $\{\lambda^{k+1}\}_{k\in\mathbb{N}}$ corresponds to the modalities of instantial neighbourhood semantics [49, 48]. It only becomes separating if we use the functor $\mathcal{P}\circ\mathcal{P}_{\mathrm{fin}}$ instead.

3 Coalgebraic dynamic logic, generalised

Before establishing syntax and semantics of general coalgebraic dynamic logic (Subsection 3.2) we introduce coalgebra operations and tests to provide semantics for the dynamic part.

3.1 Coalgebra operations and tests

For any $\mathsf{Set}$ -endofunctor $\mathsf{F}$ , we let $\mathsf{U}_{\mathsf{F}}\colon\mathsf{Coalg}({\mathsf{F}})\rightarrow\mathsf{Set}$ denote the forgetful functor sending a coalgebra to its carrier set, and we let $\mathsf{F}^{n}X=\mathsf{F}X\times\cdots\times\mathsf{F}X$ denote the $n$ -fold product (not composition of $\mathsf{F}$ ). We will often use $\vec{\gamma}$ to denote an $\mathsf{F}^{n}$ -coalgebra and identify $\vec{\gamma}$ with the $n$ -tuple $(\gamma_{1},\dots,\gamma_{n})$ of $\mathsf{F}$ -coalgebras in the obvious way. Lastly, for a category $\mathcal{C}$ we denote by $\mathcal{C}_{\mathrm{ob}}$ the discrete category (i.e., only identity morphisms) with the same objects as $\mathcal{C}$ and, slightly abusing notation, we also use $\mathsf{U}_{\mathsf{F}}$ for the analogous forgetful functor $\mathsf{Coalg}({\mathsf{F}})_{\mathrm{ob}}\to\mathsf{Set}$ .

Definition 9 (Coalgebra operation).

An $n$ -ary coalgebra operation for $\mathsf{F}$ (where $n\geq 1$ ) is a functor $O\colon\mathsf{Coalg}({\mathsf{F}^{n}})_{\mathrm{ob}}\to\mathsf{Coalg}({% \mathsf{F}})_{\mathrm{ob}}$ such that $\mathsf{U}_{\mathsf{F}}\circ O=\mathsf{U}_{\mathsf{F}^{n}}$ .

In other words, such an operation takes $n$ -many coalgebras $\gamma_{1},\dots,\gamma_{n}\colon X\to\mathsf{F}X$ and returns a composed coalgebra $O(\gamma_{1},\dots,\gamma_{n})\colon X\to\mathsf{F}X$ on the same carrier. Compatibility with morphisms is not required here, but is important later on for safety (Section 4).

Example 10.

The following are examples of coalgebra operations.

(1)
A $\mathsf{Set}$ -indexed family of maps $\theta_{X}\colon\mathsf{F}^{n}X\to\mathsf{F}X$ (not necessarily natural) induces the operation $O^{\theta}\colon\mathsf{Coalg}({\mathsf{F}^{n}})_{\mathrm{ob}}\to\mathsf{Coalg% }({\mathsf{F}})_{\mathrm{ob}}$ pointwise via $O^{\theta}(\vec{\gamma})=\theta_{X}\circ\vec{\gamma}$ . For example:
1. (i)
  
  For $\mathcal{P}$ , set-theoretical operations (e.g., $\cup$ and $\cap$ ) induce coalgebra operations.
2. (ii)
  
  More generally for $\mathcal{P}_{\mathbf{A}}$ , algebraic operations of $\mathbf{A}$ induce coalgebra operations. For example $\vee,\wedge,\odot\colon\mathcal{P}_{\mathbf{A}}^{2}X\to\mathcal{P}_{\mathbf{A}}X$ (taken pointwise) induce binary operations.
3. (iii)
  
  Similarly for $\mathcal{N}_{\mathbf{A}}$ ( $\mathcal{M}_{\mathbf{A}}$ ), any (monotone) $\mathbf{A}$ -operation induces a coalgebra operation.
4. (iv)
  
  For $\mathcal{N}_{\mathbf{A}}$ and $\mathcal{M}_{\mathbf{A}}$ , dual $(\cdot)^{\partial}$ , defined by $N^{\partial}(\sigma)=\neg N(\neg\sigma)$ , induces a unary coalgebra operation. Here, $\neg\sigma$ for $\sigma\in A^{X}$ is defined pointwise.
5. (v)
  
  The neighbourhood-wise union $N_{1}\Cup N_{2}=\{Z_{1}\cup Z_{2}\subseteq X\mid Z_{i}\in N_{i}\}$ induces a binary coalgebra operation for $\mathcal{P}\circ\mathcal{P}$ (in [48] this is the parallel composition denoted “ $\cap$ ”).
(2)
Let $(\mathsf{F},\eta,\mu)$ be a monad (see, e.g., [26, Chapter VI]). As in [17], a natural choice of sequential composition is the binary coalgebra operation given by Kleisli composition defined by $\gamma_{1}{;}\gamma_{2}=\mu_{X}\circ\mathsf{F}\gamma_{2}\circ\gamma_{1}$ . This includes the following particular examples.
1. (i)
  
  For $\mathcal{P}$ we get the usual composition of relations $x(R_{1}{;}R_{2})z\Leftrightarrow\exists y\colon xR_{1}yR_{2}z$ .
2. (ii)
  
  More generally for $\mathcal{P}_{\mathbf{A}}$ , we get the composition of $\mathbf{A}$ -labelled relations defined by $(R_{1}{;}R_{2})(x,z)=\bigvee\{R_{1}(x,y)\odot R_{2}(y,z)\mid y\in X\}$ .
3. (iii)
  
  $\mathcal{N}_{\mathbf{A}}$ and $\mathcal{M}_{\mathbf{A}}$ are monads with Kleisli composition $(\xi_{1}{;}\xi_{2})(x)(\sigma)=\xi_{1}(x)(\mathsf{ev}_{\sigma}\circ\xi_{2})$ . For $\mathbf{2}$ , this yields $S\in(N_{1}{;}N_{2})(x)\Leftrightarrow\{y\in X\mid S\in N_{2}(y)\}\in N_{1}(x)$ in particular.
(3)

For $\mathcal{P}\circ\mathcal{P}$ , which is not a monad [20], the sequential composition of instantial neighbourhoods ; of [48, Section 3] (therein denoted “ $\circ$ ”) is a binary coalgebra operation.
(4)

The counter-domain (see, e.g., [47]) is the unary coalgebra operation $\sim$ for $\mathcal{P}$ defined by ${\sim}\gamma(x)=\{x\}$ iff $\gamma(x)=\varnothing$ , otherwise ${\sim}\gamma(x)=\varnothing$ .
(5)

Lastly, Kleisli iteration $(\cdot)^{\ast}$ defined as in [16, Section 2.2] and instantial neighbourhood iteration $(\cdot)^{\ast}$ of [48, Section 4.1] are unary coalgebra operations.

The dynamic framework in [17] covers operations in items (1) and (2) of Example 10, but not the the ones in items (3) and (4).

Similarly to coalgebra operations, we now define tests. We use $\mathsf{A}$ to denote the functor of constant value $A$ (whose coalgebras are $A$ -predicates).

Definition 11 (Test).

An $A$ -test for $\mathsf{F}$ is a functor $\mathsf{test}\colon\mathsf{Coalg}({\mathsf{A}})_{\mathrm{ob}}\to\mathsf{Coalg}% ({\mathsf{F}})_{\mathrm{ob}}$ such that $\mathsf{U}_{\mathsf{F}}\circ\mathsf{test}=\mathsf{U}_{\mathsf{A}}$ .

An $A$ -test turns a formula $\varphi$ corresponding to a predicate $[\![{\varphi}]\!]\in A^{X}$ into a coalgebra $\mathsf{test}([\![{\varphi}]\!])\colon X\to\mathsf{F}X$ (intuitively speaking, the transition system for $\varphi?$ ).

Example 12.

The following are examples of tests. Our framework again generalises [17], where only tests of the form in (1) are considered.

(1)

Suppose that $\mathsf{F}$ is a pointed monad in the sense of [17, Section 2.3] and let $P\subseteq A$ be any subset (defining some “property” in $A$ ). Then we may define the $A$ -test $\mathsf{test}_{P}$ via $\mathsf{test}_{P}(\sigma)(x)=$ if $\sigma(x)\in P$ then $\eta_{X}(x)$ else $\bot_{\mathsf{F}X}$ . Informally, $\mathsf{test}_{P}(\sigma)$ can be understood as ‘if $\sigma$ evaluates to a value in $P$ then continue, else abort’. With $P=\{1\}$ , we get the tests of [17] ( $\mathbf{A}=\mathbf{2}$ ) and [45] ( $\mathbf{A}=\text{\bf\L }_{n}$ , $\mathsf{F}=\mathcal{P}$ ).
(2)

For $\mathcal{P}_{\mathbf{A}}$ , another $A$ -test (see, e.g., [44]) is given by the pointwise monoid operation $\mathsf{test}(\sigma)(x)=e_{x}\odot^{\mathrm{pw}}\sigma$ , with the “unit vector” $e_{x}(x)=1$ , otherwise $e_{x}(x^{\prime})=0$ (i.e., yielding the $\mathbf{A}$ -labelled relation $R(x,x)=\sigma(x)$ , and if $x\neq x^{\prime}$ then $R(x,x^{\prime})=0$ ).
(3)

For $\mathcal{M}_{\mathbf{A}}$ , defining $\mathsf{test}(\sigma)(x)=\mathsf{ev}_{x}\big{(}(\text{-})\odot^{\mathrm{pw}}% \sigma\big{)}$ generalizes angelic tests of game logic. E.g., in Łukasiewicz logic, $\mathsf{test}([\![{\psi}]\!])(x)([\![{\varphi}]\!])=[\![{\psi}]\!](x)\odot[\![% {\varphi}]\!](x)$ reduces the value of $[\![{\varphi}]\!](x)$ by $(1-[\![{\psi}]\!](x))$ . Demonic tests are obtained as $\mathsf{test}(\neg\sigma)^{\partial}$ , which yields $\mathsf{test}([\![{\neg\psi}]\!])^{\partial}(x)([\![{\varphi}]\!])=[\![{\psi}]% \!](x)\oplus[\![{\varphi}]\!](x)$ , i.e., adding $[\![{\psi}]\!](x)$ to $[\![{\varphi}]\!](x)$ .
(4)

For $\mathcal{P}\circ\mathcal{P}$ , the $2$ -test used in [48] can be defined similarly to (1) via $\mathsf{test}(S)(x)=\big{\{}\!\{x\}\!\big{\}}$ if $x\in S$ , otherwise $\mathsf{test}(S)(x)=\varnothing$ .

3.2 Syntax and semantics

From now on, we fix the following data and notation. Let $\mathbf{A}$ be a complete $\mathsf{FL}_{\mathrm{ew}}$ -algebra $\langle A,\wedge,\vee,\odot,\rightarrow,0,1\rangle$ , possibly extended with further operations. We write $\mathsf{sign}(\mathbf{A})$ for the algebraic signature of $\mathbf{A}$ . Let $\Lambda$ be a countable collection of $A$ -predicate liftings for the $\mathsf{Set}$ -endofunctor $\mathsf{F}$ . Let $\mathsf{Op}$ and $\mathsf{Te}$ be finite collections of coalgebra operations and $A$ -tests for $\mathsf{F}$ , respectively. We use the notation $\mathsf{ar}(o)$ , $\mathsf{ar}(\lambda)$ and $\mathsf{ar}(O)$ for the finite arity of any $o\in\mathsf{sign}(\mathbf{A})$ , $\lambda\in\Lambda$ or $O\in\mathsf{Op}$ . Lastly, let $\mathsf{Prop}$ and $\mathsf{At}$ be countably infinite sets of propositional variables and atomic actions, respectively.¹¹1We use “action” as an abstraction of “program” and “game”.

Definition 13 (Formulas & Actions).

We define the set $\mathsf{Form}$ of (dynamic) formulas and the set $\mathsf{Act}$ of actions by simultaneous induction as follows.

	$\displaystyle\mathsf{Form}\ni\varphi::=p\in\mathsf{Prop}$	$\displaystyle\text{ $\big{\|}$ }o(\varphi_{1},\dots,\varphi_{\mathsf{ar}(o)})% \phantom{.}\text{ $\big{\|}$ }\langle{a}\rangle^{\lambda}(\varphi_{1},\dots,% \varphi_{\mathsf{ar}(\lambda)})$
	$\displaystyle\mathsf{Act}\ni a::=a_{0}\in\mathsf{At}$	$\displaystyle\text{ $\big{\|}$ }O(a_{1},\dots,a_{\mathsf{ar}(O)})\text{ $\big{\|% }$ }\mathsf{test}(\varphi)$

where $o\in\mathsf{sign}(\mathbf{A})$ , $\lambda\in\Lambda$ , $O\in\mathsf{Op}$ and $\mathsf{test}\in\mathsf{Te}$ .

Note that we always have formulas of the form $\varphi\wedge\varphi$ , $\varphi\vee\varphi$ , $\varphi\odot\varphi$ and $\varphi\rightarrow\varphi$ , as well as $\top:=1$ , $\bot:=0$ and $\neg\varphi:=\varphi\rightarrow\bot$ .

Definition 14 (Model).

A (dynamic) model is a map $\gamma\colon\mathsf{Act}\to(\mathsf{F}X)^{X}$ together with a propositional valuation map $[\![{\cdot}]\!]\colon\mathsf{Prop}\to A^{X}$ .

For a model as above we write $\gamma_{a}\colon X\to\mathsf{F}X$ rather than $\gamma(a)$ . As usual, the propositional valuation is inductively extended to all formulas in $\mathsf{Form}$ via the rules

	$\displaystyle[\![{o(\varphi_{1},\dots,\varphi_{\mathsf{ar}(o)})}]\!]$	$\displaystyle=o^{\mathrm{pw}}\big{(}[\![{\varphi_{1}}]\!],\dots,[\![{\varphi_{% \mathsf{ar}(o)}}]\!]\big{)},$
	$\displaystyle[\![{\langle{a}\rangle^{\lambda}(\varphi_{1},\dots,\varphi_{% \mathsf{ar}(\lambda)})}]\!]$	$\displaystyle=\lambda_{X}\big{(}[\![{\varphi_{1}}]\!],\dots,[\![{\varphi_{% \mathsf{ar}(\lambda)}}]\!]\big{)}\circ\gamma_{a}.$

In order to fully determine a model $\gamma$ it suffices to provide a map $\gamma^{0}\colon\mathsf{At}\to(\mathsf{F}X)^{X}$ (i.e., defined on atomic actions) together with a propositional valuation map, since one can extend the valuation to all formulas as above and simultaneously extend $\gamma^{0}$ to all actions via

\gamma_{O(a_{1},\dots,a_{\mathsf{ar}(O)})}=O(\gamma_{a_{1}},\dots,\gamma_{a_{% \mathsf{ar}(O)}})\quad\text{ and }\quad\gamma_{\mathsf{test}(\varphi)}=\mathsf% {test}([\![{\varphi}]\!]).

We are mainly interested in these models which, following [17], we call standard.

Definition 15 (Standard model).

A model is called standard if it is obtained from some $\gamma^{0}\colon\mathsf{At}\to(\mathsf{F}X)^{X}$ together with a propositional valuation as explained above.

We say $\varphi$ is true at a state $x$ , if $[\![{\varphi}]\!](x)=1$ , and local semantic entailment $\Gamma\models\varphi$ holds iff every state $x$ of every standard model satisfies $[\![{\varphi}]\!](x)=1$ whenever $[\![{\psi}]\!](x)=1$ for all $\psi\in\Gamma$ .

Example 16.

The following are examples of coalgebraic dynamic logics.

(1)

To obtain $\mathbf{A}$ -valued PDL with crisp accessibility relations, set $\mathsf{F}=\mathcal{P}$ and let $\Lambda$ consist of $\lambda^{\Box}$ or $\lambda^{\Diamond}$ (or both) from 8(1), set $\mathsf{Op}=\{\cup,;,(\cdot)^{\ast}\}$ and let $\mathsf{Te}$ consist of test(s) as in 12(1). With $\mathbf{A}=\text{\bf\L }_{n}$ and $\lambda^{\Box}$ this logic is considered in [45] (used, e.g., to model searching games with errors).
(2)

To obtain $\mathbf{A}$ -valued PDL with $\mathbf{A}$ -labelled accessibility relations, set $\mathsf{F}=\mathcal{P}_{\mathbf{A}}$ , let $\Lambda$ consist of $\lambda^{\Box}$ or $\lambda^{\Diamond}$ (or both) from 8(2), set $\mathsf{Op}=\{\vee,;,(\cdot)^{\ast}\}$ and let $\mathsf{Te}$ consist of the test defined in 12(2). With $\lambda^{\Box}$ this is similar to the finitely-valued PDL considered in [44] to argue, among others, about program costs. For example, the formula $\langle{\pi_{1}}\rangle\top\rightarrow\langle{\pi_{2}}\rangle\top$ could intuitively be read as ‘executing $\pi_{1}$ is always less costly than $\pi_{2}$ ’.
(3)

To obtain $\mathbf{2}$ -valued PDL over $\mathbf{A}$ -labelled frames, again use $\mathsf{F}=\mathcal{P}_{\mathbf{A}}$ , $\mathsf{Op}=\{\vee,;,(\cdot)^{\ast}\}$ , but now with the $2$ -predicate liftings $\Lambda=\{\lambda^{r}\mid r\in A\}$ of 8(3). For example, if $\mathbf{A}$ is again thought of as describing costs of programs, the formula $\langle{\pi}\rangle^{r}\varphi$ could intuitively be read as ‘reaching $\varphi$ after executing $\pi$ may cost more than $r$ ’.
(4)

If $\mathbf{A}$ is linear and negation is involutive ( $\neg\neg r=r$ , for all $r\in A$ ) then we obtain (iteration-free) $\mathbf{A}$ -valued game logic by taking $\mathsf{F}=\mathcal{M}_{\mathbf{A}}$ with $\lambda^{\mathsf{ev}}$ of 8(4), $\mathsf{Op}=\{\vee,\wedge,(\cdot)^{\partial},;\}$ (cf. 10) and $\mathsf{Te}$ consisting of the test from 12(3). Modal formulas describe $A$ -valued strategic ability in 2-player games (say between Angel and Demon) as follows. Angel wants to maximise truth-values, Demon wants to minimise. Suppose for each game $\alpha$ , we have a monotonic neighbourhood function $S_{\alpha}\colon X\to\mathcal{M}X$ where $U\in S_{\alpha}(x)$ means that Angel has a strategy when playing $\alpha$ in state $x$ to ensure that the outcome is in $U$ . Let $N_{\alpha}(x)(\sigma)=\bigvee_{U\in S_{\alpha}(x)}\bigwedge_{y\in U}\sigma(y)$ for all states $x\in X$ and all $\sigma\in A^{X}$ . It is easy to verify monotonicity. We then have $[\![{\langle{\alpha}\rangle\varphi}]\!](x)=\bigvee_{U\in S_{\alpha}(x)}% \bigwedge_{y\in U}[\![{\varphi}]\!](y)$ , i.e., $[\![{\langle{\alpha}\rangle\varphi}]\!](x)=r$ means that at $x$ , Angel has a strategy in $\alpha$ to ensure that for any outcome $y$ , $[\![{\varphi}]\!](y)\geq r$ . In an angelic test $\langle{\psi?}\rangle\varphi$ , the truth value of $\psi$ constrains the overall truth value, and hence can be seen as a challenge for Angel, cf. 12(3). The operations ; , $(\cdot)^{\partial}$ and $\vee$ are consistent with the above interpretation and the corresponding operations on $S$ in classic game logic [34]. In particular, for all $\sigma\in A^{X}$ , $N_{\alpha^{d}}(x)(\sigma)=\neg N_{\alpha}(x)(\neg\sigma)$ is the least $\sigma$ -value that Demon can ensure when playing $\alpha$ at $x$ . If $\mathbf{A}$ is not linear or $\neg$ is not involutive then $(\cdot)^{\partial}$ can no longer be understood as introducing the other player (negation is involutive, e.g., in Łukasiewicz logic, but not in Gödel and product logic).
(5)

Setting $\mathbf{A}=\mathbf{2}$ , $\mathsf{F}=\mathcal{P}\circ\mathcal{P}$ , $\mathsf{Op}=\{\Cup,;,(\cdot)^{\ast}\}$ , $\mathsf{Te}$ consisting of the test of 12(4) and $\Lambda=\{\lambda^{k+1}\mid k\in\mathbb{N}\}$ of 8(5) we obtain Instantial PDL which was introduced in [48] as a modal logic for computation in open systems.

4 Safety and logical invariance

A fundamental compositional aspect of dynamic logics such as PDL and game logic is that operations and tests are safe for bisimilarity [47, 33], meaning that it suffices to check bisimilarity for the atomic actions to conclude bisimilarity for all actions. In our coalgebraic setting (where bisimilarity and behavioral equivalence may differ), safety can be defined as requiring that the operation preserves coalgebra morphisms.

Definition 17 (Safe coalgebra operation).

A coalgebra operation is safe if it also defines a functor $O\colon\mathsf{Coalg}({\mathsf{F}^{n}})\to\mathsf{Coalg}({\mathsf{F}})$ with $\mathsf{U}_{\mathsf{F}}\circ O=\mathsf{U}_{\mathsf{F}^{n}}$ (i.e., analogous to Definition 9).

Note that $\mathsf{U}_{\mathsf{F}}\circ O=\mathsf{U}_{\mathsf{F}^{n}}$ implies $O(f)=f$ for all coalgebra morphisms $f$ . In other words, safety ensures for $\gamma_{1},\dots,\gamma_{n}\colon X\to\mathsf{F}X$ and $\gamma^{\prime}_{1},\dots,\gamma^{\prime}_{n}\colon Y\to\mathsf{F}Y$ that if $f\colon X\to Y$ is a joint coalgebra morphism $\gamma_{i}\to\gamma^{\prime}_{i}$ , then $f$ is also a coalgebra morphism $O(\vec{\gamma})\to O(\vec{\gamma}^{\prime})$ .

The coalgebra operations of Example 10(2)-(5) are safe, which can be shown directly or for (2)-(4) as consequence of Proposition 26 later on. Contrarily, not all pointwise operations of (1) are safe (e.g., for $\mathcal{P}_{\mathbf{A}}$ it holds that $\vee$ is safe but $\wedge$ is not), due to the following.

Lemma 18.

Let $O^{\theta}\colon\mathsf{Coalg}({\mathsf{F}^{n}})_{\mathrm{ob}}\to\mathsf{Coalg% }({\mathsf{F}})_{\mathrm{ob}}$ be induced by a collection of maps $\theta_{X}\colon\mathsf{F}^{n}X\to\mathsf{F}X$ . Then $O^{\theta}$ is safe if and only if $\theta$ is a natural transformation $\mathsf{F}^{n}\Rightarrow\mathsf{F}$ .

We now define safety of tests similarly to coalgebra operations, and show that it can also be characterized by a certain naturality condition.

Definition 19 (Safe test).

An $A$ -test for $\mathsf{F}$ is safe if it also defines a functor $\mathsf{test}\colon\mathsf{Coalg}({\mathsf{A}})\to\mathsf{Coalg}({\mathsf{F}})$ with $\mathsf{U}_{\mathsf{A}}\circ O=\mathsf{U}_{\mathsf{F}}$ (i.e., analogous to Definition 11).

In the following, we use $\mathsf{F}(\text{-})^{A^{(\text{-})}}$ to denote the $\mathsf{Set}$ -functor defined by $X\mapsto(\mathsf{F}X)^{A^{X}}$ on objects and $f\mapsto\mathsf{F}f\circ(-)\circ A^{f}$ on morphisms.

Lemma 20.

A test is safe if and only if its transpose is a natural transformation $\mathsf{Id}\Rightarrow\mathsf{F}(\text{-})^{A^{(\text{-})}}$ , equivalently $\mathsf{F}f\circ\mathsf{test}(\sigma^{\prime}\circ f)=\mathsf{test}(\sigma^{% \prime})\circ f$ for every $f\colon X\to Y$ and $\sigma^{\prime}\in A^{Y}$ .

Using Lemma 20, one can show that all tests of Example 12 are safe (this is also a consequence of Proposition 35 later on).

We now state the compositionality result via safety for coalgebraic dynamic logics.

Proposition 21.

Let all members of $\mathsf{Op}$ and $\mathsf{Te}$ be safe and let $\gamma\colon\mathsf{Act}\to(\mathsf{F}X)^{X}$ and $\gamma^{\prime}\colon\mathsf{Act}\to(\mathsf{F}Y)^{Y}$ be standard models. If $f\colon\gamma_{a_{0}}\to\gamma^{\prime}_{a_{0}}$ and $[\![{p}]\!]^{\prime}\circ f=[\![{p}]\!]$ for all $a_{0}\in\mathsf{At}$ and $p\in\mathsf{Prop}$ , then this also holds for all actions $a\in\mathsf{Act}$ and formulas $\varphi\in\mathsf{Form}$ .

Since both bisimulation and behavioural equivalence are defined via joint coalgebra morphisms (see, e.g., [32, Definitions 3.5.1 & 1.3.2]), the following is an immediate consequence.

Corollary 22.

For models as in Proposition 21, if $x\in X$ and $y\in Y$ are bisimilar (beh.equiv.) for atomic actions, they also are for all actions and $[\![{\varphi}]\!](x)=[\![{\varphi}]\!]^{\prime}(y)$ holds for all $\varphi\in\mathsf{Form}$ .

Regarding expressivity of many-valued coalgebraic logics, in [3, Theorem 3] it is shown that modal equivalence implies bisimilarity for finitary, weak-pullback preserving $\mathsf{F}_{\omega}$ , given that $\Lambda$ is $\mathbf{A}$ -separating [3, Definition 4], meaning that $t_{1}\neq t_{2}$ in $\mathsf{F}(A^{n})$ implies $\lambda_{A^{n}}(\sigma)(t_{1})\neq\lambda_{A^{n}}(\sigma)(t_{2})$ for some $\lambda\in\Lambda$ and a term-definable $\sigma\colon A^{n}\to A$ . Similarly, under those circumstances one may show that in a standard model $\gamma\colon\mathsf{Act}\to(\mathsf{F}X)^{X}$ arising from $\gamma_{0}\colon\mathsf{At}\to(\mathsf{F}_{\omega}X)^{X}$ , modal equivalence implies bisimilarity with respect to all atomic actions, and therefore with respect to all actions given that every operation and test is safe.

5 Reducibility and soundness

In this section, we discuss the special classes of coalgebra operations and tests that can soundly be reduced to their constituents in a uniform (term-definable) way.

5.1 Templates and reducible coalgebra operations

Intuitively speaking, we will call the $n$ -ary coalgebra operation $O$ reducible with respect to the predicate lifting $\lambda$ if $\widehat{\lambda}\circ O(\gamma_{a_{1}},\dots,\gamma_{a_{n}})$ can be directly obtained from the logical information of $\{\widehat{\lambda^{\prime}}\circ\gamma_{a_{j}}\mid\lambda^{\prime}\in\Lambda,% j=1,\dots,n\}$ . To make this precise, we introduce the following.

Definition 23 (Template).

For $n,k\geq 1$ , the collection of $(n,k)$ -templates, denoted $\mathsf{Templ}_{n,k}$ , is the set of formulas inductively defined as follows.

\displaystyle\tau::=\omega_{1},\dots,\omega_{k}

\displaystyle\text{ $\big{|}$ }o(\tau_{1},\dots,\tau_{\mathsf{ar}(o)})\phantom% {.}\text{ $\big{|}$ }\langle{j}\rangle^{\lambda}(\tau_{1},\dots,\tau_{\mathsf{% ar}(\lambda)})\text{ with }j\in\{1,\dots,n\}

Here $\omega_{1},\dots,\omega_{k}$ are variables (“placeholders for formulas”), $o\in\mathsf{sign}(\mathbf{A})$ and $\lambda\in\Lambda$ .

Given some $(n,k)$ -template $\tau$ together with $n$ -many actions $\vec{a}=(a_{1},\dots,a_{n})$ and $k$ -many formulas $\vec{\varphi}=(\varphi_{1},\dots,\varphi_{k})$ , there is a corresponding formula $\tau[\vec{a},\vec{\varphi}]\in\mathsf{Form}$ obtained by substituting all occurrences of $\omega_{i}$ for $\varphi_{i}$ and all occurrences of $\langle{j}\rangle$ for $\langle{a_{j}}\rangle$ .

Similarly, from an $(n,k)$ -template $\tau$ together with $\vec{\gamma}=(\gamma_{1},\dots,\gamma_{n})\colon X\to\mathsf{F}^{n}X$ and $\vec{\sigma}=(\sigma_{1},\dots,\sigma_{k})\in(A^{X})^{k}$ , we inductively define $\tau[\vec{\gamma},\vec{\sigma}]\in A^{X}$ via the rules $\omega_{i}[\vec{\gamma},\vec{\sigma}]=\sigma_{i}$ and

	$\displaystyle o(\tau_{1},\dots,\tau_{\mathsf{ar}(o)})[\vec{\gamma},\vec{\sigma}]$	$\displaystyle=o^{\mathrm{pw}}\big{(}\tau_{1}[\vec{\gamma},\vec{\sigma}],\dots,% \tau_{\mathsf{ar}(o)}[\vec{\gamma},\vec{\sigma}]\big{)},$
	$\displaystyle\langle{j}\rangle^{\lambda}\big{(}\tau_{1},\dots,\tau_{\mathsf{ar% }(\lambda)})[\vec{\gamma},\vec{\sigma}]$	$\displaystyle=\lambda_{X}\big{(}\tau_{1}[\vec{\gamma},\vec{\sigma}],\dots,\tau% _{\mathsf{ar}(\lambda)}[\vec{\gamma},\vec{\sigma}]\big{)}\circ\gamma_{j},$

where, as usual, in the second equation we use $o^{\mathrm{pw}}$ to denote $o$ taken pointwise.

Definition 24 (Reducible coalgebra operation).

Let $O\in\mathsf{Op}$ be $n$ -ary and $\lambda\in\Lambda$ be $k$ -ary. We call $O$ reducible with respect to $\lambda$ if there exists an $(n,k)$ -template $\tau$ such that $\lambda_{X}(\vec{\sigma})\circ O(\vec{\gamma})=\tau[\vec{\gamma},\vec{\sigma}]$ for all $\vec{\gamma}\colon X{\to}\mathsf{F}^{n}X$ and $\vec{\sigma}\in(A^{X})^{k}$ . We call $O$ reducible if it is reducible with respect to every $\lambda\in\Lambda$ .

By design, a template witnessing reducibility yields a sound reduction axiom as follows.

Proposition 25 (Soundness).

Let $\tau$ be a $(n,k)$ -template witnessing that $O$ is reducible with respect to $\lambda$ . Then $\langle{O(a_{1},\dots,a_{n})}\rangle^{\lambda}(\varphi_{1},\dots,\varphi_{k})% \leftrightarrow\tau[\vec{a},\vec{\varphi}]$ is true at every state of any standard model.

Reducible coalgebra operations are safe (Definition 17) if $\Lambda$ is separating (Definition 7).

Proposition 26.

If $\Lambda$ is separating and $O$ is reducible, then $O$ is safe.

The converse of Proposition 26 is not necessarily true; a “typical” example of a safe but non-reducible operation being iteration (e.g., of PDL). As first examples of reducible operations we consider sequential compositions as described in Example 10. For Kleisli composition, the following is already shown in [17], the generalization from $\mathbf{2}$ to $\mathbf{A}$ being straightforward.

Example 27.

Let $\mathsf{F}$ be a monad and $\lambda\in\Lambda$ be unary with $\widehat{\lambda}\colon\mathsf{F}\to\mathcal{N}_{\mathbf{A}}$ a monad morphism. As in [17, Lemma 10], one can show $\lambda_{X}(\sigma)\circ(\gamma_{1}{;}\gamma_{2})=\lambda_{X}(\lambda_{X}(% \sigma)\circ\gamma_{2})\circ\gamma_{1}$ , in other words the operation ; is reducible with respect to $\lambda$ via the template $\tau=\langle{1}\rangle^{\lambda}\langle{2}\rangle^{\lambda}\omega$ . Thus, $\langle{a_{1}{;}a_{2}}\rangle^{\lambda}\varphi\leftrightarrow\langle{a_{1}}% \rangle^{\lambda}\langle{a_{2}}\rangle^{\lambda}\varphi$ holds in all standard models.

Example 27 applies to the logics in Example 16, items (1),(2) and (4). The next example shows that our present framework also accommodates a template for ; in item (3), where $\mathsf{F}$ is a monad but the predicate liftings $\lambda^{r}$ do not induce monad morphisms.

Example 28.

Consider the $\mathbf{2}$ -valued coalgebraic dynamic logic for $\mathcal{P}_{\mathbf{A}}$ with $\Lambda=\{\lambda^{r}\}_{r\in A}$ . If $\mathbf{A}$ is finite linear, we have $\lambda_{X}^{r}(S)\circ(\gamma_{1}{;}\gamma_{2})=\bigvee_{r_{1}\odot r_{2}\geq r% }\lambda_{X}^{r_{1}}(\lambda_{X}^{r_{2}}(S)\circ\gamma_{2})\circ\gamma_{1}$ , in other words the template $\tau=\bigvee_{r_{1}\odot r_{2}\geq r}\langle{1}\rangle^{r_{1}}\langle{2}% \rangle^{r_{2}}\omega$ witnesses ; being reducible with respect to $\lambda^{r}$ . Thus, the reduction axioms $\langle{a_{1}{;}a_{2}}\rangle^{r}\varphi\leftrightarrow\bigvee_{r_{1}\odot r_{% 2}\geq r}\langle{a_{1}}\rangle^{r_{1}}\langle{a_{2}}\rangle^{r_{2}}\varphi$ hold in all standard models.

As an example where $\mathsf{F}$ is not a monad at all, we consider Instantial PDL of Example 16(5). The reduction axioms used here are due to [48, Section 3.3].

Example 29.

For Example 16(5), the operation ; is reducible with respect to $\lambda^{k+1}$ via the $(2,k+1)$ -template $\langle{1}\rangle^{k+1}\big{(}\langle{2}\rangle^{2}(\omega_{1},\omega_{k+1}),% \dots,\langle{2}\rangle^{2}(\omega_{k},\omega_{k+1}),\langle{2}\rangle^{1}% \omega_{k+1}\big{)}$ , which is shown similarly to the proof of [48, Proposition 3]. Thus, all standard models validate the reduction axioms $\langle{a_{1}{;}a_{2}}\rangle^{k+1}(\psi_{1},\dots,\psi_{k},\varphi)% \leftrightarrow\langle{a_{1}}\rangle^{k+1}\big{(}\langle{a_{2}}\rangle^{2}(% \psi_{1},\varphi),\dots,\langle{a_{2}}\rangle^{2}(\psi_{k},\varphi),\langle{a_% {2}}\rangle^{1}\varphi\big{)}$ .

5.2 Independently reducible operations

Most remaining coalgebra operations from Example 10, in particular the ones induced by natural transformations, fall under the scope of the following “well-behaved” form of reducibility.

Definition 30 (Independent reducibility).

We call $O$ independently reducible with respect to $\lambda$ if this reducibility can be witnessed by a template in which no $\langle{j}\rangle^{\lambda^{\prime}}$ with $\lambda^{\prime}\neq\lambda$ appears.

Clearly this notion only becomes relevant if $|\Lambda|\geq 2$ . Note that in Examples 28 & 29 we already encountered reducible operations that are not independently reducible.

Independent reducibility allows us to shift our attention towards coalgebra operations for $k\mathcal{N}_{\mathbf{A}}$ and $\lambda^{\mathsf{ev}}$ taking $\mathsf{ev}_{(\sigma_{1},\dots,\sigma_{k})}\colon A^{(A^{X})^{k}}\to A$ similar to Example 8(4).

Proposition 31.

The $n$ -ary $O\in\mathsf{Op}$ is independently reducible with respect to the $k$ -ary $\lambda\in\Lambda$ if and only if there is a $n$ -ary coalgebra operation $\Omega$ for $k\mathcal{N}_{\mathbf{A}}$ that is independently reducible with respect to $\lambda^{\mathsf{ev}}$ and satisfying $\widehat{\lambda}\circ O=\Omega\circ\widehat{\lambda}^{n}$ . Reducibility of $O$ and $\Omega$ is witnessed by the same templates (up to swapping $\langle{j}\rangle^{\lambda}$ and $\langle{j}\rangle^{\lambda^{\mathsf{ev}}}$ ).

As illustrated by the following examples, one usually gets the reduction template “for free” after finding the corresponding $\Omega$ .

Example 32.

The following are examples of independent reducibility. The predicate liftings are from Example 8 and the operations from Example 10(1).

(1)

Consider $\mathcal{P}$ with $O$ induced by $\cup\colon\mathcal{P}^{2}\Rightarrow\mathcal{P}$ . For $\lambda^{\Diamond}$ , the corresponding $\Omega$ is induced by $\vee\colon\mathcal{N}_{\mathbf{A}}^{2}\to\mathcal{N}_{\mathbf{A}}$ , which is shown using the property $\bigvee_{i\in I}(r_{i}\vee s_{i})=\bigvee_{i\in I}r_{i}\vee\bigvee_{I}s_{i}$ of the complete lattice $\mathbf{A}$ . Hence we find the familiar reduction axiom $\langle{a_{1}\cup a_{2}}\rangle\varphi\leftrightarrow\langle{a_{1}}\rangle% \varphi\vee\langle{a_{2}}\rangle\varphi$ . Similarly, for $\lambda^{\Box}$ , the corresponding $\Omega$ is induced by $\wedge\colon\mathcal{N}_{\mathbf{A}}^{2}\to\mathcal{N}_{\mathbf{A}}$ , leading to $[a_{1}\cup a_{2}]\varphi\leftrightarrow[a_{1}]\varphi\wedge[a_{2}]\varphi$ .
(2)

Consider $\mathcal{P}_{\mathbf{A}}$ with $O$ induced by $\vee$ . For $\lambda^{\Diamond}$ and $\lambda^{\Box}$ we can use the same $\Omega$ as in (1). This can be shown using that the following identities hold in $\mathsf{FL}_{\mathrm{ew}}$ -algebras (see, e.g., [13, Lemma 2.6]): $(r_{1}\vee r_{2})\odot s=(r_{1}\odot s)\vee(r_{2}\odot s)\text{ and }(r_{1}% \vee r_{2})\rightarrow s=(r_{1}\rightarrow s)\wedge(r_{2}\rightarrow s).$
(3)

Consider again $\mathcal{P}_{\mathbf{A}}$ with $O$ induced by $\vee$ . If $\mathbf{A}$ is linear, then $O$ is independently reducible with respect to the ( $\mathbf{2}$ -valued) $\lambda^{r}$ , with $\Omega$ again induced by $\vee$ , due to the equivalence $\bigvee_{i\in I}s_{i}\vee s^{\prime}_{i}\geq r\text{ iff }\bigvee_{i\in I}s_{i% }\geq r\text{ or }\bigvee_{i\in I}s^{\prime}_{i}\geq r$ .
(4)

Consider $\mathcal{M}_{\mathbf{A}}$ with $O$ induced by dual $(\cdot)^{\partial}$ . With $\lambda^{\mathsf{ev}}$ , clearly $\Omega$ is itself induced by dual and we get the axiom $\langle{a^{\partial}}\rangle\varphi\leftrightarrow\neg\langle{a}\rangle\neg\varphi$ . A similar argument works for $\vee$ and $\wedge$ .
(5)

Consider $\mathcal{P}\circ\mathcal{P}$ and $O$ induced by $\Cup$ . This operation is independently reducible with respect to $\lambda^{k+1}$ by taking $\Omega$ induced by $\theta_{X}^{k+1}\colon(k+1)\mathcal{N}^{2}X\to(k+1)\mathcal{N}X$ with $\theta_{X}^{k+1}(N_{1},N_{2})\colon(S_{1},\dots,S_{k},S)\mapsto\bigvee_{K% \subseteq\{1,\dots,k\}}N_{1}(S^{K}_{1},\dots,S^{K}_{k},S)\wedge N_{2}(S^{K^{% \mathrm{c}}}_{1},\dots,S^{K^{\mathrm{c}}}_{k},S)$ , where $S_{i}^{K}=S_{i}$ if $i\in K$ , otherwise $S_{i}^{K}=X$ and $S_{i}^{K^{\mathrm{c}}}$ defined similarly for $K^{\mathrm{c}}:=\{1,\dots,k\}{\setminus}K$ (shown as in [48, Proposition 3]). Letting $\psi_{i}^{K}=\psi_{i}$ if $i\in K$ , otherwise $\psi_{i}^{K}=\top$ and similarly with $\psi_{i}^{K^{\mathrm{c}}}$ , this yields the corresponding reduction axiom $\langle{a_{1}\Cup a_{2}}\rangle(\psi_{1},\dots,\psi_{k},\varphi)% \leftrightarrow\bigvee_{K\subseteq\{1,\dots,k\}}\langle{a_{1}}\rangle(\psi^{K}% _{1},\dots,\psi^{K}_{k},\varphi)\wedge\langle{a_{2}}\rangle(\psi^{K^{\mathrm{c% }}}_{1},\dots,\psi^{K^{\mathrm{c}}}_{k},\varphi)$ .
(6)

As example with $O$ and $\Omega$ not induced operations, consider the counter-domain $\sim$ for $\mathcal{P}$ of 10(4). For $\lambda^{\Box}$ , this operation is independently reducible via $\Omega(\xi)(x)(\sigma)=\xi(x)(0)\rightarrow\sigma(x)$ , yielding the axiom $[{\sim}a]\varphi\leftrightarrow([a]\bot\rightarrow\varphi)$ .

5.3 Reducible tests

Compared to coalgebra operations, describing the condition for being able to find sound reduction axioms for tests (recall Definition 11) is rather straightforward.

Definition 33.

Let $\lambda\in\Lambda$ be a $k$ -ary predicate lifting. We call $\mathsf{test}\in\mathsf{Te}$ reducible with respect to $\lambda$ if there is a $(k+1)$ -ary $\mathbf{A}$ -term function $t(x,x_{1},\dots,x_{k})\colon A^{k+1}\to A$ such that $\lambda(\sigma_{1},\dots,\sigma_{k})\circ\mathsf{test}(\sigma)=t^{\mathrm{pw}}% (\sigma,\sigma_{1},\dots,\sigma_{k})$ for all $\sigma,\sigma_{i}\in A^{X}$ . We call $\mathsf{test}$ reducible if it is reducible with respect to every $\lambda\in\Lambda$ .

The following soundness result for tests again follows directly from the definitions.

Proposition 34.

Let $t\colon\colon A^{k+1}\to A$ witness that $\mathsf{test}$ is reducible with respect to $\lambda$ . Then $\langle{\mathsf{test}(\psi)}\rangle^{\lambda}(\varphi_{1},\dots,\varphi_{k})% \leftrightarrow t(\psi,\varphi_{1},\dots,\varphi_{k})$ is true at every state of any standard model.

We also get the following analogue of Proposition 26 for tests.

Proposition 35.

If $\Lambda$ is separating and $\mathsf{test}$ is reducible, then $\mathsf{test}$ is safe.

Example 36.

The following are examples of reducible tests.

(1)

Let $\mathsf{F}$ be a pointed monad and $\mathsf{test}_{P}$ as in 12(1), checking the “property” $P\subseteq A$ . Furthermore, assume the characteristic function $\chi_{P}$ is $\mathbf{A}$ -term definable (e.g., this holds for $\text{\bf\L }_{n}$ and any other semi-primal $\mathbf{A}$ [24]), $\lambda$ is unary and $\widehat{\lambda}$ is a monad morphism. If $\widehat{\lambda}_{X}(\bot_{\mathsf{F}X})=1$ for all $X$ (i.e., $\lambda$ is “ $\Box$ -like”), we can take $\langle{\mathsf{test}_{P}(\psi)}\rangle\varphi\leftrightarrow(\chi_{P}(\psi)% \rightarrow\varphi)$ as reduction axiom. In particular, for $P=\{1\}$ and $\mathbf{A}=\text{\bf\L }_{n}$ we recover the axiom used in [45, Proposition 2.3]. If $\widehat{\lambda}_{X}(\bot_{\mathsf{F}X})=0$ for all $X$ (i.e., $\lambda$ is “ $\Diamond$ -like”), we may take $\langle{\mathsf{test}_{P}(\psi)}\rangle\varphi\leftrightarrow(\chi_{P}(\psi)% \wedge\varphi)$ as reduction axiom.
(2)

Consider $\mathcal{P}_{\mathbf{A}}$ with $\mathsf{test}$ as in 12(2). For $\lambda^{\Box}$ we have the reduction axiom $\langle{\mathsf{test}(\psi)}\rangle\varphi\leftrightarrow(\psi\rightarrow\varphi)$ and for $\lambda^{\Diamond}$ we have the reduction axiom $\langle{\mathsf{test}(\psi)}\rangle\varphi\leftrightarrow(\psi\odot\varphi)$ .
(3)

For $\mathcal{N}_{\mathbf{A}}$ or $\mathcal{M}_{\mathbf{A}}$ , $\lambda^{\mathsf{ev}}$ and $\mathsf{test}$ from 12(3), we also have $\langle{\mathsf{test}(\psi)}\rangle\varphi\leftrightarrow(\psi\odot\varphi)$ .
(4)

For $\mathcal{P}\circ\mathcal{P}$ , $\lambda^{k+1}$ and $\mathsf{test}$ from 12(4), we get $\langle{\mathsf{test}(\psi)}\rangle^{k+1}(\varphi_{1},\dots,\varphi_{k},% \varphi)\leftrightarrow(\psi\wedge\varphi\wedge\varphi_{1}\wedge\dots\wedge% \varphi_{k})$ analogously to [48, Proposition 3].

With soundness for reducible operations taken care of, next we deal with completeness.

6 Strong completeness

From now on, assume that every member of $\mathsf{Op}$ and $\mathsf{Te}$ is reducible and that we have an axiomatization of the underlying $\mathbf{A}$ -valued coalgebraic logic of $\mathsf{F}$ and $\Lambda$ , denoted by $\mathcal{L}_{\mathsf{F}}$ .

Definition 37 (The logic $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ ).

The dynamic coalgebraic logic $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}\subseteq\mathsf{Form}$ is the smallest set of dynamic formulas satisfying the following.

$\blacksquare$

$\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ contains for every action $a\in\mathsf{Act}$ , the axioms of $\mathcal{L}_{\mathsf{F}}$ with respect to the modalities $\{\langle{a}\rangle^{\lambda}\}_{\lambda\in\Lambda}$ and is closed under the corresponding rules of $\mathcal{L}_{\mathsf{F}}$ .
$\blacksquare$

$\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ contains for every pair $(O,\lambda)\in\mathsf{Op}\times\Lambda$ , all instances of the reduction axiom $\langle{O(\vec{a})}\rangle^{\lambda}(\vec{\varphi})\leftrightarrow\tau[\vec{a}% ,\vec{\varphi}]$ , where the template $\tau$ witnesses reducibility (Subsection 5.1).
$\blacksquare$

$\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ contains for every pair $(\mathsf{test},\lambda)\in\mathsf{Te}\times\Lambda$ , all instances of the reduction axiom $\langle{\mathsf{test}(\psi)}\rangle^{\lambda}(\vec{\varphi})\leftrightarrow t(% \psi,\vec{\varphi})$ , where the term-function $t$ witnesses reducibility (Subsection 5.3).

We aim to prove strong completeness $\Gamma\models\varphi\Leftrightarrow\Gamma\vdash_{\mathcal{L}_{\mathsf{F}}^{% \mathsf{Dyn}}}\varphi$ , where the relation on the left-hand side is local semantic entailment of standard models (recall Subsection 3.2) and the relation on the right-hand side intuitively holds if $\varphi$ follows from $\Gamma$ and $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ via $\mathbf{A}$ -reasoning. It is formally defined in terms of non-modal homomorphism in the next subsection.

6.1 Non-modal homomorphisms and quasi-canonical models

Generalising maximally consistent theories for many-valued logics, we use non-modal homomorphisms [4] (also used for many-valued PDL [44] and coalgebraic logic [27]).

Definition 38 (Non-modal homomorphism).

A map $h\colon\mathsf{Form}\to\mathbf{A}$ is a non-modal homomorphism for $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ if it respects the algebraic operations of $\mathbf{A}$ and satisfies $h(\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}})=\{1\}$ .

We use $\mathcal{H}$ to denote the set of all such non-modal homomorphisms and define $\Gamma\vdash_{\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}}\varphi$ iff for all $h\in\mathcal{H}$ , $h(\Gamma)=\{1\}\Rightarrow h(\varphi)=1$ . By a standard argument, for strong completeness it suffices to find some quasi-canonical model with carrier $\mathcal{H}$ (generalising [39]).

Definition 39 (Quasi-canonical model).

A map $\zeta\colon\mathsf{Act}\to\mathsf{F}(\mathcal{H})^{\mathcal{H}}$ together with the canonical propositional valuation $[\![{p}]\!]^{\mathrm{c}}:=\mathsf{ev}_{p}$ (i.e., $h\mapsto h(p)$ ) is a quasi-canonical model for $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ if the property $[\![{\varphi}]\!]^{\mathrm{c}}=\mathsf{ev}_{\varphi}$ extends to all formulas $\varphi\in\mathsf{Form}$ .

The main result of this subsection shows that it suffices to establish a coherence property for atomic actions in order to obtain a standard quasi-canonical model.

Theorem 40.

Let $\zeta^{0}\colon\mathsf{At}\to(\mathsf{F}\mathcal{H})^{\mathcal{H}}$ be coherent for atomic actions, meaning that

\lambda_{\mathcal{H}}\big{(}\mathsf{ev}_{\varphi_{1}},\dots,\mathsf{ev}_{% \varphi_{\mathsf{ar}(\lambda)}}\big{)}\big{(}\zeta_{a_{0}}^{0}(h)\big{)}=h\big% {(}\langle{a_{0}}\rangle^{\lambda}(\varphi_{1},\dots,\varphi_{\mathsf{ar}(% \lambda)})\big{)}

holds for all $a_{0}\in\mathsf{At}$ , $\lambda\in\Lambda$ , $\varphi_{i}\in\mathsf{Form}$ and $h\in\mathcal{H}$ . Let $\zeta\colon\mathsf{Act}\to(\mathsf{F}\mathcal{H})^{\mathcal{H}}$ be the standard extension of $\zeta^{0}$ as in Definition 15. Then $\zeta$ is a quasi-canonical model for $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ .

Proof.

By mutual induction we show that $[\![{\varphi}]\!]^{c}=\mathsf{ev}_{\varphi}\colon\mathcal{H}\to A$ for all formulas $\varphi\in\mathsf{Form}$ and coherence (as in the statement) for all actions $a\in\mathsf{Act}$ hold in $\zeta$ . Only the case $\varphi=\langle{a}\rangle^{\lambda}(\varphi_{1},\dots,\varphi_{k})$ for some non-atomic action $a\in\mathsf{Act}$ and $k$ -ary $\lambda\in\Lambda$ is not immediate.

Coalgebra operations.

Let $a=O(a_{1},\dots,a_{n})$ for some $n$ -ary $O\in\mathsf{Op}$ and inductively assume that coherence holds for all $\zeta_{a_{j}}$ . Let $\tau$ be the $(n,k)$ -template corresponding to the reduction axiom for $(O,\lambda)$ contained in $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ . Then for every $h\in\mathcal{H}$ we have

h\big{(}\langle{O(a_{1},\dots,a_{n})}\rangle^{\lambda}(\varphi_{1},\dots,% \varphi_{k})\big{)}=h\big{(}\tau[a_{1},\dots,a_{n},\varphi_{1},\dots,\varphi_{% k}]\big{)},

which shows $\mathsf{ev}_{\langle{O(a_{1},\dots,a_{n})}\rangle^{\lambda}(\varphi_{1},\dots,% \varphi_{k})}=\mathsf{ev}_{\tau[a_{1},\dots,a_{n},\varphi_{1},\dots,\varphi_{k% }]}$ . On the other hand, since $\tau$ witnesses reducibility, together with the inductive hypothesis on $\varphi_{1},\dots,\varphi_{k}$ we get

	$\displaystyle[\![{\langle{O(a_{1},\dots,a_{n})}\rangle^{\lambda}(\varphi_{1},% \dots,\varphi_{k})}]\!]^{\mathrm{c}}$	$\displaystyle=\lambda_{\mathcal{H}}(\mathsf{ev}_{\varphi_{1}},\dots,\mathsf{ev% }_{\varphi_{k}})\circ O(\zeta_{a_{1}},\dots,\zeta_{a_{n}})$
		$\displaystyle=\tau[\zeta_{a_{1}},\dots,\zeta_{a_{n}},\mathsf{ev}_{\varphi_{1}}% ,\dots,\mathsf{ev}_{\varphi_{k}}].$

Thus, it suffices to show that for every $\tau\in\mathsf{Templ}_{n,k}$ it holds that $\mathsf{ev}_{\tau[\vec{a},\vec{\varphi}]}=\tau[\zeta_{\vec{a}},\mathsf{ev}_{% \vec{\varphi}}]$ , abbreviating $\zeta_{\vec{a}}=(\zeta_{a_{1}},\dots,\zeta_{a_{n}})$ and $\mathsf{ev}_{\vec{\varphi}}=(\mathsf{ev}_{\varphi_{1}},\dots,\mathsf{ev}_{% \varphi_{k}})$ . This we show by induction on the structure of $\tau$ . For $\tau=\omega_{i}$ , directly by definition we get $\mathsf{ev}_{\omega_{i}[\vec{a},\vec{\varphi}]}=\mathsf{ev}_{\varphi_{i}}=% \omega_{i}[\zeta_{\vec{a}},\mathsf{ev}_{\vec{\varphi}}]$ . For $\tau=o(\tau_{1},\dots,\tau_{\mathsf{ar}(o)})$ we use the inductive hypothesis on the $\tau_{i}$ to find

\tau[\zeta_{\vec{a}},\mathsf{ev}_{\vec{\varphi}}]=o^{\mathrm{pw}}\big{(}\tau_{% 1}[\zeta_{\vec{a}},\mathsf{ev}_{\vec{\varphi}}],\dots,\tau_{\mathsf{ar}(o)}[% \zeta_{\vec{a}},\mathsf{ev}_{\vec{\varphi}}]\big{)}=o^{\mathrm{pw}}(\mathsf{ev% }_{\tau_{1}[\vec{a},\vec{\varphi}]},\dots,\mathsf{ev}_{\tau_{\mathsf{ar}(o)}[% \vec{a},\vec{\varphi}]}).

Using that $h$ commutes with the $\mathbf{A}$ -operation $o$ we observe that this sends every $h\in\mathcal{H}$ to

o^{\mathrm{pw}}(\mathsf{ev}_{\tau_{1}[\vec{a},\vec{\varphi}]},\dots,\mathsf{ev% }_{\tau_{\mathsf{ar}(o)}[\vec{a},\vec{\varphi}]})(h)=h\big{(}o(\tau_{1}[\vec{a% },\vec{\varphi}],\dots,\tau_{\mathsf{ar}(o)}[\vec{a},\vec{\varphi}])\big{)}=h% \big{(}\tau[\vec{a},\vec{\varphi}]\big{)}

as desired. Lastly, for the case $\tau=\langle{j}\rangle^{\lambda^{\prime}}(\tau_{1},\dots,\tau_{\mathsf{ar}(% \lambda^{\prime})})$ , first we use the inductive hypothesis on the $\tau_{i}$ and get

	$\displaystyle\tau[\zeta_{\vec{a}},\mathsf{ev}_{\vec{\varphi}}]$	$\displaystyle=\lambda_{\mathcal{H}}^{\prime}\big{(}\tau_{1}[\zeta_{\vec{a}},% \mathsf{ev}_{\vec{\varphi}}],\dots,\tau_{\mathsf{ar}(\lambda^{\prime})}[\zeta_% {\vec{a}},\mathsf{ev}_{\vec{\varphi}}]\big{)}\circ\zeta_{a_{j}}$
		$\displaystyle=\lambda_{\mathcal{H}}^{\prime}(\mathsf{ev}_{\tau_{1}[\vec{a},% \vec{\varphi}]},\dots,\mathsf{ev}_{\tau_{\mathsf{ar}(\lambda^{\prime})}[\vec{a% },\vec{\varphi}]})\circ\zeta_{a_{j}}.$

Now we make use of the inductive hypothesis on coherence with respect to the action $a_{j}$ , which yields that for every $h\in\mathcal{H}$ we have

\lambda_{\mathcal{H}}^{\prime}(\mathsf{ev}_{\tau_{1}[\vec{a},\vec{\varphi}]},% \dots,\mathsf{ev}_{\tau_{\mathsf{ar}(\lambda^{\prime})}[\vec{a},\vec{\varphi}]% })\big{(}\zeta_{a_{j}}(h)\big{)}=h\big{(}\langle{a_{j}}\rangle^{\lambda^{% \prime}}(\tau_{1}[\vec{a},\vec{\varphi}],\dots,\tau_{\mathsf{ar}(\lambda^{% \prime})}[\vec{a},\vec{\varphi}])\big{)}

as desired, finishing the case of actions composed by coalgebra operations.

Tests.

The last case we discuss is $a=\mathsf{test}(\psi)$ , inductively assuming that $[\![{\psi}]\!]=\mathsf{ev}_{\psi}$ already holds. Let $t(x,x_{1},\dots,x_{k})\colon A^{k+1}\to A$ be the $\mathbf{A}$ -term-function corresponding to the reduction axiom for $(\mathsf{test},\lambda)$ in $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ . Then for any $h\in\mathcal{H}$ we get

$\displaystyle[\![{\langle{\mathsf{test}(\psi)}\rangle^{\lambda}(\vec{\varphi})% }]\!]^{\mathrm{c}}$	$\displaystyle=\lambda_{\mathcal{H}}(\mathsf{ev}_{\varphi_{1}},\dots,\mathsf{ev% }_{\varphi_{k}})\big{(}\mathsf{test}(\mathsf{ev}_{\psi})(h)\big{)}$	(Def. & Ind. Hyp.)
	$\displaystyle=t\big{(}\mathsf{ev}_{\psi}(h),\mathsf{ev}_{\varphi_{1}}(h),\dots% ,\mathsf{ev}_{\varphi_{k}}(h)\big{)}$	(Reducibility $\mathsf{test}$ )
	$\displaystyle=t\big{(}h(\psi),h(\varphi_{1}),\dots,h(\varphi_{k})\big{)}=h\big% {(}t(\psi,\vec{\varphi})\big{)}.$	(Definition $\mathsf{ev}$ , $h\in\mathcal{H}$ )

Finally, we have $h(t(\psi,\vec{\varphi}))=h(\langle{\mathsf{test}(\psi)}\rangle\vec{\varphi})$ since this reduction axiom is included in $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ . $\hfill\blacktriangleleft$

Note that this theorem does not require extra assumptions on $\mathbf{A}$ . In the next subsection we offer a way to prove existence of quasi-canonical models for finite $\mathbf{A}$ .

6.2 Finite one-step completeness

Our strategy to obtain quasi-canonical models, inspired by [39], relies on the assumption that the underlying coalgebraic logic $\mathcal{L}_{\mathsf{F}}$ is strongly one-step complete over finite sets. While [17] follows a similar strategy, here we adapt the proof of [39, Theorem 2.5] more directly.

First, recall that a formula is rank-1 if every propositional variable is in the scope of precisely one modality. For any set $X$ , we define the set of formal expressions $\Lambda(A^{X}):=\{\heartsuit^{\lambda}(\sigma_{1},\dots,\sigma_{\mathsf{ar}(% \lambda)})\mid\lambda\in\Lambda,\sigma_{i}\in A^{X}\}$ . We call $H\colon\Lambda(A^{X})\to A$ a rank-1 non-modal homomorphism for $\mathcal{L}_{\mathsf{F}}$ if $H$ (extended to $\mathbf{A}$ -term combinations of $\Lambda(A^{X})$ in the obvious way) sends all instances of rank-1 formulas of $\mathcal{L}_{\mathsf{F}}$ to $1$ . We say that $H$ is (one-step) satisfiable if there exists some $\alpha\in\mathsf{F}X$ such that $\lambda_{X}(\sigma_{1},\dots,\sigma_{\mathsf{ar}(\lambda)})(\alpha)=H\big{(}% \heartsuit^{\lambda}(\sigma_{1},\dots,\sigma_{\mathsf{ar}(\lambda)})\big{)}$ holds for all $\lambda\in\Lambda$ and $\sigma_{i}\in A^{X}$ . The following is a generalisation of [39, Definition 2.4].

Definition 41 (Finite one-step completeness).

$\mathcal{L}_{\mathsf{F}}$ is strongly one-step complete over finite sets if every rank-1 non-modal homomorphism $H\colon\Lambda(A^{X})\to A$ with finite $X$ is satisfiable.

Recalling more terminology of [39], a surjective $\omega$ -cochain of finite sets is a sequence of finite sets $(X_{m})_{m\in\mathbb{N}}$ together with surjective projection maps $p_{m}\colon X_{m+1}\to X_{m}$ . Its inverse limit $\varprojlim X_{m}$ consists of all sequences $(x_{m})\in\prod X_{m}$ that are coherent, that is $p_{m}(x_{m+1})=x_{m}$ . The functor $\mathsf{F}$ weakly preserves inverse limits of surjective $\omega$ -cochains of finite sets if $\mathsf{F}(\varprojlim X_{i})\to\varprojlim\mathsf{F}X_{i}$ is surjective. For brevity we call such $\mathsf{F}$ weakly preserving.

The main theorem of this subsection is the following adaptation of [39, Theorem 2.5] to the dynamic setting. In order to use Definition 41, we need $\mathbf{A}$ itself to be finite.

Theorem 42.

For $\mathbf{A}$ finite, $\Lambda$ separating, $\mathsf{F}$ weakly preserving, and $\mathcal{L}_{\mathsf{F}}$ strongly one-step complete over finite sets, there exists a quasi-canonical model for $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ .

Proof.

Fix an arbitrary atomic action $a\in\mathsf{At}$ and an arbitrary non-modal homomorphism $h\in\mathcal{H}$ . It suffices to show that there exists some $\alpha\in\mathsf{F}\mathcal{H}$ such that

\lambda_{\mathcal{H}}(\mathsf{ev}_{\varphi_{1}},\dots,\mathsf{ev}_{\varphi_{% \mathsf{ar}(\lambda)}})(\alpha)=h\big{(}\langle{a}\rangle^{\lambda}(\varphi_{1% },\dots,\varphi_{\mathsf{ar}(\lambda)})\big{)}

for all $\lambda\in\Lambda$ and all $\varphi_{1},\dots,\varphi_{\mathsf{ar}(\lambda)}\in\mathsf{Form}$ , since we can then define $\zeta_{a}^{0}(h):=\alpha$ , which ensures $\zeta_{a}^{0}$ is coherent as in Theorem 40. Equivalently, setting $\mathcal{F}=\{\mathsf{ev}_{\varphi}\mid\varphi\in\mathsf{Form}\}\subseteq A^{% \mathcal{H}}$ and letting $H_{a}\colon\Lambda(\mathcal{F})\to A$ be defined by $\heartsuit^{\lambda}(\mathsf{ev}_{\varphi_{1}},\dots,\mathsf{ev}_{\varphi_{% \mathsf{ar}(\lambda)}})\mapsto h(\langle{a}\rangle(\varphi_{1},\dots,\varphi_{% \mathsf{ar}(\lambda)}))$ , we need to show that $H_{a}$ is one-step satisfiable in $\mathsf{F}\mathcal{H}$ .

Enumerate the sets $\mathsf{Prop}$ , $\mathsf{Act}$ and $\Lambda$ (recall from Subsection 3.2 that these were assumed countable). For all $m\in\mathbb{N}$ , let $\mathsf{Form}^{(m)}\subseteq\mathsf{Form}$ be the set of formulas $\varphi$ such that $\varphi$ only contains the first $m$ -many propositional variables, actions and predicate liftings according to these enumerations, and $\varphi$ has modal depth at most $m$ and at most $m$ occurrences of $\mathbf{A}$ -connectives. Note that $\mathsf{Form}^{(m)}$ is finite. Furthermore, for all $m\in\mathbb{N}$ , define the collection of restrictions of non-modal homomorphisms $\mathcal{H}^{(m)}=\{h{\restriction}_{\mathsf{Form}^{(m)}}\mid h\in\mathcal{H}\}$ . Since $\mathbf{A}$ and $\mathsf{Form}^{(m)}$ are finite, the sets $\mathcal{H}^{(m)}$ are also finite. It is easily seen that $\mathcal{H}\cong\varprojlim\mathcal{H}^{(m)}$ where all projection maps are given by restrictions.

Now set $\mathcal{F}^{(m)}=\{\mathsf{ev}_{\varphi}\mid\varphi\in\mathsf{Form}^{(m)}\}% \subseteq A^{\mathcal{H}^{(m)}}$ and let $H^{(m)}_{a}\colon\Lambda(\mathcal{F}^{(m)})\to A$ be the corresponding restriction of $H_{a}$ . Since we included the axioms for $\mathcal{L}_{\mathsf{F}}$ (“instantiated” for $a$ ) in $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ and since $h$ is a non-modal homomorphism for $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ , it follows that $H^{(m)}_{a}$ is a rank-1 non-modal homomorphism for $\mathcal{L}_{\mathsf{F}}$ . Thus, by strong one-step completeness over finite sets, we get some $\alpha^{(m)}\in\mathsf{F}(\mathcal{H}^{(m)})$ which one-step satisfies $H^{(m)}_{a}$ .

Since $\Lambda$ is separating, the sequence $(\alpha^{(m)})$ is coherent, that is, an element of $\varprojlim\mathcal{H}^{(m)}$ . Lastly, since $\mathsf{F}$ is weakly preserving, there exists some $\alpha\in\mathsf{F}\mathcal{H}$ which induces this sequence. To check that this $\alpha$ one-step satisfies $H_{a}$ , for $\lambda\in\Lambda$ and $\varphi_{1},\dots,\varphi_{\mathsf{ar}(\lambda)}$ choose $m$ sufficiently large to ensure $\langle{a}\rangle^{\lambda}(\varphi_{1},\dots,\varphi_{\mathsf{ar}(\lambda)})% \in\mathsf{Form}^{(m)}$ . Then naturality of $\lambda$ applied to the limit projection $\mathcal{H}\to\mathcal{H}^{(m)}$ finally yields

	$\displaystyle\lambda_{\mathcal{H}}(\mathsf{ev}_{\varphi_{1}},\dots,\mathsf{ev}% _{\varphi_{\mathsf{ar}(\lambda)}})(\alpha)$	$\displaystyle=\lambda_{\mathcal{H}^{(m)}}(\mathsf{ev}_{\varphi_{1}},\dots,% \mathsf{ev}_{\varphi_{\mathsf{ar}(\lambda)}})(\alpha^{(m)})$
		$\displaystyle=H_{a}^{(m)}\big{(}\heartsuit^{\lambda}(\mathsf{ev}_{\varphi_{1}}% ,\dots,\mathsf{ev}_{\varphi_{\mathsf{ar}(\lambda)}})\big{)}$
		$\displaystyle=H_{a}\big{(}\heartsuit^{\lambda}(\mathsf{ev}_{\varphi_{1}},\dots% ,\mathsf{ev}_{\varphi_{\mathsf{ar}(\lambda)}})\big{)}=h\big{(}\langle{a}% \rangle^{\lambda}(\varphi_{1},\dots,\varphi_{\mathsf{ar}(\lambda)})\big{)}$

as desired, due to our construction of the $\alpha^{(m)}$ . This finishes the proof. $\hfill\blacktriangleleft$

Lastly, we apply this to (the iteration-free parts of) the dynamic logics of Example 16.

Example 43 (Many-valued PDL, crisp accessibility).

Consider the iteration-free part of the dynamic logic from Example 16(1), in particular, $\mathsf{F}=\mathcal{P}$ and $\Lambda=\{\lambda^{\Box}\}$ (Example 8(1)). Since $\mathcal{P}$ is weakly preserving [39, Example 3.1], for finite $\mathbf{A}$ we can apply Theorem 42 with the reduction axioms (for the last reduction axiom, we need $\chi_{P}$ to be term-definable in $\mathbf{A}$ )

[a_{1}{;}a_{2}]p\leftrightarrow[a_{1}][a_{2}]p,\quad[a_{1}\cup a_{2}]p% \leftrightarrow[a_{1}]p\wedge[a_{2}]p,\quad[\mathsf{test}_{P}(\varphi)]p% \leftrightarrow(\chi_{P}(\varphi)\rightarrow p)

of Example 27, Example 32(1), Example 36(1), respectively. For the underlying logic $\mathcal{L}_{\mathsf{F}}$ , one may consider the axiomatizations of [4, Subsection 4.4] if $\mathbf{A}$ is endowed with truth-constants and has a unique coatom (for $\mathbf{A}=\mathbf{G}_{n}$ a finite Gödel chain without constants see [5, Section 4]) or [24, Subsection 4.1] if $\mathbf{A}$ is semi-primal. In particular, the latter holds for finite Łukasiewicz-chains $\text{\bf\L }_{n}$ (also see [18, 4]), hence this may be used to obtain strong completeness for the iteration-free part of $\text{\bf\L }_{n}$ -valued PDL with crisp accessibility relations considered in [45].

Example 44 (Many-valued PDL, labelled accessibility).

Consider the iteration-free part of the dynamic logic from Example 16(2), in particular, $\mathsf{F}=\mathcal{P}_{\mathbf{A}}$ and $\Lambda=\{\lambda^{\Box}\}$ (Example 8(2)). If $\mathbf{A}$ is linear, then $\mathcal{P}_{\mathbf{A}}$ is weakly preserving (whether linearity is necessary is left open here). Thus, Theorem 42 is applicable for finite linear $\mathbf{A}$ with reduction axioms

[a_{1}{;}a_{2}]p\leftrightarrow[a_{1}][a_{2}]p,\quad[a_{1}\vee a_{2}]p% \leftrightarrow[a_{1}]p\wedge[a_{2}]p,\quad[\mathsf{test}(\varphi)]p% \leftrightarrow(\varphi\rightarrow p)

of Example 27, Example 32(2), Example 36(2), respectively. If $\mathbf{A}$ is endowed with canonical truth-constants $\check{c}$ for all $c\in\mathbf{A}$ , for an axiomatization of $\mathcal{L}_{\mathsf{F}}$ consider the one from [4, Subsection 4.2] (for $\mathbf{A}=\text{\bf\L }_{n}$ without constants see [4, Subsection 5.1]). In particular, this may be used to obtain strong completeness for the iteration-free part of $\mathbf{A}$ -valued PDL with $\mathbf{A}$ -labelled accessibility relations of [44] (with tests added). Using $\Lambda=\{\lambda^{\Diamond}\}$ instead (note that $\Box$ and $\Diamond$ are not necessarily inter-definable since $\neg$ need not be involutive), the corresponding reduction axioms are $\langle{a_{1}{;}a_{2}}\rangle p\leftrightarrow\langle{a_{1}}\rangle\langle{a_{% 2}}\rangle p$ , $\langle{a_{1}\vee a_{2}}\rangle p\leftrightarrow\langle{a_{1}}\rangle p\vee% \langle{a_{2}}\rangle p$ and $\langle{\mathsf{test}(\varphi)p}\rangle\leftrightarrow(\varphi\odot p)$ . For $\mathcal{L}_{\mathsf{F}}$ , we can use the axiomatization $\Diamond(p\vee q)\leftrightarrow\Diamond p\vee\Diamond q$ and $\Diamond(p\odot\check{c})\leftrightarrow\Diamond p\odot\check{c}$ for all $c\in\mathbf{A}$ .

Example 45 (Two-valued PDL, labelled accessibility).

Consider the iteration-free part of the dynamic logic from Example 16(3), in particular, $\mathsf{F}=\mathcal{P}_{\mathbf{A}}$ and $\Lambda=\{\lambda^{r}\mid r\in A\}$ , the $2$ -predicate liftings of Example 8(3). Let $\mathbf{A}$ be finite linear, then Theorem 42 applies with the reduction axioms

\langle{a_{1}{;}a_{2}}\rangle^{r}p\leftrightarrow\bigvee_{r_{1}\odot r_{2}\geq r% }\langle{a_{1}}\rangle^{r_{1}}\langle{a_{2}}\rangle^{r_{2}}p,\quad\langle{a_{1% }\vee a_{2}}\rangle^{r}p\leftrightarrow\langle{a_{1}}\rangle^{r}p\vee\langle{a% _{2}}\rangle^{r}p,\quad\langle{\mathsf{test}(\varphi)}\rangle^{r}p% \leftrightarrow(\varphi\wedge p)

of Example 28, Example 32(3) and Example 12(1), respectively. An axiomatization of the underlying $\mathcal{L}_{\mathsf{F}}$ is found in [28, Definition 4.5].

Example 46 (Many-valued game logic).

Consider the iteration-free part of the dynamic logic of Example 16(4), in particular, $\mathsf{F}=\mathcal{M}_{\mathbf{A}}$ , $\Lambda=\{\lambda^{\mathsf{ev}}\}$ (Example 8(4)) and $\mathbf{A}$ is finite, linear with involutive negation (e.g., $\mathbf{A}=\text{\bf\L }_{n}$ ). The functor $\mathcal{M}_{\mathbf{A}}$ is weakly preserving for any $\mathsf{FL}_{\mathrm{ew}}$ -algebra $\mathbf{A}$ . Since $\mathbf{A}$ is finite, Theorem 42 applies with the reduction axioms

	$\displaystyle\langle{a_{1}{;}a_{2}}\rangle p\leftrightarrow\langle{a_{1}}% \rangle\langle{a_{2}}\rangle p,\quad\langle{a_{1}\vee a_{2}}\rangle p% \leftrightarrow\langle{a_{1}}\rangle p\vee\langle{a_{2}}\rangle p,\quad\langle% {a_{1}\wedge a_{2}}\rangle p\leftrightarrow\langle{a_{1}}\rangle p\wedge% \langle{a_{2}}\rangle p,$
	$\displaystyle\quad\langle{a^{\partial}}\rangle p\leftrightarrow\neg\langle{a}% \rangle\neg p,\quad\quad\quad\langle{\mathsf{test}(\varphi)}\rangle p% \leftrightarrow(\varphi\odot p)$

of Example 27, Example 32(4) and Example 36(3). For $\mathcal{L}_{\mathsf{F}}$ with $\mathbf{A}=\text{\bf\L }_{n}$ , we can add the monotonicity axiom $\heartsuit^{\mathsf{ev}}p\rightarrow\heartsuit^{\mathsf{ev}}(p\vee q)$ to the axiomatisation of $\text{\bf\L }_{n}$ in [6] to obtain strong completeness for $\text{\bf\L }_{n}$ -based game logic.

Example 47 (Instantial PDL).

Consider iteration-free Instantial PDL similarly to Example 16(5) with $\mathsf{F}=\mathcal{P}\circ\mathcal{P}_{\mathrm{fin}}$ (to ensure separation, the case $\mathcal{P}\circ\mathcal{P}$ is left open here) and $\Lambda=\{\lambda^{k+1}\mid k\geq 0\}$ as in Example 8(5). This functor is weakly preserving, which is proved as for $\mathcal{P}$ . Thus, Theorem 42 is applicable with the reduction axioms from [48] (see also Examples 29 & 5.2(5) & 36(4)) for $\mathsf{Op}=\{;,\Cup\}$ and $\mathsf{Te}=\{\mathsf{test}\}$ as in Example 12(4). For the underlying logic $\mathcal{L}_{\mathsf{F}}$ , a clear candidate is the rank-1 axiomatization of [49, Section 4].

To the best of our knowledge, Examples 45 and 46, Example 44 with $\lambda^{\Diamond}$ (or tests included) and Example 43 with $\mathbf{A}\neq\text{\bf\L }_{n}$ are novel results. Example 47 is not covered by the results in [17] and thus further demonstrates the generality of the present framework.

7 Future work

An obvious question for future consideration is how to prove completeness with non-reducible operations like iteration. Since this paper generalises [17], one would reasonably attempt to generalise its follow-up [16]. However, this could be challenging in the many-valued case, for example [44] needs to replace $(\cdot)^{\ast}$ by $(\cdot)^{+}$ and omit tests for technical reasons. A coalgebraic analysis may shed light on the nature of these issues, helping to resolve them in the future.

Other interesting questions arise regarding safety. For PDL, [47] shows that all safe first-order definable $\mathcal{P}$ -operations are combinations of $\cup$ , ; , $\sim$ and propositional tests. A similar result for game logic is shown in [33]. One could try to characterise safe coalgebra operations that are first-order definable via coalgebraic correspondence theory [40]. In work on behavioural/logical distances [1], algebras of truth-values are often assumed to be commutative integral quantales. We note that complete $\mathsf{FL}_{\mathrm{ew}}$ -algebras can be seen as a subclass of these. In this context, safety could perhaps be studied as non-expansion of behavioural/logical distance.

While we only consider $\mathsf{Set}$ -functors here, it would be interesting to explore these topics over various other base categories, such as the category of measurable spaces to accommodate probabilistic dynamic logics [21, 9]. This category could also be quantale-enriched (relating this to the previous paragraph) or poset-enriched (as in positive coalgebraic logic [8]).

Lastly we mention that completeness, as in Section 6, for coalgebraic logics valued in an infinite $\mathbf{A}$ currently seems out of reach. One likely reason for this is the (as of yet) lack of research in many-valued coalgebraic logic (some of the few examples are [42, 2, 3, 23, 24, 27]). Therefore, we also advocate for future research in this area.

References

[1] Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive Quantale-Valued Logics for Coalgebras: An Adjunction-Based Approach. In Olaf Beyersdorff, Mamadou M. Kanté, Orna Kupferman, and Daniel Lokshtanov, editors, 41st International Symposium on Theoretical Aspects of Computer Science (STACS’24), volume 289 of Leibniz International Proceedings in Informatics, pages 10:1–10:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.STACS.2024.10.
[2] Marta Bílková and Matěj Dostál. Many-valued relation lifting and Moss’ coalgebraic logic. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science (CALCO’13), pages 66–79. Springer, 2013. doi:10.1007/978-3-642-40206-7_7.
[3] Marta Bílková and Matěj Dostál. Expressivity of many-valued modal logics, coalgebraically. In Jouko Väänänen, Åsa Hirvonen, and Ruy de Queiroz, editors, Logic, Language, Information, and Computation (WoLLIC’16), pages 109–124. Springer, 2016. doi:10.1007/978-3-662-52921-8_8.
[4] Félix Bou, Francesc Esteva, Lluís Godo, and Ricardo O. Rodríguez. On the minimum many-valued modal logic over a finite residuated lattice. Journal of Logic and Computation, 21(5):739–790, 2011. doi:10.1093/logcom/exp062.
[5] Xavier Caicedo and Ricardo O. Rodríguez. Standard Gödel modal logics. Studia Logica, 94(2):189–214, 2010. doi:10.1007/s11225-010-9230-1.
[6] Roberto L. O. Cignoli, Itala M. L. D’Ottaviano, and Daniele Mundici. Algebraic Foundations of Many-Valued Reasoning, volume 7 of Trends in Logic. Springer, 2000.
[7] Petr Cintula and Carles Noguera. Neighborhood semantics for modal many-valued logics. Fuzzy Sets and Systems, 345:99–112, 2018. doi:10.1016/j.fss.2017.10.009.
[8] Fredrik Dahlqvist and Alexander Kurz. The positivication of coalgebraic logics. In Filippo Bonchi and Barbara König, editors, Algebra and Coalgebra in Computer Science (CALCO’17), volume 72 of Leibniz International Proceedings in Informatics, pages 9:1–9:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.CALCO.2017.9.
[9] Ernst-Erich Doberkat. Towards a probabilistic interpretation of game logic. In Wolfram Kahl, Michael Winter, and José Oliveira, editors, Relational and Algebraic Methods in Computer Science (RAMiCS’15), pages 43–47. Springer, 2015. doi:10.1007/978-3-319-24704-5_3.
[10] Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194–211, 1979. doi:10.1016/0022-0000(79)90046-1.
[11] Melvin C. Fitting. Many-valued modal logics. Fundamenta Informaticae, 15(3-4):235–254, 1991. doi:10.3233/FI-1991-153-404.
[12] Melvin C. Fitting. Many-valued modal logics II. Fundamenta Informaticae, 17(1-2):55–73, 1992. doi:10.3233/FI-1992-171-205.
[13] Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. Residuated Lattices: An algebraic glimpse at substructural logics, volume 151 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2007.
[14] Petr Hájek. Metamathematics of Fuzzy Logic, volume 4 of Trends in Logic. Springer, 1998. doi:10.1007/978-94-011-5300-3.
[15] Petr Hájek, Lluís Godo, and Francesc Esteva. A complete many-valued logic with product-conjunction. Archive for Mathematical Logic, 35(3):191–208, 1996. doi:10.1007/BF01268618.
[16] Helle H. Hansen and Clemens Kupke. Weak Completeness of Coalgebraic Dynamic Logics. In Ralph Matthes and Matteo Mio, editors, Tenth International Workshop on Fixed Points in Computer Science (FICS’15), volume 191 of EPTCS, pages 90–104, 2015. doi:10.4204/EPTCS.191.9.
[17] Helle H. Hansen, Clemens Kupke, and Raul A. Leal. Strong completeness for iteration-free coalgebraic dynamic logics. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, 8th International Conference on Theoretical Computer Science (TCS’14), pages 281–295. Springer, 2014. doi:10.1007/978-3-662-44602-7_22.
[18] Georges Hansoul and Bruno Teheux. Extending Łukasiewicz logics with a modality: Algebraic approach to relational semantics. Studia Logica, 101(3):505–545, 2013. doi:10.1007/s11225-012-9396-9.
[19] David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. MIT Press, 2000.
[20] Bartek Klin and Julian Salamanca. Iterated covariant powerset is not a monad. Electronic Notes in Theoretical Computer Science, 341:261–276, 2018. doi:10.1016/j.entcs.2018.11.013.
[21] Dexter Kozen. A probabilistic PDL. Journal of Computer and System Sciences, 30(2):162–178, 1985. doi:10.1016/0022-0000(85)90012-1.
[22] Clemens Kupke and Dirk Pattinson. Coalgebraic semantics of modal logics: An overview. Theoretical Computer Science, 412(38):5070–5094, 2011. doi:10.1016/j.tcs.2011.04.023.
[23] Alexander Kurz and Wolfgang Poiger. Many-Valued Coalgebraic Logic: From Boolean Algebras to Primal Varieties. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO’23), volume 270 of Leibniz International Proceedings in Informatics, pages 17:1–17:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.CALCO.2023.17.
[24] Alexander Kurz, Wolfgang Poiger, and Bruno Teheux. Many-valued coalgebraic logic over semi-primal varieties. Logical Methods in Computer Science, 20(3), 2024. doi:10.46298/lmcs-20(3:6)2024.
[25] Alexander Kurz, Wolfgang Poiger, and Bruno Teheux. New perspectives on semi-primal varieties. Journal of Pure and Applied Algebra, 228(4):article no. 107525, 2024. doi:10.1016/j.jpaa.2023.107525.
[26] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer, second edition, 1997. doi:10.1007/978-1-4757-4721-8.
[27] Chun-Yu Lin and Churn-Jung Liau. Many-valued coalgebraic modal logic: One-step completeness and finite model property. Fuzzy Sets and Systems, 467:article no. 108564, 2023. doi:10.1016/j.fss.2023.108564.
[28] Minghui Ma and Shanxia Wang. Finite-chain graded modal logic. In Shier Ju, Hu Liu, and Hiroakira Ono, editors, Modality, Semantics and Interpretations: The Second Asian Workshop on Philosophical Logic, pages 71–85. Springer, 2015. doi:10.1007/978-3-662-47197-5_4.
[29] Eric Pacuit. Neighborhood Semantics for Modal Logic. Short Textbooks in Logic. Springer, 2017. doi:10.1007/978-3-319-67149-9.
[30] Rohit Parikh. Propositional game logic. In 24th Annual Symposium on Foundations of Computer Science, pages 195–200. IEEE Computer Society, 1983. doi:10.1109/SFCS.1983.47.
[31] Dirk Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1):177–193, 2003. doi:10.1016/S0304-3975(03)00201-9.
[32] Dirk Pattinson. An introduction to the theory of coalgebras. Lecture notes for NASSLLI’03. Available online at https://ncatlab.org/nlab/files/Pattinson-Coalgebras.pdf (Accessed: Feb 26, 2025), 2003.
[33] Marc Pauly. From programs to games: Invariance and safety for bisimulation. In Peter G. Clote and Helmut Schwichtenberg, editors, Computer Science Logic, volume 1862 of Lecture Notes in Computer Science, pages 485–496. Springer, 2000. doi:10.1007/3-540-44622-2_33.
[34] Marc Pauly and Rohit Parikh. Game logic - An overview. Studia Logica, 75(2):165–182, 2003. doi:10.1023/A:1027354826364.
[35] André Platzer. Differential game logic. ACM Trans. Comput. Log., 17(1):1–51, 2015. doi:10.1145/2817824.
[36] Norbert Preining. Gödel logics – A survey. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’10), pages 30–51. Springer, 2010. doi:10.1007/978-3-642-16242-8_4.
[37] Ricardo O. Rodríguez and Amanda Vidal. Axiomatization of crisp Gödel modal logic. Studia Logica, 109(2):367–395, 2021. doi:10.1007/s11225-020-09910-5.
[38] J.J.M.M. Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.
[39] Lutz Schröder and Dirk Pattinson. Strong completeness of coalgebraic modal logics. In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science (STACS’09), volume 3 of Leibniz International Proceedings in Informatics, pages 673–684, 2009. doi:10.4230/LIPICS.STACS.2009.1855.
[40] Lutz Schröder and Dirk Pattinson. Coalgebraic correspondence theory. In Luke Ong, editor, Foundations of Software Science and Computational Structures (FoSSaCS’10), pages 328–342. Springer, 2010. doi:10.1007/978-3-642-12032-9_23.
[41] Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2):230–247, 2008. doi:10.1016/j.tcs.2007.09.023.
[42] Lutz Schröder and Dirk Pattinson. Description logics and fuzzy probability. In Toby Walsh, editor, 22nd International Joint Conference on Artificial Intelligence. International Joint Conference on Artificial Intelligence (IJCAI’11). AAAI Press, 2011.
[43] Igor Sedlàr. Propositional dynamic logic with Belnapian truth values. In Stéphane Demri Lev Beklemishev and András Máté’, editors, Advances in Modal Logic (AiML’16), volume 11, pages 503–519. College Publications, 2016. URL: http://www.aiml.net/volumes/volume11/Sedlar.pdf.
[44] Igor Sedlàr. Finitely-valued Propositional Dynamic Logic. In Nicola Olivetti, Rineke Verbrugge, Sara Negri, and Gabriel Sandu, editors, Advances in Modal Logic (AiML’20), volume 13, pages 561–579. College Publications, 2020. URL: http://www.aiml.net/volumes/volume13/Sedlar.pdf.
[45] Bruno Teheux. Propositional dynamic logic for searching games with errors. Journal of Applied Logic, 12(4):377–394, 2014. doi:10.1016/j.jal.2014.04.001.
[46] Samuel Teuber, Stefan Mitsch, and André Platzer. Provably safe neural network controllers via differential dynamic logic. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors, Advances in Neural Information Processing Systems 38 (NeurIPS’24), 2024.
[47] Johan van Benthem. Program constructions that are safe for bisimulation. Studia Logica, 60:311–330, 1998. doi:10.1023/A:1005072201319.
[48] Johan van Benthem, Nick Bezhanishvili, and Sebastian Enqvist. A propositional dynamic logic for instantial neighborhood semantics. Studia Logica, 107(4):719–751, 2019. doi:10.1007/s11225-018-9825-5.
[49] Johan van Benthem, Nick Bezhanishvili, Sebastian Enqvist, and Junhua Yu. Instantial neighbourhood logic. The Review of Symbolic Logic, 10(1):116–144, 2017. doi:10.1017/S1755020316000447.

Appendix A Appendix

Here, we provide additional proofs and details omitted in the main body of this paper.

Ad Example 5(2) & Example 10(2).

To see that $\mathcal{P}_{\mathbf{A}}$ is a functor, given $f\colon X\to Y$ and $g\colon Y\to Z$ , on $\sigma\in A^{X}$ and $z\in Z$ note

\mathcal{P}_{\mathbf{A}}(g\circ f)(\sigma)(z)=\bigvee_{g(f(x)){=}z}\sigma(x)=% \bigvee_{g(y)=z}\bigvee_{f(x)=y}\sigma(x)=\bigvee_{g(y)=z}\mathcal{P}_{\mathbf% {A}}f(\sigma)(y)=\mathcal{P}_{\mathbf{A}}g\mathcal{P}_{\mathbf{A}}f(\sigma)(z).

This functor is a monad with unit $\eta_{X}(x)=e_{x}\colon X\to A$ being the “unit vector” $e_{x}(x)=1$ , otherwise $e_{x}(x^{\prime})=0$ and $\mu$ defined on $\nu\in A^{A^{X}}$ by $\mu_{X}(\nu)(x)=\bigvee_{\sigma\in A^{X}}\nu(\sigma)\odot\sigma(x)$ . $\hfill\blacktriangleleft$

Ad Example 12(3).

Note that for $\mathbf{A}=\text{\bf\L }_{n}$ , demonic tests are given by $(\mathsf{test}(\neg\sigma)(x))^{\partial}$ taking $\rho\in A^{X}$ to

\big{(}\mathsf{test}(\neg\sigma)(x)\big{)}^{\partial}(\rho)=\neg\mathsf{test}(% \neg\sigma)(x)(\neg\rho)=\neg(\neg\sigma(x)\odot\neg\rho(x))=\sigma(x)\oplus% \rho(x)

using the operation $x\oplus y=\mathrm{min}\{x+y,1\}$ , equivalently defined by $x\oplus y=\neg(\neg x\odot\neg y)$ as usual (see, e.g., [6, page 9]). $\hfill\blacktriangleleft$

Ad Example 16(4).

With $S_{\alpha^{d}}\colon X\to\mathcal{M}X$ defined as usual by $V\in S_{\alpha^{d}}(x)\Leftrightarrow X{\setminus}V\notin S_{\alpha}(x)$ , we want to show that

N_{\alpha^{d}}(x)(\sigma)=\bigvee_{V\in S_{\alpha^{d}}(x)}\bigwedge_{v\in V}% \sigma(v)=:r

and

\neg N_{\alpha}(x)(\neg\sigma)=\neg\bigvee_{U\in S_{\alpha}(x)}\bigwedge_{u\in U% }\neg\sigma(u)=\bigwedge_{U\in S_{\alpha}(x)}\bigvee_{u\in U}\sigma(u)=:s

coincide (in the last equation we used that $\neg$ is an involution on a lattice, hence satisfies De Morgan’s laws). To see $r\leq s$ , note that whenever $V\in S_{\alpha^{d}}(x)$ and $U\in S_{\alpha}(x)$ , then there is some $y\in U\cap V$ , thus we get $\bigwedge_{v\in V}\sigma(v)\leq\sigma(y)\leq\bigvee_{u\in U}\sigma(U)$ and since $U$ and $V$ were arbitrary this implies $r\leq s$ .

Conversely, to see $s\leq r$ , note that it suffices to show that $U^{\prime}:=\{u\in X\mid\sigma(u)\leq r\}\in S_{\alpha}(x)$ , since this implies $s\leq\bigvee_{u\in U^{\prime}}\sigma(u)\leq r$ . By definition we have $U^{\prime}\in S_{\alpha}(x)\Leftrightarrow X{\setminus}U^{\prime}\notin S_{% \alpha^{d}}(x)$ , and note that $X{\setminus}U^{\prime}=\{v\in X\mid\sigma(v)>r\}\in S_{\alpha^{d}}(x)$ would lead to

r=\bigvee_{V\in S_{\alpha^{d}}(x)}\bigwedge_{v\in V}\sigma(v)\geq\bigwedge_{v% \in X{\setminus}U^{\prime}}\sigma(v)>r,

a contradiction. $\hfill\blacktriangleleft$

Proof of Lemma 18.

If $\theta$ is natural, the following commutes, given that the left square commutes.

Conversely, if $\theta$ does not define a natural transformation, there are $f\colon X\to Y$ and $(t_{1},\dots,t_{n})\in\mathsf{F}^{n}X$ such that $\mathsf{F}f(\theta_{X}(t_{1},\dots,t_{n}))\neq\theta_{Y}(\mathsf{F}f(t_{1}),% \dots,\mathsf{F}f(t_{n}))$ . Define the constant coalgebras $\gamma_{i}(x)=t_{i}$ and $\gamma_{i}^{\prime}(x)=\mathsf{F}f(t_{i})$ , then $f$ witnesses that $O^{\theta}$ is not safe. $\hfill\blacktriangleleft$

Proof of Proposition 21.

By simultaneous induction on the structure of the action $a\in\mathsf{Act}$ and the formula $\varphi\in\mathsf{Form}$ , we show that $f$ is a coalgebra morphism $\gamma_{a}\to\gamma^{\prime}_{a}$ and that $[\![{\varphi}]\!]^{\prime}\circ f=[\![{\varphi}]\!]$ .

If $a=O(a_{1},\dots,a_{n})$ is obtained using some $n$ -ary coalgebra operation, then safety of $O$ together with the inductive hypothesis that $f$ is a coalgebra morphism $\gamma_{a_{i}}\to\gamma^{\prime}_{a_{i}}$ for all $i=1,\dots,n$ immediately yields that it also is a coalgebra morphism $\gamma_{O(a_{1},\dots,a_{n})}\to\gamma^{\prime}_{O(a_{1},\dots,a_{n})}$ . If $a=\mathsf{test}(\psi)$ is obtained via some test, then the inductive hypothesis $[\![{\psi}]\!]^{\prime}\circ f=[\![{\psi}]\!]$ together with safety of $\mathsf{test}$ (recall Lemma 20) yields the desired

\mathsf{F}f\circ\gamma_{a}=\mathsf{F}f\circ\mathsf{test}([\![{\psi}]\!])=% \mathsf{F}f\circ\mathsf{test}([\![{\psi}]\!]^{\prime}\circ f)=\mathsf{test}([% \![{\psi}]\!]^{\prime})\circ f=\gamma^{\prime}_{a}\circ f.

If $\varphi=o(\varphi_{1},\dots,\varphi_{m})$ is obtained using some $m$ -ary algebraic operation $o\in\mathsf{sign}(\mathbf{A})$ , using the inductive hypothesis $[\![{\varphi_{j}}]\!]^{\prime}\circ f=[\![{\varphi_{j}}]\!]$ for all $j=1,\dots,m$ we simply compute

o^{\mathrm{pw}}\big{(}[\![{\varphi_{1}}]\!],\dots,[\![{\varphi_{m}}]\!]\big{)}% =o^{\mathrm{pw}}\big{(}[\![{\varphi_{1}}]\!]^{\prime}\circ f,\dots,[\![{% \varphi_{m}}]\!]^{\prime}\circ f\big{)}=o^{\mathrm{pw}}\big{(}[\![{\varphi_{1}% }]\!]^{\prime},\dots,[\![{\varphi_{m}}]\!]^{\prime}\big{)}\circ f

as desired. If $\varphi=\langle{a}\rangle^{\lambda}(\varphi_{1},\dots,\varphi_{k})$ for the $k$ -ary $\lambda\in\Lambda$ , we use the inductive hypothesis $f\colon\gamma_{a}\to\gamma^{\prime}_{a}$ and $[\![{\varphi_{j}}]\!]^{\prime}\circ f=[\![{\varphi}]\!]$ together with naturality of $\lambda$ to find

\lambda_{X}\big{(}[\![{\varphi_{1}}]\!]^{\prime}\circ f,\dots,[\![{\varphi_{k}% }]\!]^{\prime}\circ f\big{)}\circ\gamma_{a}=\lambda_{Y}\big{(}[\![{\varphi_{1}% }]\!]^{\prime},\dots,[\![{\varphi_{k}}]\!]\big{)}\circ\mathsf{F}f\circ\gamma_{% a}=\lambda_{Y}\big{(}[\![{\varphi_{1}}]\!]^{\prime},\dots,[\![{\varphi_{k}}]\!% ]\big{)}\circ\gamma^{\prime}_{a}\circ f

as desired, finishing the proof. $\hfill\blacktriangleleft$

Proof of Proposition 25.

This follows immediately from Definition 24 after showing that in every standard model $\gamma$ , for all $(n,k)$ -templates $\tau$ it holds that $[\![{\tau[\vec{a},\vec{\varphi}]}]\!]=\tau[\vec{\gamma}_{a},[\![{\vec{\varphi}% }]\!]]$ , where $\vec{\gamma}_{a}=(\gamma_{a_{1}},\dots,\gamma_{a_{n}})$ and $[\![{\vec{\varphi}}]\!]=([\![{\varphi_{1}}]\!],\dots,[\![{\varphi_{k}}]\!])$ . This is easily shown using induction on the structure of $\tau$ . $\hfill\blacktriangleleft$

Proof of Proposition 26.

Say $\mathsf{ar}(O)=:n$ and let $\vec{\gamma}\colon X\to\mathsf{F}^{n}X$ and $\vec{\gamma}^{\prime}\colon Y\to\mathsf{F}^{n}Y$ be coalgebras. We show that if $f\colon\vec{\gamma}\to\vec{\gamma}^{\prime}$ then $f\colon O(\vec{\gamma})\to O(\vec{\gamma}^{\prime})$ . By separation, it suffices to show that for every $\lambda\in\Lambda$ it holds that $\widehat{\lambda}_{Y}\circ\mathsf{F}f\circ O(\vec{\gamma})=\widehat{\lambda}_{% Y}\circ O(\vec{\gamma}^{\prime})\circ f$ .

Say $\mathsf{ar}(\lambda)=:k$ and choose some $\tau\in\mathsf{Templ}_{n,k}$ witnessing that $O$ is reducible with respect to $\lambda$ . Starting on the left-hand side, by naturality of $\widehat{\lambda}$ we have $\widehat{\lambda}_{Y}\circ\mathsf{F}f\circ O(\vec{\gamma})=k\mathcal{N}_{% \mathbf{A}}f\circ\widehat{\lambda}_{X}\circ O(\vec{\gamma}).$ Now, for any $x\in X$ and $\sigma_{1},\dots,\sigma_{k}\in A^{Y}$ , using reducibility we get

	$\displaystyle k\mathcal{N}_{\mathbf{A}}f\circ\widehat{\lambda}_{X}\circ O(\vec% {\gamma})(x)(\vec{\sigma})$	$\displaystyle=\widehat{\lambda}_{X}\circ O(\vec{\gamma})(x)(\vec{\sigma}\circ f% ^{k})$
		$\displaystyle=\lambda_{X}(\vec{\sigma}\circ f^{k})\circ O(\vec{\gamma})(x)=% \tau[\vec{\gamma},\vec{\sigma}\circ f^{k}](x).$

On the other hand, we use reducibility as well and get

\widehat{\lambda}_{Y}\circ O(\vec{\gamma}^{\prime})\circ f(x)(\vec{\sigma})=% \lambda_{Y}(\vec{\sigma})\circ O(\vec{\gamma}^{\prime})\big{(}f(x)\big{)}=\tau% [\vec{\gamma}^{\prime},\vec{\sigma}]\big{(}f(x)\big{)}.

Thus, we are done once we show $\tau[\vec{\gamma},\vec{\sigma}\circ f^{k}]=\tau[\vec{\gamma}^{\prime},\vec{% \sigma}]\circ f$ for all $\tau\in\mathsf{Templ}_{n,k}$ , which we do by induction on the structure of $\tau$ . The cases $\tau=\omega_{i}$ and $\tau=o(\tau_{1},\dots,\tau_{\mathsf{ar}(o)})$ are completely straightforward, for the case $\tau=\langle{j}\rangle^{\lambda^{\prime}}(\tau_{1},\dots,\tau_{\mathsf{ar}(% \lambda^{\prime})})$ compute

$\displaystyle\tau[\vec{\gamma},\vec{\sigma}\circ f^{k}]$	$\displaystyle=\lambda^{\prime}_{X}\big{(}\tau_{1}[\vec{\gamma},\vec{\sigma}% \circ f^{k}],\dots,\tau_{\mathsf{ar}(\lambda^{\prime})}[\vec{\gamma},\vec{% \sigma}\circ f^{k}]\big{)}\circ\gamma_{j}$	(Definition)
	$\displaystyle=\lambda^{\prime}_{X}\big{(}\tau_{1}[\vec{\gamma}^{\prime},\vec{% \sigma}]\circ f,\dots,\tau_{\mathsf{ar}(\lambda^{\prime})}[\vec{\gamma}^{% \prime},\vec{\sigma}]\circ f\big{)}\circ\gamma_{j}$	(Ind.Hyp. on $\tau_{i}$ ’s)
	$\displaystyle=\lambda^{\prime}_{Y}\big{(}\tau_{1}[\vec{\gamma}^{\prime},\vec{% \sigma}],\dots,\tau_{\mathsf{ar}(\lambda^{\prime})}[\vec{\gamma}^{\prime},\vec% {\sigma}]\big{)}\circ\mathsf{F}f\circ\gamma_{j}$	(Naturality $\lambda$ )
	$\displaystyle=\lambda^{\prime}_{Y}\big{(}\tau_{1}[\vec{\gamma}^{\prime},\vec{% \sigma}],\dots,\tau_{\mathsf{ar}(\lambda^{\prime})}[\vec{\gamma}^{\prime},\vec% {\sigma}]\big{)}\circ\gamma^{\prime}_{j}\circ f=\tau[\vec{\gamma}^{\prime},% \vec{\sigma}]\circ f$	( $f\colon\gamma_{j}\to\gamma_{j}^{\prime}$ )

as desired, finishing the proof. $\hfill\blacktriangleleft$

Proof of Example 28.

Since $\mathbf{A}$ is assumed to be finite, the right-hand side yields a well-defined formula. Linearity yields that $\bigvee_{i\in I}s_{i}\geq s\Leftrightarrow\exists i\in I\colon s_{i}\geq s$ always holds. Let $S\in 2^{X}$ and $\gamma_{1},\gamma_{2}\colon X\to A^{X}$ be $\mathcal{P}_{\mathbf{A}}$ -coalgebras. Then we have the chain of equivalences

	$\displaystyle\lambda_{X}^{r}(S)\circ(\gamma_{1}{;}\gamma_{2})(x)=1$	$\displaystyle\Longleftrightarrow\bigvee_{z\in S}\gamma_{1}{;}\gamma_{2}(x)(z)\geq r$
		$\displaystyle\Longleftrightarrow\bigvee_{z\in S}\bigvee_{y\in X}\gamma_{1}(x)(% y)\odot\gamma_{2}(y)(z)\geq r$
		$\displaystyle\Longleftrightarrow\exists z\in S,y\in X\colon\gamma_{1}(x)(y)% \odot\gamma_{2}(y)(z)\geq r$
		$\displaystyle\Longleftrightarrow\exists z\in S,y\in X,r_{1}\odot r_{2}\geq r:% \gamma_{1}(x)(y)\geq r_{1},\gamma_{2}(y)(z)\geq r_{2}$
		$\displaystyle\Longleftrightarrow\exists y\in X,r_{1}\odot r_{2}\geq r\colon% \gamma_{1}(x)(y)\geq r_{1},\bigvee_{z\in Z}\gamma_{2}(y)(z)\geq r_{2}$
		$\displaystyle\Longleftrightarrow\exists r_{1}\odot r_{2}\geq r:\bigvee_{% \lambda_{X}^{r_{2}}(S)(\gamma_{2}(y))=1}\gamma_{1}(x)(y)\geq r_{1}$
		$\displaystyle\Longleftrightarrow\exists r_{1}\odot r_{2}\geq r:\lambda_{X}^{r_% {1}}(\lambda_{X}^{r_{2}}(Z)\circ\gamma_{2})(\gamma_{1}(x))=1$
		$\displaystyle\Longleftrightarrow\bigvee_{r_{1}\odot r_{2}\geq r}\lambda_{X}^{r% _{1}}(\lambda_{X}^{r_{2}}(S)\circ\gamma_{2})\circ\gamma_{1}(x)=1.$

This shows that the template $\tau=\bigvee_{r_{1}\odot r_{2}\geq r}\langle{1}\rangle^{r_{1}}\langle{2}% \rangle^{r_{2}}\omega$ witnesses that ; is reducible with respect to $\lambda^{r}$ . $\hfill\blacktriangleleft$

Proof of Example 29.

Untangling the definitions, for $S_{1},\dots,S_{k},S\in 2^{X}$ and $\gamma_{1},\gamma_{2}\colon X\to(\mathcal{P}\circ\mathcal{P})(X)$ we get

	$\displaystyle\lambda^{k+1}_{X}(S_{1},\dots,S_{k},S)((\gamma_{1}{;}\gamma_{2})(% x))=1$
	$\displaystyle\Longleftrightarrow\exists Z\in(\gamma_{1}{;}\gamma_{2})(x)\colon Z% \subseteq S\wedge\forall i\colon Z\cap S_{i}\neq\varnothing$
	$\displaystyle\Longleftrightarrow\exists Z^{\prime}\in\gamma_{1}(x),F\subseteq% \bigcup_{x^{\prime}\in Z^{\prime}}\gamma_{2}(x^{\prime})\colon\bigcup F% \subseteq S\wedge\forall i\colon\bigcup F\cap S_{i}\neq\varnothing$

on the one hand and

	$\displaystyle\lambda_{X}^{k+1}(\lambda_{2}(S_{1},S)\circ\gamma_{2},\dots,% \lambda_{2}(S_{k},S)\circ\gamma_{2},\lambda^{1}(S)\circ\gamma_{2})(\gamma_{1}(% x))=1$
	$\displaystyle\Longleftrightarrow\exists Z^{\prime}\in\gamma_{1}(x)\colon Z^{% \prime}\subseteq\lambda^{1}(S)\circ\gamma_{2}\wedge\forall i\colon Z^{\prime}% \cap\lambda_{2}(S_{i},S)\circ\gamma_{2}\neq\varnothing$
	$\displaystyle\Longleftrightarrow\exists Z^{\prime}\in\gamma_{1}(x)\colon% \forall x^{\prime}\in Z^{\prime}\colon\exists U\in\gamma_{2}(x^{\prime})\colon U% \subseteq S\wedge$
	$\displaystyle\phantom{\Longleftrightarrow\exists Z^{\prime}\in\gamma_{1}(x)% \colon i}\forall i\colon\exists x_{i}^{\prime}\in Z^{\prime},U_{i}\in\gamma_{2% }(x_{i}^{\prime})\colon U_{i}\cap S_{i}\neq\varnothing$

on the other hand. Using the same $Z^{\prime}$ , the former immediately implies the latter and the converse is obtained setting $F=\{U\mid U\subseteq S\wedge\exists y\in Z^{\prime}\colon U\in\gamma_{2}(y)\}$ as in [48, Proposition 3].

Thus it is shown that ; is reducible with respect to $\lambda^{k+1}$ via the $(2,k+1)$ -template $\langle{1}\rangle^{k+1}\big{(}\langle{2}\rangle^{2}(\omega_{1},\omega_{k+1}),% \dots,\langle{2}\rangle^{2}(\omega_{k},\omega_{k+1}),\langle{2}\rangle^{1}% \omega_{k+1}\big{)}$ . $\hfill\blacktriangleleft$

Proof of Proposition 31.

If $\tau$ is some $(n,k)$ -reduction template in which $\langle{j}\rangle^{\lambda}$ are the only modal connectives, let $\tau^{\mathsf{ev}}$ denote the corresponding template replacing them by $\langle{j}\rangle^{\lambda^{\mathsf{ev}}}$ . Note that $\tau^{\mathsf{ev}}$ defines itself a $n$ -ary coalgebra operation $\Omega^{\tau}\colon\mathsf{Coalg}({k\mathcal{N}_{\mathbf{A}}^{n}})\to\mathsf{% Coalg}({k\mathcal{N}_{\mathbf{A}}})$ via $\Omega^{\tau}(\vec{\xi})(x)(\vec{\sigma})=\tau^{\mathsf{ev}}[\vec{\xi},\vec{% \sigma}](x)$ .

With this, the statement easily follows once we show that for all $\vec{\gamma}\colon X\to\mathsf{F}^{n}X$ and $\vec{\sigma}\in(A^{X})^{k}$ it holds that $\tau[\vec{\gamma},\vec{\sigma}]=\tau^{\mathsf{ev}}[\widehat{\lambda}^{n}_{X}% \circ\vec{\gamma},\vec{\sigma}]$ , which we do by induction on the structure of $\tau$ . The cases $\tau=\omega_{i}$ and $\tau=o(\tau_{1},\dots,\tau_{\mathsf{ar}(o)})$ are straightforward by definitions, thus let $\tau=\langle{j}\rangle^{\lambda}(\tau_{1},\dots,\tau_{k})$ and suppose the statement already holds for $\tau_{1},\dots,\tau_{k}$ . We compute

	$\displaystyle\tau[\vec{\gamma},\vec{\sigma}](x)$	$\displaystyle=\lambda_{X}\big{(}\tau_{1}[\vec{\gamma},\vec{\sigma}],\dots,\tau% _{k}[\vec{\gamma},\vec{\sigma}]\big{)}\circ\gamma_{j}(x)$
		$\displaystyle=\lambda_{X}\big{(}\tau^{\mathsf{ev}}_{1}[\widehat{\lambda}_{X}^{% n}\circ\vec{\gamma},\vec{\sigma}],\dots,\tau^{\mathsf{ev}}_{k}[\widehat{% \lambda}_{X}^{n}\circ\vec{\gamma},\vec{\sigma}]\big{)}\circ\gamma_{j}(x)$
		$\displaystyle=\widehat{\lambda}_{X}\circ\gamma_{j}(x)\big{(}\tau^{\mathsf{ev}}% _{1}[\widehat{\lambda}_{X}^{n}\circ\vec{\gamma},\vec{\sigma}],\dots,\tau^{% \mathsf{ev}}_{k}[\widehat{\lambda}_{X}^{n}\circ\vec{\gamma},\vec{\sigma}]\big{)}$
		$\displaystyle=\lambda^{\mathsf{ev}}_{X}\big{(}\tau^{\mathsf{ev}}_{1}[\widehat{% \lambda}_{X}^{n}\circ\vec{\gamma},\vec{\sigma}],\dots,\tau^{\mathsf{ev}}_{k}[% \widehat{\lambda}_{X}^{n}\circ\vec{\gamma},\vec{\sigma}]\big{)}\circ\widehat{% \lambda}_{X}\circ\gamma_{j}(x)=\tau^{\mathsf{ev}}[\widehat{\lambda}^{n}_{X}% \circ\vec{\gamma},\vec{\sigma}](x)$

as desired, finishing the proof. $\hfill\blacktriangleleft$

Proof of Proposition 35.

To use Lemma 20, let $f\colon X\to Y$ and $\sigma\in A^{Y}$ . By separation, it suffices to show that for every $\lambda\in\Lambda$ it holds that $\widehat{\lambda}_{Y}\circ\mathsf{F}f\circ\mathsf{test}(\sigma\circ f)=% \widehat{\lambda}_{Y}\circ\mathsf{test}(\sigma)\circ f$ .

Say $\mathsf{ar}(\lambda)=:k$ and let $t$ be the $(k+1)$ -ary term-function witnessing reducibility with respect to $\lambda$ . Starting on the left-hand side, note $\widehat{\lambda}_{Y}\circ\mathsf{F}f\circ\mathsf{test}(\sigma\circ f)=k% \mathcal{N}_{\mathbf{A}}f\circ\widehat{\lambda}_{X}\circ\mathsf{test}(\sigma% \circ f)$ by naturality. From here, for any $x\in X$ and $\sigma_{1},\dots,\sigma_{k}\in A^{Y}$ we compute

	$\displaystyle(k\mathcal{N}_{\mathbf{A}}f\circ\widehat{\lambda}_{X}\circ\mathsf% {test}(\sigma\circ f))(x)(\sigma_{1},\dots,\sigma_{k})$	$\displaystyle=(\lambda_{X}(\sigma_{1}\circ f,\dots,\sigma_{k}\circ f)\circ% \mathsf{test}(\sigma\circ f))(x)$
		$\displaystyle=t^{\mathrm{pw}}(\sigma\circ f,\sigma_{1}\circ f,\dots,\sigma_{k}% \circ f)(x).$

On the other hand we use reducibility as well and get

	$\displaystyle(\widehat{\lambda}_{Y}\circ\mathsf{test}(\sigma)\circ f)(x)(% \sigma_{1},\dots,\sigma_{k})$	$\displaystyle=(\lambda_{Y}(\sigma_{1},\dots,\sigma_{k})\circ\mathsf{test}(% \sigma))\big{(}f(x)\big{)}$
		$\displaystyle=t^{\mathrm{pw}}(\sigma,\sigma_{1},\dots,\sigma_{k})\big{(}f(x)% \big{)}.$

Since both of these equal $t\big{(}\sigma(f(x)),\sigma_{1}(f(x)),\dots,\sigma_{k}(f(x))\big{)}$ , this finishes the proof. $\hfill\blacktriangleleft$

Ad Examples 44 & 45.

To see that $\mathcal{P}_{\mathbf{A}}$ is weakly preserving, let $(\sigma_{m})\in\varprojlim\mathcal{P}_{\mathbf{A}}X_{m}$ be coherent, i.e., $\sigma_{m}(x^{m})=\bigvee\{\sigma_{m+1}(x^{m+1})\mid p_{m}(x^{m+1}=x^{m})\}$ . This sequence is induced by $\sigma\in\mathcal{P}_{\mathbf{A}}(\varprojlim X_{m})$ defined by $\sigma((x_{m}))=\bigwedge_{m\in\mathbf{N}}\sigma_{m}(x_{m})$ .

In Example 44 with $\lambda^{\Diamond}$ and truth-constants in $\mathbf{A}$ , to see strong one-step completeness over finite sets, take a rank-1 non-modal homomorphism $H\colon\Lambda(A^{X})\to A$ with $X$ finite and define $\alpha\in A^{X}$ by $\alpha(x)=H(\Diamond e_{x})$ . This $\alpha$ one-step satisfies $H$ since

	$\displaystyle\lambda^{\Diamond}(\sigma)(\alpha)$	$\displaystyle=\bigvee_{x\in X}\sigma(x)\odot\alpha(x)=\bigvee_{x\in X}\check{% \sigma}_{x}\odot H(\Diamond e_{x})$
		$\displaystyle=\bigvee_{x\in X}H\big{(}\Diamond(\check{\sigma}_{x}\odot e_{x})% \big{)}=H\big{(}\Diamond\bigvee_{x\in X}(\check{\sigma}_{x}\odot e_{x})\big{)},$

where $\check{\sigma}_{x}$ is the truth-constant of $\sigma(x)$ . Note that $\bigvee_{x\in X}(\check{\sigma}_{x}\odot e_{x})=\sigma$ as desired.

In Example 45, for strong one-step completeness over finite sets one checks that a rank-1 non-modal homomorphism $H\colon\Lambda(2^{X})\to 2$ is one-step satisfied by $\alpha\in A^{X}$ defined by $\alpha(x)=\bigvee\{r\mid H(\heartsuit^{r}\{x\})=1)\}$ . $\hfill\blacktriangleleft$

Ad Example 46.

To see that $\mathcal{M}_{\mathbf{A}}$ is weakly preserving, let $(N_{m})\in\varprojlim\mathcal{M}_{\mathbf{A}}X_{m}$ be coherent, i.e., $N_{m}(\sigma_{m})=N_{m+1}(\sigma_{m}\circ p_{m+1})$ . Then this sequence is induced by $N\in\mathcal{M}_{\mathbf{A}}(\varprojlim X_{m})$ defined by $N(\sigma)=\bigvee_{m\in\mathbb{N}}\bigvee\{N_{m}(\rho^{m})\mid\rho^{m}\circ\pi% _{m}=\sigma\}$ where $\pi_{m}\colon\varprojlim X_{n}\to X_{m}$ .

Strong one-step completeness over finite sets holds since every rank-1 non-modal homomorphism $H$ is one-step satisfied by $N(\sigma):=H(\heartsuit^{\mathsf{ev}}\sigma)$ . $\hfill\blacktriangleleft$

[bib.bib1] [1] Harsh Beohar, Sebastian Gurke, Barbara König, Karla Messing, Jonas Forster, Lutz Schröder, and Paul Wild. Expressive Quantale-Valued Logics for Coalgebras: An Adjunction-Based Approach. In Olaf Beyersdorff, Mamadou M. Kanté, Orna Kupferman, and Daniel Lokshtanov, editors, 41st International Symposium on Theoretical Aspects of Computer Science (STACS’24), volume 289 of Leibniz International Proceedings in Informatics, pages 10:1–10:19. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2024. doi:10.4230/LIPIcs.STACS.2024.10.

[bib.bib2] [2] Marta Bílková and Matěj Dostál. Many-valued relation lifting and Moss’ coalgebraic logic. In Reiko Heckel and Stefan Milius, editors, Algebra and Coalgebra in Computer Science (CALCO’13), pages 66–79. Springer, 2013. doi:10.1007/978-3-642-40206-7_7.

[bib.bib3] [3] Marta Bílková and Matěj Dostál. Expressivity of many-valued modal logics, coalgebraically. In Jouko Väänänen, Åsa Hirvonen, and Ruy de Queiroz, editors, Logic, Language, Information, and Computation (WoLLIC’16), pages 109–124. Springer, 2016. doi:10.1007/978-3-662-52921-8_8.

[bib.bib4] [4] Félix Bou, Francesc Esteva, Lluís Godo, and Ricardo O. Rodríguez. On the minimum many-valued modal logic over a finite residuated lattice. Journal of Logic and Computation, 21(5):739–790, 2011. doi:10.1093/logcom/exp062.

[bib.bib5] [5] Xavier Caicedo and Ricardo O. Rodríguez. Standard Gödel modal logics. Studia Logica, 94(2):189–214, 2010. doi:10.1007/s11225-010-9230-1.

[bib.bib6] [6] Roberto L. O. Cignoli, Itala M. L. D’Ottaviano, and Daniele Mundici. Algebraic Foundations of Many-Valued Reasoning, volume 7 of Trends in Logic. Springer, 2000.

[bib.bib7] [7] Petr Cintula and Carles Noguera. Neighborhood semantics for modal many-valued logics. Fuzzy Sets and Systems, 345:99–112, 2018. doi:10.1016/j.fss.2017.10.009.

[bib.bib8] [8] Fredrik Dahlqvist and Alexander Kurz. The positivication of coalgebraic logics. In Filippo Bonchi and Barbara König, editors, Algebra and Coalgebra in Computer Science (CALCO’17), volume 72 of Leibniz International Proceedings in Informatics, pages 9:1–9:15. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2017. doi:10.4230/LIPIcs.CALCO.2017.9.

[bib.bib9] [9] Ernst-Erich Doberkat. Towards a probabilistic interpretation of game logic. In Wolfram Kahl, Michael Winter, and José Oliveira, editors, Relational and Algebraic Methods in Computer Science (RAMiCS’15), pages 43–47. Springer, 2015. doi:10.1007/978-3-319-24704-5_3.

[bib.bib10] [10] Michael J. Fischer and Richard E. Ladner. Propositional dynamic logic of regular programs. Journal of Computer and System Sciences, 18(2):194–211, 1979. doi:10.1016/0022-0000(79)90046-1.

[bib.bib11] [11] Melvin C. Fitting. Many-valued modal logics. Fundamenta Informaticae, 15(3-4):235–254, 1991. doi:10.3233/FI-1991-153-404.

[bib.bib12] [12] Melvin C. Fitting. Many-valued modal logics II. Fundamenta Informaticae, 17(1-2):55–73, 1992. doi:10.3233/FI-1992-171-205.

[bib.bib13] [13] Nikolaos Galatos, Peter Jipsen, Tomasz Kowalski, and Hiroakira Ono. Residuated Lattices: An algebraic glimpse at substructural logics, volume 151 of Studies in Logic and the Foundations of Mathematics. Elsevier, 2007.

[bib.bib14] [14] Petr Hájek. Metamathematics of Fuzzy Logic, volume 4 of Trends in Logic. Springer, 1998. doi:10.1007/978-94-011-5300-3.

[bib.bib15] [15] Petr Hájek, Lluís Godo, and Francesc Esteva. A complete many-valued logic with product-conjunction. Archive for Mathematical Logic, 35(3):191–208, 1996. doi:10.1007/BF01268618.

[bib.bib16] [16] Helle H. Hansen and Clemens Kupke. Weak Completeness of Coalgebraic Dynamic Logics. In Ralph Matthes and Matteo Mio, editors, Tenth International Workshop on Fixed Points in Computer Science (FICS’15), volume 191 of EPTCS, pages 90–104, 2015. doi:10.4204/EPTCS.191.9.

[bib.bib17] [17] Helle H. Hansen, Clemens Kupke, and Raul A. Leal. Strong completeness for iteration-free coalgebraic dynamic logics. In Josep Díaz, Ivan Lanese, and Davide Sangiorgi, editors, 8th International Conference on Theoretical Computer Science (TCS’14), pages 281–295. Springer, 2014. doi:10.1007/978-3-662-44602-7_22.

[bib.bib18] [18] Georges Hansoul and Bruno Teheux. Extending Łukasiewicz logics with a modality: Algebraic approach to relational semantics. Studia Logica, 101(3):505–545, 2013. doi:10.1007/s11225-012-9396-9.

[bib.bib19] [19] David Harel, Dexter Kozen, and Jerzy Tiuryn. Dynamic Logic. MIT Press, 2000.

[bib.bib20] [20] Bartek Klin and Julian Salamanca. Iterated covariant powerset is not a monad. Electronic Notes in Theoretical Computer Science, 341:261–276, 2018. doi:10.1016/j.entcs.2018.11.013.

[bib.bib21] [21] Dexter Kozen. A probabilistic PDL. Journal of Computer and System Sciences, 30(2):162–178, 1985. doi:10.1016/0022-0000(85)90012-1.

[bib.bib22] [22] Clemens Kupke and Dirk Pattinson. Coalgebraic semantics of modal logics: An overview. Theoretical Computer Science, 412(38):5070–5094, 2011. doi:10.1016/j.tcs.2011.04.023.

[bib.bib23] [23] Alexander Kurz and Wolfgang Poiger. Many-Valued Coalgebraic Logic: From Boolean Algebras to Primal Varieties. In Paolo Baldan and Valeria de Paiva, editors, 10th Conference on Algebra and Coalgebra in Computer Science (CALCO’23), volume 270 of Leibniz International Proceedings in Informatics, pages 17:1–17:17. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2023. doi:10.4230/LIPIcs.CALCO.2023.17.

[bib.bib24] [24] Alexander Kurz, Wolfgang Poiger, and Bruno Teheux. Many-valued coalgebraic logic over semi-primal varieties. Logical Methods in Computer Science, 20(3), 2024. doi:10.46298/lmcs-20(3:6)2024.

[bib.bib25] [25] Alexander Kurz, Wolfgang Poiger, and Bruno Teheux. New perspectives on semi-primal varieties. Journal of Pure and Applied Algebra, 228(4):article no. 107525, 2024. doi:10.1016/j.jpaa.2023.107525.

[bib.bib26] [26] Saunders Mac Lane. Categories for the Working Mathematician, volume 5 of Graduate Texts in Mathematics. Springer, second edition, 1997. doi:10.1007/978-1-4757-4721-8.

[bib.bib27] [27] Chun-Yu Lin and Churn-Jung Liau. Many-valued coalgebraic modal logic: One-step completeness and finite model property. Fuzzy Sets and Systems, 467:article no. 108564, 2023. doi:10.1016/j.fss.2023.108564.

[bib.bib28] [28] Minghui Ma and Shanxia Wang. Finite-chain graded modal logic. In Shier Ju, Hu Liu, and Hiroakira Ono, editors, Modality, Semantics and Interpretations: The Second Asian Workshop on Philosophical Logic, pages 71–85. Springer, 2015. doi:10.1007/978-3-662-47197-5_4.

[bib.bib29] [29] Eric Pacuit. Neighborhood Semantics for Modal Logic. Short Textbooks in Logic. Springer, 2017. doi:10.1007/978-3-319-67149-9.

[bib.bib30] [30] Rohit Parikh. Propositional game logic. In 24th Annual Symposium on Foundations of Computer Science, pages 195–200. IEEE Computer Society, 1983. doi:10.1109/SFCS.1983.47.

[bib.bib31] [31] Dirk Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theoretical Computer Science, 309(1):177–193, 2003. doi:10.1016/S0304-3975(03)00201-9.

[bib.bib32] [32] Dirk Pattinson. An introduction to the theory of coalgebras. Lecture notes for NASSLLI’03. Available online at https://ncatlab.org/nlab/files/Pattinson-Coalgebras.pdf (Accessed: Feb 26, 2025), 2003.

[bib.bib33] [33] Marc Pauly. From programs to games: Invariance and safety for bisimulation. In Peter G. Clote and Helmut Schwichtenberg, editors, Computer Science Logic, volume 1862 of Lecture Notes in Computer Science, pages 485–496. Springer, 2000. doi:10.1007/3-540-44622-2_33.

[bib.bib34] [34] Marc Pauly and Rohit Parikh. Game logic - An overview. Studia Logica, 75(2):165–182, 2003. doi:10.1023/A:1027354826364.

[bib.bib35] [35] André Platzer. Differential game logic. ACM Trans. Comput. Log., 17(1):1–51, 2015. doi:10.1145/2817824.

[bib.bib36] [36] Norbert Preining. Gödel logics – A survey. In Christian G. Fermüller and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR’10), pages 30–51. Springer, 2010. doi:10.1007/978-3-642-16242-8_4.

[bib.bib37] [37] Ricardo O. Rodríguez and Amanda Vidal. Axiomatization of crisp Gödel modal logic. Studia Logica, 109(2):367–395, 2021. doi:10.1007/s11225-020-09910-5.

[bib.bib38] [38] J.J.M.M. Rutten. Universal coalgebra: A theory of systems. Theoretical Computer Science, 249(1):3–80, 2000. doi:10.1016/S0304-3975(00)00056-6.

[bib.bib39] [39] Lutz Schröder and Dirk Pattinson. Strong completeness of coalgebraic modal logics. In Susanne Albers and Jean-Yves Marion, editors, 26th International Symposium on Theoretical Aspects of Computer Science (STACS’09), volume 3 of Leibniz International Proceedings in Informatics, pages 673–684, 2009. doi:10.4230/LIPICS.STACS.2009.1855.

[bib.bib40] [40] Lutz Schröder and Dirk Pattinson. Coalgebraic correspondence theory. In Luke Ong, editor, Foundations of Software Science and Computational Structures (FoSSaCS’10), pages 328–342. Springer, 2010. doi:10.1007/978-3-642-12032-9_23.

[bib.bib41] [41] Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theoretical Computer Science, 390(2):230–247, 2008. doi:10.1016/j.tcs.2007.09.023.

[bib.bib42] [42] Lutz Schröder and Dirk Pattinson. Description logics and fuzzy probability. In Toby Walsh, editor, 22nd International Joint Conference on Artificial Intelligence. International Joint Conference on Artificial Intelligence (IJCAI’11). AAAI Press, 2011.

[bib.bib43] [43] Igor Sedlàr. Propositional dynamic logic with Belnapian truth values. In Stéphane Demri Lev Beklemishev and András Máté’, editors, Advances in Modal Logic (AiML’16), volume 11, pages 503–519. College Publications, 2016. URL: http://www.aiml.net/volumes/volume11/Sedlar.pdf.

[bib.bib44] [44] Igor Sedlàr. Finitely-valued Propositional Dynamic Logic. In Nicola Olivetti, Rineke Verbrugge, Sara Negri, and Gabriel Sandu, editors, Advances in Modal Logic (AiML’20), volume 13, pages 561–579. College Publications, 2020. URL: http://www.aiml.net/volumes/volume13/Sedlar.pdf.

[bib.bib45] [45] Bruno Teheux. Propositional dynamic logic for searching games with errors. Journal of Applied Logic, 12(4):377–394, 2014. doi:10.1016/j.jal.2014.04.001.

[bib.bib46] [46] Samuel Teuber, Stefan Mitsch, and André Platzer. Provably safe neural network controllers via differential dynamic logic. In Amir Globersons, Lester Mackey, Danielle Belgrave, Angela Fan, Ulrich Paquet, Jakub M. Tomczak, and Cheng Zhang, editors, Advances in Neural Information Processing Systems 38 (NeurIPS’24), 2024.

[bib.bib47] [47] Johan van Benthem. Program constructions that are safe for bisimulation. Studia Logica, 60:311–330, 1998. doi:10.1023/A:1005072201319.

[bib.bib48] [48] Johan van Benthem, Nick Bezhanishvili, and Sebastian Enqvist. A propositional dynamic logic for instantial neighborhood semantics. Studia Logica, 107(4):719–751, 2019. doi:10.1007/s11225-018-9825-5.

[bib.bib49] [49] Johan van Benthem, Nick Bezhanishvili, Sebastian Enqvist, and Junhua Yu. Instantial neighbourhood logic. The Review of Symbolic Logic, 10(1):116–144, 2017. doi:10.1017/S1755020316000447.

Safety and Strong Completeness via Reducibility for Many-Valued Coalgebraic Dynamic Logics

Abstract

Keywords and phrases:

Funding:

Copyright and License:

2012 ACM Subject Classification:

DOI:

Event:

Editors:

Series and Publisher:

1 Introduction

Related work.

2 Preliminaries

2.1 Many-valued modal logic

Definition 1 (𝖥𝖫ew-algebra).

Example 2.

▶ Remark 3 (Semi-primal 𝖥𝖫ew-algebras).

2.2 Coalgebraic logic via predicate liftings

Definition 4 (Coalgebra).

Example 5.

Definition 6 (Predicate lifting).

Definition 7 (Separating).

Example 8.

3 Coalgebraic dynamic logic, generalised

3.1 Coalgebra operations and tests

Definition 9 (Coalgebra operation).

Example 10.

Definition 11 (Test).

Example 12.

3.2 Syntax and semantics

Definition 13 (Formulas & Actions).

Definition 14 (Model).

Definition 15 (Standard model).

Example 16.

4 Safety and logical invariance

Definition 17 (Safe coalgebra operation).

Lemma 18.

Definition 19 (Safe test).

Lemma 20.

Proposition 21.

Corollary 22.

5 Reducibility and soundness

5.1 Templates and reducible coalgebra operations

Definition 23 (Template).

Definition 24 (Reducible coalgebra operation).

Proposition 25 (Soundness).

Proposition 26.

Example 27.

Example 28.

Example 29.

5.2 Independently reducible operations

Definition 30 (Independent reducibility).

Proposition 31.

Example 32.

5.3 Reducible tests

Definition 33.

Proposition 34.

Proposition 35.

Example 36.

6 Strong completeness

Definition 37 (The logic ℒ𝖥𝖣𝗒𝗇).

6.1 Non-modal homomorphisms and quasi-canonical models

Definition 38 (Non-modal homomorphism).

Definition 39 (Quasi-canonical model).

Theorem 40.

Proof.

Coalgebra operations.

Tests.

6.2 Finite one-step completeness

Definition 41 (Finite one-step completeness).

Theorem 42.

Proof.

Example 43 (Many-valued PDL, crisp accessibility).

Example 44 (Many-valued PDL, labelled accessibility).

Example 45 (Two-valued PDL, labelled accessibility).

Example 46 (Many-valued game logic).

Example 47 (Instantial PDL).

7 Future work

References

Appendix A Appendix

Definition 1 ( $\mathsf{FL}_{\mathrm{ew}}$ -algebra).

$\blacktriangleright$ Remark 3 (Semi-primal $\mathsf{FL}_{\mathrm{ew}}$ -algebras).

Definition 37 (The logic $\mathcal{L}_{\mathsf{F}}^{\mathsf{Dyn}}$ ).