How to Agree without Understanding Each Other: Public Announcement Logic with Boolean Definitions

TL;DR

This paper extends Public Announcement Logic to include agents' knowledge about both truth and meaning of propositions, allowing for nuanced understanding of agreement and understanding in multi-agent systems.

Contribution

It introduces a conservative extension of PAL with Boolean Definitions, providing a complete axiomatization and exploring complex knowledge scenarios.

Findings

Agents can understand without knowing truth values.

Multiple agents can agree on facts without sharing meanings.

The logic captures nuanced epistemic states.

Abstract

In standard epistemic logic, knowing that p is the same as knowing that p is true, but it does not say anything about understanding p or knowing its meaning. In this paper, we present a conservative extension of Public Announcement Logic (PAL) in which agents have knowledge or belief about both the truth values and the meanings of propositions. We give a complete axiomatization of PAL with Boolean Definitions and discuss various examples. An agent may understand a proposition without knowing its truth value or the other way round. Moreover, multiple agents can agree on something without agreeing on its meaning and vice versa.

Equations

$$P::=p\mid \neg P\mid (P\wedge P)$$

$$\phi ::=P\mid P\equiv P\mid \neg \phi \mid (\phi \wedge \phi )\mid {\square }_{\_}i\phi \mid [\phi ]\phi$$

$$\begin{array}[]{rcl}\textsf{def}_{\_}w(p)&:=&\textsf{DEF}_{\_}w(p)\\ \textsf{def}_{\_}w(\lnot P)&:=&\lnot\textsf{def}_{\_}w(P)\\ \textsf{def}_{\_}w((P_{\_}1\land P_{\_}2))&:=&(\textsf{def}_{\_}w(P_{\_}1)\land\textsf{def}_{\_}w(P_{\_}2))\\ \end{array}$$

$$\begin{array}[]{lcl}\mathcal{M},w\vDash p&\iff&V_{\_}w(p)=1\\ \mathcal{M},w\vDash P_{\_}1\equiv P_{\_}2&\iff&\textsf{def}_{\_}w(P_{\_}1)=\textsf{def}_{\_}w(P_{\_}2)\\ \mathcal{M},w\vDash\lnot\varphi&\iff&\text{not }\mathcal{M},w\vDash\varphi\\ \mathcal{M},w\vDash(\varphi\land\psi)&\iff&\mathcal{M},w\vDash\varphi\text{ and }\mathcal{M},w\vDash\psi\\ \mathcal{M},w\vDash\Box_{\_}i\varphi&\iff&\text{for all }v:wR_{\_}iv\text{ implies }\mathcal{M},v\vDash\varphi\\ \mathcal{M},w\vDash[\varphi]\psi&\iff&\mathcal{M},w\vDash\varphi\text{ implies }\mathcal{M}^{\varphi},w\vDash\psi\\ \end{array}$$

$${\square }_{\_}a(p\equiv (q\wedge r))\wedge {\square }_{\_}b(p\equiv (q\wedge r))$$

$${\square }_{\_}b(p\equiv (\neg q_{\_}1\wedge r))\wedge \neg {\square }_{\_}a(p\equiv (\neg q_{\_}1\wedge r))$$

$${\square }_{\_}a(p\equiv (q\wedge \neg r_{\_}1))\wedge \neg {\square }_{\_}b(p\equiv (q\wedge \neg r_{\_}1))$$

$$\begin{array}[]{ll}p\equiv q\land r\\ q\equiv p\land r\\ s\equiv p\\ \hline\cr s\equiv q\land r\\ s\equiv(p\land r)\land r\\ s\equiv((q\land r)\land r)\land r\\ \vdots\\ \end{array}$$

$$\begin{array}[]{lcl}l(p)&:=&1\\ l(\neg P)&:=&l(P)+1\\ l((P\land Q))&:=&l(P)+l(Q)+3\end{array}$$

$$\begin{array}[]{lcl}v(p)&:=&\{p\}\\ v(\neg P)&:=&v(P)\\ v((P\land Q))&:=&v(P)\cup v(Q)\end{array}$$

$${[P]}_{\_}\Gamma =\{Q\in {\mathcal{L}}_{\_}B(\mathsf{Prop})\mid (P\equiv Q)\in \Gamma \}$$

$$\begin{array}[]{lcll}\mathsf{merge}(p,q)&:=&\text{if }p<q\text{ then }p\text{ else }q\\ \mathsf{merge}(p,Q)\ \text{ when }Q\not=q&:=&Q\\ \mathsf{merge}(P,q)\ \text{ when }P\not=p&:=&P\\ \mathsf{merge}((P\land Q),(R\land S))&:=&(\mathsf{merge}(P,R)\land\mathsf{merge}(Q,S))\\ \mathsf{merge}(\lnot P,\lnot R)&:=&\lnot\mathsf{merge}(P,R)\\[5.0pt] \mathsf{merge}(\lnot P,(Q\land R))&:=&\text{undefined}\\ \mathsf{merge}((Q\land R),\lnot P)&:=&\text{undefined}\\ \end{array}$$

$$Q_{\_}0\stackrel{\overline{k:p\mapsto R}}{\to }{Q}_{\_}1\stackrel{\overline{m:q\mapsto T}}{\to }{Q}_{\_}2\cdots$$

$${\text{def}}_{\_}\Gamma (\neg Q)\stackrel{\text{Def. refdef:canonicalm}}{=}\neg {\text{def}}_{\_}\Gamma (Q)\stackrel{\text{IH}}{=}\neg \mathsf{pick}({[Q]}_{\_}\Gamma )\stackrel{\ast }{=}\mathsf{pick}({[\neg Q]}_{\_}\Gamma )$$

$${\min }_{\_}<\{P\in {[\neg Q]}_{\_}\Gamma \mid \forall R\in {[\neg Q]}_{\_}\Gamma :l(P)\ge l(R)\}$$

$${\min }_{\_}<\{\neg P\mid P\in {[Q]}_{\_}\Gamma \text{ and }\forall R\in {[Q]}_{\_}\Gamma :l(\neg P)\ge l(\neg R)\}.$$

$$\neg {\min }_{\_}<\{P\in {[Q]}_{\_}\Gamma \mid \forall R\in {[Q]}_{\_}\Gamma :l(P)\ge l(R)\}$$

$$P\equiv Q\in \Gamma ⟺\mathcal{M},\Gamma \models P\equiv Q$$

$${[P]}_{\_}\Gamma ={[Q]}_{\_}\Gamma ⟺{\text{def}}_{\_}\Gamma (P)={\text{def}}_{\_}\Gamma (Q).$$

$$\mathcal{M},w\models {\text{Kd}}_{\_}i(P)⟺\forall w^{\prime }:w{R}_{\_}i{w}^{\prime }\text{ implies }{\text{def}}_{\_}w(P)={\text{def}}_{\_}{w}^{\prime }(P)$$

$${\text{Kx}}_{\_}i(P):={\square }_{\_}iP\wedge {\text{Kd}}_{\_}i(P)$$

$$\mathcal{M},w\models p:=P⟺{\text{DEF}}_{\_}w(p)=P$$

Full text

1 Introduction

Konnyaku Mondo (jelly dialogue) is a story from the traditional Japanese comic storytelling in the rakugo form. Quoting [14], the story goes like the following:

There was a temple where no monks were living any longer. A devil’s tongue jelly maker, named Rokubei, lived next door. He moved into the temple and started pretending to be a monk. One day, a traveling Zen Buddhist monk passed by and challenged Rokubei to a debate on Buddhism, Rokubei had no knowledge on Buddhism and was not able to have a debate. He tried to refuse, but he could not escape and finally agreed. The Buddhist dialogue started but Rokubei didn’t know how to perform and therefore, he kept silent. The Buddhist monk tried to communicate to Rokubei in many ways. After some time, Rokubei started responding with gestures to the body movements the monk made. The monk took this as a style of dialogue and tried to answer in gestures, too. They exchanged gestures, and after some time, the monk told Rokubei, “your thoughts are profound and mine are of no comparison. I am very sorry to have bothered you”, After saying this, he left the temple.

In fact, the monk thought “the master” (Rokubei) had expressed deep Buddhist thoughts by his gestures, but Rokubei had never learned any Buddhist thoughts. Rather, from some stage on, he thought the monk was talking badly about his jelly with those gestures, thus he gave the monk a lesson by some angry moves, and apparently defeated the monk.

The intriguing nature of the story is that, as remarked in [14], it seems the proposition Rokubei has defeated the monk is common knowledge between the two, but it is based on mutual misunderstanding. The two actually have completely different understanding for the commonly agreed “defeat of the monk”. Such mutual misunderstanding also happens a lot in everyday life communications, even in academic exchanges when people “agree” to the same thing due to different interpretations or definitions of the same concept. See [14] for excellent (and entertaining) interactive discussions about such Konnyaku Mondo phenomena in Game theory.

Mutual misunderstanding is not always harmful. To postpone immediate conflicts and achieve some consensus, it is sometimes even intended to allow respective interpretations of the same proposition, which happens in diplomatic scenarios. For example, two brothers may disagree about who represents officially their father, but they may reach the temporary consensus that there is one and only one successor in order to avoid immediate conflicts.

Philosophically, if we require that knowledge should be at least properly justified as Gettier’s examples suggest [12], we can hardly say both Rokubei and the monk “know” that Rokubei has defeated the monk, since the same proposition is justified by two different reasons by different parties. The tricky thing here is that perhaps there is no single “real” justification for the defeat. More crucially, it is debatable in this particular case, whether there is a fixed “real” meaning of the proposition that Rokubei has defeated the monk.

As logicians, the story makes us think about how to represent such situations in the framework of epistemic logic, where $K_{\_}ip$ expresses that agent $i$ knows that $p$. According to the standard Kripke semantics, $K_{\_}ip$ merely means that agent $i$ is certain that $p$ is true, and there is nothing about the meaning of $p$ in the semantics. For example, suppose you do not understand Chinese, but someone said a Chinese sentence $p$ and guaranteed you its truth, then it seems you indeed know the truth value of $p$, but without knowing its meaning. Now suppose the speaker then tells you that by $p$, he actually meant $r\land q$ in your own language, then you know both the meaning of $p$ and its truth value (and the truth values of $q$ and $r$). Note that, even when $p$ is uttered in a language that you know, it still can have a different meaning than the surface one, e.g, when a Chinese says “we will think about it later” when asked a yes-no question, it often means “no”. It is crucial to see that knowing that $p$* means $\varphi$* is different from knowing that $p\leftrightarrow\varphi$, where the latter is again simply about the truth value. For example, knowing that $p\leftrightarrow\top$ does not imply that $p$* means $\top$*. We need new techniques to handle knowledge of meanings in epistemic logic.

More generally, knowing the value of something does not imply understanding what information it carries. For example, knowing the ID number of a Chinese person (e.g., 110105198002290022) does not tell you much, unless you know that the first 6 digits encode the residence (Chaoyang District in Beijing), the next 8 digits encode the birth date (29th of February 1980) and so on. Clearly, the interpretation of the structure of the ID is important to your understanding. You may also only know part of the meaning of the message and there are different “layers” of your understanding. You may or may not know that the gender of the person is given by the parity of the second to last digit (in this case even for female). Merely knowing that the first 6 digits code the residence does not tell you the exact city where this person is registered, you may need to know further that the fist three digits code the city and 110 is the code for Beijing. Therefore, by limited knowledge of the structure, you may only get part of the meaning.

Coming back to the propositional setting in this paper, for a sentence $\varphi$, you might also just understand some part of it, e.g., knowing what $q$ means in $p\lor q$ but only understand $p$ as $\neg r$ for some incomprehensible $r$. Now, if others elaborate that $r$ means $q\land o$, then you have a deeper understanding of $p\lor q$. We may also enhance our understanding by matching the structure of the proposition — if someone utters $(p\land p^{\prime})\lor p^{\prime\prime}$ and later explains that it means $q\lor(r\land r^{\prime})$, then we know $q$ means $p\land p^{\prime}$, and $p^{\prime\prime}$ means $(r\land r^{\prime})$. The technical goal of this paper is to formally flesh out such reasoning patterns with a minimal extension of public announcement logic [18, 19]. The basic idea is to treat incomprehensible propositions as atomic propositions with boolean definitions based on the basic atomic propositions.

Concerning related work, the distinction between knowing the value and knowing the meaning is crucial in cryptographic message passing. The goal of encryption schemes is to hide the meaning of a message, even if the transmitted ciphertext is known [20, 5]. Another related recent attempt [7], based on a logic of knowing value [23, 10, 2], introduces a functional dependency operator to express that the agent knows a function which can explain the dependency between variables $c$ and $d$. However, as the author of [7] also remarked, it is not enough to capture the meaning of variables. In [17], the meaning of an utterance by an agent depends on the type of the agent, which is a function mapping the uttered proposition to its actual meaning. Similarly, protocols can also give meaning to communicative actions, as demonstrated in [3, 21, 8], where the meaning of an action is defined by the corresponding precondition of the protocol regarding this. We discuss other related work in the conclusion.

In the rest of this paper, we first layout the language and semantics of our logic in Section 2, and then axiomatize it in Section 3, before concluding with ideas for future work.

2 PAL with Boolean Definitions

2.1 Language, Models, Semantics

Throughout the paper our languages and models are parameterized by a set of proposition letters $\mathsf{Prop}$ and a finite set of agents $I$. The language we study consists of two parts: a purely boolean layer for which our models will also provide definitions, and on top of that a version of Public Announcement Logic (PAL) as in [18, 9].

Definition 1** (Language).**

The boolean language $\mathcal{L}_{\_}B$ is defined by

[TABLE]

where $p\in\mathsf{Prop}$, a countable set of propositional letters. We already note that the parentheses are essential for pattern matching as we will see later.

The full language $\mathcal{L}$ is given by

[TABLE]

where $P\in\mathcal{L}_{\_}B$ and $i\in I$. We write $Q\not\equiv P$ for $\lnot(Q\equiv P)$ and use the standard abbreviations for other boolean operators $\varphi\lor\psi:=\lnot(\lnot\varphi\land\lnot\psi)$, $\varphi\to\psi:=\lnot\varphi\lor\psi$ and $\varphi\leftrightarrow\psi:=(\varphi\to\psi)\land(\psi\to\varphi)$.

For modalities we use the notation $\Box_{\_}i$ and avoid the symbol $K_{\_}i$ which would suggest knowledge. This is because we will not assume additional modal axioms besides $K$. Our framework can easily be adapted to multi-agent $KD45$, $S5$ and other logics.

We read $P_{\_}1\equiv P_{\_}2$ as “$P_{\_}1$ and $P_{\_}2$ have the same meaning” or “$P_{\_}1$ and $P_{\_}2$ are equivalent by definition”. For example, if $p$ means $r\lor r^{\prime}$ and $q$ means $\neg o$, then our semantics below will also imply that $p\land\neg o$ has the same meaning as $((r\lor r^{\prime})\land q)$.

We avoid reading the $\equiv$ operator as “…is defined as …” which would suggest a directedness and uniqueness on the right side. In fact, while our models will contain unique definitions for which one might write $:=$, we do not refer to the definition. The formal language can only express that certain propositions are equivalent by definition.

A model in our framework is a Kripke model with a local definition function $\textsf{DEF}_{\_}w$ on each world $w$, which assigns to each $p\in\mathsf{Prop}$ a definition as its (most thorough) meaning. To stay as general as possible, we do not assume any frame property in this paper. Intuitively, if a proposition letter $p$ is assigned itself as the definition, this means that $p$ is self-evident or truly basic. Based on those definitions, we can then “unravel” each boolean formula in $\mathcal{L}_{\_}B$ to obtain its meaning by recursively applying $\textsf{DEF}_{\_}w$. Further constraints are imposed to avoid circularity and make sure each non-self-evident proposition is assigned a definition using self-evident propositions.

Definition 2** (Models).**

A premodel $\mathcal{M}$ is a tuple $(W,R,V,\textsf{DEF})$ where $W$ is a non-empty set of worlds, $R_{\_}i\subseteq W\times W$ is a relation for each agent $i$, $V\colon W\to\mathsf{Prop}\to\{0,1\}$ is a valuation function and $\textsf{DEF}\colon W\to\mathsf{Prop}\to\mathcal{L}_{\_}B$ is a definition function.

We write $V_{\_}w$ for the valuation at $w$ and lift it to $\mathcal{L}_{\_}B$ as usual by the standard boolean semantics included in Definition 3 below. Similarly, we lift the definition function $\textsf{DEF}_{\_}w$ at $w$ from $\mathsf{Prop}$ to $\mathcal{L}_{\_}B$ using definitions from the premodel for atoms and recursing over $\lnot$ and $\land$. Formally, let $\textsf{def}_{\_}w:\mathcal{L}_{\_}B\to\mathcal{L}_{\_}B$ be defined by:

[TABLE]

Intuitively, $\textsf{def}_{\_}w(P)$ is obtained by replacing all the propositions letters in $P$ by their definitions.

A premodel is a model iff we have for all worlds $w$:

• •

For all $P,Q\in\mathcal{L}_{\_}B$: If $\textsf{def}_{\_}w(P)=\textsf{def}_{\_}w(Q)$, then $V_{\_}w(P)=V_{\_}w(Q)$.

• •

For all $p,q\in\mathsf{Prop}$: If $p$ is in $\textsf{DEF}_{\_}w(q)$, then $\textsf{DEF}_{\_}w(p)=p$.

To connect definitions and truthvalues the first model constraint demands that whatever is definitionally equivalent is also assigned the same truth value. We note that only demanding this condition for atomic propositions does not suffice for our purposes.

The second model constraint ensures well-foundedness: Models never contain circular definitions like $p:=(p\land q)$. Moreover, they also do not contain chains of definitions that would imply such a definition if they were unraveled, for example $p:=r$ and $r:=(p\land q)$. While some of these might actually make sense as fixpoints or infinite conjunctions, for now we do not allow them in our framework.

Definition 3** (Semantics).**

We interpret $\mathcal{L}$ on models as follows.

[TABLE]

where $\mathcal{M}^{\varphi}$ is the restriction of $\mathcal{M}$ to the new set of worlds $\{v\in W\mid\mathcal{M},v\vDash\varphi\}$.

In the second condition, the $=$ symbol on the right side is syntactic equality within $\mathcal{L}_{\_}B$. As we mentioned, parentheses in $\equiv$ formulas matter, e.g., $(p\land(q\land r))\not\equiv((p\land q)\land r)$ is valid. In contrast $(p\land(q\land r))\leftrightarrow((p\land q)\land r)$ is clearly valid, where we can omit the parentheses. Note that all clauses besides the one for $\equiv$ are standard PAL as in [18, 9]. In particular, the result of announcements is defined as usual, preserving the valuation and now also the local definitions at each world.

2.2 Examples

To illustrate our semantics and to show that it can describe various different scenarios, we now give some examples.

Example 1** (Knowing without Understanding).**

As mentioned in the introduction, you can know that something is true without knowing what it means and without knowing that its meaning is true. Figure 2 shows such a model. We use undirected edges to indicate an equivalence relation and we omit the self-evident definitions for $q$ and $r$ in all three worlds. At the actual world in the middle we have $\Box_{\_}ip\land(p\equiv q)\land\lnot\Box_{\_}i(p\equiv q)\land\neg\Box_{\_}iq$. Moreover, even if $p\leftrightarrow q$ were announced, only the right world would be removed. The agent would then know that $p\leftrightarrow q$ but still not know the stronger $p\equiv q$.

Example 2** (Understanding without Knowing).**

Conversely, an agent can know the meaning of a proposition but still not know whether it is true. Both worlds in the model shown in Figure 2 satisfy $\Box_{\_}i(p\equiv q)\land\Box_{\_}i(p\leftrightarrow q)\land\lnot\Box_{\_}ip$.

Example 3** (Understanding different parts).**

Two agents can also have different partial knowledge of the meaning of some proposition. The middle world of the model in Figure 3 satisfies these three formulas:

[TABLE]

[TABLE]

[TABLE]

Note that if the agents would combine their knowledge by announcing both partial meanings, they would arrive at the most thorough meaning, which is more informative than what either of them knows at the moment. Formally, we have $[r\equiv\lnot r_{\_}1][q\equiv\lnot q_{\_}1](\land_{\_}{i=a,b}\Box_{\_}i(p\equiv(\lnot q_{\_}1\land(\lnot r_{\_}1))))$.

Example 4** (Consensus with misunderstanding).**

As in the Konnyaku Mondo example, two agents can agree on something but actually have different beliefs about what it means. In the model from Figure 4, at the middle world, we have $p\land\Box_{\_}ip\land\Box_{\_}jp$ but also $\Box_{\_}i((p\equiv r)\land r\land\lnot q)$ and $\Box_{\_}j((p\equiv q)\land q\land\lnot r)$.

3 Axiomatization

Note that the addition of $\equiv$ does not invalidate the standard reduction axioms of PAL. We can rather think of $\varphi\equiv\psi$ as a new atomic proposition which is evaluated purely locally.

Definition 4**.**

A formula $P\equiv Q$ is a circular formula iff there is an atomic $p$ such that either (i) $P=p$ and $Q\neq p$ and $p$ occurs in $Q$ or (ii) vice versa.

For example the formulas $p\equiv(p\land q)$ and $\lnot q\equiv q$ are both circular, but $p\equiv p$ is not circular.

Definition 5** (Axioms and Rules).**

We define the following proof system $\mathbb{SPALD}$ for $\mathcal{L}$. We call the system without the PAL reduction axioms $\mathbb{SMLD}$.

Axiom Schemes

• •

All propositional tautologies.

• •

The $K$ axiom: $\Box_{\_}i(\varphi\to\psi)\to(\Box_{\_}i\varphi\to\Box_{\_}i\psi)$

• •

PAL reduction axioms:

• –

$[\varphi]p\leftrightarrow(\varphi\to p)$**

• –

$[\varphi](P\equiv Q)\leftrightarrow(\varphi\to(P\equiv Q))$**

• –

$[\varphi]\lnot\psi\leftrightarrow(\varphi\rightarrow\lnot[\varphi]\psi)$**

• –

$[\varphi](\psi\land\theta)\leftrightarrow([\varphi]\psi\land[\varphi]\theta)$**

• –

$[\varphi]\Box_{\_}i\psi\leftrightarrow(\varphi\rightarrow\Box_{\_}i(\varphi\rightarrow[\varphi]\psi))$**

• –

$[\varphi][\psi]\xi\leftrightarrow[\varphi\land[\varphi]\psi]\xi$**

• •

Definition axioms

• –

Reflexivity: $(P\equiv P)$

• –

Symmetry: $(P\equiv Q)\to(Q\equiv P)$

• –

Transitivity: $((P\equiv Q)\land(Q\equiv R))\to(P\equiv R)$

• –

Equivalence: $(P\equiv Q)\to(P\leftrightarrow Q)$

• –

*Atomic occurrence substitution: $((p\equiv Q)\land(R\equiv S))\to(R\equiv[k\mathopen{:}p\mapsto Q]S)$ where $k\mathopen{:}p$ denotes the *$k$th occurrence of $p$ in $S$.

• –

Pattern $\lnot$: $(\lnot P\equiv\lnot Q)\leftrightarrow(P\equiv Q)$

• –

Pattern $\land$: $((P\land Q)\equiv(R\land S))\leftrightarrow((P\equiv R)\land(Q\equiv S))$

• –

Pattern mismatch: $\lnot P\not\equiv(Q\land R)$

• –

Non-circularity: $p\not\equiv P$ where $p$ occurs in $P$ but $P\neq p$

Rules

• •

Modus Ponens: from $\varphi$ and $\varphi\to\psi$ infer $\vdash\psi$.

• •

Necessitation for $\Box_{\_}i$: from $\vdash\varphi$ infer $\Box_{\_}i\varphi$.

Somewhat non-standard in our axiom system is the usage of occurrence substitutions, in contrast to standard substitutions which usually replace all occurrences of a given atom. We also use the notation $[k\mathopen{:}p\mapsto Q]$ in proofs in the next section and it will become more clear there.

We note that our logic does not allow replacement of equivalents in $\equiv$ formulas, hence this is not an admissible proof rule. For example, $p\leftrightarrow(p\land p)$ is valid and so is $p\equiv p$, but $p\equiv(p\land p)$ is not valid and in fact a contradiction, by the non-circularity axiom. Finally, we note that necessitation for $[\varphi]$ is an admissible rule [22].

Theorem 1**.**

The axiom system $\mathbb{SPALD}$ from Definition 5 is sound for the semantics from Definition 3.

4 Completeness

To show the completeness of our axiomatization, we can first show the completeness of $\mathbb{SMLD}$ for announcement-free formulas. Then by using the reduction axioms we can obtain the completeness of $\mathbb{SPALD}$ in the usual way [18]. In the following, we write $\vdash\varphi$ if $\varphi$ is provable in $\mathbb{SMLD}$.

Before we go on, note that our axioms enforce non-circularity but not well-foundedness. That is, the set $\{p_{\_}i\equiv p_{\_}{i+1}\land p_{\_}{i+2}\mid i\in\mathbb{N}\}$ is consistent according to the proof system above, but it does not have a model, since you cannot give definitions to $p_{\_}i$ using some self-evident atoms. However, any finite subset of this set has a model, hence our logic is not compact and we cannot show strong completeness.

Fortunately, we can still show completeness because any finite set of formulas only uses finitely many atomic propositions.

For the rest of this section, we fix a finite vocabulary $\mathsf{Prop}$.

Example 5**.**

Consider the following three formulas and an infinite sequence of consequences:

[TABLE]

Note that none of these formulas alone is circular. However, it is easy to spot another consequence $p\equiv(p\land r)\land r$ which is circular. Hence the original set of three formulas is inconsistent.

The main idea for our completeness proof is that Example 5 is not an exception: Whenever a set of equivalent definitions is infinite we can systematically derive a circular formula. Before stating our central Lemma 1 we need a few more definitions.

Definition 6**.**

For each boolean formula $P\in\mathcal{L}_{\_}B$ we define its length $l(P)$ as follows:

[TABLE]

Additionally, we define its vocabulary $v(P)$ as follows:

[TABLE]

As an example, $l(\lnot p)=2$ and $l(p\land(p\land q))=9$. Note that the parentheses also count.

Definition 7**.**

Given a maximally consistent set $\Gamma\subseteq\mathcal{L}(\mathsf{Prop})$, we define a relation over $\mathcal{L}_{\_}B(\mathsf{Prop})$ by $P\equiv_{\_}\Gamma Q\ :\iff\ (P\equiv Q)\in\Gamma$. Per relevant axioms in Definition 5 this is an equivalence relation. For each $P\in\mathcal{L}_{\_}B(\mathsf{Prop})$ we denote its $\equiv_{\_}\Gamma$-equivalence class by

[TABLE]

and call it the set of $\Gamma$-definitions of $P$.

Lemma 1**.**

For each maximally consistent set $\Gamma\subseteq\mathcal{L}(\mathsf{Prop})$ and each atomic proposition $p\in\mathsf{Prop}$, the set ${[p]}_{\_}\Gamma$ is finite.

To prove Lemma 1, we first need some definitions and notation. We fix an enumeration of $\mathsf{Prop}$, say alphabetically. This induces a lexicographic ordering $<$ over $\mathcal{L}_{\_}B$. For example, we have $p<q$, therefore also $\lnot p<\lnot q$ and similarly for conjunctions.

Definition 8**.**

Let $\mathsf{merge}\colon\mathcal{L}_{\_}B\times\mathcal{L}_{\_}B\to\mathcal{L}_{\_}B$ be defined as follows:

[TABLE]

By definition, $\mathsf{merge}$ is symmetric: $\mathsf{merge}(P,Q)=\mathsf{merge}(Q,P)$.

Example 6**.**

We have $\mathsf{merge}((p\land(q\land r)),(\lnot s\land t))=(\lnot s\land(q\land r))$.

It is also easy to see that, viewed as term-rewriting rules, $\mathsf{merge}$ always terminates, since the recursive clauses reduce the complexity of the formulas.

Definition 9**.**

Let $[k\mathopen{:}p\mapsto P]Q$ denote the result of replacing the $k$-th occurrence of $p$ in $Q$ with $P$. For multiple such occurrence substitutions, let $[k\mathopen{:}p\mapsto P\ \oplus\ k^{\prime}\mathopen{:}p^{\prime}\mapsto R]Q$ denote their simultaneous application to $Q$.

Example 7**.**

We have $[2\mathopen{:}p\mapsto(q\land r)](p\land p)\ =(\ p\land(q\land r))$. As an example of two simultaneous occurrence substitutions, we have $[2\mathopen{:}p\mapsto(q\land r)\ \oplus\ 1\mathopen{:}q\mapsto\lnot r]((p\land p)\land q)\ =\ ((p\land(q\land r))\land\lnot r)$.

Lemma 2**.**

For all $P,Q$ such that $P\equiv Q\in\Gamma$ we have:

1. (i)

$\mathsf{merge}(P,Q)\equiv P\in\Gamma$** 2. (ii)

There are indices $k_{\_}1,\ldots,k_{\_}n\in\mathbb{N}$, atoms $p_{\_}1,\ldots,p_{\_}n\in\mathsf{Prop}$ and formulas $R_{\_}1,\ldots,R_{\_}n\in\mathcal{L}_{\_}B$ for some fixed $n\geq 0$ such that we have $\mathsf{merge}(P,Q)=[k_{\_}n\mathopen{:}p_{\_}n\mapsto R_{\_}n\ \oplus\ldots\oplus\ k_{\_}1\mathopen{:}p_{\_}1\mapsto R_{\_}1]P$ and $p_{\_}i\equiv R_{\_}i\in\Gamma$ for all $i\leq n$. (Note that $n=0$ iff $\mathsf{merge}(P,Q)=P$.)

Proof.

Since $\Gamma$ is consistent, if $P\equiv Q\in\Gamma$ then $\mathsf{merge}(P,Q)$ is always defined, based on the axioms of pattern mismatch.

For (i) we do induction on the structure of $P$.

Suppose $P=p$, then $\mathsf{merge}(P,Q)$ is $p$ or $Q$. Then it is straightforward that $\mathsf{merge}(P,Q)\equiv P\in\Gamma$, since $P\equiv Q\in\Gamma$.

Suppose $P=\neg P^{\prime}$. Since $P\equiv Q\in\Gamma$, the shape of $Q$ is either $q$ or $\neg Q^{\prime}$ due to the pattern mismatch axiom and the fact that $\Gamma$ is consistent. The first case reduces to the above case due to the axiom of symmetry and the fact that $\mathsf{merge}$ is symmetric. For the second case, by pattern inference we have $P^{\prime}\equiv Q^{\prime}\in\Gamma$. Now by induction hypothesis, $\mathsf{merge}(P^{\prime},Q^{\prime})\equiv P^{\prime}\in\Gamma$. Therefore $\neg\mathsf{merge}(P^{\prime},Q^{\prime})\equiv\neg P^{\prime}\in\Gamma$ by pattern inference axiom, namely $\mathsf{merge}(P,Q)\equiv P\in\Gamma$.

The case of $P=(P_{\_}1\land P_{\_}2)$ is similar.

For (ii), we also do induction on the structure of $P$.

Suppose $P=p$, then $\mathsf{merge}(P,Q)$ is $p$ or $Q$. In the first case we just need a trivial substitution $[1\mathopen{:}p\mapsto p]$ since $p\equiv p\in\Gamma$. In the second case we take $[1\mathopen{:}p\mapsto Q]$ since $p\equiv Q\in\Gamma$.

Suppose $P=\neg P^{\prime}$. As in the proof of (i) we can show that $Q$ is in the shape of either $q$ or $\neg Q^{\prime}$. For the first case, $\mathsf{merge}(P,q)=P=\neg P^{\prime}$ by definition of $\mathsf{merge}$. Then we can take the trivial substitution to prove the claim. In the second case, $\mathsf{merge}(P,Q)=\neg\mathsf{merge}(P^{\prime},Q^{\prime})$. Since $P\equiv Q\in\Gamma$, $P^{\prime}\equiv Q^{\prime}\in\Gamma$ by pattern inference. Now by induction hypothesis, there are substitutions to turn $P^{\prime}$ into $\mathsf{merge}(P^{\prime},Q^{\prime})$. The same substitutions can also turn $P=\neg P^{\prime}$ into $\mathsf{merge}(P,Q)=\neg\mathsf{merge}(P^{\prime},Q^{\prime})$.

Again the case of $P=(P_{\_}1\land P_{\_}2)$ is similar. ∎

Lemma 3**.**

For all $p\in\mathsf{Prop}$ and all $P,Q\in{[p]}_{\_}\Gamma$ we have:

1. (i)

$\mathsf{merge}(P,Q)\in{[p]}_{\_}\Gamma$** 2. (ii)

$l(\mathsf{merge}(P,Q))\geq\max(l(P),l(Q))$** 3. (iii)

There are indices $k_{\_}1,\ldots,k_{\_}n\in\mathbb{N}$, atoms $p_{\_}1,\ldots,p_{\_}n\in\mathsf{Prop}$ and formulas $R_{\_}1,\ldots,R_{\_}n\in\mathcal{L}_{\_}B$ for some fixed $n\geq 0$ such that we have $\mathsf{merge}(P,Q)=[k_{\_}n\mathopen{:}p_{\_}n\mapsto R_{\_}n\ \oplus\ldots\oplus\ k_{\_}1\mathopen{:}p_{\_}1\mapsto R_{\_}1]P$ and $p_{\_}i\equiv R_{\_}i\in\Gamma$ for all $i\leq n$.

Proof.

For (i): Suppose $P,Q\in{[p]}_{\_}\Gamma$. Then $P\equiv Q\in\Gamma$ and according to part (i) of Lemma 2 we have $\mathsf{merge}(P,Q)\equiv P\in\Gamma$. Since $P\in{[p]}_{\_}\Gamma$, thus by transitivity axiom, $\mathsf{merge}(P,Q)\in{[p]}_{\_}\Gamma$.

For (ii): a simple induction on the clauses of $\mathsf{merge}$ suffices.

Finally, (iii) is a special case of part $(ii)$ in Lemma 2 since $P,Q\in{[p]}_{\_}\Gamma$ implies $P\equiv Q\in\Gamma$. ∎

Intuitively, Lemma 3 says that the result of merging two $\Gamma$-definitions of $p$ (i) is also a $\Gamma$-definition of $p$, (ii) is at least as long as the longest given formula, and (iii) can be reached by replacing atom occurrences step by step.

In fact, the occurrence substitutions given by (iii) are unique up to enumeration and trivial substitutions of the form $[k\mathopen{:}p\mapsto p]$. Moreover, the pattern matching axioms imply that $R_{\_}i\in{[p_{\_}i]}_{\_}\Gamma$.

Proof of Lemma 1.

Suppose ${[p]}_{\_}\Gamma$ is infinite.

Then in particular the length of formulas in ${[p]}_{\_}\Gamma$ is unbounded, because $\mathsf{Prop}$ is finite. Hence there must be an infinite chain $P_{\_}0=p,P_{\_}1,P_{\_}2,\ldots$ in ${[p]}_{\_}\Gamma$ which is unbounded in length. Note that there might be big “jumps” in length and in general the formulas will not be related systematically.

To deduce a circular formula and thus a contradiction, we now define a second chain $Q_{\_}0,Q_{\_}1,\ldots$ using $\mathsf{merge}$. Let $Q_{\_}0:=P_{\_}0=p$ and for all $k\geq q$ let $Q_{\_}k:=\mathsf{merge}(Q_{\_}{k-1},P_{\_}k)$. From Lemma 3 we now get that (i) the chain of $Q_{\_}i$s is also a chain in ${[p]}_{\_}\Gamma$, (ii) $l(Q_{\_}i)\geq l(P_{\_}i)$ and thus this chain is also unbounded in length, and (iii) for each step from $Q_{\_}i$ to $Q_{\_}{i+1}$ there are finitely many atoms that are replaced with longer formulas.

Let us list such a sequence of substitutions as:

[TABLE]

where $\overline{k\mathopen{:}p\mapsto R}$ denotes the simultaneous substitution $[k_{\_}{n}\mathopen{:}p_{\_}n\mapsto R_{\_}n\ \oplus\ldots\oplus\ k_{\_}1\mathopen{:}p_{\_}1\mapsto R_{\_}1]$ for some $n$. We can denote each single substitution as ${[k:p\mapsto R]}^{i}$ where the superscript $i$ means the substitution happens at $Q_{\_}i$.

Now let $(N,\rightsquigarrow)$ be the graph where $N$ is the set of all occurrence substitutions in the $Q$ chain (indexed with superscripts) and there is an edge ${[m\mathopen{:}p\mapsto R]}^{i}\rightsquigarrow{[n\mathopen{:}q\mapsto S]}^{j}$ iff $i<j$ and $n\mathopen{:}q$ is an occurrence within $R$ of $Q_{\_}{i+1}$. Then $(N,\rightsquigarrow)$ is a tree with the first substitution ${[1\mathopen{:}p\mapsto P_{\_}1]}^{0}$ as its root. Intuitively, we have an edge from one substitution to another iff the second “happens within” the result of the first. This tree of substitutions is illustrated in Figures 5 and 6 below as examples.

The $Q_{\_}i$ chain of formulas is infinite, hence there are infinitely many substitutions and $N$ is infinite. However, each occurrence of an atomic proposition can be replaced with a longer formula only once. Hence the number of children of each node in $(N,\rightsquigarrow)$ is bounded by the length of the formula. Formally, each node ${[k\mathopen{:}p\mapsto R]}^{i}$ can only have as many children as there are occurrences of atoms in $R$.

Together, $(N,\rightsquigarrow)$ is an infinite but also finitely branching tree. By Kőnig’s Lemma [16, 11] there must be an infinite branch. In particular, there must be a branch longer than $|\mathsf{Prop}|$ and there must be two substitutions of the same atom along this branch. We now use this branch to derive a circular formula in $\Gamma$.

Let $R_{\_}i$ be the sequence of formulas starting with $R_{\_}0:=p$ and then applying the substitutions from the branch. For each $i$, let ${[k_{\_}i\mathopen{:}q_{\_}i\mapsto S_{\_}i]}^{\iota_{\_}i}$ be the substitution at node $i$ happening at $Q_{\_}{\iota_{\_}i}$. Note that the branch need not have a node at every level, hence $\iota_{\_}i\geq i$ but not necessarily $\iota_{\_}i=i$.

Because $|\mathsf{Prop}|$ is finite there must be $j<k$ such that $q_{\_}j=q_{\_}k=:q$. Then we have $q\in R_{\_}j$ and $q\in R_{\_}k$ and $S_{\_}j,S_{\_}k\in{[q]}_{\_}\Gamma$. Now consider the sequence of substitutions $R$s:

[TABLE]

In particular, because these substitutions happen along the same branch, $k_{\_}m\mathopen{:}q_{\_}m$ is an occurrence in $Q_{\_}j$. Hence, reasoning inside $\Gamma$ we have $q\equiv Q_{\_}j$ and $q\equiv{[k_{\_}m\mathopen{:}q_{\_}m\mapsto Q_{\_}m]}^{\iota_{\_}m}Q_{\_}j$. But because $q$ occurs in $Q_{\_}m$, the latter is a circular formula in $\Gamma$. Contradiction! ∎

To illustrate our proof method, we give two examples.

Example 8**.**

The chain of $Q_{\_}i$ might for example be all right parts of consequences in Example 5. That is, in the set ${[s]}_{\_}\Gamma$ we have $Q_{\_}0=p$, $Q_{\_}1=(q\land r)$, $Q_{\_}2=((p\land r)\land r)$, $Q_{\_}3=(((q\land r)\land r)\land r)$, and so on. The sequence of occurrence substitutions is then ${[1\mathopen{:}p\mapsto(q\land r)]}^{0}$, ${[1\mathopen{:}q\mapsto(p\land r)]}^{1}$, ${[1\mathopen{:}p\mapsto(q\land r)]}^{2}$, and so on. This is an easy case: each step replaces an occurrence within the previous substituens. Hence the tree of substitutions shown in Figure 5 only has one branch.

Example 9**.**

An example which yields a proper tree is shown in Figure 6. On the left side we first show the $P_{\_}i$ chain. Note that its formulas are strictly increasing in complexity, but for example $P_{\_}2$ and $P_{\_}3$ are not directly related via substitutions. The second chain $Q_{\_}i$ is obtained using the $\mathsf{merge}$ function from Definition 8 and restores this property. For example, we can go from $Q_{\_}2$ to $Q_{\_}3$ via the substitution ${[2\mathopen{:}r\mapsto\lnot\lnot s]}^{2}$. All those substitutions are then arranged in the $(N,\rightsquigarrow)$ tree. Finally, we show how two substitutions of the same proposition ($r$) in the same branch lead to a circular formula ($r\equiv\lnot\lnot(r\rightarrow p)$).

Given that all ${[p]}_{\_}\Gamma$ sets are finite, we can now choose a definition for each $p\in\mathsf{Prop}$, namely the longest and among those the lexicographically least formula in ${[p]}_{\_}\Gamma$. In fact, this is the same as applying all possible substitutions until reaching the leaves in the substitution trees from the proof of Lemma 1.

Definition 10**.**

For any finite set of boolean formulas $X\subseteq\mathcal{L}_{\_}B$, we define $\mathsf{pick}(X)$ as the longest element of $X$ and among those the lexicographically first.

Formally, let $\mathsf{pick}(X):=\min_{\_}<\{P\in X\mid\forall Q\in X:l(P)\geq l(Q)\}$

Definition 11** (Canonical Model).**

For a finite vocabulary $\mathsf{Prop}$ the corresponding canonical model $\mathcal{M}=(W,R,V,\textsf{DEF})$ is defined as follows:

• •

$W:=\{\Gamma\subseteq\mathcal{L}(\mathsf{Prop})\mid\Gamma\text{ is maximally consistent}\}$**

• •

$\Gamma_{\_}1R_{\_}i\Gamma_{\_}2:\iff\{\varphi\mid\Box_{\_}i\varphi\in\Gamma_{\_}1\}\subseteq\Gamma_{\_}2$**

• •

$V(\Gamma):=\Gamma\cap\mathsf{Prop}$**

• •

For each $\Gamma$ and any $p\in\mathsf{Prop}$, let $\textsf{DEF}_{\_}\Gamma(p):=\mathsf{pick}({[p]}_{\_}\Gamma)$

Lemma 4**.**

The canonical model is indeed a model, and not just a premodel.

Proof.

We need to show two properties.

• •

For all $P,Q\in\mathcal{L}_{\_}B$: If $\textsf{def}_{\_}w(P)=\textsf{def}_{\_}w(Q)$, then we also have $V_{\_}w(P)=V_{\_}w(Q)$. This follows from the equivalence axiom $(P\equiv Q)\to(P\leftrightarrow Q)$ and the boolean part of the Truth Lemma 6 below which can be shown independently.

• •

For all $p,q\in\mathsf{Prop}$, we need to show that if $p$ occurs in $\textsf{DEF}_{\_}w(q)$, then $\textsf{DEF}_{\_}w(p)=p$. Now, take any $p$ in $\textsf{DEF}_{\_}w(q)$. Because $\textsf{DEF}_{\_}w(q)$ is among the longest formulas in ${[q]}_{\_}\Gamma$, there cannot be any $P\in{[p]}_{\_}\Gamma$ with $l(P)>1$. Namely, ${[p]}_{\_}\Gamma$ only consists of propositional letters.

Because $\textsf{DEF}_{\_}w(q)$ is the lexicographically first among the longest formulas in ${[q]}_{\_}\Gamma$, also $p$ must be lexicographically first in ${[p]}_{\_}\Gamma$, for otherwise we can replace it in $\textsf{DEF}_{\_}w(q)$ by another propositional letter which is lexicographically smaller than $p$ to obtain a lexicographically smaller formula in ${[q]}_{\_}\Gamma$. Together, we have $\textsf{DEF}_{\_}w(p)=p$.∎

Lemma 5**.**

In the canonical model we have for all $P\in\mathcal{L}_{\_}B(\mathsf{Prop})$ that $\textsf{def}_{\_}\Gamma(P)=\mathsf{pick}({[P]}_{\_}\Gamma)$.

Proof.

By induction on the structure of $P$. The base case $P=p$ follows from Definition 11.

For the induction step, consider the case $P=\lnot Q$. Then we have the following chain of identities:

[TABLE]

where the step IH is by induction hypothesis and the step $\ast$ is shown as follows. By definition of $\mathsf{pick}$ we have that $\mathsf{pick}({[\lnot Q]}_{\_}\Gamma)$ is

[TABLE]

which by pattern matching is the same as

[TABLE]

Because $<$ and $\geq$ with respect to $l(\cdot)$ is preserved under negation, this is the same as

[TABLE]

which is $\lnot\mathsf{pick}({[Q]}_{\_}\Gamma)$.

A similar chain covers the case $P=(Q_{\_}1\land Q_{\_}2)$. ∎

Lemma 6** (Truth Lemma).**

Consider the canonical model $\mathcal{M}$. For all worlds $\Gamma$ and all formulas $\varphi$ without announcement operators we have $\mathcal{M},\Gamma\vDash\varphi$ iff $\varphi\in\Gamma$.

Proof.

By induction on the complexity of $\varphi$. The only non-standard case is the $\equiv$ operator. We want to show

[TABLE]

for which it suffices to show

[TABLE]

For left to right, suppose ${[P]}_{\_}\Gamma={[Q]}_{\_}\Gamma$. This implies $\mathsf{pick}({[P]}_{\_}\Gamma)=\mathsf{pick}({[Q]}_{\_}\Gamma)$. Hence we have $\textsf{def}_{\_}\Gamma(P)=\textsf{def}_{\_}\Gamma(Q)$ by Lemma 5.

For right to left, suppose we have $\textsf{def}_{\_}\Gamma(P)=\textsf{def}_{\_}\Gamma(Q)$. Then by Lemma 5 we have a single formula $R:=\mathsf{pick}({[P]}_{\_}\Gamma)=\mathsf{pick}({[Q]}_{\_}\Gamma)$. In particular we have $R\in{[P]}_{\_}\Gamma$ and $R\in{[Q]}_{\_}\Gamma$. Hence $P\equiv R\in\Gamma$ and $R\equiv Q\in\Gamma$. Now by transitivity from Definition 5 we have $P\equiv Q\in\Gamma$. Therefore ${[P]}_{\_}\Gamma={[Q]}_{\_}\Gamma$. ∎

Finally, we can state and prove completeness.

Theorem 2** (Completeness).**

$\mathbb{SMLD}$* is weakly complete for announcement-free fragment of $\mathcal{L}$, and $\mathbb{SPALD}$ is weakly complete for the full $\mathcal{L}$.*

Proof.

Suppose $\varphi$ is not provable. By the PAL reduction axioms there is a formula $\varphi^{\prime}$ without announcements such that $\vdash\varphi\leftrightarrow\varphi^{\prime}$. Hence $\varphi^{\prime}$ is not provable and therefore $\lnot\varphi^{\prime}$ is consistent.

Let $\mathsf{Prop}$ be the vocabulary of $\varphi^{\prime}$. Let $\mathcal{M}$ be the canonical model for $\mathsf{Prop}$ per Definition 11. Let $\Gamma$ be any maximally consistent set containing $\lnot\varphi^{\prime}$. Such a set always exists and can be defined using a standard Lindenbaum Lemma [4, p. 197]. In particular, $\Gamma$ is an element of $W$ in $\mathcal{M}$. Then by the Truth Lemma we have $\mathcal{M},\Gamma\vDash\lnot\varphi^{\prime}$.

The reduction axioms are also semantically valid, so we have $\mathcal{M},\Gamma\vDash\lnot\varphi$. Hence $\varphi$ is not semantically valid. ∎

5 Knowing the Definition

Our language does not allow us to express that an agent knows the definition of a proposition. We can add this using an operator similar to $Kv$ from [23]. Formally, let $\textit{Kd}_{\_}iP$ where $P\in\mathcal{L}_{\_}B$ have the following semantics:

[TABLE]

As we have shown in Examples 1 and 2 knowing whether something is true and knowing its definition are contingent, neither implies the other.

We can then also define the notion of explicitly knowing, which is the combination of knowing that and knowing the definition:

[TABLE]

However, in our framework it is only possible to know propositional formulas explicitly. For example, the formula $\textit{Kx}_{\_}i(\Box_{\_}j(p\land q))$ is not in the language.

Also adding the definition itself to the language, with the following operator $:=$ could be helpful.

[TABLE]

For example we then have the following validities:

• •

$p:=P\rightarrow p\equiv P$  (definition implies equivalence)

• •

$p:=P\rightarrow\lnot(p:=Q)$ for all $P\neq Q$  (uniqueness)

• •

$(p:=P\land\textit{Kd}_{\_}i(p))\rightarrow\Box_{\_}i(p:=P)$

• •

$\textit{Kd}_{\_}iP\land\Box_{\_}i(P\equiv Q)\to\textit{Kd}_{\_}iQ$

In fact, the $:=$ operator could also simplify our original completeness proof. Choosing definitions for the canonical model is trivial for this extended language, because each maximally consistent set $\Gamma$ will contain exactly one formula of the form $p:=P$ for each $p\in\mathsf{Prop}$.222We thank Alexandru Baltag for pointing out how $:=$ may simplify our logic.

We leave it as future work to axiomatize the extension of our logic with Kd.

6 Conclusion and Future Work

We presented an extension of Public Announcement Logic (PAL) to model the knowledge of meanings with boolean definitions. In our logic agents can understand a proposition without knowing its truth value or the other way round. Moreover, multiple agents can agree on something without agreeing on its meaning and vice versa.

We also presented a sound and complete axiomatization with intuitive axioms to characterize the equivalence operator $\equiv$. The completeness proof is based on a standard canonical model construction, extended with two new ideas for boolean definitions. We use $\mathsf{merge}$ to combine different possible definitions and then use a tree of occurrence substitutions to ensure that there are only finitely many definitions to choose from.

Our formal contributions are thus more about pattern matching and less the epistemic and dynamic operators. Nevertheless, we think that our logic showcases an interesting interaction between boolean definitions and the standard operators $K$ and $[\varphi]$. On the other hand, as a subsystem of our proof system, the pattern matching logic regarding $\equiv$ seems interesting on its own. It may be applied in computer science or combined with other philosophical logics. In fact, our pattern matching and mismatching axioms are reminiscent of term rewriting rules. We therefore conjecture that our central Lemma 1 can also be shown using Kruskal’s Theorem applied to term rewriting, as discussed in [6].333We thank one of the anonymous reviewers for suggesting this connection.

Our work can be extended in several ways.

The framework is compatible with the range of multi-agent epistemic logics from $K_{\_}n$ to ${S5}_{\_}n$. The usual axioms for frame properties can be added, for example one might add transitivity for positive introspection, or reflexivity for truthfulness of knowledge.

We already mentioned in the last section that our logic relates to the Kv operator from [23]. We think that “knowing value” models could also be equipped with definitions for their general variables instead of propositions. This can then be combined with “public inspection” from [10] and the resulting framework might give a new perspective on knowledge of terms.

The distinction between value and meaning is best illustrated in the setting of cryptographic protocols, where you may know the value of the message but only part of the meaning. To illustrate this, suppose you have your own private key $k$. If you receive an encrypted message ${\{a,{\{b\}}_{\_}{k^{\prime}}\}}_{\_}k$, then you can decode the outer level and learn the value of $a$. But you cannot learn $b$ if it is encrypted by another key $k^{\prime}$ that you do not have. In fact, you might not even know that the message you received is of this form and only understand ${\{a,x\}}_{\_}k$. Such phenomena also happen in everyday communication. You may only get part of the meaning of a sentence, but by asking “what do you mean by …?” you can learn more.

After seeing the details of our framework one might wonder how it relates to other logics of ambiguity. We only mention two related works and leave more detailed comparisons for the future.

A semantic approach is [13] where agents are given different valuation functions to encode their disagreement about (ambiguous) atomic propositions. In our models with definitions there is no need for additional valuation functions and our approach is more syntactic. In our logic, knowing the meaning of a proposition is not reducible to knowing the valuation, e.g., two tautologies can still be very different definitionally. Moreover, we also handle uncertainty about the actual meaning of propositions and provide agents with a way to learn it by update and pattern matching.

Another related approach to model syntactic ambiguity is [15] where the meaning of connectives is not fixed. For example, an agent might wonder whether $p\ast q$ means $p\lor q$ or $p\land q$. A similar example could be modelled in our logic with $r\equiv(p\lor q)$ vs. $r\equiv(p\land q)$.

Finally, there are two obvious limitations of our logic. First, all definitions are boolean but in principle also modal definitions like $p:=\Box_{\_}jq$ are interesting. Second, as mentioned above, logical equivalence and equivalence by definition are not connected. For example, $\lnot(p\land q)$ and $\lnot p\lor\lnot q$ are logically equivalent, but due to the pattern mismatch axiom we can never have $\lnot(p\land q)\equiv(\lnot p\lor\lnot q)$. Depending on the application, users of our logic might consider this a problem or a feature. We think that our ideas can be extended in both directions, but leave this as future work.