Dynamic Epistemic Logics of Introspection

Abstract

This work studies positive and negative introspection not as properties, but rather as actions that change the agent’s knowledge. The actions are introduced as model update operations, with matching modalities expressing their effects. Sound and complete axiom systems are provided, and some properties are explored.

1 Introduction

One of the reasons of the widespread use of epistemic logic (EL; [1]) is that it deals not only with an agent’s knowledge about propositional facts, but also with her knowledge about her own (and eventually other agents’) knowledge (high-order knowledge). This has been the starting point for the study of more complex multi-agent epistemic notions (e.g., common knowledge) that are crucial in multi-agent interaction, thus allowing EL to extend its range of applications, including not only philosophy (epistemology [2]), but also computer science (artificial intelligence [3]) and economics (game theory [4]).

In the study of agents with high-order knowledge, two of the most important concepts have been positive introspection (if the agent knows something, she knows that she knows it) and negative introspection (if the agent does not know something, she knows that she does not know it). One of the main advantages of the standard EL semantic structure, relational models, is that these two properties correspond, at the level of frames, to simple relational properties: to work with full positively introspection, it is enough to consider a transitive indistinguishability relation, and to deal with full negative introspection, it is enough to ask for such relation to be Euclidean. When these properties are not enforced, the agent might lack introspection, thus making her more ‘real’. But, as in real life, not being introspective should not imply one will never be.

Recent works have studied properties of an EL agent’s knowledge from a dynamic point of view, thinking about them in terms of the actions the agent can perform to achieve them. For example, closure under logical consequence can be seen not as a ‘static’ property, but rather as the eventual result of awareness raising and ‘syntactic’ inference steps within awareness relational models [5, 6], and also as the result of dynamics of evidence or deductive inference within neighbourhood models [7,8,9]. Following this idea, the present work studies introspection properties by defining epistemic actions that allow a non-introspective agent to reach them. These actions are represented in a dynamic epistemic logic (DEL; [10, 11]) style: as accessibility-changing model operations. There are several examples of such operations in the literature, as the actions for belief revision and/or preference change studied in [12,13,14,15] and the logics for reasoning about dynamic policies investigated in [16, 17]. There are also the more ‘abstract’ edge-deleting sabotage operation of [18], the edge-adding and swapping proposals in [19,20,21,22] and the general arrow update approach of [23].

The article is organised as follows. Section 2 introduces basic definitions about epistemic logic and propositional dynamic logic. Section 3 defines model operations to achieve positive introspection for general knowledge and also with respect to a formula. Section 4 focuses on similar operations for negative introspection. In all cases we study some properties of the operations, providing also sound and complete axiomatizations for their respective modalities. Finally, Sect. 5 draws conclusions.

2 Basic Definitions

This section recalls not only the basic definitions of basic epistemic logic, but also extensions that will be useful when providing axiom systems for modalities representing the introspection operations. Throughout this paper, let $\mathtt {P}$ be a countable set of atomic propositions.

Definition 2.1

(Relational Frame, Relational Model, Relational State). A relational frame is a tuple $F = \left\langle W, R \right\rangle$ with W a non-empty set of possible worlds and $R \subseteq (W \times W)$ a binary relation, the agent’s indistinguishability relation (which is not required to satisfy any property). A relational model is a tuple $M = \left\langle F, V \right\rangle$ with F a relational frame and $V:\mathtt {P}\rightarrow \wp ({W})$ an atomic valuation. A tuple (M, w) with M a relational model and w a world in it (the evaluation point) is called a relational state.

Next we introduce the basic epistemic language $\mathcal {L}_{\Diamond }$.

Definition 2.2

(Language $\mathcal {L}_{\Diamond }$ ). Formulas $\varphi , \psi$ of $\mathcal {L}_{\Diamond }$ are given by

with $p \in \mathtt {P}$. Other Boolean connectives and constants as well as the modality $\Box$ are defined as usual ($\mathop {\Box }{\varphi } := \lnot \mathop {\Diamond }{\lnot \varphi }$ for the latter), and formulas of the form $\mathop {\Box }{\varphi }$ are read as “the agent knows $\varphi$”. For the semantic interpretation, given a relational state (M, w) with $M = \left\langle W, R, V \right\rangle$, formulas in $\mathcal {L}_{\Diamond }$ are interpreted as usual, with the cases of atomic propositions and the ‘diamond’ modality being

A formula $\varphi$ is true at w in M when $(M, w) \Vdash \varphi$. A formula $\varphi$ is valid (notation: $\Vdash \varphi$) when it is true in every world w of every model M.

Theorem 2.1

(Axiom System for $\mathcal {L}_{\Diamond }$ ). As it is well-known (e.g., [24, 25]), axiom schemes and rules on the first block of Table 1 form a sound and strongly complete axiom system ($\mathsf {L}_{\Diamond }$) for formulas of $\mathcal {L}_{\Diamond }$ w.r.t. relational models.

Table 1. Axiom systems for $\mathcal {L}_{\Diamond }$ and some of its extensions.

The following sections study languages with modalities for actions of introspection. To introduce their corresponding axiom systems, some extensions of the basic epistemic language will be useful. First, a transitive closure modality.

Definition 2.3

(Language  ). The language adds to $\mathcal {L}_{\Diamond }$. Given a relational state (M, w) with $M = \left\langle W, R, V \right\rangle$ and $R^+$ the transitive closure of R,

The dual modality $\boxplus$ is defined in the usual way ().

Theorem 2.2

(Axiom System for  ). The axioms and rules on the first and second block of Table 1 form sound and weakly complete axiom system () for formulas of w.r.t. relational models [3].

Second, the propositional dynamic logic (PDL; [26]) framework with a converse modality, with operations for building more complex relations (cf. [27]).

Definition 2.4

(Language $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}}}$ ). Formulas $\varphi , \psi$ and program expressions $\alpha , \beta$ in $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}}}$ are given, respectively, by

with $p \in \mathtt {P}$. The fragment of $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}}}$ without $\textsf {?}$ is called $\mathcal {L}_{ PDL ^{\lhd }}$. Given (M, w) with $M=\left\langle W, R, V \right\rangle$, the semantics of the new modality is defined as

with the relation $R_{\alpha }$ defined inductively as

where , ${\text {Id}}^{M}_{\varphi } := \left\{ (u, u) \mid (M, u) \Vdash \varphi ) \right\}$ and $R^* := R^+ \cup {\text {Id}}^{M}_{\top }$.

Theorem 2.3

(Axiom System for $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}}}$ ). The axioms and rules on the third block of Table 1 form sound and weakly complete axiom system ($\mathsf {L}_{ PDL ^{\lhd ,?}}$) for formulas of $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}}}$ w.r.t. relational models [26, 28, 29]. $\mathsf {L}_{ PDL ^{\lhd }}$ denotes the axiom system for the fragment $\mathcal {L}_{ PDL ^{\lhd }}$, given by $\mathsf {L}_{ PDL ^{\lhd ,?}}$ minus axiom $\textsf {?}$.

3 Positive Introspection

3.1 General Positive Introspection

When looking for a model operation for representing an action of positive introspection, the first idea is simple: if transitivity makes the positive introspection axiom $\mathop {\Box }{\varphi } \rightarrow \mathop {\Box }{\mathop {\Box }{\varphi }}$ valid, then make the accessibility relation transitive.

Definition 3.1

(General Positive Introspection Operation). Take a relational model $M = \left\langle W, R, V \right\rangle$. The general positive introspection operation yields the model ${M}^{\varvec{+}} = \left\langle W, R^+, V \right\rangle$.

Definition 3.2

(Language $\mathcal {L}_{\Diamond , \varvec{+}}$ ). The language $\mathcal {L}_{\Diamond , \varvec{+}}$ extends $\mathcal {L}_{\Diamond }$ with $\mathop {\mathop {\langle {\varvec{+}}\rangle }}{}$. For its semantic interpretation, let (M, w) be a relational state. Then,

As the model operation is deterministic and its associated modality lacks a precondition, the dual modality $\mathop {\mathop {[{\varvec{+}}]}}{\varphi } := \lnot \mathop {\mathop {\langle {\varvec{+}}\rangle }}{\lnot \varphi }$ is equivalent to $\mathop {\mathop {\langle {\varvec{+}}\rangle }}{}$ (self-duality).

Some Properties.  The operation makes the accessibility relation transitive; then, after applying it, the agent has full positive introspection about any $\varphi$.

Proposition 3.1

Let $\varphi$ an $\mathcal {L}_{\Diamond , \varvec{+}}$-formula. Then $\Vdash \mathop {\mathop {[{\varvec{+}}]}}{(\mathop {\Box }{\varphi } \rightarrow \mathop {\Box }{\mathop {\Box }{\varphi }})}$.

However, the operation does not take the agent from a state in which she knows a given $\varphi$ without knowing she knows it, $\mathop {\Box }{\varphi } \wedge \lnot \mathop {\Box }{\mathop {\Box }{\varphi }}$, to a state in which she knows $\varphi$ and is positively introspective about it, $\mathop {\Box }{\varphi } \wedge \mathop {\Box }{\mathop {\Box }{\varphi }}$.

Fact 3.1

The formula $\mathop {\Box }{\varphi } \rightarrow \mathop {\mathop {[{\varvec{+}}]}}{(\mathop {\Box }{\varphi } \wedge \mathop {\Box }{\mathop {\Box }{\varphi }})}$ is not valid, not even for $\varphi$ propositional.

Proof

Take $\varphi$ as p. In the relational state below on the left (reflexivity assumed), $(M, w_1) \Vdash \mathop {\Box }{p} \wedge \lnot \mathop {\Box }{\mathop {\Box }{p}}$. Nevertheless, after the operation (relational state on the right), she does not know p anymore: $({M}^{\varvec{+}}, w_1) \Vdash \lnot \mathop {\Box }{p}$, i.e., $(M, w_1) \Vdash \mathop {\mathop {\langle {\varvec{+}}\rangle }}{\lnot \mathop {\Box }{p}}$. Thus, $(M, w_1) \Vdash \mathop {\Box }{p} \wedge \mathop {\mathop {\langle {\varvec{+}}\rangle }}{\lnot \mathop {\Box }{p}}$.

Making the accessibility relation transitive might increase the worlds reachable in one step. Thus, although the operation makes the agent’s knowledge positively introspective, it does not do it by increasing her knowledge; rather, it discards the knowledge that was non-introspective.

Axiom System.  When providing an axiom system for a modality representing a model operation, a useful DEL strategy is to provide reduction axioms: valid formulas and validity-preserving rules indicating how to translate a formula with occurrences of this model-changing modality (a formula in the ‘dynamic’ language) into a provably equivalent one without them (a formula in the ‘basic’ language). Then, while soundness follows from the validity and validity-preserving properties of the new axioms and rules, completeness follows from the completeness of the axiom system for the basic language.

Note how this strategy requires a basic language expressive enough to describe the changes the model operation induces. In this case, $\mathcal {L}_{\Diamond }$ is not enough to deal with the changes the general positive introspection operation brings about: it cannot describe what holds in worlds that can be reached by an arbitrary (finite non-zero) number of R-steps (i.e., a single $R^+$-step). Thus, in order to provide reduction axioms for $\mathop {\mathop {\langle {\varvec{+}}\rangle }}{}$, the basic language will be .

Table 2. Axioms and rule for the modality $\mathop {\langle \varvec{+}\rangle }$.

Theorem 3.2

(Axiom System for  ). The axioms and rules of Table 2, together with (first and second blocks in Table 1), form a sound and weakly complete axiom system for formulas of w.r.t. relational models.

3.2 Particular Positive Introspection

The operation of Definition 3.1 allows the agent to have positive introspection at the cost of losing knowledge. As such, it does not follow the intuition of what an actual positive introspection reasoning step should do. An operation closer to this intuition would take the agent from knowing $\chi$ without knowing she knows it, to knowing $\chi$ and knowing she knows it. But then the operation should be radically different. If at (M, w) the agent knows a given $\chi$ without having full positive introspection about it, then although every world R-reachable from w in one step satisfies $\chi$, there is at least one world R-reachable from w (in two or more steps) where $\chi$ fails. In order for the agent to have full positive introspection about $\chi$, such $\lnot \chi$-worlds should not be R-reachable anymore. In other words, the operation should not add edges, but rather remove them.

Definition 3.3

( U -disconnecting Operation). Let $M = \left\langle W, R, V \right\rangle$ be a relational model; take $U \subseteq W$. The U-disconnecting operation yields the model ${M}_{\varvec{+}{U}} = \left\langle W, R', V \right\rangle$, with $R' := R \setminus (U \times \overline{U})$ (for $\overline{U} := W \setminus U$). Thus, this operation removes edges from worlds on U to worlds not in U.

When the parameter U of this model operation is given by the truth-set of a formula $\chi$, then the operation can be understood as a particular positive $\chi$ -introspection operation: it removes edges from worlds satisfying $\chi$ to worlds not satisfying $\chi$. The modality for this operation will be introduced in two stages, the first one being the definition of an auxiliary modality.

Definition 3.4

(Language $\mathcal {L}_{\Diamond , \varvec{+}{'\chi }}$ ). The language $\mathcal {L}_{\Diamond , \varvec{+}{'\chi }}$ extends $\mathcal {L}_{\Diamond }$ with a modality $\mathop {\langle \varvec{+}{'\chi }\rangle }$ for each formula $\chi$. For the semantic interpretation, let (M, w) be a relational state; use $\llbracket {\chi } \rrbracket ^{M}$ to denote the set of worlds in M in which $\chi$ holds.

The operation is deterministic and its modality does not have a precondition, so the modality $\mathop {\mathop {[\varvec{+}{'}]}}{}$, defined as $\mathop {\mathop {[\varvec{+}{'\chi }]}}{\varphi } := \lnot \mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{\lnot \varphi }$, is equivalent to $\mathop {\mathop {\langle \varvec{+}{'}\rangle }}{}$.

This auxiliary modality allows the language to describe the effects of the positive $\chi$-introspection operation. Still, it differs from what one might expect in one crucial way: its semantic interpretation has no precondition, thus indicating that the epistemic action it represents, an introspective reasoning step, can take place in any situation (even in those in which the agent does not know $\chi$). This issue can be solved in a second stage by introducing another modality:

$$ \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\varphi } := \mathop {\Box }{\chi } \wedge \mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{\varphi }. $$

The reader familiar with DEL might notice here a departure from the standard approach: why the auxiliary ‘preconditionless’ modality $\mathop {\langle \varvec{+}{'\chi }\rangle }$ instead of defining $\mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{}$ directly with the appropriate precondition? The reason is that the former simplifies the formulation of reduction axioms.

Some Properties.  First, here it is a validity characterizing the knowledge of the agent after the operation.

Proposition 3.2

Let $\chi$ and $\varphi$ be formulas in $\mathcal {L}_{\Diamond , \varvec{+}{'\chi }}$. The agent can perform a particular positive introspection step for $\chi$ after which she will know $\varphi$ iff she knows both $\chi$ and that, after the ‘preconditionless’ operation, $\varphi$ will be the case. More precisely, $\Vdash \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box }{\varphi }} \;\leftrightarrow \;\mathop {\Box }{(\chi \wedge \mathop {\mathop {[\varvec{+}{'\chi }]}}{\varphi })}$.

Proof

Take any (M, w) with $M = \left\langle W, R, V \right\rangle$. From left to right, $(M, w) \Vdash \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box }{\varphi }}$ yields, by definition, $(M, w) \Vdash \mathop {\Box }{\chi }$ and $(M, w) \Vdash \mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{\mathop {\Box }{\varphi }}$. From the first, Rwu implies $(M, u) \Vdash \chi$; from the latter, $({M}_{\varvec{+}{\chi }}, w) \Vdash \mathop {\Box }{\varphi }$, i.e. $R'wu$ implies $({M}_{\varvec{+}{\chi }}, u) \Vdash \varphi$. Take now any $u \in W$ with Rwu: then $(M, u) \Vdash \chi$ and hence, from the definition of $R'$ in ${M}_{\varvec{+}{\chi }}$, $R'wu$, so $({M}_{\varvec{+}{\chi }}, u) \Vdash \varphi$ and then $(M, u) \Vdash \mathop {\mathop {[\varvec{+}{'\chi }]}}{\varphi }$. Thus, Rwu implies $(M, u) \Vdash \chi \wedge \mathop {\mathop {[\varvec{+}{'\chi }]}}{\varphi }$; hence, $(M, w) \Vdash \mathop {\Box }{(\chi \wedge \mathop {\mathop {[\varvec{+}{'\chi }]}}{\varphi })}$. From right to left, $(M, w) \Vdash \mathop {\Box }{(\chi \wedge \mathop {\mathop {[\varvec{+}{'\chi }]}}{\varphi })}$ implies, first, $(M, w) \Vdash \mathop {\Box }{\chi }$, and second, $(M, w) \Vdash \mathop {\Box }{\mathop {\mathop {[\varvec{+}{'\chi }]}}{\varphi }}$, with the latter stating that Rwu implies $(M, u) \Vdash \mathop {\mathop {[\varvec{+}{'\chi }]}}{\varphi }$. Take now any $u \in W$ with $R'wu$: since $R' \subseteq R$, then Rwu and hence $(M, u) \Vdash \mathop {\mathop {[\varvec{+}{'\chi }]}}{\varphi }$, i.e., $({M}_{\varvec{+}{\chi }}, u) \Vdash \varphi$. Thus, $({M}_{\varvec{+}{\chi }}, w) \Vdash \mathop {\Box }{\varphi }$ and so $(M, w) \Vdash \mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{\mathop {\Box }{\varphi }}$. But recall the first: $(M, w) \Vdash \mathop {\Box }{\chi }$. Hence, $(M, w) \Vdash \mathop {\Box }{\chi } \wedge \mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{\mathop {\Box }{\varphi }}$ and thus, by definition, $(M, w) \Vdash \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box }{\varphi }}$.

In order to show how this operation behaves as expected, consider the instance of the previous validity with $\varphi$ replaced by $\mathop {\Box }{\chi }$:

$$ \Vdash \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box }{\mathop {\Box }{\chi }}} \leftrightarrow \mathop {\Box }{(\chi \wedge \mathop {\mathop {[\varvec{+}{'\chi }]}}{\mathop {\Box }{\chi }})}. $$

The formula states what is needed for the agent to have a one-level positive introspection about $\chi$ ($\mathop {\Box }{\mathop {\Box }{\chi }}$) after the operation. One might expect for the second conjunct inside the scope of $\Box$ in the right-side, $\mathop {\mathop {[\varvec{+}{'\chi }]}}{\mathop {\Box }{\chi }}$, to collapse to $\top$, so the necessary and sufficient condition for the agent to reach one-level positive $\chi$-introspection is for her to know $\chi$. This is not the case.

Fact 3.3

The formula $\mathop {\Box }{\chi } \rightarrow \mathop {\mathop {[\varvec{+}{'\chi }]}}{\mathop {\Box }{\chi }}$ is not valid, and so neither is $\mathop {\mathop {[\varvec{+}{'\chi }]}}{\mathop {\Box }{\chi }}$.

Proof

Take $\chi := p \wedge \mathop {\Diamond }{\mathop {\Diamond }{\lnot p}}$ and the relational state below on the left (reflexivity assumed); $\chi$ holds at $w_{1}$ and $w_{2}$ (so $(M, w_{1}) \Vdash \mathop {\Box }{\chi }$), but fails at $w_3$. Thus, the operation yields the relational state on the right, with $\chi$ false at $w_{2}$; then, $({M}_{\varvec{+}{\chi }}, w_{1}) \Vdash \lnot \mathop {\Box }{\chi }$ and hence $(M, w_{1}) \Vdash \mathop {\Box }{\chi } \wedge \mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{\lnot \mathop {\Box }{\chi }}$: the agent knows $\chi$, but she will not know it anymore after a positive $\chi$-introspection action.

Note how $(M, w_{1}) \Vdash \lnot \mathop {\Box }{\mathop {\Box }{\chi }}$, so the introspection action is not redundant. Even more, $(M, w_{1}) \Vdash \mathop {\Box }{\chi }$, so the state satisfies $\mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\lnot \mathop {\Box }{\chi }}$ and hence $\lnot \mathop {\mathop {[\varvec{+}{\chi }]}}{\mathop {\Box }{\chi }}$.

Fact 3.3 is just one more instance of Moorean phenomena, commonly known as formulas which, after being truthfully announced, become false [30].¹ Here it appears as formulas that are known but, after a particular positive introspection action, are not known anymore. This is because, though the operation does not change the atomic valuation, it changes the accessibility relation, thus affecting the agent’s knowledge. Nevertheless, the operation behaves as expected when the truth-value of the involved formula $\chi$ is preserved by the operation.

Proposition 3.3

If $\Vdash \chi \rightarrow \mathop {\mathop {[\varvec{+}{'\chi }]}}{\chi }$, then after the operation the agent will have positive introspection about $\chi$, $\Vdash \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box }{\mathop {\Box }{\chi }}} \;\leftrightarrow \;\mathop {\Box }{\chi }$.

Proof

The ‘$\rightarrow$’ direction follows by replacing $\varphi$ with $\mathop {\Box }{\chi }$ in the validity of Proposition 3.2. For ‘$\leftarrow$’, take any (M, w) with $M = \left\langle W, R, V \right\rangle$, and suppose $(M, w) \Vdash \mathop {\Box }{\chi }$; then Rwu implies $(M, u) \Vdash \chi$. Now take any $u \in W$ with $R'wu$ and any $v \in W$ with $R'uv$. Since $R' \subseteq R$, then Rwu and hence $(M, u) \Vdash \chi$. But $R'uv$ so the definition of $R'$ yields $(M, v) \Vdash \chi$. Then, by the assumption, $(M, v) \Vdash \mathop {\mathop {[\varvec{+}{'\chi }]}}{\chi }$, that is, $({M}_{\varvec{+}{\chi }}, v) \Vdash \chi$. Since v is an arbitrary $R'$-successor of u, $({M}_{\varvec{+}{\chi }}, u) \Vdash \mathop {\Box }{\chi }$; since u is an arbitrary $R'$-successor of w, $({M}_{\varvec{+}{\chi }}, w) \Vdash \mathop {\Box }{\mathop {\Box }{\chi }}$. Hence, $(M, w) \Vdash \mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{\mathop {\Box }{\mathop {\Box }{\chi }}}$ and, as the precondition holds, $(M, w) \Vdash \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box }{\mathop {\Box }{\chi }}}$.

The right-to-left direction of this validity, $\mathop {\Box }{\chi } \rightarrow \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box }{\mathop {\Box }{\chi }}}$, is a dynamic version of the positive introspection axiom $\mathop {\Box }{\chi } \rightarrow \mathop {\Box }{\mathop {\Box }{\chi }}$: the agent might lack positive introspection for $\chi$, but she can achieve it. Even more: under the same requirement for $\chi$, after the action the agent will have full positive $\chi$-introspection.

Proposition 3.4

If $\Vdash \chi \rightarrow \mathop {\mathop {[\varvec{+}{'\chi }]}}{\chi }$, then after the operation the agent will have full positive introspection about $\chi$, that is, $\Vdash \mathop {\Box }{\chi } \rightarrow \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box ^{n}}{\mathop {\Box }{\chi }}}$ for any $n \ge 0$, with $\mathop {\Box ^{0}}{\varphi } := \varphi$ and $\mathop {\Box ^{k+1}}{\varphi } := \mathop {\Box ^{k}}{\mathop {\Box }{\varphi }}$.

Proof

Take a relational state (M, w) with $M = \left\langle W, R, V \right\rangle$, and suppose $(M, w) \Vdash \mathop {\Box }{\chi }$; then Rwu implies $(M, u) \Vdash \chi$. The first step is to show, by induction on $n \ge 0$, how $(R')^{n+1}wu$ implies $(M, u) \Vdash \chi$. The base case is immediate: $(R')^{1}wu$ is $R'wu$, and since $R' \subseteq R$, then Rwu and thus $(M, u) \Vdash \chi$. For the inductive case, suppose $(R')^{n+2}wu$. Then there is $v \in W$ such that $(R')^{n+1}wv$ and $R'vu$, and hence $(M, v) \Vdash \chi$ (from the first and inductive hypothesis) and Rvu (from the second and $R' \subseteq R$). But $R'vu$ so, from the definition of $R'$, it follows that $(M, u) \Vdash \chi$.

For $(M, w) \Vdash \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box ^{n}}{\mathop {\Box }{\chi }}}$, take $n \ge 0$ and any $u \in W$ with $(R')^{n+1}wu$. Then $(M, u) \Vdash \chi$ and hence, by the assumption, $(M, u) \Vdash \mathop {\mathop {[\varvec{+}{'\chi }]}}{\chi }$, i.e., $({M}_{\varvec{+}{\chi }}, u) \Vdash \chi$. Thus, $(R')^{n+1}wu$ implies $({M}_{\varvec{+}{\chi }}, u) \Vdash \chi$, that is, $({M}_{\varvec{+}{\chi }}, w) \Vdash \mathop {\Box ^{n}}{\mathop {\Box }{\chi }}$ so $(M, w) \Vdash \mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{\mathop {\Box ^{n}}{\mathop {\Box }{\chi }}}$. But $\mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{}$’s precondition holds; thus, $(M, w) \Vdash \mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\mathop {\Box ^{n}}{\mathop {\Box }{\chi }}}$.

Thus, if the operation does not affect $\chi$’s truth-value, the action’s precondition (to know $\chi$) guarantees that the agent will have (knowledge and) full positive introspection about $\chi$. This operation is closer to what comes to mind when one thinks about ‘real life’: the agent knows $\chi$ without noticing it, and thus she only needs to make a further ‘introspective’ effort to realise it. The operation does not yield positive introspection for all formulas, but it does the work for the particular $\chi$ (modulo the extra assumption).

Particular Introspection vs Public Announcement.  The reader familiar with public announcement logic (PAL; [31]) will have noted the similarities between the operation of Definition 3.3 and the public announcement operation: in the new model, former $\chi$-worlds can only reach former $\chi$-worlds. Thus, when the evaluation point is a $\chi$-world, the resulting models are bisimilar. There is, however, an important difference in the precondition of their associated modalities: the one for a $\chi$-announcement requires $\chi$, but the one for a $\chi$-introspection requires $\mathop {\Box }{\chi }$. This is why, while the public announcement modality has ‘straightforward’ reduction axioms (there is a match between the precondition and the requirement for a world to be reachable after the operation), the introspection modality requires an auxiliary ‘preconditionless’ version.

Despite the technical similarities, the two operations represent actions of a very different nature: a public announcement is about external communication, but introspection is about self-reflection. It is then remarkable how, in this setting, their representations are so similar. It could be argued that the presented introspection action is too drastic: it removes any ‘eventual’ (i.e., possibility of having a possibility) uncertainty the agent might have about the given formula. This is indeed the case, but it is the interpretation of edges in relational models what gives no other choice in order to represent this specific epistemic action.

Axiom System.  For an axiom system for the modality $\mathop {\langle \varvec{+}{\chi }\rangle }$, the first step is to provide reduction axioms for its ‘preconditionless’ counterpart.

Theorem 3.4

(Axiom System for $\mathcal {L}_{\Diamond , \varvec{+}{'\chi }}$ ). The axioms and rules of Table 3, together with the axiom system $\mathsf {L}_{\Diamond }$ (see Table 1), form a sound and strongly complete axiom system for formulas of $\mathcal {L}_{\Diamond , \varvec{+}{'\chi }}$ w.r.t. relational models.

Table 3. Axioms and rule for the modality $\varvec{+}{'\chi }$.

The previous theorem provides a sound and strongly complete axiom system for $\mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{}$. As $\mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{}$ is just an abbreviation, it requires no axioms; still, its definition makes $\mathop {\mathop {\langle \varvec{+}{\chi }\rangle }}{\varphi } \;\leftrightarrow \;(\mathop {\Box }{\chi } \wedge \mathop {\mathop {\langle \varvec{+}{'\chi }\rangle }}{\varphi })$ valid.

4 Negative Introspection

4.1 General Negative Introspection

Analogous to its positive introspection counterpart, the operation for achieving full negative introspection is simply an Euclidean closure operation.

Definition 4.1

(General Negative Introspection Operation). Take a relational model $M = \left\langle W, R, V \right\rangle$. The general negative introspection operation yields the model ${M}^{\varvec{-}} = \langle W, R^E, V \rangle$ in which $R^E$ is the Euclidean closure of R, that is,

Definition 4.2

(Language $\mathcal {L}_{\Diamond , \varvec{-}}$ ). The language $\mathcal {L}_{\Diamond , \varvec{-}}$ extends $\mathcal {L}_{\Diamond }$ with $\mathop {\mathop {\langle {\varvec{-}}\rangle }}{}$ ($\mathop {\mathop {[{\varvec{-}}]}}{}$ defined as usual). For its semantic interpretation, let (M, w) be a relational state.

Clearly, $R^E$ can be equivalently defined in PDL plus the converse operator. This suggests that $\mathcal {L}_{ PDL ^{\lhd }}$ from Definition 2.4 will be useful to provide reduction axioms for this operation. But first, here are some of its properties.

Some Properties.  Since $R^E$ is indeed R’s Euclidean closure, after the operation the agent has negative introspection.

Lemma 4.1

For any $R \subseteq (W \times W)$, the relation is R’s Euclidean closure, i.e., the smallest Euclidean relation containing R.²

Proposition 4.1

Let $\varphi$ an $\mathcal {L}_{\Diamond , \varvec{-}}$-formula. Then, $\Vdash \mathop {\mathop {[{\varvec{-}}]}}{(\lnot \mathop {\Box }{\varphi } \rightarrow \mathop {\Box }{\lnot \mathop {\Box }{\varphi }})}$.

Even more. Different from the positive introspection case, in the propositional case the operation makes the agent’s knowledge negatively introspective in the sense of taking her from $\lnot \mathop {\Box }{\varphi } \wedge \lnot \mathop {\Box }{\lnot \mathop {\Box }{\varphi }}$ to $\lnot \mathop {\Box }{\varphi } \wedge \mathop {\Box }{\lnot \mathop {\Box }{\varphi }}$.

Proposition 4.2

If $\varphi$ is propositional, then $\Vdash \lnot \mathop {\Box }{\varphi } \rightarrow \mathop {\mathop {[{\varvec{-}}]}}{(\lnot \mathop {\Box }{\varphi } \wedge \mathop {\Box }{\lnot \mathop {\Box }{\varphi }})}$.

Proof

Take a relational state (M, w) with $M = \left\langle W, R, V \right\rangle$, and suppose $(M, w) \Vdash \lnot \mathop {\Box }{\varphi }$; then there is $u \in W$ such that Rwu and $(M, u) \Vdash \lnot \varphi$, so $R^Ewu$ (definition) and $({M}^{\varvec{-}}, u) \Vdash \lnot \varphi$ ($\varphi$ is propositional). Thus, first, $({M}^{\varvec{-}}, w) \Vdash \mathop {\Diamond }{\lnot \varphi }$, i.e., $({M}^{\varvec{-}}, w) \Vdash \lnot \mathop {\Box }{\varphi }$. Second, for every $u' \in W$, $R^Ewu'$ implies $R^Eu'u$ ($R^E$ is Euclidean), and hence $({M}^{\varvec{-}}, u') \Vdash \mathop {\Diamond }{\lnot \varphi }$ so $({M}^{\varvec{-}}, w) \Vdash \mathop {\Box }{\mathop {\Diamond }{\lnot \varphi }}$, i.e., $({M}^{\varvec{-}}, w) \Vdash \mathop {\Box }{\lnot \mathop {\Box }{\varphi }}$. Thus, $(M, w) \Vdash \mathop {\mathop {[{\varvec{-}}]}}{(\lnot \mathop {\Box }{\varphi } \wedge \mathop {\Box }{\lnot \mathop {\Box }{\varphi }})}$.

This validity, a dynamic version of the negative introspection axiom $\lnot \mathop {\Box }{\varphi } \rightarrow \mathop {\Box }{\lnot \mathop {\Box }{\varphi }}$, shows how the operation behaves properly in the propositional case. Still, as expected, it also has Moorean behaviour for arbitrary formulas.

Fact 4.1

The formula $\lnot \mathop {\Box }{\varphi } \rightarrow \mathop {\mathop {[{\varvec{-}}]}}{\mathop {\Box }{\lnot \mathop {\Box }{\varphi }}}$ is not valid.

Proof

Consider $\varphi := \lnot \mathop {\Box }{p}$ and the relational state $(M, w_1)$ below on the left (reflexivity assumed). Note how $(M, w_1) \Vdash \mathop {\Diamond }{\mathop {\Box }{p}}$, i.e., $(M, w_1) \Vdash \lnot \mathop {\Box }{(\lnot \mathop {\Box }{p})}$. The operation produces the relational state on the right, where $({M}^{\varvec{-}}, w_{1}) \Vdash \mathop {\Diamond }{\mathop {\Box }{\mathop {\Diamond }{\lnot p}}}$, i.e., $({M}^{\varvec{-}}, w_{1}) \Vdash \lnot \mathop {\Box }{\lnot }{\mathop {\Box }{(\lnot \mathop {\Box }{p})}}$ so $(M, w_{1}) \Vdash \mathop {\mathop {\langle {\varvec{-}}\rangle }}{\lnot \mathop {\Box }{\lnot }{\mathop {\Box }{(\lnot \mathop {\Box }{p})}}}$.

Axiom System.  $\mathcal {L}_{\Diamond }$ is not expressive enough to describe the effects of this operation, but the clearly more expressive $\mathcal {L}_{ PDL ^{\lhd }}$ is. The Boolean cases are as those in Tables 2 and 3; the modal case is different: in $\mathop {\langle \alpha \rangle }\varphi$, the expression $\alpha$ is an arbitrary program expression, and thus an appropriate translation in each case must be presented. The program transformer defined below, a simplification of that of [32] for providing reduction axioms for PDL-expressions after action-model operations, captures this: it takes a program $\alpha$ describing a path in the new model ${M}^{\varvec{-}}$, returning its ‘matching’ path ${\text {T}}(\alpha )$ in M (Proposition 4.3).

Definition 4.3

(Program Transformer). A program transformer ${\text {T}}$ is a function from program expressions to program expressions defined inductively as

Proposition 4.3

Let $M = \left\langle W, R, V \right\rangle$ be any relational model, and recall that ${M}^{\varvec{-}} = \langle W, R^E, V \rangle$. Then, for every program expression $\alpha$, $R^E_{\alpha } = R_{{\text {T}}(\alpha )}$.

Proof

The proof is by structural induction on $\alpha$. For $R^E_{\rhd }$ ($R^E_{\lhd }$ is similar),

For the inductive cases (inductive hypothesis: $R^E_{\alpha } = R_{{\text {T}}(\alpha )}$, $R^E_{\beta } = R_{{\text {T}}(\beta )}$),

Theorem 4.2

(Axiom System for $\mathcal {L}_{ PDL ^{\lhd }, \varvec{-}}$ ). The axioms and rules of Table 4, together with the axiom system $\mathsf {L}_{ PDL ^{\lhd }}$ (see Table 1), form a sound and weakly complete axiom system for formulas of $\mathcal {L}_{ PDL ^{\lhd }, \varvec{-}}$ w.r.t. relational models.

Table 4. Axioms and rule for the modality $\mathop {\langle \varvec{-}\rangle }$.

4.2 Particular Negative Introspection

Different from the positive introspection counterpart, the operation of Definition 4.1 already behaves as expected: it preserves the agent’s (propositional) lack of knowledge while giving her negative introspection (Proposition 4.2). Still, for uniformity, this section explores a negative introspection action over a given $\chi$.

A model operation for achieving full negative introspection about $\chi$ should then make sure that all worlds R-reachable from the evaluation point (in zero or more steps, so the original lack of knowledge is preserved and full introspection is reached) can see a $\lnot \chi$-world. Assuming that initially the agent does not know $\chi$, this property can be achieved by using a particular instance of the Euclidean closure operation of Definition 4.1 in which the new edges point only to $\lnot \chi$-worlds.

Definition 4.4

( U -connecting Operation). Let $M = \left\langle W, R, V \right\rangle$ be a relational model; let $U \subseteq W$. The U-connecting operation gives the model ${M}_{\varvec{-}{U}} = \langle W, R', V \rangle$, with its indistinguishability relation $R'$ given (with ${\text {Id}}^{M}_{U} := \left\{ (u, u) \mid u \in U \right\}$) by

A modality for a particular full negative introspection can be defined by instantiating U with the set of worlds satisfying $\lnot \chi$ in the original model. Here is a ‘preconditionless’ version.

Definition 4.5

(Language $\mathcal {L}_{\Diamond , \varvec{-}{'\chi }}$ ). The language $\mathcal {L}_{\Diamond , \varvec{-}{'\chi }}$ extends $\mathcal {L}_{\Diamond }$ with a modality $\mathop {\langle \varvec{-}{'\chi }\rangle }$ for each formula $\chi$. For the semantic interpretation,

A modality with an appropriate precondition is defined in the obvious way:

$$ \mathop {\mathop {\langle \varvec{-}{\chi }\rangle }}{\varphi } := \lnot \mathop {\Box }{\chi } \wedge \mathop {\mathop {\langle \varvec{-}{'\chi }\rangle }}{\varphi }. $$

Thus, the agent can perform an act of particular negative $\chi$-introspection after which $\varphi$ is the case, $\mathop {\mathop {\langle \varvec{-}{\chi }\rangle }}{\varphi }$, iff she does not know $\chi$, $\lnot \mathop {\Box }{\chi }$, and after the particular negative $\chi$-introspection operation, $\varphi$ is the case, $\mathop {\mathop {\langle \varvec{-}{'\chi }\rangle }}{\varphi }$.

Some Properties.  As expected, the analogous of Proposition  3.4 holds.

Proposition 4.4

If $\Vdash \chi \rightarrow \mathop {\mathop {[\varvec{-}{'\chi }]}}{\chi }$, then after the operation the agent will have full negative introspection about $\chi$, $\Vdash \lnot \mathop {\Box }{\chi } \rightarrow \mathop {\mathop {\langle \varvec{-}{\chi }\rangle }}{\mathop {\Box ^{n}}{\lnot \mathop {\Box }{\chi }}}$ for any $n \ge 0$.

Proof

Take a relational state (M, w) with $M = \left\langle W, R, V \right\rangle$, and suppose $(M, w) \Vdash \lnot \mathop {\Box }{\chi }$; then there is $v \in W$ such that Rwv and $(M, v) \Vdash \lnot \chi$, with the latter implying ${\text {Id}}^{M}_{\lnot \chi }vv$ (by definition) and $({M}_{\varvec{-}{\chi }}, v) \Vdash \lnot \chi$ (by the assumption). The first step is to show (by induction on $n \ge 0$) how, in ${M}_{\varvec{-}{\chi }}$, any world that can be reached from w in zero or more steps can also reach v, that is, how $(R')^{n}wu$ implies $R'uv$. The base case ($n=0$, i.e., $u=w$) is immediate, as the supposition states Rwv, and thus $R'wv$. For the inductive case, suppose $(R')^{n+2}wu$. Then there is $u' \in W$ such that $(R')^{n+1}wu'$ and $R'u'u$, and hence (inductive hypothesis) $R'u'v$ and $R'u'u$. It is not hard to see that, in each of the four cases the definition of $R'$ yields, $R'uv$.

Now, in order to prove $(M, w) \Vdash \mathop {\mathop {\langle \varvec{-}{\chi }\rangle }}{\mathop {\Box ^{n}}{\lnot \mathop {\Box }{\chi }}}$, take any $n \ge 0$ and any $u \in W$ such that $(R')^{n}wu$. Then $R'uv$ and, from $({M}_{\varvec{-}{\chi }}, v) \Vdash \lnot \chi$, it follows that $({M}_{\varvec{-}{\chi }}, u) \Vdash \mathop {\Diamond }{\lnot \chi }$, that is, $({M}_{\varvec{-}{\chi }}, w) \Vdash \mathop {\Box ^{n}}{\lnot \mathop {\Box }{\chi }}$ so $(M, w) \Vdash \mathop {\mathop {\langle \varvec{-}{'\chi }\rangle }}{\mathop {\Box ^{n}}{\lnot \mathop {\Box }{\chi }}}$. But $\mathop {\mathop {\langle \varvec{-}{\chi }\rangle }}{}$’s precondition holds; thus, $(M, w) \Vdash \mathop {\mathop {\langle \varvec{-}{\chi }\rangle }}{\mathop {\Box ^{n}}{\lnot \mathop {\Box }{\chi }}}$, as required.

Note how both negative introspection operations add edges. This differs from the positive introspection case: the general operation adds edges, but the particular one needs to remove them.

Axiom System.  The basic language will be now $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}}}$ (Definition 2.4), as the ‘test’ operator $\textsf {?}$ is required. Thus, $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}, \varvec{-}{'\chi }}}$ extends $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}}}$ with the ‘dynamic’ negative $\chi$-introspection modality; for reduction axioms, the program transformer of Definition 4.3 is redefined in the following way.

Definition 4.6

(Program Transformer). A $\chi$ -program transformer ${\text {T}}_\chi$ is a function from program expressions to program expressions defined as follows

The remaining cases (for $\varvec{\cup }$, $\mathbin {\varvec{;}}$ and $^*$) are as in Definition  4.3.

Proposition 4.5

Let $M = \left\langle W, R, V \right\rangle$ be any relational model, and recall that ${M}_{\varvec{-}{\chi }} = \langle W, R', V \rangle$. Then, for every program expression $\alpha$, $R'_{\alpha } = R_{{\text {T}}_{\chi }(\alpha )}$.

Proof

As in Proposition 4.3, the proof is by structural induction on $\alpha$. The common cases are similar; for the ‘test’,

Theorem 4.3

(Axiom System for $\mathcal {L}_{ PDL ^{\lhd }, \varvec{-}}$ ). The axioms and rules of Table 5, together with the axiom system $\mathsf {L}_{ PDL ^{\lhd ,?}}$ (see Table 1) form a sound and weakly complete axiom system for formulas of $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}, \varvec{-}{'\chi }}}$ w.r.t. relational models.

Table 5. Axioms and rule for the modality $\mathop {\langle \varvec{-}{'\chi }\rangle }$.

With the language extended and the axiom system introduced, it is possible to provide further validities describing the behaviour of the operation. First, here is how the operation affects the agent’s knowledge (now described by $\mathop {[\rhd ]}$).

Proposition 4.6

Suppose $\chi$ and $\varphi$ are both formulas in $\mathcal {L}_{ PDL ^{\lhd , \textsf {?}, \varvec{-}{'\chi }}}$; then, $\Vdash \mathop {\mathop {\langle \varvec{-}{\chi }\rangle }}{\mathop {[\rhd ]}{\varphi }} \leftrightarrow (\lnot \mathop {[\rhd ]}\chi \wedge \mathop {[{\text {T}}_\chi (\rhd )]}\mathop {\mathop {[\varvec{-}{'\chi }]}}{\varphi })$.

From this and the axiom system, one can obtain a validity characterising the requirements for the agent to have negative introspection about a given $\chi$ after the operation: $\Vdash \mathop {\mathop {\langle \varvec{-}{\chi }\rangle }}{\mathop {[\rhd ]}{\lnot \mathop {[\rhd ]}\chi }} \;\leftrightarrow \;(\lnot \mathop {[\rhd ]}\chi \wedge \mathop {[{\text {T}}_\chi (\rhd )]}\mathop {\mathop {[\varvec{-}{'\chi }]}}{\lnot \mathop {[\rhd ]}\chi })$.

5 Conclusion and Further Work

This paper studies positive and negative introspection as epistemic actions that modify the agent’s knowledge. In both cases two possibilities are considered: a general operation, and a particular one working relative to a given formula. In all cases, the basic epistemic language is extended with modalities representing the effects of the model operations, presenting their sound and complete axiom systems, and exploring some properties of the new languages.

In the case of positive introspection, the general operation follows a straightforward idea: make the accessibility relation transitive. Yet, this approach boils down to assume that introspection fails not because of what the agent knows about her knowledge, but rather because of what she knows; thus, as a result, non-introspective knowledge is lost, and only the introspective one is preserved. The particular operation has the opposite perspective: to get positive introspection about a given $\chi$, it eliminates edges from $\chi$-worlds to $\lnot \chi$-worlds, thus forcing positive introspection on $\chi$ while keeping the rest of her knowledge ‘as before’. For the negative introspection case, the general operation makes the accessibility relation Euclidean, and thus reaches negative introspection by ensuring the agent knows what she does not know. The particular operation follows the same idea while adding only edges pointing to $\lnot \chi$-worlds. Both cases about edge-addition; thus, they have a similar behaviour.

For future work, one direction is to explore operations that raise the agent’s introspection in just one level (e.g., from $\mathop {\Box }{p} \wedge \lnot \mathop {\Box }{\mathop {\Box }{p}}$ to $\mathop {\Box }{p} \wedge \mathop {\Box }{\mathop {\Box }{p}} \wedge \lnot \mathop {\Box }{\mathop {\Box }{\mathop {\Box }{p}}}$). A more interesting project is to investigate similar operations in a multi-agent setting (e.g., public, private versions of these operations), focusing also on operations for reaching common knowledge.