[Las17a] (apparatus) / [Las11] (want application) — Expected-value desire

[Las17a] ch.7 ("Scalar goodness", not a desire chapter) develops an expected-value semantics for evaluative gradable predicates; [Las11] (NYU dissertation, ch.6) applies the apparatus to want. The book extends the good analysis to want in a single sentence at §8.13 (p.249) — want is gradable like like, matter, care, need.

This study file:

• §1 builds the bare-threshold conflict-witness model (4 worlds, uniform prior 1/4, V = (10, 4, 4, 0), θ = 3/2, p = {w₀, w₁}).
• §2 replicates the conflict predictions: want_p ∧ want_negp.
• §3 cross-paper bridge to [CL16]: C&L's consistency-driven belief-compatibility forbids the witness; the Lassiter bare apparatus exhibits it. Different mechanisms.
• §4 cross-paper bridge to [Hei92]: same configuration is Conditional.Defined-OK, but Conditional.Want.not_compl rules out joint truth. Heim's (40) amendment is the structural analog of Lassiter's Sloman.
• §5 Sloman's Principle blocks the witness for Lassiter's full account. The bare-threshold conflict witness is exactly Cariani's Weakening counter-model (Lassiter's Table 8.4 reconstruction of the [Car16] actualist Weakening attack, applied to EV; Cariani's own counter-model uses actualist closeness, not EV) p.239); Lassiter's response is Sloman's Principle, which excludes it. The witness is a falsifier of the bare form, not of Lassiter's actual position.

The chronological-dependency rule applies: this file references [PB25] only in docstring prose (PB is later); PhillipsBrown2025.lean already cross-references Lassiter via its BeliefBasedDesireSemantics typology (the paper's own §2 packaging, formalized in that study file).

§1. The 4-world conflict-witness model

Following [Las17a] §7.6 eq. 7.22 (apparatus) and [Las11] ch.6 (want application). Uniform prior over Fin 4; value function asymmetric on {w₀, w₁} vs {w₂, w₃}.

@[reducible, inline]

abbrev Lassiter2017Desire.W : Type

Worlds.

Equations

• Lassiter2017Desire.W = Fin 4

def Lassiter2017Desire.prior : W → ℚ

Uniform prior 1/4 over the 4 worlds.

Equations

• Lassiter2017Desire.prior x✝ = 1 / 4

def Lassiter2017Desire.value : W → ℚ

Value function: V(w₀) = 10, V(w₁) = 4, V(w₂) = 4, V(w₃) = 0.

Equations

• Lassiter2017Desire.value 0 = 10
• Lassiter2017Desire.value 1 = 4
• Lassiter2017Desire.value 2 = 4
• Lassiter2017Desire.value 3 = 0

def Lassiter2017Desire.threshold : ℚ

Threshold for "significantly above neutral" — Lassiter 2017 §7.9 treats this as contextually supplied.

Equations

• Lassiter2017Desire.threshold = 3 / 2

def Lassiter2017Desire.belTotal : Set W

The agent's belief state: total uncertainty (all worlds compatible). Matches Lassiter's D = epistemically possible worlds convention (§7.6 p.187).

Equations

• Lassiter2017Desire.belTotal = Set.univ

@[instance_reducible]

instance Lassiter2017Desire.instDecidablePredWMemSetBelTotal : DecidablePred fun (x : W) => x ∈ belTotal

Equations

• Lassiter2017Desire.instDecidablePredWMemSetBelTotal x✝ = isTrue trivial

def Lassiter2017Desire.targetProp : Set W

The target proposition p = {w₀, w₁}.

Equations

• Lassiter2017Desire.targetProp = {0, 1}

@[instance_reducible]

instance Lassiter2017Desire.instDecidablePredWMemSetTargetProp : DecidablePred fun (x : W) => x ∈ targetProp

Equations

• Lassiter2017Desire.instDecidablePredWMemSetTargetProp w = Lassiter2017Desire.instDecidablePredWMemSetTargetProp._aux_1 w

§2. The conflict predictions

E_V(p | belS) = (1/4 · 10 + 1/4 · 4) / (1/4 + 1/4) = (14/4) / (1/2) = 7 E_V(¬p | belS) = (1/4 · 4 + 1/4 · 0) / (1/4 + 1/4) = 1 / (1/2) = 2 With θ = 3/2, both are above threshold → both are wanted.

theorem Lassiter2017Desire.cell_targetProp : Desire.ExpectedValue.cell belTotal targetProp = {0, 1}

theorem Lassiter2017Desire.cell_targetProp_compl : Desire.ExpectedValue.cell belTotal targetPropᶜ = {2, 3}

theorem Lassiter2017Desire.want_p : Desire.ExpectedValue.Want prior value threshold belTotal targetProp

theorem Lassiter2017Desire.want_negp : Desire.ExpectedValue.Want prior value threshold belTotal targetPropᶜ

theorem Lassiter2017Desire.conflict_concrete : Desire.ExpectedValue.Want prior value threshold belTotal targetProp ∧ Desire.ExpectedValue.Want prior value threshold belTotal targetPropᶜ

§3. Cross-paper bridge: [CL16]

C&L's PreferenceStructure.maxElts_pair_belief_compatible says that for any preferential background P pointwise consistent with the belief state, Preferential.Want P a φ w ∧ Preferential.Want P a ψ w implies (φ ∩ ψ) ∩ B(a, w) ≠ ∅. Specialized to ψ = φᶜ: the intersection is empty, so simultaneous truth is impossible.

Lassiter's bare-threshold apparatus exhibits exactly such a configuration. The two frameworks make orthogonal predictions on the 4-world model.

theorem Lassiter2017Desire.condoravdiLauer_blocks_lassiter_witness {Agent : Type} {B : Agent → W → Set W} (P : Agent → W → PreferenceStructure W) (hC : ∀ (a : Agent) (w : W), (P a w).consistent (B a w)) (a : Agent) (w : W) (φ : Set W) (hφ : Desire.Preferential.Want P a φ w) (hnegφ : Desire.Preferential.Want P a φᶜ w) : False

C&L blocks any pair Want φ ∧ Want ¬φ over a consistent background — C&L cannot reproduce Lassiter's witness.

§4. Cross-paper bridge: [Hei92]

Heim's (40) amendment + comparative-belief semantics block simultaneous want p ∧ want ¬p (substrate's Conditional.Want.not_compl). The 4-world conflict witness configuration is Conditional.Defined-OK on targetProp (both p-worlds and ¬p-worlds are in belTotal), so Heim's no-go applies — and Heim's prediction differs from Lassiter's.

This is the analog: Heim's (40) plays the role for comparative-belief that Sloman plays for Lassiter — both block single-V/single-context conflict.

theorem Lassiter2017Desire.defined_on_witness : Desire.Conditional.Defined belTotal targetProp

theorem Lassiter2017Desire.heim_blocks_witness (F : Desire.Conditional.Frame W) (w_eval : W) [Std.Antisymm (F.pref w_eval)] (h : Desire.Conditional.Want F belTotal w_eval targetProp) : ¬Desire.Conditional.Want F belTotal w_eval targetPropᶜ

On the witness configuration, Heim's no-go theorem applies — for any frame with antisymmetric desirability, want cannot make both targetProp and its negation true.

§5. Sloman's Principle blocks the witness for Lassiter's full account

Per [Las17a] §8.11 (p.245): "we should not weaken the semantics to make room for the simultaneous truth of ought(φ) and ought(¬φ). Instead, we should allow that there are various, possibly conflicting sources of value..." Sloman's Principle (eq. 8.16, p.216) is the constraint that excludes single-V conflict.

On the witness model with alts = [targetProp, ¬targetProp]:

• E_V(targetProp) = 7, E_V(¬targetProp) = 2.
• Sloman for targetProp: requires 7 > 2 ✓.
• Sloman for ¬targetProp: requires 2 > 7 ✗.

So WantWithSloman blocks the conflict on this configuration — matching Lassiter's actual stated position. The bare-threshold witness is exhibited by conflict_concrete only because it ignores Sloman; Lassiter himself would say this is the wrong way to formalize his account.

def Lassiter2017Desire.targetFinset : Finset W

The target proposition as a Finset, derived from targetProp.

Equations

• Lassiter2017Desire.targetFinset = {x : Lassiter2017Desire.W | x ∈ Lassiter2017Desire.targetProp}

def Lassiter2017Desire.witnessAlts : List (Finset W)

The two-element alternative set for the witness model.

Equations

• Lassiter2017Desire.witnessAlts = [Lassiter2017Desire.targetFinset, Lassiter2017Desire.targetFinsetᶜ]

theorem Lassiter2017Desire.wantWithSloman_blocks_conflict_on_witness (h : Desire.ExpectedValue.WantWithSloman prior value threshold belTotal witnessAlts targetFinset) : ¬Desire.ExpectedValue.WantWithSloman prior value threshold belTotal witnessAlts targetFinsetᶜ

Lassiter's full account blocks the witness via Sloman's Principle (WantWithSloman.not_compl).