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

Metatheory. Captures bounded rationality. Various axiom systems. Decidable. Models unawareness properly. Interactive unawareness subtle.

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

Limitations. Multiple formalizations. Introspection of unawareness problematic. Dynamic awareness complex. Philosophy debates.