Preference Structures

@cite{condoravdi-lauer-2012} @cite{lauer-2013} @cite{condoravdi-lauer-2016} @cite{condoravdi-lauer-2011}

A preference structure (@cite{condoravdi-lauer-2012} (65)) is a pair ⟨P, ≺⟩ where P ⊆ ℘(W) is a set of propositions and ≺ is a strict partial order on P.

Layout

• PreferenceStructure W — the bare carrier; a strict order on prefs.Elem packaged as an IsStrictOrder instance for compatibility with mathlib's order API.
• maxElts (eq. 70) — maximal elements, returned as Set (Set W) so consumers don't have to package membership proofs.
• consistent (B : Set W) (eq. 66) — strong, subset-quantified version (distinct from the pairwise consistent of @cite{condoravdi-lauer-2011}; fn. 29 of the anankastics paper). Quantifies over arbitrary X ⊆ prefs.
• realistic (B : Set W) (eq. 67) — preferences are belief-compatible.
• consistent_implies_realistic — eq. 67 derived from eq. 66 via the singleton-X case.

structure Core.Order.PreferenceStructure (W : Type u) : Type u

A preference structure: a set of propositions equipped with a strict partial order on the subtype.

prec : prefs → prefs → Prop is typed on the subtype, so the IsStrictOrder instance is meaningful (no vacuous-off-prefs trap). For ergonomic raw access, use prec p q with elements of prefs.Elem (i.e., ⟨_, _⟩ packaged with their membership proof).

• prefs : Set (Set W)

  The propositions the agent has preferences over.

• prec : ↑self.prefs → ↑self.prefs → Prop

  The strict ranking on the subtype of preferences. prec p q reads "q is strictly preferred to p".

• isStrictOrder : IsStrictOrder (↑self.prefs) self.prec

  The strict-partial-order axioms, packaged as a mathlib typeclass.

instance Core.Order.PreferenceStructure.instIsStrictOrderElemSetPrefsPrec {W : Type u} (P : PreferenceStructure W) : IsStrictOrder (↑P.prefs) P.prec

def Core.Order.PreferenceStructure.maxElts {W : Type u} (P : PreferenceStructure W) : Set (Set W)

The maximal elements of the preference structure (@cite{condoravdi-lauer-2016} (70)), returned as propositions in Set (Set W).

Equations

• P.maxElts = Subtype.val '' {p : ↑P.prefs | ∀ (q : ↑P.prefs), ¬P.prec p q}

theorem Core.Order.PreferenceStructure.maxElts_subset_prefs {W : Type u} (P : PreferenceStructure W) : P.maxElts ⊆ P.prefs

theorem Core.Order.PreferenceStructure.mem_maxElts {W : Type u} (P : PreferenceStructure W) {φ : Set W} : φ ∈ P.maxElts ↔ ∃ (hp : φ ∈ P.prefs), ∀ (q : ↑P.prefs), ¬P.prec ⟨φ, hp⟩ q

Membership in maxElts unwrapped: φ is maximal iff it's in prefs and no preference in prefs is strictly above it.

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

Consistency w.r.t. an information state B (@cite{condoravdi-lauer-2016} (66)): for any subfamily of preferences whose joint realization is incompatible with B, some pair is strictly ranked. The quantification over arbitrary X ⊆ prefs (not just pairs) is the strong form, distinct from @cite{condoravdi-lauer-2011}'s pairwise variant (fn. 29).

Equations

• P.consistent B = ∀ X ⊆ P.prefs, B ∩ ⋂ p ∈ X, p = ∅ → ∃ p ∈ X, ∃ q ∈ X, ∃ (hp : p ∈ P.prefs) (hq : q ∈ P.prefs), P.prec ⟨p, hp⟩ ⟨q, hq⟩

def Core.Order.PreferenceStructure.realistic {W : Type u} (P : PreferenceStructure W) (B : Set W) : Prop

Realism w.r.t. an information state (@cite{condoravdi-lauer-2016} (67)): every preference is belief-compatible.

Equations

• P.realistic B = ∀ p ∈ P.prefs, p ∩ B ≠ ∅

theorem Core.Order.PreferenceStructure.consistent_implies_realistic {W : Type u} (P : PreferenceStructure W) {B : Set W} (hC : P.consistent B) : P.realistic B

@cite{condoravdi-lauer-2016} fn. 30: realism follows from consistency via the singleton-X case combined with irreflexivity.

theorem Core.Order.PreferenceStructure.maxElts_pair_belief_compatible {W : Type u} (P : PreferenceStructure W) {B : Set W} (hC : P.consistent B) {φ ψ : Set W} (hφ : φ ∈ P.maxElts) (hψ : ψ ∈ P.maxElts) : φ ∩ ψ ∩ B ≠ ∅

Pair belief-consistency of maximal preferences — abstract version of @cite{condoravdi-lauer-2016} p. 30 (end of § 5.4): given consistent B, two maximal preferences cannot have an empty intersection w.r.t. B. The four cases of the consistency conclusion ∃ p, q ∈ {φ, ψ}, prec p q are blocked by IsStrictOrder irreflexivity (diagonal pairs) and maximality (off-diagonal pairs).