Łukasiewicz Public Announcement Logic

Abstract

In this work we lay a theoretical framework for developing dynamic epistemic logics in a many-valued setting. We consider in particular the logic of Public Announcements, which is one of the simplest and best-known dynamic epistemic systems in the literature. We show how to develop a Public Announcement Logic based on finite-valued Łukasiewicz modal logic. We define our logic through a relational semantics based on many-valued Kripke models, and also introduce an alternative but equivalent algebra-based semantics using MV-algebras endowed with modal operators. We provide a Hilbert-style calculus for our logic and prove completeness with respect to both semantics.

1 Introduction

Dynamic epistemic logics (DEL) are formal systems designed to model the change brought about by epistemic actions, that is, actions that affect the cognitive state of (a group of) reasoning agents, rather than the facts of the world themselves. A prominent and simple example of an epistemic action is the public announcement of a certain proposition $\alpha$. In this scenario one considers how $\alpha$ becoming publicly known affects the beliefs of a group of agents. In the tradition of modal logic, DEL formally represent the beliefs of agents as algebraic or relational (Kripke-style) models. An epistemic action such as a public announcement induces a change on such models, which is accordingly modelled through an algebraic or frame-theoretic construction.

For example, viewing the set of beliefs of an agent as a Kripke model (a set of worlds that the agent considers possible, plus an accessibility relation and a valuation), the public announcement of a proposition $\alpha$ causes certain worlds (those where $\alpha$ is not true) to be no longer plausible, that is, precisely, to be no longer “possible worlds” from the agent’s perspective. These worlds are therefore “deleted” and a new Kripke model is created, whose underlying set of worlds is essentially just the extension of $\alpha$ (all worlds which satisfied $\alpha$ in the original model) and where the relation and the valuation are restricted in a straightforward way. This construction is known as an epistemic update. One then uses this new model to define the semantics of sentences of type $\langle \alpha \rangle \varphi$, whose intended meaning is: the proposition $\alpha$ has been announced, and after that $\varphi$ holds. Now if $\varphi$ itself contained an epistemic modal operator, then we would for example have a sentence like $\langle \alpha \rangle \Box \psi$, whose intended meaning is: the proposition $\alpha$ has been announced, and after that the agent knows (believes, etc.) that $\psi$ is the case.

The system of DEL that was introduced to deal with public announcements is called precisely Public Announcement Logic (PAL): see e.g. [1, 2]. This is essentially a language expansion of classical modal logic with so-called dynamic modal operators $\langle \alpha \rangle$ and $[ \alpha ]$, whose meaning and semantics is the one introduced above. A series of more recent papers [7, 9, 10] considers systems of PAL built on a non-classical propositional base. The motivation for the introduction of non-classical PAL is along the following lines.

On the one hand, PAL and related systems based on classical propositional logic have been used to provide a formal solution to epistemic problems such as the Muddy Children Puzzle and the Byzantine Generals Problem. It can be shown, however, that at least for some of these scenarios the full power of classical inference principles may not be needed: for example [7] provides a constructive solution to the Muddy Children Puzzle using intuitionistic logic.

Secondly, there are reasoning contexts where the strength of classical logic makes it unsuitable, a prominent example being reasoning in the presence of inconsistent information. The papers [9, 10] provide a framework for building a logic of public announcements that may be applied in such contexts.

Lastly, from a theoretical point of view, one may ask which structural conditions make it possible to extend a given modal epistemic system to a dynamic setting. The above-mentioned papers [6, 7, 9, 10] point at certain conditions that seem to be sufficient, at least in the cases that have been studied so far, and the present paper, as we will argue, provides further evidence and tools in this direction. However, the more general problem of formulating mathematically precise conditions that can be proven to be necessary and sufficient is still open, and constitutes, in our opinion, an intriguing direction for future research.

In the present paper we take the generalization of PAL to non-classical settings proposed in [7, 9, 10] one step further: namely, we show how to define a logic of public announcements having as base n-valued Łukasiewicz modal logic, n being an arbitrary positive integer. In doing so, we believe we are providing a tool that can be useful for reasoning in all those contexts where graded properties and predicates are involved, which are the main scope of many-valued and fuzzy logics. On the other hand, as mentioned above, we also hope that our study will shed further light on the mathematical nature of epistemic updates performed on relational structures and on algebras, thus helping to define a most general context in which these constructions can be performed.

The epistemic update constructions and the logical methods used in the present paper are essentially those of [6, 7], that we extend using insights of [9, 10]. These methods are applied to the family of finite-valued Łukasiewicz modal systems developed in [5], relying on on the duality for finitely-generated modal MV-algebras of [8].

The paper is organized as follows. Section 2 contains an introduction to Public Announcement Logic and to Łukasiewicz modal logic, which are the two main ingredients that are going to be combined in our treatment. In Sect. 3 we officially introduce Łukasiewicz Public Announcement Logic (Ł$_n$PAL). We define a relational semantics based on many-valued Kripke models and present a Hilbert-style calculus for Ł$_n$PAL. Section 4 is an intermezzo on the equivalence between algebraic and relational semantics of Łukasiewicz modal logic: this result is needed in order to introduce and develop our algebraic semantics for Ł$_n$PAL. In Sect. 5 we define the mechanism of epistemic updates in the algebraic setting of modal $\mathcal {MV}$-algebras (Subsect. 5.1). This will allow us to provide an algebraic semantics for Ł$_n$PAL (Subsect. 5.2) that is alternative but equivalent to the relational one, and to prove soundness (and completeness) for our Hilbert-style calculus (Subsect. 5.3). Lastly, Sect. 6 contains concluding remarks and suggestions for future work.

2 Preliminaries

2.1 The Logic of Public Announcements

The logic of public announcements [1, 2] is a dynamic logic that models the epistemic change on the cognitive state of a group of agents resulting from a given fact (expressed by some proposition, that we will denote by $\alpha$) becoming publicly known.

From a syntactic point of view, PAL is a language expansion of (classical) modal logic where, besides the so-called “static” modal operators $\Box$ and $\Diamond$ (whose intended interpretation is epistemic), we have “dynamic” operators $\langle \alpha \rangle$ and $[ \alpha ]$ for each formula $\alpha$ in the language. The intended meaning of a formula of type $\langle \alpha \rangle \varphi$ is: the proposition $\alpha$ has been announced, and after the announcement $\varphi$ is the case. The other dynamic operator, which in the classical and Łukasiewicz case is the dual of $\langle \alpha \rangle$, has the following interpretation: $[ \alpha ] \varphi$ means that if the proposition $\alpha$ has been announced, then after the announcement $\varphi$ is the case.

The formulas of PAL are built from a countable set of propositional letters Var through the following inductive rule:

$$ \varphi \,{:}{:}\!= \, p \in Var \, | \, \lnot \varphi \, | \, \varphi \rightarrow \varphi \, | \, \Box \varphi \, | \, [ \varphi ] \varphi $$

In this paper we focus on this language, because all other connectives are term-definable from these in both classical and Łukasiewicz logic. In particular we have $\Diamond \varphi : = \lnot \Box \lnot \varphi$ and $\langle \alpha \rangle \varphi : = \lnot [ \alpha ] \lnot \varphi$.

As mentioned above, the underlying (static) modal logic is usually taken to be a system modeling the knowledge of an agent, for example modal logic S5, whose semantics is provided in the standard way by relational models $\langle W, R, v \rangle$ with R an equivalence relation. In order to provide a semantics for formulas involving dynamic modalities, one needs to introduce the epistemic update construction. Let $M = \langle W, R, v \rangle$ be a model, where $v :Fm \times W \rightarrow \{0,1\}$ is the valuation map, and let $\alpha$ be a formula in the above-defined language. We define a new model $M^{\alpha } = \langle W^{\alpha }, R^{\alpha }, v^{\alpha } \rangle$ where $W^{\alpha } : = \{ w \in W : M, w \models \alpha \}$, $R^{\alpha } : = R \cap (W^{\alpha } \times W^{\alpha })$ and $v^{\alpha } :Fm \times W^{\alpha } \rightarrow \{0,1\}$ is the restriction of the map v to $W^{\alpha }$. Notice that, although M and $M^{\alpha }$ are different models, the set $W^{\alpha }$ can be embedded into W in the obvious way. This justifies the abuse of language of the following definitions:

$$ M, w \models [\alpha ] \varphi \qquad \text { iff } \qquad M,w \models \alpha \quad \text { implies } \quad M^{\alpha },w \models \varphi . $$

Dually, one sets

$$ M, w \models \langle \alpha \rangle \varphi \qquad \text { iff } \qquad M,w \models \alpha \quad \text { and } \quad M^{\alpha },w \models \varphi . $$

Given these definitions, the notion of modal consequence (usually one focuses on the so-called local one) is introduced in the standard way.

Classical PAL admits a simple Hilbert-style axiomatization. One expands the set of axioms and rules for modal logic (S5) with the following schemes:

• 1.    $\langle \alpha \rangle p \leftrightarrow (\alpha \wedge p )$

• 2.    $\langle \alpha \rangle \lnot \varphi \leftrightarrow ( \alpha \wedge \lnot \langle \alpha \rangle \psi )$

• 3.    $\langle \alpha \rangle ( \varphi \vee \psi ) \leftrightarrow (\langle \alpha \rangle \varphi \vee \langle \alpha \rangle \psi )$

• 4.    $\langle \alpha \rangle \Diamond \varphi \leftrightarrow ( \alpha \wedge \Diamond (\alpha \wedge \langle \alpha \rangle \varphi ))$

where $p \in Var$ and $\alpha , \varphi , \psi \in Fm$, together with the monotonicity rule:

$$ \text {from } \quad \emptyset \vdash \varphi \rightarrow \psi \quad \text {derive } \quad \emptyset \vdash \langle \alpha \rangle \varphi \rightarrow \langle \alpha \rangle \psi . $$

The restriction that $p \in Var$ in the first axiom reflects the important fact that the consequence relation of PAL is not substitution-invariant. Taken together, the above axioms suggest that any PAL-formula having the dynamic operator as main connective can be proven to be inter-derivable in the calculus to one where the dynamic operator has been pushed inside the scope of some other propositional or static modal operator. This is indeed the case, as we will see, and is the key to a completeness proof that relies on reducing any PAL-formula to a formula that does not contain any dynamic operator. In fact, also when moving from classical to a non-classical version of PAL, it is sufficient to check soundness of the set of proposed axioms with respect to the intended semantics, and completeness can be proven using the same reduction strategy that works for the classical case (see [7, 9, 10]). This is also the approach that we will take in our treatment of Łukasiewicz PAL.

2.2 Łukasiewicz n-valued Modal Logic

The main ingredients that we need to introduce our Łukasiewicz PAL are: (1) a “static” Łukasiewicz modal logic base to build upon, defined in terms of a (Hilbert-style) calculus which is sound and complete with respect to a relational semantics; (2) a suitable adaptation of the techniques for dealing with non-classical dynamic epistemic logics developed in [6, 7, 9, 10]; (3) in order to be able to successfully apply these techniques, it is also desirable to have at hand a workable duality theory connecting the relational and the algebraic semantics of (the static fragment of) the logic. As mentioned earlier on, the first item is provided by the work of Hansoul and Teheux [5], while the third is due to Teheux [8].

In this section we recall the main definitions and facts that we shall need about the modal extension of Łukasiewicz logic introduced in [5], which is going to be the static base of our Łukasiewicz PAL. We begin by recalling the essentials of Łukasiewicz (non-modal) logic, and then turn to its modal counterpart.

Łukasiewicz logic can be defined as the logic of $\mathcal {MV}$-algebras (built in the language $\langle \rightarrow , \lnot , 1 \rangle$ of type $\langle 2,1, 0\rangle$ and defined as in [3, Definition 4.2.1]). We use the following abbreviations: $0 : = \lnot 1$, $x \oplus y : = \lnot x \rightarrow y$, $x \odot y : = \lnot ( x \rightarrow \lnot y)$, $x \vee y : = (x \rightarrow y) \rightarrow y$, $x \wedge y : = \lnot (\lnot x \vee \lnot y)$. We also abbreviate $x^m : = x \odot \ldots \odot x$ (m times) and $m \, x : = x \oplus \ldots \oplus x$ (m times). As the notation suggests, the $\{\wedge ,\vee , 0, 1 \}$-reduct of any $\mathcal {MV}$-algebra is a bounded (distributive) lattice. As often happens in many-valued logics, algebras whose lattice order is total play a key role within the variety of $\mathcal {MV}$-algebras. It is in particular well-known that, for every positive integer n, there is up to isomorphism only one totally ordered n-element $\mathcal {MV}$-algebra. We denote it by $\mathbf{\L _{n}}$, and by $\mathcal {MV}_n$ the variety generated by $\mathbf{\L _{n}}$.

The logics that we shall focus on have as non-modal base n -valued Łukasiewicz logic . This is the logic defined by the the logical matrix $\langle \mathbf{\L _{n}}, \{ 1 \} \rangle$ in the standard way. For formulas $\varGamma \cup \{ \varphi \} \subseteq Fm$, we set $\varGamma \models _{\mathbf{\L _{n}}} \varphi$ iff, for every $\mathcal {MV}$-algebra homomorphism $h :\mathbf {Fm} \rightarrow \mathbf{\L _{n}}$, it holds that $h(\varphi ) = 1$ whenever $h[\varGamma ] \subseteq \{ 1 \}$. Logically, we think of $\rightarrow$ as an implication and $\lnot$ as a negation, while $\oplus , \vee$ are two different types of disjunction and $\odot , \wedge$ are two different conjunctions.

The above consequence relation is extended in [5] to the language $\langle \rightarrow , \lnot , \Box , 1 \rangle$ which is augmented with a unary (necessity-type) modal operator $\Box$ through a many-valued generalization of Kripke semantics. The notion of Kripke frame is defined in the usual way: a frame is a structure $\mathcal {F}= \langle W, R \rangle$ with W a non-empty set of ‘worlds’ and $R \subseteq W \times W$ an accessibility relation. An n -valued Kripke model is a structure $\mathcal {M}= \langle W, R, v \rangle$ such that $\langle W, R \rangle$ is a frame and $v :\mathbf {Fm} \times W \rightarrow \mathbf{\L _{n}}$ is a valuation map satisfying the following requirements: for all $\varphi , \psi \in Fm$ and any $w \in W$,

• $v (\lnot \varphi , w) = \lnot ^{\mathbf{\L _{n}}} v(\varphi , w )$

• $v ( \varphi \rightarrow \psi , w) = v(\varphi , w ) \rightarrow ^{\mathbf{\L _{n}}} v(\psi , w )$

• $v ( \Box \varphi , w) = \bigwedge ^{\mathbf{\L _{n}}} \{ v(\varphi , w') : w R w' \}$ where $\bigwedge ^{\mathbf{\L _{n}}}$ is the lattice meet in $\mathbf{\L _{n}}$.

Note that arbitrary meets always exist in the finite algebra $\mathbf{\L _{n}}$, and in fact the meet is a minimum because $\mathbf{\L _{n}}$ is a chain. A dual possibility operator $\Diamond$ can be defined by $\Diamond \varphi := \lnot \Box \lnot \varphi$, and it is easy to check that, for any valuation v, any $\varphi \in Fm$ and all $w \in W$, we have $v ( \Diamond \varphi , w) = \bigvee ^{\mathbf{\L _{n}}} \{ v(\varphi , w') : w R w' \}$, where $\bigvee ^{\mathbf{\L _{n}}}$ is the lattice join (or maximum) in $\mathbf{\L _{n}}$.

As usual, we say that an n-valued model $\mathcal {M}= \langle W, R, v \rangle$ satisfies a formula $\varphi$ at a world $w \in W$, denoted $\mathcal {M}, w \models \varphi$, when $v (\varphi , w) = 1^{\mathbf{\L _{n}}}$ (we omit the parameters n and $\mathbf{\L _{n}}$ when they are clear from the context). We can then define a (local) modal consequence relation by setting $\varGamma \models ^l_n \varphi$ iff, for every n-valued model $\mathcal {M}$ and every $w \in W$, $\mathcal {M}, w \models \gamma$ for all $\gamma \in \varGamma$ implies $\mathcal {M}, w \models \varphi$.

In this paper (as in [5]) we focus on the local logic. The local consequence relation over a given $\mathbf{\L _{n}}$ is axiomatized by the following Hilbert-style calculus [5, Theorem 6.2].

The set of axioms is the least set of formulas $\varSigma$ that is closed under modus ponens (if $\varphi , \, \varphi \rightarrow \psi \in \varSigma$, then $\psi \in \varSigma$), under substitutions, necessitation (if $\varphi \in \varSigma$, then $\Box \varphi \in \varSigma$) and that contains:

• an axiomatic base for Łukasiewicz n-valued logic (see [4]),

• $\Box (\varphi \rightarrow \psi ) \rightarrow (\Box \varphi \rightarrow \Box \psi )$

• $\Box (\varphi \oplus \varphi ) \leftrightarrow (\Box \varphi \oplus \Box \varphi )$

• $\Box (\varphi \odot \varphi ) \leftrightarrow (\Box \varphi \odot \Box \varphi )$.

The only inference rule that can be used without restrictions is modus ponens.

Notice that the set of axioms $\varSigma$ of the above calculus includes all propositional Łukasiewcz tautologies, and that if $\varphi$ is a propositional tautology, then, by necessitation, $\Box \varphi \in \varSigma$. However, it is not true that if we have derived $\varphi$ from a set of formulas $\varGamma$ in the whole calculus, then we can derive $\Box \varphi$ from $\varGamma$. This reflects the fact that the calculus is designed to capture the notion of local modal consequence relation, not the global one. If we add necessitation as a rule that can be applied without restrictions, then indeed we obtain a calculus for the global modal consequence relation.

Writing $\varGamma \vdash ^l_{n} \varphi$ when there is a proof (in the standard sense) of $\varphi$ from $\varGamma$ using the axioms and rule of the above calculus, we can state completeness as follows:

$$\varGamma \vdash ^l_{n} \varphi \quad \text { if and only if } \quad \varGamma \models ^l_{n} \varphi . $$

3 Łukasiewicz Public Announcement Logic

The language of Łukasiewicz Public Announcement Logic is the same as classical PAL. For the single-agent case¹, formulas are built from a countable set of propositional letters Var through the following inductive rule:

$$ \varphi \,{:}{:}\!\!= \, p \in Var \, | \, \lnot \varphi \, | \, \varphi \rightarrow \varphi \, | \, \Box \varphi \, | \, [ \varphi ] \varphi $$

Following the usual conventions, we set $\Diamond \varphi : = \lnot \Box \lnot \varphi$ and $\langle \alpha \rangle \varphi : = \lnot [ \alpha ] \lnot \varphi$.

For a given n, we can define the semantics of the static modal fragment of n-valued Łukasiewicz Public Announcement Logic (abbreviated Ł$_n$PAL) using n-valued Kripke models as described in the preceding section. In order to provide a semantics for formulas of type $[ \alpha ] \varphi$, we need to define a notion of epistemic update on n-valued Kripke models.

Let $\mathcal {M}= \langle W, R, v \rangle$ be an n-valued model, and let $\alpha$ be a formula. Mimicking the classical case, we set

$$ W^{\alpha } : = \{ w \in W : v (\alpha , w) = 1^{\mathbf{\L _{n}}} \}. $$

Notice that $W^{\alpha } = W^{\alpha \odot \alpha }$, because $v (\alpha , w) = 1^{\mathbf{\L _{n}}}$ iff $v (\alpha \odot \alpha , w) = 1^{\mathbf{\L _{n}}}$. In fact, writing $\alpha ^m$ instead of $\alpha \odot \ldots \odot \alpha$ (m times), we have $W^{\alpha } = W^{\alpha ^m}$ for any $m \ge 1$. This means that there is no difference between announcing $\alpha$ and announcing $\alpha ^m$, because we are only looking at formulas that are “absolutely true”. This fact will play an important role in our definition of epistemic updates in the n-valued setting.

The accessibility relation can be restricted just as in the classical case, that is we set $R^{\alpha } : = R \cap (W^{\alpha } \times W^{\alpha })$. Similarly, we define $v^{\alpha } :Fm \times W^{\alpha } \rightarrow \mathbf{\L _{n}}$ to be the restriction of the map v to $W^{\alpha }$. In this way we obtain the updated model $\mathcal {M}^{\alpha } = \langle W^{\alpha }, R^{\alpha }, v^{\alpha } \rangle$, which allows us to define

$$ M, w \models [\alpha ] \varphi \qquad \text { iff } \qquad M,w \models \alpha \quad \text { implies } \quad M^{\alpha },w \models \varphi . $$

Given that we are in a many-valued setting, the reader might wonder whether the above definition is sufficient to determine the semantic value of arbitrary formulas involving dynamic operators. This may not evident at this point, but will be easily checked by looking at the algebraic semantics that we are going to define in Sect. 5.2 (which is, as we will show, equivalent to the relational one via duality). This is indeed one of the main reasons why we find it useful to present a double perspective (relational as well as algebraic) on Ł$_n$PAL.

Having provided a notion of satisfaction for arbitrary formulas, the definition of consequence in Ł$_n$PAL is just a reformulation of the one we have stated above for the static fragment. We define the (local) modal consequence relation by setting $\varGamma \models ^l_{\mathrm {\L }_n\text {PAL}} \varphi$ iff, for every n-valued model $\mathcal {M}$ and every $w \in W$, $\mathcal {M}, w \models \gamma$ for all $\gamma \in \varGamma$ implies $\mathcal {M}, w \models \varphi$.

We now introduce an axiomatization that we will later on prove to be sound and complete with respect to the above-defined semantics. We abbreviate $\langle \alpha \rangle \varphi := \lnot [ \alpha ] \lnot \varphi$. The axioms of Ł$_n$PAL are all axioms and rules of $\mathcal {MMV}_n$ [5, Definition 3.1] plus the following:

• Interaction with 1               $[\alpha ]1 \leftrightarrow 1$

• Interaction with $\rightarrow$              $[\alpha ](\varphi \rightarrow \psi ) \leftrightarrow ( \langle \alpha \rangle \varphi \rightarrow \langle \alpha \rangle \psi )$

• Interaction with $\lnot$               $[\alpha ]\lnot \varphi \leftrightarrow (\alpha ^n \rightarrow \lnot [ \alpha ] \varphi )$

• Interaction with $\Box$               $[\alpha ]\Box \varphi \leftrightarrow ( \alpha ^n \rightarrow \Box [ \alpha ] \varphi )$

• Preservation of facts           $[\alpha ]p \leftrightarrow (\alpha ^n \rightarrow p)$

where $\varphi , \psi , \alpha$ are arbitrary formulas, while p is a propositional variable. We further require the set of theorems to be closed under $[\alpha ]$-monotonicity:

$$ \vdash \varphi \rightarrow \psi \quad \Rightarrow \quad \vdash [\alpha ] \varphi \rightarrow [\alpha ] \psi . $$

The only rule of our calculus is modus ponens: $\varphi , \ \varphi \rightarrow \psi \vdash \psi$.

This defines the calculus $\vdash ^l_{\mathrm {\L }_n\text {PAL}}$ for Ł$_n$PAL.

As the reader will have noticed, the shape of the axioms defining the interaction of the dynamic operator with the other connectives resembles that of the classical (and intuitionistic: see [7]) case, and their role in our completeness proof is analogous. The main difference worth mentioning is the presence of the formula $\alpha ^n$, which is a shorthand for $\alpha \odot \ldots \odot \alpha$ (n times; recall that $\alpha \odot \alpha$ is itself a shorthand for $\lnot ( \alpha \rightarrow \lnot \alpha )$). The parameter n obviously distinguishes one finite-valued Łukasiewicz public announcement logic from another. However, for the purpose of axiomatization, all that matters is that the n appearing in the axioms be big enough. In fact we might use any $m \ge n$ for providing a complete axiomatization of Ł$_n$PAL, for $\alpha ^m$ is semantically equivalent in Ł$_n$PAL to $\alpha ^n$ for each $m \ge n$. The role of these exponents will be further clarified when we look at the algebraic semantics of Ł$_n$PAL.

Let us also highlight that the static modal logic we build on is a many-valued analogue of the minimal normal modal logic K (rather than, say, of modal logic S5). This choice was made just for the sake of generality, for we will show that, once we have axiomatized the minimal Ł$_n$PAL, it is easy to deal with extensions obtained by adding axioms to its static fragment.

As mentioned earlier, completeness of Ł$_n$PAL can be proved using the same strategy as the classical case. For this, we will need to check the soundness of the above-introduced axioms, which is most easily done with respect to the algebraic semantics of Ł$_n$PAL. Then, assuming we know that the algebraic and the relational semantics are equivalent, we will have completed the proof. This equivalence can indeed be easily obtained exploiting Teheux’s duality for modal $\mathcal {MV}$-algebras [8]. It is therefore convenient to recall the main results of this duality before we introduce our algebraic semantics for Ł$_n$PAL and go on to develop the epistemic update construction on algebraic models.

4 On Duality for Modal $\mathcal {MV}$-algebras

The Hilbert-style calculus for Łukasiewicz n-valued modal logic of Subsect. 2.2 not only enjoys completeness with respect to the relational semantics of n-valued Kripke models, but can also be endowed with an algebraic semantics provided by the class of modal n -valued $\mathcal {MV}$ -algebras ($\mathcal {MMV}_n$-algebras). These play a key role in our semantic approach to Ł$_n$PAL, therefore in this section we take a closed look at them and in particular at the duality relating $\mathcal {MMV}_n$-algebras to n-valued Kripke frames.

An $\mathcal {MMV}$ -algebra is a structure $\langle \mathbf {A} , \rightarrow , \lnot , \Box , 1 \rangle$ such that the reduct $\langle \mathbf {A} , \rightarrow , \lnot , 1 \rangle$ is an $\mathcal {MV}$-algebra and the following equations are satisfied:

• (MO1) $\Box 1 = 1$

• (MO2) $\Box (x \rightarrow y ) \rightarrow (\Box x \rightarrow \Box y) = 1$

• (MO3) $\Box (x \oplus x)= \Box x \oplus \Box x$ and $\Box (x \odot x)= \Box x \odot \Box x$

• (MO4) $\Box (x \oplus x^{m}) = \Box x \oplus (\Box x)^{m}$ for every natural number m.

A dual operator $\Diamond$ can be defined by $\lnot \Box \lnot$ as for classical modal logic. An $\mathcal {MMV}_n$ -algebra is an $\mathcal {MMV}$-algebra whose $\Box$-free reduct belongs to $\mathcal {MV}_n$. In this case one can prove that (MO4) follows from (MO1)-(MO3), which also explains why we have omitted the corresponding axiom in the Hilbert-style calculus for n-valued modal logic of Subsect. 2.2.

An important notion, both from a logical and a duality point of view, is that of filter. Given an algebra $\mathbf {A}$ having an $\mathcal {MV}$-algebra reduct (thus also any algebra in $\mathcal {MMV}$ or $\mathcal {MMV}_n$), a filter of $\mathbf {A}$ is defined as a non-empty set $F \subseteq A$ which is an up-set w.r.t. the lattice order of $\mathbf {A}$ and is moreover closed under the $\odot$ operation, i.e. $a, b \in F$ implies $a \odot b \in F$. Every $\mathcal {MV}$-algebra $\mathbf {A}$ has a least filter which is the singleton $\{1^{\mathbf {A} }\}$.

An algebraic model of modal n-valued Łukasiewicz logic is a pair $\langle \mathbf {A} , v \rangle$ where $\mathbf {A} \in \mathcal {MMV}$ and $v :\mathbf {Fm} \rightarrow \mathbf {A}$ is a homomorphism of $\mathcal {MMV}$-algebras. Through this notion we can define, as with the relational semantics, a local consequence relation. We set $\varGamma \models _{\mathcal {MMV}_n} \varphi$ when, for any algebraic model $\langle \mathbf {A} , v \rangle$ and any filter $F\subseteq A$, we have $v (\varphi ) \in F$ whenever $v(\gamma ) \in F$ for all $\gamma \in \varGamma$.

The Hilbert-style calculus of [5] introduced in Subsect. 2.2 is complete, for each modal n-valued Łukasiewicz system, w.r.t. to the corresponding above-defined local consequence; this result can be proved either directly or, via duality (see below), using completeness w.r.t. to n-valued Kripke models. For details and proofs about the duality for n-valued Łukasiewicz modal logics, we refer the reader to [5, 8]. Here we just recall the main bits that are needed for our treatment of Ł$_n$PAL.

If we have an algebraic model for our logic $\langle \mathbf {A} , v \rangle$, where $\mathbf {A} \in \mathcal {MMV}_n$ and $v :\mathbf {Fm} \rightarrow \mathbf {A}$, we can use duality to turn it into a n-valued Kripke model as follows. We construct the canonical frame $\mathbf {A} _+ = \langle \mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}}), R \rangle$, where $\mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}})$ is the set of $\mathcal {MV}$-algebra homomorphisms (i.e., not necessarily $\Box$-preserving) from $\mathbf {A}$ to $\mathbf{\L _{n}}$ and the accessibility relation $R_{\, \Box } \subseteq \mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}}) \times \mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}})$ is defined, for all $h,h' \in \mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}})$, by

$$\begin{aligned} \langle h, h' \rangle \in R_{\, \Box } \quad \text { iff } \quad \forall a \in A \ \ h(\Box a) = 1^{\mathbf{\L _{n}}} \ \text { implies } \ h'(a) = 1^{\mathbf{\L _{n}}}. \end{aligned}$$

Denoting by $\mathbf {[0,1} ]$ the $\mathcal {MV}$-algebra having as universe the real interval [0, 1], it is easy to show that $\mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}}) \cong \mathcal {MV}(\mathbf {A} , \mathbf {[0,1} ])$ for any $\mathbf {A} \in \mathcal {MMV}_n$. This explains why we can rephrase [5, Definition 5.2] replacing the algebra $\mathbf {[0,1} ]$ by $\mathbf{\L _{n}}$. Given an algebraic model $\langle \mathbf {A} , v \rangle$, the canonical model $\langle \mathbf {A} _+, v_+ \rangle$ is obtained by defining the valuation $v_+ :\mathbf {Fm} \times \mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}}) \rightarrow \mathbf{\L _{n}}$ as

$$ v_+ \langle h, \varphi \rangle = (h \cdot v) (\varphi ) $$

for all $h \in \mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}})$ and $\varphi \in Fm$. It can be checked that $v_+$ indeed respects all connectives of the logic and is therefore a modal valuation. It is also easy to check that, for any formula $\varphi$, we have $v(\varphi ) = 1^{\mathbf {A} }$ if and only if $v_+ \langle h, \varphi \rangle = 1^{\mathbf{\L _{n}}}$ for all $h \in \mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}})$, that is, if and only if $\varphi$ is valid in the model $\langle \mathbf {A} _+, v_+ \rangle$.

Conversely, any n-valued Kripke model $\mathcal {M}= \langle \mathcal {F}, v \rangle$, where $\mathcal {F}= \langle W, R \rangle$ and $v :Fm \times W \rightarrow \mathbf{\L _{n}}$, can be turned into an algebraic one in the following way. We have the $\mathcal {MV}_n$-algebra $\mathcal {F}^+ = \mathbf{\L _{n}}^{\!\!\!\!W}$ whose elements are all maps $f :W \rightarrow \mathbf{\L _{n}}$, which can be endowed with a modal operator $\Box _R$ defined by

$$\begin{aligned} \Box _R (f)(w) : = \bigwedge ^{\ \mathbf{\L _{n}}} \{ f(u) : u \in W \text { and } w R u \}. \end{aligned}$$

(1)

We have then a $\mathcal {MMV}_n$-algebra $\mathcal {F}^+ = \langle \mathbf{\L _{n}}^{\!\!\!\!W}, \Box _R \rangle$, on which we define a valuation $v^+$, for all $\varphi \in Fm$ and $w \in W$, as

$$ v^+(\varphi )(w) := v(\varphi , w). $$

A formula $\varphi$ is valid in $\mathcal {M}$ if and only if $v^+(\varphi )$ is the constant map $1^{\mathbf{\L _{n}}}$.

Analogously to the case of modal Boolean algebras, it can be shown that every n-valued frame $\mathcal {F}$ is embeddable into its double dual $(\mathcal {F}^+)_+$. Likewise, an arbitrary $\mathcal {MMV}_n$-algebra $\mathbf {A}$ need not be isomorphic to its double dual $(\mathbf {A} _+)^+$ but it will be embeddable in it. This is sufficient to prove that the algebra-based and the frame-based semantics are equivalent.

We prove the equivalence by contraposition. First, suppose $\varGamma \not \models _{\mathcal {MMV}_n} \varphi$, which means that there is an algebraic model $\langle \mathbf {A} , v \rangle$ and a filter $F\subseteq A$ with $v (\varphi ) \notin F$ and $v(\gamma ) \in F$ for all $\gamma \in \varGamma$. Now F can be extended to a maximal filter $F' \supseteq F$ with $v (\varphi ) \notin F'$, and $F'$ corresponds to an $\mathcal {MV}$-algebra homomorphism $h_{F'} \in \mathcal {MV}(\mathbf {A} , \mathbf{\L _{n}})$ such that $h_{F'}(\gamma ) = 1^{\mathbf{\L _{n}}}$ for all $\gamma \in \varGamma$ and $h_{F'}(\varphi ) \ne 1^{\mathbf{\L _{n}}}$. Thus we have $\langle \mathbf {A} _+, v_+ \rangle , h_{F'} \models \gamma$ for all $\gamma \in \varGamma$ while $\langle \mathbf {A} _+, v_+ \rangle , h_{F'} \not \models \varphi$. Hence, $\varGamma \not \models ^l_n \varphi$.

Conversely, assume $\varGamma \not \models ^l_n \varphi$, which means that there is an n-valued model $\mathcal {M}= \langle \mathcal {F}, v \rangle$ with $\mathcal {F}= \langle W, R \rangle$ and a point $w \in W$ such that $\mathcal {M}, w \models \gamma$ for all $\gamma \in \varGamma$ while $\mathcal {M}, w \not \models \varphi$. Thus, in the dual algebra $\mathcal {F}^+ = \langle \mathbf{\L _{n}}^{\!\!\!\!W}, \Box _R \rangle$ we have elements $a_{\gamma }$ for each $\gamma \in \varGamma$ and an element $a_{\varphi }$ such that $a_{\gamma }(w) = 1^{\mathbf{\L _{n}}} \ne a_{\varphi }(w)$. This means that $a_{\gamma } \not \le a_{\varphi }$ for each $\gamma \in \varGamma$, which implies that the filter F generated by all $a_{\gamma }$ does not contain $a_{\varphi }$. Thus, the algebraic model $\langle \mathcal {F}^+, v^+ \rangle$ together with the filter F is a counter-model to $\varGamma \, \models _{\mathcal {MMV}_n} \varphi$, as was required to prove.

5 Algebraic Models and Completeness

5.1 Epistemic Updates on Modal $\mathcal {MV}$-algebras

Given the n-valued Kripke model $\mathcal {M}= \langle \mathcal {F}, v \rangle$ where $\mathcal {F}= \langle W, R \rangle$, we have an $\mathcal {MV}_n$-algebra $\mathbf{\L _{n}}^{\!\!\!\!W}$ whose elements are all maps $f :W \rightarrow \mathbf{\L _{n}}$. Following Teheux, we endow this algebra with a modal operator $\Box _R$ defined as in (1) and we have an $\mathcal {MMV}_n$-algebra $\langle \mathbf{\L _{n}}^{\!\!\!\!W}, \Box _R \rangle$. Now let $\alpha \in Fm$, and consider the updated model $\mathcal {M}^{\alpha } = \langle W^{\alpha }, R^{\alpha }, v^{\alpha } \rangle$ defined as in Sect. 3. To this model corresponds, via duality, the $\mathcal {MMV}_n$-algebra $\langle \mathbf{\L _{n}}^{\!\!\!\!W^{\alpha }}, \Box _{R^{\alpha }} \rangle$, whose elements are maps $g :W^{\alpha } \rightarrow \mathbf{\L _{n}}$, which are precisely the restrictions of the maps in $\mathbf{\L _{n}}^{\!\!\!\!W}$ to $W^{\alpha }$. We are going to see that the algebra $\langle \mathbf{\L _{n}}^{\!\!\!\!W^{\alpha }}, \Box _{R^{\alpha }} \rangle$ is isomorphic to a pseudo-quotient of $\mathcal {MMV}_n$-algebra $\langle \mathbf{\L _{n}}^{\!\!\!\!W}, \Box _R \rangle$, defined as below.

Let $\mathbf {A} = \langle \mathbf{\L _{n}}^{\!\!\!\!W}, \Box _R \rangle$ be the algebra dual to $\langle W, R \rangle$, and let $a \in A$ be the element corresponding to the map $v(\alpha ,\cdot ) :W \rightarrow \mathbf{\L _{n}}$. We define the following equivalence relation: for all $b,c \in \mathbf {A}$,

$$ b \mathbin \equiv _{a}c \quad \text { iff } \quad b \odot a^n = c \odot a^n. $$

Notice that, since the non-modal reduct of $\mathbf {A}$ is in the variety generated by $\mathbf{\L _{n}}$, the equation $a^n = a^{n+1}$ holds in $\mathbf {A}$. This means that $a^n$ is an idempotent element of $\mathbf {A}$, which implies that in fact we have:

$$ b \mathbin \equiv _{a}c \quad \text { iff } \quad b \odot a^n = c \odot a^n \quad \text { iff } \quad b \wedge a^n = c \wedge a^n. $$

Thanks to the idempotency of $a^n$, the above-defined relation is a congruence of the $\mathcal {MV}$-algebra reduct of $\mathbf {A}$. In fact, the possibility of finding such an idempotent element one of the main technical reasons for working with finitely-generated algebras: at the moment we are not aware of a definition of pseudo-quotient that would work for general $\mathcal {MV}$-algebras.

Although $\mathbin \equiv _{a}$ need not be compatible with the modal operator $\Box$, we can define, for each $[b]_{\mathbin \equiv _{a}} \in \mathbf {A} / \mathbin \equiv _{a}$,

$$ \Box ^{a}[b]_{\mathbin \equiv _{a}} : = [\Box (a^n \rightarrow b)]_{\mathbin \equiv _{a}} $$

and we obtain an $\mathcal {MMV}_n$-algebra $\langle \mathbf {A} / \mathbin \equiv _{a}, \Box ^{a}\rangle$, which we call the pseudo-quotient and denote by $\mathbf {A} ^{a}$ (see Proposition 1 below). As usual, the operator dual to $\Box ^{a}$ is defined by $\Diamond ^{a}[b]_{\mathbin \equiv _{a}} := \lnot \Box ^{a}\lnot [b]_{\mathbin \equiv _{a}}$ which gives

$$ \Diamond ^{a}[b]_{\mathbin \equiv _{a}} = [\Diamond (b \wedge a^n)]_{\mathbin \equiv _{a}} $$

Lemma 1

The algebra $\langle \mathbf{\L _{n}}^{\!\!\!\!W^{\alpha }}, \Box _{R^{\alpha }} \rangle$ is isomorphic to the pseudo-quotient $\mathbf {A} ^{a}$.

Proof

Let $\eta :\mathbf {A} {^a} \rightarrow \mathbf{\L _{n}}^{\!\!\!\!W^{\alpha }}$ be defined by $\eta [b] = b\upharpoonright W^{\alpha }$ (from now on we shall write [b] instead of $[b]_{\mathbin \equiv _{a}}$ to simplify the notation). Notice that if $[b] = [c]$, i.e. $b \wedge a^n = c \wedge a^n$, then, for all $w \in W^{\alpha }$, we have $a(w) = 1$ and so $a^n(w)=1$. Hence, $b (w) = (b \wedge a^n) (w) = (c \wedge a^n) (w) = c(w)$. That is, if $[b] = [c]$, then $\eta [b] = \eta [c]$. Thus the map $\eta$ is well-defined. To see that it is injective, notice that, for any $w \in W$, the element $a^n(w)$ is an idempotent of $\mathbf{\L _{n}}$, that is, $a^n(w) \in \{0^{\mathbf{\L _{n}}}, 1^{\mathbf{\L _{n}}} \}$. Now, assuming $[b] \ne [c]$, we have $(b \wedge a^n) (w) \ne (c \wedge a^n) (w)$ for some $w \in W$. If $w \notin W^{\alpha }$, one would have $1^{\mathbf{\L _{n}}} > a(w)$ and so necessarily $1^{\mathbf{\L _{n}}} > a(w) \ge a^n(w) = 0^{\mathbf{\L _{n}}}$. So we must have $w \in W^{\alpha }$, which means that $a^n(w)= 1^{\mathbf{\L _{n}}}$ and so $b(w) = (b \wedge a^n) (w) \ne (c \wedge a^n) (w) = c(w)$, i.e. $\eta [b] \ne \eta [c]$. Surjectivity of $\eta$ is straightforward: if $b \in \mathbf{\L _{n}}^{\!\!\!\!W^{\alpha }}$, then b is the restriction of some $b' \in \mathbf{\L _{n}}^W$, and so $\eta [b'] = b$.

Hence $\eta$ is a bijection between the universe of $\langle \mathbf{\L _{n}}^{\!\!\!\!W^{\alpha }}, \Box _{R^{\alpha }} \rangle$ and that of $\mathbf {A} ^{a}$. It is also obvious that $\eta$ is an $\mathcal {MV}$-algebra homomorphism. Furthermore, it is easy to show that, for all $w \in W^{\alpha }$,

$$ \eta (\Box ^{a}_R [b]) (w) = \eta [\Box _R (a^n \rightarrow b) ](w) = \Box _{R^{\alpha }} (b)(w) = (\Box _{R^{\alpha }} (\eta [b]))(w). $$

The equality

$$ \bigwedge ^{\ \mathbf{\L _{n}}} \{ (a^n \rightarrow b)(u) : u \in W \text { and } w R u \} = \bigwedge ^{\ \mathbf{\L _{n}}} \{ (a^n \rightarrow b)(u) : u \in W^{\alpha } \text { and } w R^{\alpha } u \}$$

holds because, when computing the infimum, any world outside $W^{\alpha }$ can be disregarded. In fact, if $u \notin W^{\alpha }$, then $a^n(u)= 0^{\mathbf{\L _{n}}}$ as we have seen earlier, and so $(a^n \rightarrow b)(u) = 1^{\mathbf{\L _{n}}}$.

We thus conclude that $\eta$ is an $\mathcal {MMV}_n$-algebra isomorphism.

In light of Lemma 1, we shall adopt the above-defined pseudo-quotient as our official construction for epistemic updates on $\mathcal {MMV}_n$-algebras.

Lemma 2

Let $u \in A$ be an idempotent element of an $\mathcal {MV}$-algebra $\mathbf {A}$. Then, for all $a,b \in A$,

• (i) $u \odot a = u \wedge a$ and $u \oplus a = u \vee a$

• (ii) $u \rightarrow (a \odot b ) = (u \rightarrow a) \odot (u \rightarrow b)$

• (iii) $u \rightarrow (a \oplus b ) = (u \rightarrow a) \oplus (u \rightarrow b)$

Proof

It suffices to check that the above items hold in any $\mathcal {MV}$-chain, for it is well-known that the variety of $\mathcal {MV}$-algebras is generated (as a quasivariety) by its chains. It is also well-known that in an $\mathcal {MV}$-chain the only idempotents are the top and the bottom element, for which the above statements follow trivially.

Proposition 1

For any $\mathbf {A} \in \mathcal {MMV}_n$ and any $a\in A$, we have $\mathbf {A} ^a = \langle \mathbf {A} / \! \!\equiv _a, \Box ^a \rangle \in \mathcal {MMV}_n$.

Proof

That $\mathbin \equiv _{a}$ is a congruence follows from, e.g., [3, Proposition 1.2.6], so we have $\mathbf {A} / \! \! \equiv _a \, \in \mathcal {MV}$, and if $\mathbf {A} \in \mathcal {MV}_n$ then $\mathbf {A} /\! \! \equiv _a \, \in \mathcal {MV}_n$. It remains to check that $\Box ^a$ is a modal operator satisfying equations (MO1)–(MO3) of [8, Definition 3.1]. The proof of these facts follows straighforwardly from Lemma 2 and the fact that $a^n$ is idempotent.

As mentioned in Sect. 3, we take as static base the minimal n-valued modal Łukasiewicz logic. It is however easy to see that the pseudo-quotient construction introduced above can be applied also to $\mathcal {MMV}_n$-algebras satisfying additional equations, which correspond to axiomatic extensions of the basic logic. All that needs to be checked is that, if $\mathbf {A} \in \mathcal {MMV}_n$ satisfies some extra equation $\delta$, then the pseudo-quotient algebra $\mathbf {A} ^a$ will also satisfy $\delta$. For equations in the pure language of $\mathcal {MV}$-algebras, this is straightforward, for the non-modal reduct of $\mathbf {A} ^a$ is actually just a quotient of the corresponding reduct of $\mathbf {A}$. On the other hand, if $\delta$ contains some modal operator, then it may not be preserved. A simple example is the equation $\Diamond 1 = 1$. On the contrary, it is easy to check e.g. that the equation $\Box x \rightarrow x = 1$ (which corresponds, also in the setting of n-valued frames, to reflexivity of the relation) is preserved.

In general, reasoning on frames, it is not hard to see that a sufficient condition for an equation to be preserved is that it corresponds to some property that is preserved by the update, which consists essentially in deleting some worlds from a model. This is of course not a characterization, and indeed providing such a characterization might prove an interesting topic for future research. It is, however, sufficient to establish that it is possible to define an n-valued analogue of, e.g., modal logic S5 by adding appropriate axioms/equations, and to take this logic as the static base for Ł$_n$PAL.

5.2 Algebraic Semantics for Ł$_n$PAL

We are now going to use the notion of algebraic model for modal Łukasiewicz logic introduced in Sect. 4 to provide an alterative but equivalent semantics for Ł$_n$PAL. This semantics, which is based on $\mathcal {MMV}_n$-algebras, is in certain respects easier to handle than the relational one, and will allow us to give us a simple(r) proof of completeness.

Recall that an algebraic model for Łukasiewicz n -valued modal logic is a pair $\langle \mathbf {A} , v \rangle$ where $\mathbf {A} \in \mathcal {MMV}_n$ (for we focus here on finitely-generated $\mathcal {MMV}$-algebras) and $v :\mathbf {Fm} \rightarrow \mathbf {A}$ is a homomorphism of $\mathcal {MMV}$-algebras (thus, $\Box$-preserving, too). To a formula $\alpha$ that is being announced corresponds an element $v(\alpha ) = a \in \mathbf {A}$, which we can use to build the pseudo-quotient algebra $\mathbf {A} ^a$ as shown earlier. Notice that each equivalence class $[b] \in \mathbf {A} ^a$ has a minimum element (w.r.t. the lattice order of $\mathbf {A}$), namely $b \wedge a^n$. This means (cfr. [7, Fact 6.1]) that we can define an injective map $\iota :\mathbf {A} ^a \rightarrow \mathbf {A}$ given by $\iota [b] := b \wedge a^n$. Via $\iota$ we can view $\mathbf {A} ^a$ as a pseudo-subalgebra of $\mathbf {A}$, and we can also extend the algebraic semantics for n-valued modal logic to formulas with dynamic operators, as shown in the following definition.

An algebraic model for $\L _n$ PAL is a pair $\langle \mathbf {A} , v \rangle$ where $\mathbf {A} \in \mathcal {MMV}_n$ and $v :\mathbf {Fm} \rightarrow \mathbf {A}$ is a homomorphism of $\mathcal {MMV}$-algebras. The map v is extended to formulas containing dynamic operators as follows:

$$ v( [ \alpha ] \varphi ) := v( \alpha ^n ) \rightarrow ^{\mathbf {A} } (\iota \cdot v^{\alpha }) (\varphi ). $$

where $v^{\alpha } :\mathbf {Fm} \rightarrow \mathbf {A} ^{v(\alpha )}$ is the unique $\mathcal {MMV}_n$-homomorphism extending the map $v^{\alpha } :Var \rightarrow \mathbf {A} ^{v(\alpha )}$ defined by $v^{\alpha }(p) := [v(p)]_{\equiv _{v(\alpha )}}$ for each $p\in Var$. We do not take the dynamic diamond $\langle \alpha \rangle$ as primitive, but if we did, we would define, analogously to classical and intuitionistic PAL,

$$ v( \langle \alpha \rangle \varphi ) := v( \alpha ^n ) \wedge ^{\mathbf {A} } (\iota \cdot v^{\alpha }) (\varphi ). $$

At this point we can use algebraic models to introduce a notion of (local) consequence relation. We set $\varGamma \models ^l_{\mathrm {\L }_n\text {PAL}} \varphi$ if and only if for every algebraic model $\langle \mathbf {A} , v \rangle$ and every filter $F \subseteq A$, we have that $\llbracket \gamma \rrbracket \in F$ for all $\gamma \in \varGamma$ implies $\llbracket \varphi \rrbracket \in F$.

5.3 Soundness and Completeness

As mentioned earlier, in the case of public announcement logics the less straightforward part of the completeness proof consists in proving soundness. For this we find it more convenient to work with algebraic rather than relational models, and we will need to establish a few technical lemmas. We won’t include proofs because of space constraints, but these are analogous to the corresponding ones in [7, 10].

Lemma 3

Let $\mathbf {A}$ be an $\mathcal {MMV}_n$-algebra and $\mathbf {A} ^{a}$ the pseudo-quotient relative to some $a \in \mathbf {A}$. Then the map $\iota :\mathbf {A} ^a \rightarrow \mathbf {A}$ defined by $\iota [b] := a^n \wedge ^{\mathbf {A} } b$ for all $b \in \mathbf {A}$ satisfies the following:

• (i) $\iota (\lnot ^{\mathbf {A} ^a} [ b]) = a^n \wedge ^{\mathbf {A} } \lnot ^{\mathbf {A} } \iota [b]$.

• (ii) $\iota (\Box ^a[ b]) = a^n \wedge ^{\mathbf {A} } \Box ^{\mathbf {A} } (a^n \rightarrow ^{\mathbf {A} } \iota [b])$.

• (iii) $\iota ([b] \rightarrow ^{\mathbf {A} ^a} [c]) = a^n \wedge ^{\mathbf {A} } (\iota [b] \rightarrow ^{\mathbf {A} ^a} \iota [c])$.

Lemma 4

Let $(\mathbf {A} , v)$ be an algebraic model, $\alpha , \varphi , \psi \in Fm$ and $p \in Var$. Then,

• (i) $v( \langle \alpha \rangle \varphi ) = v( \alpha ^n ) \wedge ^{\mathbf {A} } (\iota \cdot v^{\alpha }) (\varphi )$

• (ii) $v ([\alpha ]\, 1) = 1^{\mathbf {A} }$

• (iii) $v ([\alpha ] \, p ) = v( \alpha ^n ) \rightarrow ^{\mathbf {A} } v(p)$

• (iv) $v( [\alpha ]\lnot \varphi ) = v( \alpha ^n ) \rightarrow ^{\mathbf {A} } \lnot ^{\mathbf {A} } v( [ \alpha ] \varphi )$

• (v) $v ([ \alpha ] (\varphi \rightarrow \psi ) ) = v( \langle \alpha \rangle \varphi ) \rightarrow ^{\mathbf {A} } v( \langle \alpha \rangle \psi )$

• (vi) $v( [ \alpha ] \Box \varphi ) = v( \alpha ^n ) \rightarrow ^{\mathbf {A} } \Box ^{\mathbf {A} } v( [ \alpha ] \varphi )$

• (vii) if $v( \varphi \rightarrow \psi ) = 1^{\mathbf {A} }$, then $v( [ \alpha ]\varphi \rightarrow [ \alpha ]\psi ) = 1^{\mathbf {A} }$.

Notice that the first item of Lemma 4 actually shows that the dynamic operators $[\alpha ]$ and $\langle \alpha \rangle$ are dual to one another, which justifies our choice of focusing on one only.

Theorem 1

The calculus $\vdash ^l_{\mathrm {\L }_n\text {PAL}}$ is sound and complete w.r.t. the consequence of Ł$_n$PAL.

6 Conclusions and Future Work

The present paper is part of an ongoing enterprise that aims, on the applied logic side, at extending dynamic epistemic logics outside the boundaries of classical reasoning and, on the theoretical side, at better understanding the mechanism itself of epistemic updates. Many issues are still open on both sides. It has been shown in [6, 7] that certain epistemic reasoning contexts can be alternatively, and perhaps more appropriately be handled using intuitionistic logic instead of the classical one. In the case of Ł$_n$PAL this is an almost trivial exercise, for we can simply recover classical logic by restricting semantic valuations to $\{0,1\}$-valued ones. More interesting will be the study of specific scenarios for which we can argue that classical logic would be unsuitable altogether; for this enterprise we hope to have at least provided a mathematically sound framework which can serve as a starting point.

The framework itself can and most likely needs to be improved in many directions. An obvious extension is to consider a more general product update construction such as those of [1, 6], which would allow us to consider more complex epistemic actions than public announcements. This might prove a relatively straightforward task, but also one that may lead to interesting applications. Another potentially promising line of research could result from dropping the assumption that propositions are announced with the highest possible truth degree, which entails, as mentioned earlier, that announcing $\alpha$ is equivalent to announcing $\alpha ^m$ for any m. This fact played a central rôle in this paper from a technical point of view; in a many-valued setting, however, a very natural thing to do would be to allow for graded announcements such as “$\alpha$ has at least true degree k / n”. This choice, which is supported by a strong semantic intuition, would give rise to the novel notion of graded epistemic action. A technically more challenging issue, even in the simplest public announcement setting, is whether and how it is possible to apply our methods to infinite-valued Łukasiewicz modal logic.