Condoravdi & Lauer: The Effective Preference Theory of want

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

The C&L analysis treats want as parameterized by a preferential background — analogous to Kratzer's modal base/ordering source. The distinguished background is the agent's effective preference function EP (Core.Order.EffectivePreference).

Layout

• PreferentialBackground, EffectivePreferentialBackground — types.
• wantP{Exact, Success, QH} — the three readings from @cite{condoravdi-lauer-2016} eq. 71. Exact-match is canonical (eq. 69) and implies the other two (wantPExact_implies_*).
• wantEP — exact-match against the effective preferential background.
• maxOrderingSource — Set-valued max[EP(Ad, w)] (eq. 88), the ordering source consumed by the inner modal in the double-modal anankastic analysis.

Anankastic-conditional analyses live in Phenomena/Conditionals/Studies/; imperative analyses (C&L 2012, contra @cite{roberts-2023}'s modal-in-LF account) in Phenomena/Directives/Studies/; discourse-particle uses (@cite{deo-2025-bara}) in Phenomena/SentenceMood/Studies/.

@[reducible, inline]

abbrev Semantics.Attitudes.CondoravdiLauer.PreferentialBackground (Agent W : Type u) : Type u

A preferential background: a function from agents and worlds to preference structures. The C&L analog of Kratzer's ConvBackground.

Equations

• Semantics.Attitudes.CondoravdiLauer.PreferentialBackground Agent W = (Agent → W → Core.Order.PreferenceStructure W)

@[reducible, inline]

abbrev Semantics.Attitudes.CondoravdiLauer.EffectivePreferentialBackground (Agent W : Type u) (B : Agent → W → Set W) : Type u

An effective preferential background returns, at each world, the agent's effective preference structure (consistent + realistic). @cite{condoravdi-lauer-2016} (68): EP(a, w).

Equations

• Semantics.Attitudes.CondoravdiLauer.EffectivePreferentialBackground Agent W B = ((a : Agent) → (w : W) → Core.Order.EffectivePreference W (B a w))

The semantics of want — three readings (@cite{condoravdi-lauer-2016} (71))

def Semantics.Attitudes.CondoravdiLauer.wantPExact {Agent W : Type u} (P : PreferentialBackground Agent W) (a : Agent) (φ : Set W) (w : W) : Prop

Exact-match (eq. 71c, the canonical reading; eq. 69): wantP(a, φ) iff φ ∈ max[P(a, w)].

Equations

• Semantics.Attitudes.CondoravdiLauer.wantPExact P a φ w = (φ ∈ (P a w).maxElts)

def Semantics.Attitudes.CondoravdiLauer.wantPSuccess {Agent W : Type u} (P : PreferentialBackground Agent W) (a : Agent) (φ : Set W) (w : W) : Prop

Success-oriented (eq. 71a): "satisfied if φ is true." Some maximal preference is entailed by φ.

Equations

• Semantics.Attitudes.CondoravdiLauer.wantPSuccess P a φ w = ∃ p ∈ (P a w).maxElts, φ ⊆ p

def Semantics.Attitudes.CondoravdiLauer.wantPQH {Agent W : Type u} (P : PreferentialBackground Agent W) (a : Agent) (φ : Set W) (w : W) : Prop

Quine-Hintikka (eq. 71b): "satisfied only if φ is true." Some maximal preference entails φ.

Equations

• Semantics.Attitudes.CondoravdiLauer.wantPQH P a φ w = ∃ p ∈ (P a w).maxElts, p ⊆ φ

theorem Semantics.Attitudes.CondoravdiLauer.wantPExact_implies_success {Agent W : Type u} {P : PreferentialBackground Agent W} {a : Agent} {φ : Set W} {w : W} (h : wantPExact P a φ w) : wantPSuccess P a φ w

theorem Semantics.Attitudes.CondoravdiLauer.wantPExact_implies_QH {Agent W : Type u} {P : PreferentialBackground Agent W} {a : Agent} {φ : Set W} {w : W} (h : wantPExact P a φ w) : wantPQH P a φ w

Monotonicity in φ (@cite{condoravdi-lauer-2016} p. 31)

The three readings differ in their entailment direction in the propositional argument:

• wantPSuccess is downward-entailing in φ (Zimmermann's note, cited p. 31): if φ ⊆ ψ and wantPSuccess holds for the weaker ψ, it holds for the stronger φ.
• wantPQH is upward-entailing in φ (explicit on p. 31): if φ ⊆ ψ and wantPQH holds for the stronger φ, it holds for the weaker ψ.
• wantPExact is neither upward- nor downward-entailing — see C&L's discussion of (62)/(63)/(64) on pp. 27–28. Counterexample-construction deferred.

theorem Semantics.Attitudes.CondoravdiLauer.wantPSuccess_downward_entailing {Agent W : Type u} {P : PreferentialBackground Agent W} {a : Agent} {φ ψ : Set W} {w : W} (hφψ : φ ⊆ ψ) (h : wantPSuccess P a ψ w) : wantPSuccess P a φ w

theorem Semantics.Attitudes.CondoravdiLauer.wantPQH_upward_entailing {Agent W : Type u} {P : PreferentialBackground Agent W} {a : Agent} {φ ψ : Set W} {w : W} (hφψ : φ ⊆ ψ) (h : wantPQH P a φ w) : wantPQH P a ψ w

def Semantics.Attitudes.CondoravdiLauer.wantEP {Agent W : Type u} {B : Agent → W → Set W} (EP : EffectivePreferentialBackground Agent W B) (a : Agent) (φ : Set W) (w : W) : Prop

Exact-match want against the effective preferential background.

Equations

• Semantics.Attitudes.CondoravdiLauer.wantEP EP a φ w = Semantics.Attitudes.CondoravdiLauer.wantPExact (fun (a : Agent) (w : W) => (EP a w).toPreferenceStructure) a φ w

theorem Semantics.Attitudes.CondoravdiLauer.wantEP_jointly_belief_consistent {Agent W : Type u} {B : Agent → W → Set W} (EP : EffectivePreferentialBackground Agent W B) {a : Agent} {φ ψ : Set W} {w : W} (hφ : wantEP EP a φ w) (hψ : wantEP EP a ψ w) : φ ∩ ψ ∩ B a w ≠ ∅

Joint belief-consistency of EP-want (@cite{condoravdi-lauer-2016} p. 30, end of § 5.4): "when want targets a preference structure P(a,w) that must be consistent — in particular, when it targets effective preferences — then wantP(a, φ) and wantP(a, ψ) are incompatible if φ and ψ are believed to be incompatible by agent a at w."

Stated contrapositively: if both wantEP EP a φ w and wantEP EP a ψ w hold, then φ ∩ ψ is not belief-empty — the agent does not believe that φ and ψ cannot jointly hold.

Proof: delegates to the abstract PreferenceStructure.maxElts_pair_belief_compatible lemma. The abstract version captures the same content at the order-theoretic level: any two maximal elements of a consistent preference structure are jointly belief-compatible.

def Semantics.Attitudes.CondoravdiLauer.maxOrderingSource {Agent W : Type u} {B : Agent → W → Set W} (EP : EffectivePreferentialBackground Agent W B) (Ad : Agent) : W → Set (Set W)

The set-valued ordering source at addressee Ad derived from an effective preferential background: at each world, the maximal preferences in EP(Ad, w). @cite{condoravdi-lauer-2016} (88): g_epA(w) = max[EP(Ad, w)].

Equations

• Semantics.Attitudes.CondoravdiLauer.maxOrderingSource EP Ad w = (EP Ad w).maxElts