Awareness Logic

Origin. Fagin and Halpern (1988). Agents may be unaware of some propositions. Awareness function: what agent considers. Explicit vs implicit knowledge. Foundation for bounded reasoning.

Models. Awareness function A: agent → set of formulas. Can only know formulas one is aware of. Distinguishes implicit from explicit knowledge.

Formalism.

Awareness function: Aᵢ(s): set of formulas agent i is aware of at state s. Awareness closed under subformulas (typically).

Explicit knowledge: Xᵢφ: agent i explicitly knows φ Xᵢφ iff Kᵢφ ∧ Aᵢφ Must know it and be aware of it.

Implicit knowledge: Kᵢφ: standard epistemic knowledge Can implicitly know φ without awareness.

Awareness operator: Aᵢφ: agent i is aware of φ Propositional or formula-level awareness.

Axioms: Xᵢφ → Aᵢφ (explicit knowledge requires awareness) Kᵢφ ∧ Aᵢφ → Xᵢφ (awareness + implicit = explicit) Aᵢ(φ ∧ ψ) ↔ Aᵢφ ∧ Aᵢψ (awareness of parts)

Unawareness: Uᵢφ ≡ ¬Aᵢφ Agent doesn't consider φ possible.

Speculative knowledge: What agent would know if made aware. Counterfactual awareness.

Symbols.

Symbol	Unicode	Name	Meaning
Aᵢ	—	Aware	i is aware of
Xᵢ	—	Explicit	Explicitly knows
Kᵢ	—	Implicit	Implicitly knows
Uᵢ	—	Unaware	Not aware of
Aᵢ(s)	—	Awareness set	Formulas i is aware of at state s
¬	U+00AC	Negation	Uᵢφ as ¬Aᵢφ
∧	U+2227	Conjunction	Xᵢφ as Kᵢφ ∧ Aᵢφ
↔	U+2194	Biconditional	Closure of awareness under subformulas
≡	U+2261	Definitional equivalence	Abbreviation, not a connective

Metatheory. Fagin and Halpern's logic of general awareness (1988) keeps the implicit operator Kᵢ normal and defines explicit knowledge as Xᵢφ ≡ Kᵢφ ∧ Aᵢφ, with the awareness set an arbitrary function from agents and states to formulas. Because Aᵢ is unconstrained, Xᵢ obeys no distribution axiom and is not closed under implication, so explicit knowledge escapes logical omniscience while implicit knowledge does not; the resulting system is sound, complete and decidable. Dekel, Lipman and Rustichini (1998) proved that a single state space cannot carry non-trivial unawareness: any model satisfying plausibility (Uᵢφ → ¬Kᵢφ), KU-introspection (¬KᵢUᵢφ) and AU-introspection (Uᵢφ → UᵢUᵢφ) makes unawareness trivial, so an agent unaware of one proposition is unaware of every proposition. Heifetz, Meier and Schipper (2006) escape the impossibility by replacing the single space with a lattice of state spaces of differing expressive richness, and Halpern (2001) by decoupling awareness from knowledge — which is what Fagin and Halpern had already done syntactically.

Applies to. Bounded rationality. Game theory. Contract theory. Economics. AI agents. Limited reasoning.

Limitations. Awareness is a primitive. The function Aᵢ is stipulated state by state and the logic constrains it only by the optional closure under subformulas, so the framework records unawareness rather than explaining it and any pattern of awareness whatever is a model. Implicit knowledge remains fully omniscient, so the omniscience problem is relocated rather than solved: the agent still implicitly knows every validity, and Xᵢ avoids omniscience only because Aᵢ is arbitrary. KU-introspection encodes the point that an agent cannot know it is unaware of a specific proposition, so self-attributed ignorance of content is inexpressible, and by Dekel, Lipman and Rustichini the alternative is a single space with no unawareness at all. Becoming aware needs operators the static logic does not have, and interactive unawareness — reasoning about what others are unaware of — is where the single-space impossibility bites hardest.