Awareness Logic: A Kripke-based Rendition of the Heifetz-Meier-Schipper Model

TL;DR

This paper introduces a Kripke-based awareness logic that models uncertainty and unawareness separately, providing a formal, language-based framework that is equivalent to the existing HMS lattice model.

Contribution

It presents a new Kripke model framework for awareness that separates uncertainty from unawareness and proves their equivalence to the HMS lattice model.

Findings

Models are equivalent via satisfaction-preserving transformations.

The new model achieves completeness results similar to HMS.

Uncertainty and unawareness are represented distinctly.

Abstract

Heifetz, Meier and Schipper (HMS) present a lattice model of awareness. The HMS model is syntax-free, which precludes the simple option to rely on formal language to induce lattices, and represents uncertainty and unawareness with one entangled construct, making it difficult to assess the properties of either. Here, we present a model based on a lattice of Kripke models, induced by atom subset inclusion, in which uncertainty and unawareness are separate. We show the models to be equivalent by defining transformations between them which preserve formula satisfaction, and obtain completeness through our and HMS' results.