Preference structures

A preference structure, in the sense of Condoravdi and Lauer, is a set of propositions with a strict ranking by importance. A structure is consistent with an information state when any family of its preferences that the information rules out jointly contains a strictly ranked pair, and realistic when each preference is compatible with the information. Consistency entails realism and makes the maximal preferences jointly realizable.

Want relates an agent to the maximal elements of the effective preference structure its context supplies, which plays the role of a Kratzerian conversational background. Its readings differ in how a maximal preference relates to the complement: identity is the exact-match reading, a preference the complement entails gives the success-oriented reading, downward entailing in the complement, and a preference that entails the complement gives the Quine–Hintikka reading, upward entailing. Over a consistent background, want φ and want ¬φ do not hold together on the exact-match reading.

Main definitions

• PreferenceStructure, with maxElts, Consistent and Realistic.
• PreferenceStructure.discrete, PreferenceStructure.rankBelow: the unranked structure on a set of preferences, and the one that ranks a single preference below another.
• Desire.Preferential.Want, Desire.Preferential.WantSufficient, Desire.Preferential.WantNecessary: the exact-match, success-oriented and Quine–Hintikka readings of want.

Main statements

• PreferenceStructure.Consistent.realistic: consistency entails realism.
• PreferenceStructure.Consistent.inter_sInter_maxElts_nonempty: the maximal preferences of a consistent structure are jointly compatible with the information.
• PreferenceStructure.consistent_of_realistic_of_isChain: a realistic chain is consistent.
• Desire.Preferential.WantSufficient.anti, Desire.Preferential.WantNecessary.mono: the success-oriented reading is downward and the Quine–Hintikka reading upward entailing.
• Desire.Preferential.Want.not_compl: over a consistent background, a proposition and its negation are not both wanted.

Implementation notes

The ranking is a strict order on all of Set W, of which only its restriction to the preferences is observed.

References

• [CL11]
• [CL12]
• [CL16]
• [Lau13]
• [LC14]
• [Kra81b]

structure PreferenceStructure (W : Type u_2) : Type u_2

A preference structure is a set of propositions prefs with a strict ranking prec, where prec p q reads "q is strictly preferred to p". The ranking is a relation on all of Set W, and only its restriction to prefs is ever observed.

• prefs : Set (Set W)

  The propositions the agent has preferences over.

• prec : Set W → Set W → Prop

  The strict ranking, where prec p q reads "q is strictly preferred to p".

• isStrictOrder : IsStrictOrder (Set W) self.prec

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

instance PreferenceStructure.instIsStrictOrderSetPrec {W : Type u_1} (P : PreferenceStructure W) : IsStrictOrder (Set W) P.prec

def PreferenceStructure.maxElts {W : Type u_1} (P : PreferenceStructure W) : Set (Set W)

The maximal elements of the preference structure are the preferences with nothing in prefs strictly above them.

Equations

• P.maxElts = {p : Set W | p ∈ P.prefs ∧ ∀ q ∈ P.prefs, ¬P.prec p q}

@[simp]

theorem PreferenceStructure.mem_maxElts {W : Type u_1} (P : PreferenceStructure W) {φ : Set W} : φ ∈ P.maxElts ↔ φ ∈ P.prefs ∧ ∀ q ∈ P.prefs, ¬P.prec φ q

theorem PreferenceStructure.maxElts_subset_prefs {W : Type u_1} (P : PreferenceStructure W) : P.maxElts ⊆ P.prefs

def PreferenceStructure.Consistent {W : Type u_1} (P : PreferenceStructure W) (B : Set W) : Prop

A preference structure is consistent with respect to an information state B when any subfamily of preferences whose joint realization is incompatible with B contains a strictly ranked pair.

Equations

• P.Consistent B = ∀ X ⊆ P.prefs, B ∩ ⋂₀ X = ∅ → ∃ p ∈ X, ∃ q ∈ X, P.prec p q

def PreferenceStructure.Realistic {W : Type u_1} (P : PreferenceStructure W) (B : Set W) : Prop

A preference structure is realistic with respect to an information state when every preference is compatible with it.

Equations

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

theorem PreferenceStructure.Consistent.mono {W : Type u_1} {P : PreferenceStructure W} {B H : Set W} (hC : P.Consistent B) (h : B ⊆ H) : P.Consistent H

Consistency relative to an information state persists to any weaker one.

theorem PreferenceStructure.Consistent.realistic {W : Type u_1} {P : PreferenceStructure W} {B : Set W} (hC : P.Consistent B) : P.Realistic B

Consistency entails realism, by the singleton subfamilies and irreflexivity.

theorem PreferenceStructure.Consistent.nonempty {W : Type u_1} {P : PreferenceStructure W} {B : Set W} (hC : P.Consistent B) : B.Nonempty

A consistent structure has a nonempty information state, as the empty subfamily shows.

theorem PreferenceStructure.Consistent.prec_of_mem_maxElts {W : Type u_1} {P : PreferenceStructure W} {B : Set W} (hC : P.Consistent B) {p q : Set W} (hp : p ∈ P.maxElts) (hq : q ∈ P.prefs) (h : B ∩ (p ∩ q) = ∅) : P.prec q p

A preference incompatible with a maximal one is ranked strictly below it.

theorem PreferenceStructure.Consistent.inter_sInter_maxElts_nonempty {W : Type u_1} {P : PreferenceStructure W} {B : Set W} (hC : P.Consistent B) : (B ∩ ⋂₀ P.maxElts).Nonempty

The maximal preferences of a consistent structure are jointly belief-compatible.

theorem PreferenceStructure.Consistent.inter_inter_nonempty_of_mem_maxElts {W : Type u_1} {P : PreferenceStructure W} {B : Set W} (hC : P.Consistent B) {φ ψ : Set W} (hφ : φ ∈ P.maxElts) (hψ : ψ ∈ P.maxElts) : (B ∩ (φ ∩ ψ)).Nonempty

Two maximal preferences of a consistent structure are jointly belief-compatible, which blocks conflicting desires.

theorem PreferenceStructure.consistent_of_realistic_of_isChain {W : Type u_1} {P : PreferenceStructure W} {B : Set W} (hR : P.Realistic B) (hc : IsChain P.prec P.prefs) (hB : B.Nonempty) : P.Consistent B

A chain of realistic preferences is consistent.

Unranked preferences

def PreferenceStructure.discrete {W : Type u_1} (S : Set (Set W)) : PreferenceStructure W

The discrete structure has the preferences S and no ranking, so all of them are maximal.

Equations

• PreferenceStructure.discrete S = { prefs := S, prec := fun (x x_1 : Set W) => False, isStrictOrder := ⋯ }

@[simp]

theorem PreferenceStructure.maxElts_discrete {W : Type u_1} (S : Set (Set W)) : (discrete S).maxElts = S

theorem PreferenceStructure.consistent_discrete {W : Type u_1} {S : Set (Set W)} {B : Set W} (h : (B ∩ ⋂₀ S).Nonempty) : (discrete S).Consistent B

Unranked preferences are consistent when jointly belief-compatible.

@[reducible, inline]

abbrev PreferenceStructure.single {W : Type u_1} (p : Set W) : PreferenceStructure W

The structure with the single preference p.

Equations

• PreferenceStructure.single p = PreferenceStructure.discrete {p}

@[simp]

theorem PreferenceStructure.maxElts_single {W : Type u_1} (p : Set W) : (single p).maxElts = {p}

theorem PreferenceStructure.consistent_single {W : Type u_1} {p B : Set W} (h : (p ∩ B).Nonempty) : (single p).Consistent B

Ranking one preference below another

def PreferenceStructure.rankBelow {W : Type u_1} (S : Set (Set W)) {p q : Set W} (h : p ≠ q) : PreferenceStructure W

The structure on S that ranks p strictly below q and leaves the rest unranked.

Equations

• PreferenceStructure.rankBelow S h = { prefs := S, prec := fun (r s : Set W) => r = p ∧ s = q, isStrictOrder := ⋯ }

theorem PreferenceStructure.maxElts_rankBelow {W : Type u_1} {S : Set (Set W)} {p q : Set W} (h : p ≠ q) (hq : q ∈ S) : (rankBelow S h).maxElts = S \ {p}

Once q is a preference, everything but p is maximal.

theorem PreferenceStructure.consistent_rankBelow {W : Type u_1} {S : Set (Set W)} {p q : Set W} (h : p ≠ q) {B : Set W} (hp : (B ∩ ⋂₀ (S \ {p})).Nonempty) (hq : (B ∩ ⋂₀ (S \ {q})).Nonempty) : (rankBelow S h).Consistent B

Ranking p below q resolves every conflict when the preferences without p and those without q are each jointly compatible with the information.

Effective-preference want

def Desire.Preferential.Want {Agent : Type u_2} {W : Type u_3} (P : Agent → W → PreferenceStructure W) (a : Agent) (φ : Set W) (w : W) : Prop

On the exact-match reading, a wants φ at w when φ is itself a maximal preference of the background P a w.

Equations

• Desire.Preferential.Want P a φ w = (φ ∈ (P a w).maxElts)

def Desire.Preferential.WantSufficient {Agent : Type u_2} {W : Type u_3} (P : Agent → W → PreferenceStructure W) (a : Agent) (φ : Set W) (w : W) : Prop

On the success-oriented reading, a wants φ when φ entails a maximal preference, which φ then satisfies.

Equations

• Desire.Preferential.WantSufficient P a φ w = ∃ p ∈ (P a w).maxElts, φ ⊆ p

def Desire.Preferential.WantNecessary {Agent : Type u_2} {W : Type u_3} (P : Agent → W → PreferenceStructure W) (a : Agent) (φ : Set W) (w : W) : Prop

On the Quine–Hintikka reading, a wants φ when a maximal preference entails φ, so that the preference is satisfied only if φ holds.

Equations

• Desire.Preferential.WantNecessary P a φ w = ∃ p ∈ (P a w).maxElts, p ⊆ φ

theorem Desire.Preferential.Want.wantSufficient {Agent : Type u_2} {W : Type u_3} {P : Agent → W → PreferenceStructure W} {a : Agent} {φ : Set W} {w : W} (h : Want P a φ w) : WantSufficient P a φ w

theorem Desire.Preferential.Want.wantNecessary {Agent : Type u_2} {W : Type u_3} {P : Agent → W → PreferenceStructure W} {a : Agent} {φ : Set W} {w : W} (h : Want P a φ w) : WantNecessary P a φ w

theorem Desire.Preferential.Want.not_compl {Agent : Type u_2} {W : Type u_3} {P : Agent → W → PreferenceStructure W} {a : Agent} {φ : Set W} {w : W} {B : Set W} (hC : (P a w).Consistent B) (h : Want P a φ w) : ¬Want P a φᶜ w

Over a consistent background a proposition and its negation are not both wanted.

theorem Desire.Preferential.WantSufficient.anti {Agent : Type u_2} {W : Type u_3} {P : Agent → W → PreferenceStructure W} {a : Agent} {φ : Set W} {w : W} {ψ : Set W} (hφψ : φ ⊆ ψ) (h : WantSufficient P a ψ w) : WantSufficient P a φ w

theorem Desire.Preferential.WantNecessary.mono {Agent : Type u_2} {W : Type u_3} {P : Agent → W → PreferenceStructure W} {a : Agent} {φ : Set W} {w : W} {ψ : Set W} (hφψ : φ ⊆ ψ) (h : WantNecessary P a φ w) : WantNecessary P a ψ w