Phillips-Brown (2025): Some-Things-Considered Desire

Phillips-Brown gives a question-based semantics for desire ascriptions. Conflicting ascriptions, you want to take a nap and you don't want to take a nap both true, falsify the belief-based semantics of Heim and von Fintel, which evaluate the agent's preferences over her whole belief set with no context sensitivity, and a context-sensitive preference relation that values whole worlds overgenerates, predicting you want to fail the exam wherever Nap is true. The proposal evaluates an ascription against a contextual question, a partition of the worlds: the answers compatible with the beliefs are ranked by the desires they entail, S wants p holds when every best answer entails p (Want), and the ascription is defined only if the question decides p, is diverse, does not stack the deck, and the beliefs are sensitive to it (Defined).

Main results

• vonFintel_no_conflict, heim_no_conflict: the belief-based semantics cannot make Nap and Not-nap both true.
• closure_under_doxastic_equivalence, cpr_overgenerates: on a belief-based semantics wanting the act is wanting its believed cost, Villalta's closure under doxastic equivalence.
• act_true, not_act_true, cost_undefined: Nap and Not-nap are each true in their own context, and Fail is undefined in the first.
• not_rain_deckstacked, deckstacked_excluded: the deck-stacked question of Lu's case is excluded by the anti-deckstacking constraint, which the level playing field satisfies.
• undefined_of_insensitive, want_strawsonEntails: an agent whose beliefs are insensitive to every question deciding p has S wants p undefined, which leaves the semantics Strawson upward monotone.
• want_bot_iff: on the finest question the semantics is the best-worlds one, Desire.BestWorlds.Want.

Implementation notes

• A question is a Setoid, its answers the cells; the question raised by a list of issues is their Setoid.ofProps, and p is considered relative to a question when the question decides it. Answers are ordered by the desires they entail, Kratzer's ordering with entailment as satisfaction (entailed), and the best answers are the MaximalFor elements of that valuation.
• The act, its benefit and its cost are the three issues of the nap and lobster cases (nap, feeling rested, failing the exam; eating the lobster, the gustatory experience, dying), the beliefs tying benefit and cost to the act, and the desires being the benefit and not the cost. The Anti-deckstacking Constraint quantifies over all propositions; read so, it admits only the finest partition (antiDeckstacking_univ_singleton), so it is restricted here to a list of salient propositions, the issues of each case.
• Heim's semantics is the conditional one, Desire.Conditional.Want. Levinson's expected-value comparison, the sufficient-desirability semantics of §2.4, and the Heimian question-based semantics of footnote 16 are prose.

References

• [PB25]
• [Hei92]
• [vF99a]
• [Vil08]
• [Yal18]
• [Kra81b]

Question-based desire (§3)

def PhillipsBrown2025.Live {W : Type u_1} (s : Setoid W) (bel : Set W) (w : W) : Prop

An answer, the cell of w, compatible with the beliefs.

Equations

• PhillipsBrown2025.Live s bel w = ∃ v ∈ s.cell w, v ∈ bel

@[reducible, inline]

abbrev PhillipsBrown2025.entailed {W : Type u_1} (G : List (Finset W)) (s : Setoid W) : W → Set (Finset W)

The desires an answer entails, by whose inclusion answers are ordered.

Equations

• PhillipsBrown2025.entailed G s = Preorder.satisfied (fun (w : W) (g : Finset W) => s.cell w ⊆ ↑g) {g : Finset W | g ∈ G}

def PhillipsBrown2025.Want {W : Type u_1} (G : List (Finset W)) (s : Setoid W) (bel p : Set W) : Prop

S wants p holds when every best live answer entails p.

Equations

• PhillipsBrown2025.Want G s bel p = ∀ (w : W), MaximalFor (PhillipsBrown2025.Live s bel) (PhillipsBrown2025.entailed G s) w → s.cell w ⊆ p

def PhillipsBrown2025.IsDiverse {W : Type u_1} (s : Setoid W) (p : Set W) : Prop

Some answer entails p and some entails ¬p.

Equations

• PhillipsBrown2025.IsDiverse s p = ((∃ (w : W), s.cell w ⊆ p) ∧ ∃ (w : W), s.cell w ⊆ pᶜ)

def PhillipsBrown2025.IsAntiDeckstacking {W : Type u_1} (N : List (Finset W)) (s : Setoid W) : Prop

Every salient proposition in N that some answer entails is itself decided.

Equations

• PhillipsBrown2025.IsAntiDeckstacking N s = ∀ q ∈ N, (∃ (w : W), s.cell w ⊆ ↑q) → s.Decides ↑q

def PhillipsBrown2025.IsBelSensitive {W : Type u_1} (s : Setoid W) (bel : Set W) : Prop

The beliefs discriminate among the answers when some answer is live and some is not.

Equations

• PhillipsBrown2025.IsBelSensitive s bel = ((∃ (w : W), PhillipsBrown2025.Live s bel w) ∧ ∃ (w : W), ¬PhillipsBrown2025.Live s bel w)

def PhillipsBrown2025.Defined {W : Type u_1} (N : List (Finset W)) (s : Setoid W) (bel p : Set W) : Prop

The four metasemantic constraints jointly.

Equations

• PhillipsBrown2025.Defined N s bel p = (s.Decides p ∧ PhillipsBrown2025.IsDiverse s p ∧ PhillipsBrown2025.IsAntiDeckstacking N s ∧ PhillipsBrown2025.IsBelSensitive s bel)

noncomputable def PhillipsBrown2025.want {W : Type u_1} (G N : List (Finset W)) (s : Setoid W) (bel p : Set W) : W → SignType

Question-based want as a trivalent proposition, with its definedness conditions as presupposition.

Equations

• PhillipsBrown2025.want G N s bel p = {_w : W | PhillipsBrown2025.Defined N s bel p}.indicator fun (x : W) => SignType.ofProp (PhillipsBrown2025.Want G s bel p)

@[instance_reducible]

instance PhillipsBrown2025.instDecidableLive {W : Type u_1} (s : Setoid W) (bel : Set W) [Fintype W] [DecidableRel ⇑s] [DecidablePred fun (x : W) => x ∈ bel] (w : W) : Decidable (Live s bel w)

Equations

• PhillipsBrown2025.instDecidableLive s bel w = { decide := decide (∃ a ∈ Finset.univ, (fun (v : W) => v ∈ s.cell w ∧ v ∈ bel) a), reflects_decide := ⋯ }

@[instance_reducible]

instance PhillipsBrown2025.instDecidableMaximalForSetFinsetLiveEntailed {W : Type u_1} (G : List (Finset W)) (s : Setoid W) (bel : Set W) [Fintype W] [DecidableEq W] [DecidableRel ⇑s] [DecidablePred fun (x : W) => x ∈ bel] (w : W) : Decidable (MaximalFor (Live s bel) (entailed G s) w)

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instDecidableWant {W : Type u_1} (G : List (Finset W)) (s : Setoid W) (bel p : Set W) [Fintype W] [DecidableEq W] [DecidableRel ⇑s] [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Want G s bel p)

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instDecidableIsDiverse {W : Type u_1} (s : Setoid W) (p : Set W) [Fintype W] [DecidableRel ⇑s] [DecidablePred fun (x : W) => x ∈ p] : Decidable (IsDiverse s p)

Equations

• PhillipsBrown2025.instDecidableIsDiverse s p = { decide := decide (∃ (w : W), s.cell w ⊆ p) && decide (∃ (w : W), s.cell w ⊆ pᶜ), reflects_decide := ⋯ }

@[instance_reducible]

instance PhillipsBrown2025.instDecidableIsAntiDeckstacking {W : Type u_1} (N : List (Finset W)) (s : Setoid W) [Fintype W] [DecidableEq W] [DecidableRel ⇑s] : Decidable (IsAntiDeckstacking N s)

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instDecidableIsBelSensitive {W : Type u_1} (s : Setoid W) (bel : Set W) [Fintype W] [DecidableRel ⇑s] [DecidablePred fun (x : W) => x ∈ bel] : Decidable (IsBelSensitive s bel)

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instDecidableDefined {W : Type u_1} (N : List (Finset W)) (s : Setoid W) (bel p : Set W) [Fintype W] [DecidableEq W] [DecidableRel ⇑s] [DecidablePred fun (x : W) => x ∈ bel] [DecidablePred fun (x : W) => x ∈ p] : Decidable (Defined N s bel p)

Equations

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

theorem PhillipsBrown2025.Want.mono {W : Type u_1} {G : List (Finset W)} {s : Setoid W} {bel p q : Set W} (hpq : p ⊆ q) (h : Want G s bel p) : Want G s bel q

theorem PhillipsBrown2025.exists_best {W : Type u_1} {G : List (Finset W)} {s : Setoid W} {bel : Set W} [Finite W] (h : ∃ (w : W), Live s bel w) : ∃ (w : W), MaximalFor (Live s bel) (entailed G s) w

A best live answer exists whenever some answer is live.

theorem PhillipsBrown2025.not_want_of_not_exists {W : Type u_1} {G : List (Finset W)} {s : Setoid W} {bel p : Set W} [Finite W] (hlive : ∃ (w : W), Live s bel w) (hp : ¬∃ (w : W), s.cell w ⊆ p) : ¬Want G s bel p

Without a p-answer the ascription is false as soon as some answer is live, which the diversity constraint against vacuous falsity rules out.

theorem PhillipsBrown2025.want_of_decides_of_not_exists {W : Type u_1} {G : List (Finset W)} {s : Setoid W} {bel p : Set W} (hc : s.Decides p) (hnp : ¬∃ (w : W), s.cell w ⊆ pᶜ) : Want G s bel p

With the question deciding p and no ¬p-answer the ascription is true, which the diversity constraint against vacuous truth rules out.

theorem PhillipsBrown2025.want_strawsonEntails {W : Type u_1} {G N : List (Finset W)} {s : Setoid W} {bel p q : Set W} (hpq : p ⊆ q) : Presupposition.strawsonEntails (want G N s bel p) (want G N s bel q)

The semantics is Strawson upward monotone, since where both ascriptions are defined, want p entails want q for p ⊆ q.

theorem PhillipsBrown2025.want_bot_iff {W : Type u_1} {G : List (Finset W)} {bel p : Set W} : Want G ⊥ bel p ↔ Desire.BestWorlds.Want ((fun (s : Finset W) (w : W) => w ∈ s) '' {s : Finset W | s ∈ G}) bel p

On the finest question, question-based want is best-worlds want (§3.4).

The nap and lobster cases (§2.1, §2.2)

structure PhillipsBrown2025.World : Type

A state records whether the act is done, whether its benefit obtains and whether its cost obtains.

• act : Bool
• benefit : Bool
• cost : Bool

@[instance_reducible]

instance PhillipsBrown2025.instDecidableEqWorld : DecidableEq World

Equations

• PhillipsBrown2025.instDecidableEqWorld = PhillipsBrown2025.instDecidableEqWorld.decEq

def PhillipsBrown2025.instDecidableEqWorld.decEq (x✝ x✝¹ : World) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instFintypeWorld : Fintype World

Equations

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

def PhillipsBrown2025.act : Finset World

The act is napping, or eating the lobster.

Equations

• PhillipsBrown2025.act = {x : PhillipsBrown2025.World | x.act = true}

def PhillipsBrown2025.benefit : Finset World

Its benefit is feeling rested, or the gustatory experience.

Equations

• PhillipsBrown2025.benefit = {x : PhillipsBrown2025.World | x.benefit = true}

def PhillipsBrown2025.cost : Finset World

Its cost is failing the exam, or dying of anaphylactic shock.

Equations

• PhillipsBrown2025.cost = {x : PhillipsBrown2025.World | x.cost = true}

def PhillipsBrown2025.bel : Set World

The beliefs have the benefit and the cost each come exactly with the act.

Equations

• PhillipsBrown2025.bel = {w : PhillipsBrown2025.World | w.benefit = w.act ∧ w.cost = w.act}

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWorldMemSetBel : DecidablePred fun (x : World) => x ∈ bel

Equations

• PhillipsBrown2025.instDecidablePredWorldMemSetBel w = { decide := decide (w.benefit = w.act) && decide (w.cost = w.act), reflects_decide := ⋯ }

def PhillipsBrown2025.desires : List (Finset World)

The desires are the benefit and not the cost.

Equations

• PhillipsBrown2025.desires = [PhillipsBrown2025.benefit, PhillipsBrown2025.costᶜ]

theorem PhillipsBrown2025.vonFintel_no_conflict (A : Set (World → Prop)) : ¬(Desire.BestWorlds.Want A bel ↑act ∧ Desire.BestWorlds.Want A bel (↑act)ᶜ)

Von Fintel's semantics cannot make Nap and Not-nap both true, whatever the desires, since some belief-world is best and it settles the act one way.

theorem PhillipsBrown2025.heim_no_conflict (F : Desire.Conditional.Frame World) (w : World) [Std.Antisymm (F.pref w)] (hd : Desire.IsContingent bel ↑act) : ¬(Desire.Conditional.Want F bel w ↑act ∧ Desire.Conditional.Want F bel w (↑act)ᶜ)

Neither can Heim's, under her definedness amendment and antisymmetric desirability.

theorem PhillipsBrown2025.closure_under_doxastic_equivalence (A : Set (World → Prop)) (h : Desire.BestWorlds.Want A bel ↑act) : Desire.BestWorlds.Want A bel ↑cost

On a belief-based semantics, the cost being believed to come exactly with the act, wanting the act is wanting the cost, Nap entailing Fail, the closure under doxastic equivalence of §4.1.

@[instance_reducible]

def PhillipsBrown2025.instDecidableRelWorldLe : DecidableRel LE.le

Equations

• PhillipsBrown2025.instDecidableRelWorldLe w z = decidable_of_iff (z ∈ PhillipsBrown2025.benefit → w ∈ PhillipsBrown2025.benefit) ⋯

theorem PhillipsBrown2025.cpr_overgenerates : Desire.BestWorlds.Want {fun (x : World) => x ∈ benefit} bel ↑act ∧ Desire.BestWorlds.Want {fun (x : World) => x ∈ benefit} bel ↑cost

A context-sensitive preference relation overgenerates (§2.2), since the value of feeling rested makes Nap true, and with it Fail.

Some-things-considered desire (§3)

def PhillipsBrown2025.qBenefit : Setoid World

The question considering whether the act is done and whether its benefit obtains (Figure 3).

Equations

• PhillipsBrown2025.qBenefit = Setoid.ofProps {PhillipsBrown2025.act, PhillipsBrown2025.benefit}

def PhillipsBrown2025.qCost : Setoid World

The question considering whether the act is done and whether its cost obtains (Figure 5).

Equations

• PhillipsBrown2025.qCost = Setoid.ofProps {PhillipsBrown2025.act, PhillipsBrown2025.cost}

@[instance_reducible]

instance PhillipsBrown2025.instDecidableRelWorldR : DecidableRel ⇑qBenefit

Equations

• PhillipsBrown2025.instDecidableRelWorldR a b = Setoid.instDecidableRelROfDecidableEq_linglib_1 {PhillipsBrown2025.act, PhillipsBrown2025.benefit} a b

@[instance_reducible]

instance PhillipsBrown2025.instDecidableRelWorldR_1 : DecidableRel ⇑qCost

Equations

• PhillipsBrown2025.instDecidableRelWorldR_1 a b = Setoid.instDecidableRelROfDecidableEq_linglib_1 {PhillipsBrown2025.act, PhillipsBrown2025.cost} a b

def PhillipsBrown2025.issues : List (Finset World)

The salient propositions of the case, the test set of the anti-deckstacking constraint.

Equations

• PhillipsBrown2025.issues = [PhillipsBrown2025.act, PhillipsBrown2025.benefit, PhillipsBrown2025.cost]

theorem PhillipsBrown2025.act_true : Defined issues qBenefit bel ↑act ∧ Want desires qBenefit bel ↑act

Considering the act and its benefit, Nap and Lobster are defined and true.

theorem PhillipsBrown2025.cost_undefined : ¬qBenefit.Decides ↑cost

In that context the cost is ignored, so Fail and Die are undefined (§3.6), which blocks the inference from Nap to Fail (§4.1).

theorem PhillipsBrown2025.not_act_true : Defined issues qCost bel (↑act)ᶜ ∧ Want desires qCost bel (↑act)ᶜ ∧ Want desires qCost bel (↑cost)ᶜ

Considering the act and its cost, not doing the act is wanted, Not-nap and Not-lobster, and so is avoiding the cost, Not-die.

Deck-stacking (§3.7)

structure PhillipsBrown2025.LuWorld : Type

A state of Lu's case records whether it rains and whether Lu is happy.

• rain : Bool
• happy : Bool

@[instance_reducible]

instance PhillipsBrown2025.instDecidableEqLuWorld : DecidableEq LuWorld

Equations

• PhillipsBrown2025.instDecidableEqLuWorld = PhillipsBrown2025.instDecidableEqLuWorld.decEq

def PhillipsBrown2025.instDecidableEqLuWorld.decEq (x✝ x✝¹ : LuWorld) : Decidable (x✝ = x✝¹)

Equations

• PhillipsBrown2025.instDecidableEqLuWorld.decEq { rain := a, happy := a_1 } { rain := b, happy := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance PhillipsBrown2025.instFintypeLuWorld : Fintype LuWorld

Equations

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

def PhillipsBrown2025.rain : Finset LuWorld

It rains tomorrow.

Equations

• PhillipsBrown2025.rain = {x : PhillipsBrown2025.LuWorld | x.rain = true}

def PhillipsBrown2025.happy : Finset LuWorld

Lu is happy tomorrow.

Equations

• PhillipsBrown2025.happy = {x : PhillipsBrown2025.LuWorld | x.happy = true}

def PhillipsBrown2025.belLu : Set LuWorld

Lu believes she is happy whatever the weather.

Equations

• PhillipsBrown2025.belLu = {w : PhillipsBrown2025.LuWorld | w.happy = true}

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredLuWorldMemSetBelLu : DecidablePred fun (x : LuWorld) => x ∈ belLu

Equations

• PhillipsBrown2025.instDecidablePredLuWorldMemSetBelLu w = PhillipsBrown2025.instDecidablePredLuWorldMemSetBelLu._aux_1 w

def PhillipsBrown2025.qStacked : Setoid LuWorld

The deck-stacked question (Figure 7) asks whether it rains, and if not, whether Lu is happy.

Equations

• PhillipsBrown2025.qStacked = Setoid.ker fun (w : PhillipsBrown2025.LuWorld) => if w.rain = true then none else some w.happy

def PhillipsBrown2025.qFair : Setoid LuWorld

The level playing field (Figure 9).

Equations

• PhillipsBrown2025.qFair = Setoid.ofProps {PhillipsBrown2025.rain, PhillipsBrown2025.happy}

@[instance_reducible]

instance PhillipsBrown2025.instDecidableRelLuWorldR : DecidableRel ⇑qStacked

Equations

• PhillipsBrown2025.instDecidableRelLuWorldR = PhillipsBrown2025.instDecidableRelLuWorldR._aux_1

@[instance_reducible]

instance PhillipsBrown2025.instDecidableRelLuWorldR_1 : DecidableRel ⇑qFair

Equations

• PhillipsBrown2025.instDecidableRelLuWorldR_1 a b = Setoid.instDecidableRelROfDecidableEq_linglib_1 {PhillipsBrown2025.rain, PhillipsBrown2025.happy} a b

theorem PhillipsBrown2025.not_rain_deckstacked : Want [happy] qStacked belLu (↑rain)ᶜ ∧ ¬Want [happy] qFair belLu (↑rain)ᶜ

Without the constraint the deck-stacked question makes Lu wants it not to rain true, though Lu is indifferent to the weather; the level playing field makes it false.

theorem PhillipsBrown2025.deckstacked_excluded : ¬IsAntiDeckstacking [happy] qStacked ∧ ∀ (q : Finset LuWorld), (∃ (w : LuWorld), qFair.cell w ⊆ ↑q) → qFair.Decides ↑q

The deck-stacked question violates the constraint at happy, which one answer entails and another leaves open, while the level playing field satisfies it for every proposition.

theorem PhillipsBrown2025.antiDeckstacking_univ_singleton {W : Type u_1} {s : Setoid W} (h : ∀ (q : Set W), (∃ (w : W), s.cell w ⊆ q) → s.Decides q) {w₁ w₂ w₃ : W} (h₁₂ : s w₁ w₂) (h₁₃ : ¬s w₁ w₃) : w₁ = w₂

Read with q ranging over all propositions, the Anti-deckstacking Constraint admits only the finest partition. Two worlds in one cell, with a second cell available, are equal, since the union of the second cell with the first minus one of the worlds is entailed by an answer and decided by none.

Belief-sensitivity (§4.2)

theorem PhillipsBrown2025.undefined_of_insensitive {W : Type u_1} {bel p : Set W} (h : ∀ (s : Setoid W), s.Decides p → ¬IsBelSensitive s bel) (N : List (Finset W)) (s : Setoid W) : ¬Defined N s bel p

An agent whose beliefs are insensitive to every question that decides p, William III and England avoiding nuclear war with France, has S wants p undefined in every context, since where p is decided the beliefs are insensitive, and where they are sensitive p is not decided.