Logic of Awareness for Nested Knowledge

TL;DR

This work addresses the gap between human-like, limited reasoning and standard epistemic logic by introducing Awareness Logic with Partitions and Chains ($ALPC$). It extends Kripke semantics with an awareness-based indistinguishability relation and a finite chain of belief for awareness to model nested explicit knowledge, alongside a rich language that includes $A_{\\theta}$, $I_i$, $[\\approx]_{\\theta}$, $C_{\\theta}$, and $E_{\\theta}$. A Hilbert-style calculus for $ALPC$ is developed and shown to be sound and complete via a divided-canonical-model construction that accommodates global awareness and nested viewpoints. The framework provides a formal tool for analyzing strategic reasoning in multi-agent contexts with incomplete awareness, with potential applications in computer science and game theory for describing and analyzing agent communication and behavior.

Abstract

Reasoning abilities of human beings are limited. Logics that treat logical inference for human knowledge should reflect these limited abilities. Logic of awareness is one of those logics. In the logic, what an agent with a limited reasoning ability actually knows at a given moment (explicit knowledge) is distinguished from the ideal knowledge that an agent obtains by performing all possible inferences with what she already knows (implicit knowledge). This paper proposes a logic for explicit knowledge. In particular, we focus more on nested explicit knowledge, which means another agent's knowledge that an agent actually knows at a given moment. We develope a new formalization of two ideas and propose Kripke-style semantics. The first idea is the effect on an agent's reasoning ability by a state of an agent's awareness. We incorporate a relation on possible worlds called an indistinguishable relation to represent ignorance due to lack of awareness. The second idea is a state of each agent's awareness in the other agent's mind. We incorporate a non-empty finite sequence of agents called \textit{a chain of belief for awareness}. Our logic is called Awareness Logic with Partitions and Chains (ALPC). Employing an example, we show how nested explicit knowledge is formalized with our logic. Thereafter, we propose the proof system and prove the completeness. Finally, we discuss directions for extending and applying our logic and conclude. Our logic offers a foundation for a formal representation of human knowledge. We expect that the logic can be applied to computer science and game theory by describing and analyzing strategic behavior in a game and practical agent communication.

Figures (2)

• Figure 1: A two multi-agent model in which a set of possible worlds is $\{w_1,w_2,w_3\}$. Propositions inside a possible world are true propositions in the world. An arrow represents an accessibility relation. Reflexive arrows are omitted. Agent $a$ is aware of $p$ and $q$, but agent $b$ is only aware of $p$. Rounded rectangles that contain a proposition refer to that $b$ is aware of the proposition. A rounded rectangle that contains worlds refers to $b$ does not distinguish the worlds.
• Figure 2:

Theorems & Definitions (35)

• Example 1
• Definition 1
• Definition 2
• Definition 3
• Definition 4
• Definition 5
• Theorem 1
• proof
• Definition 6
• Lemma 1