Preference in attitude semantics

The two mathematizations of preference that attitude semantics runs on, gathered: qualitative preference orderings on propositions and quantitative preference degrees measured against thresholds.

A preference structure ([CL12] (65)) is a pair ⟨P, ≺⟩ where P ⊆ ℘(W) is a set of propositions and ≺ is a strict partial order — the mathematical spine of Condoravdi & Lauer's effective-preference framework ([CL11], [Lau13], [CL16]), consumed by the want semantics in Desire.lean and the dynamic necessity operator of Semantics/Dynamic/UpdateSemantics/Necessity.lean. maxElts (their eq. 70) collects the maximal elements. Relative to an information state B, consistent (eq. 66) demands that any subfamily of preferences jointly incompatible with B contain a strictly ranked pair, and realistic (eq. 67) — derivable from consistency (consistent_implies_realistic, their fn. 30) — demands every preference be belief-compatible. maxElts_pair_belief_compatible is the conflicting-desires blocker: two maximal preferences of a consistent structure meet inside B. maxInducedLe is the world-side preorder induced by maximal preferences, the Kratzer-style ([Kra81]) derivation of a world ordering from an ordering source.

A preferential predicate ([Vil08]) measures preference as a degree: ⟦x V p⟧(C) = μ(x, p) > θ(C), for a preference degree function μ and a contextual threshold θ over a comparison class C. [QOR+25] classify non-veridical preferentials by clausal distributivity (Distributivity.IsDistributive) and evaluative valence: the degree-comparison predicates built here are distributive by construction (mkDegreeComparison_isDistributive), while worry and Mandarin qidai carry an extra global condition on the question that breaks distributivity (worry_not_distributive). ThresholdSignificance is the presupposition [US19] posit for degree constructions — triggered by positive preferentials, not by negative ones ([QOR+25] §3.2) — from which the anti-rogativity of the distributive positive class is derived in Studies/UegakiSudo2019.lean; the classification's cross-linguistic support lives in Studies/QingEtAl2025.lean, and the emotive doxastic refinement of hope and fear ([AH13]) in Studies/AnandHacquard2013.lean.

structure PreferenceStructure (W : Type u_2) : Type u_2

A preference structure: a set of propositions prefs and a strict ranking prec, with prec p q read "q is strictly preferred to p". The ranking is a relation on all of Set W; 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. 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: 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

Consistency w.r.t. an information state B: any subfamily of preferences whose joint realization is incompatible with B contains a strictly ranked pair.

Equations

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

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

Realism w.r.t. an information state: every preference is belief-compatible.

Equations

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

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

Realism follows from consistency via the singleton-X case combined with irreflexivity.

theorem PreferenceStructure.maxElts_pair_belief_compatible {W : Type u_1} (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: given consistent B, two maximal preferences cannot have an empty intersection w.r.t. B. The four cases of the consistency conclusion are blocked by irreflexivity (diagonal pairs) and maximality (off-diagonal pairs).

The world preorder induced by maximal preferences

def PreferenceStructure.maxInducedLe {W : Type u_1} (P : PreferenceStructure W) : W → W → Prop

The world-level preorder induced by maximal preferences: maxInducedLe w v iff w verifies every maximal preference that v verifies.

Equations

• P.maxInducedLe w v = ∀ p ∈ P.maxElts, v ∈ p → w ∈ p

theorem PreferenceStructure.maxInducedLe_refl {W : Type u_1} (P : PreferenceStructure W) (w : W) : P.maxInducedLe w w

theorem PreferenceStructure.maxInducedLe_trans {W : Type u_1} (P : PreferenceStructure W) {w v u : W} (hwv : P.maxInducedLe w v) (hvu : P.maxInducedLe v u) : P.maxInducedLe w u

Degree-comparison preferential predicates

structure Preferential.PreferentialPredicate (W : Type u_4) (E : Type u_5) : Type (max u_4 u_5)

A preferential attitude predicate: an evaluative valence, a preference degree function, a contextual threshold, and propositional and question semantics relative to a comparison class of propositions.

• valence : Features.AttitudeValence

  Evaluative valence (positive for hope, negative for fear).

• μ : E → Finset W → ℚ

  Preference degree function: μ x p is how strongly x prefers (or, for negative valence, dreads) p.

• θ : List (Finset W) → ℚ

  Contextual threshold over a comparison class.

• propSemantics : E → Finset W → List (Finset W) → Prop

  ⟦x V p⟧(C), the propositional semantics.

• questionSemantics : E → List (Finset W) → List (Finset W) → Prop

  ⟦x V Q⟧(C), the question semantics.

def Preferential.PreferentialPredicate.IsDistributive {W : Type u_2} {E : Type u_3} (V : PreferentialPredicate W E) : Prop

A preferential predicate is clausally distributive when its question semantics is the existential over its propositional semantics — the world-free instance of Distributivity.IsDistributive (preferential semantics are world-independent because the predicates are non-veridical).

Equations

• V.IsDistributive = ∀ (x : E) (Q C : List (Finset W)), V.questionSemantics x Q C ↔ ∃ p ∈ Q, V.propSemantics x p C

Degree-comparison predicates

def Preferential.mkDegreeComparison {W : Type u_2} {E : Type u_3} (valence : Features.AttitudeValence) (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) : PreferentialPredicate W E

Degree-comparison predicate ([Vil08]): ⟦x V p⟧(C) = μ(x, p) > θ(C), with the question semantics the pointwise existential.

Equations

• One or more equations did not get rendered due to their size.

theorem Preferential.mkDegreeComparison_isDistributive {W : Type u_2} {E : Type u_3} (valence : Features.AttitudeValence) (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) : (mkDegreeComparison valence μ θ).IsDistributive

Degree-comparison predicates are clausally distributive by construction: the question semantics is the existential over the propositional semantics.

def Preferential.hope {W : Type u_2} {E : Type u_3} (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) : PreferentialPredicate W E

hope: degree comparison, positive valence. What distinguishes hope from want is an additional doxastic component ([AH13]), formalized in Studies/AnandHacquard2013.lean.

Equations

• Preferential.hope μ θ = Preferential.mkDegreeComparison Features.AttitudeValence.positive μ θ

def Preferential.fear {W : Type u_2} {E : Type u_3} (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) : PreferentialPredicate W E

fear: degree comparison, negative valence.

Equations

• Preferential.fear μ θ = Preferential.mkDegreeComparison Features.AttitudeValence.negative μ θ

def Preferential.expect {W : Type u_2} {E : Type u_3} (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) : PreferentialPredicate W E

expect: degree comparison, positive valence.

Equations

• Preferential.expect μ θ = Preferential.mkDegreeComparison Features.AttitudeValence.positive μ θ

def Preferential.wish {W : Type u_2} {E : Type u_3} (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) : PreferentialPredicate W E

wish: degree comparison, positive valence.

Equations

• Preferential.wish μ θ = Preferential.mkDegreeComparison Features.AttitudeValence.positive μ θ

def Preferential.dread {W : Type u_2} {E : Type u_3} (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) : PreferentialPredicate W E

dread: degree comparison, negative valence.

Equations

• Preferential.dread μ θ = Preferential.mkDegreeComparison Features.AttitudeValence.negative μ θ

Non-distributive preferentials

def Preferential.worry {W : Type u_2} {E : Type u_3} (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) (Uncertain : E → List (Finset W) → Prop) : PreferentialPredicate W E

worry: propositionally a degree comparison, but the question semantics adds a global uncertainty condition on the question — not reducible to the existential over answers ([QOR+25] §3.1.2).

Equations

• One or more equations did not get rendered due to their size.

def Preferential.qidai {W : Type u_2} {E : Type u_3} (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) (AnticipatesResolution : E → List (Finset W) → Prop) : PreferentialPredicate W E

Mandarin qidai "look forward to": positive valence, with an anticipation-of-resolution condition on the question — a positive non-distributive preferential ([QOR+25] §3.1.1).

Equations

• One or more equations did not get rendered due to their size.

theorem Preferential.worry_not_distributive {W : Type u_2} {E : Type u_3} (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) (Uncertain : E → List (Finset W) → Prop) (x : E) (Q C : List (Finset W)) (hu : ¬Uncertain x Q) (h : ∃ p ∈ Q, μ x p > θ C) : ¬(worry μ θ Uncertain).IsDistributive

worry is not clausally distributive: when the agent is not uncertain about Q but some answer clears the threshold, the existential over the propositional semantics holds while the question semantics fails.

Threshold significance

def Preferential.ThresholdSignificance {W : Type u_2} {E : Type u_3} (μ : E → Finset W → ℚ) (θ : List (Finset W) → ℚ) (x : E) (C : List (Finset W)) : Prop

The Threshold Significance Presupposition ([US19]): some member of the comparison class clears the threshold. Degree constructions presuppose it generally; positive preferentials trigger it while negative ones do not ([QOR+25] §3.2), which is how fear-type predicates escape the anti-rogativity triviality derived in Studies/UegakiSudo2019.lean.

Equations

• Preferential.ThresholdSignificance μ θ x C = ∃ p ∈ C, μ x p > θ C