Effective-preference desire semantics

a wants φ holds at w iff some maximal preference of a's preferential background P a w stands in a designated relation to φ — [CL16]'s analysis, where the background plays the role of a Kratzerian conversational background ([CL11], [CL12], [Lau13], [LC14]). The relation fixes the reading: identity is the canonical exact-match reading (Want); reverse inclusion gives a preference satisfied if φ holds (WantSufficient, their success-oriented reading), which is downward entailing in φ; inclusion gives a preference satisfied only if φ holds (WantNecessary, their Quine–Hintikka reading), which is upward entailing. Blocking of simultaneous want φ and want ¬φ over a consistent background is PreferenceStructure.maxElts_pair_belief_compatible.

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

Exact-match want: φ itself is a maximal preference, φ ∈ max[P(a, w)].

Equations

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

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

Some maximal preference is entailed by φ: a preference satisfied if φ holds.

Equations

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

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

Some maximal preference entails φ: a preference 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_1} {W : Type u_2} {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_1} {W : Type u_2} {P : Agent → W → PreferenceStructure W} {a : Agent} {φ : Set W} {w : W} (h : Want P a φ w) : WantNecessary P a φ w

theorem Desire.Preferential.WantSufficient.anti {Agent : Type u_1} {W : Type u_2} {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_1} {W : Type u_2} {P : Agent → W → PreferenceStructure W} {a : Agent} {φ : Set W} {w : W} {ψ : Set W} (hφψ : φ ⊆ ψ) (h : WantNecessary P a φ w) : WantNecessary P a ψ w