Effective Preference Structures

[CL12] [Lau13] [CL16]

The agent's distinguished PreferenceStructure used to guide action choice ([CL16] (68): EP(a, w)). Distinguished from arbitrary preference structures by the consistency + realism axioms ([CL12] (66)–(67)).

structure Core.Order.EffectivePreference (W : Type u) (B : Set W) extends Core.Order.PreferenceStructure W : Type u

An effective preference structure at world w, relative to the agent's information state B : Set W: a PreferenceStructure that is consistent and realistic w.r.t. B.

• prefs : Set (Set W)
• prec : ↑self.prefs → ↑self.prefs → Prop
• isStrictOrder : IsStrictOrder (↑self.prefs) self.prec
• isConsistent : self.consistent B
• isRealistic : self.realistic B

@[reducible, inline]

abbrev Core.Order.EffectivePreference.effectivePrefs {W : Type u} {B : Set W} (E : EffectivePreference W B) : Set (Set W)

The agent's effective preferences: the maximal elements of the effective preference structure.

Equations

• E.effectivePrefs = E.maxElts

def Core.Order.EffectivePreference.ofConsistent {W : Type u} {B : Set W} (P : PreferenceStructure W) (hC : P.consistent B) : EffectivePreference W B

Smart constructor: realism is derivable from consistency (PreferenceStructure.consistent_implies_realistic).

Equations

• Core.Order.EffectivePreference.ofConsistent P hC = { toPreferenceStructure := P, isConsistent := hC, isRealistic := ⋯ }