@cite{phillips-brown-2025} — Some-Things-Considered Desire

Question-based semantics for desire ascriptions: ⟦S wants p⟧^c is true relative to a contextual question Q_c iff every undominated answer in Q_c-Bel_S entails p. The proposal handles conflicting-desire cases — "S wants p" + "S wants ¬p" — by varying Q_c.

This study file replicates the Nap, Lobster, Lu/Happy/Rain (deck-stacking), and William-III/nuclear-war scenarios of @cite{phillips-brown-2025}, plus a §11 cross-paper bridge to @cite{condoravdi-lauer-2016} (an effective-preferential alternative that refuses simultaneous want(p) and want(¬p)).

The substrate is Theories/Semantics/Attitudes/Desire.lean. All theorems here either compute by decide over an 8-world model (3 binary dimensions: nap × rested × pass = lobster × gustatory × ¬die) or delegate to the substrate's general theorems (wantVF_no_simultaneous_pq_and_negpq, wantQuestionBased_strawson_upward_monotonic, …).

§-by-§ map

Paper	Study file
§2.1 vF no-go	§5 (vf_cannot_predict_both, delegates to general)
§3.3 Q-relative belief	§3, §4
§3.4 finest=vF	§8
§3.5 best-answer semantics	§3, §4
§3.6 Considering	§3, §4
§3.7 Diversity, Anti-deckstacking	§3, §7
§4.1 doxastic-closure blocking	§6
§4.2 Belief-sensitivity	§10
§5 cross-framework	§11 (CondoravdiLauer bridge)

Parallel discovery: Cariani 2013 isVisible

PB's isConsidered (§3.6) is the same predicate as @cite{cariani-2013}'s isVisible (§4 p.545–546): both require every cell of the partition/option-set to settle the prejacent. PB doesn't cite Cariani; Cariani doesn't anticipate PB. The identification is exposed in Phenomena/Modality/Studies/Cariani2013.lean, where Cariani's isVisible is defined as abbrev isVisible rc p := isConsidered rc.options p and the bridge theorem isVisible_iff_isConsidered reduces to Iff.rfl. The agreement is independent reinvention across the desire/deontic-modality boundary, surfaced by the substrate sharing a common predicate.

§1. Eight-world model

3 binary dimensions: d₁ × d₂ × d₃. For Nap: d₁ = nap, d₂ = rested, d₃ = pass. For Lobster (paper §2.2): d₁ = lobster, d₂ = gustatory, d₃ = ¬die. The Lobster scenario reuses the Nap dimensions via abbrev — see lobster := nap, gustatory := rested, die := fail below; the structural isomorphism is documented and not coincidental (lobster_true := nap_true is the same theorem under renaming).

inductive PhillipsBrown2025.W : Type

• w0 : W
• w1 : W
• w2 : W
• w3 : W
• w4 : W
• w5 : W
• w6 : W
• w7 : W

@[implicit_reducible]

instance PhillipsBrown2025.instDecidableEqW : DecidableEq W

Equations

• PhillipsBrown2025.instDecidableEqW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance PhillipsBrown2025.instReprW : Repr W

Equations

• PhillipsBrown2025.instReprW = { reprPrec := PhillipsBrown2025.instReprW.repr }

def PhillipsBrown2025.instReprW.repr : W → ℕ → Std.Format

Equations

• PhillipsBrown2025.instReprW.repr PhillipsBrown2025.W.w0 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PhillipsBrown2025.W.w0")).group prec✝
• PhillipsBrown2025.instReprW.repr PhillipsBrown2025.W.w1 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PhillipsBrown2025.W.w1")).group prec✝
• PhillipsBrown2025.instReprW.repr PhillipsBrown2025.W.w2 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PhillipsBrown2025.W.w2")).group prec✝
• PhillipsBrown2025.instReprW.repr PhillipsBrown2025.W.w3 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PhillipsBrown2025.W.w3")).group prec✝
• PhillipsBrown2025.instReprW.repr PhillipsBrown2025.W.w4 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PhillipsBrown2025.W.w4")).group prec✝
• PhillipsBrown2025.instReprW.repr PhillipsBrown2025.W.w5 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PhillipsBrown2025.W.w5")).group prec✝
• PhillipsBrown2025.instReprW.repr PhillipsBrown2025.W.w6 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PhillipsBrown2025.W.w6")).group prec✝
• PhillipsBrown2025.instReprW.repr PhillipsBrown2025.W.w7 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "PhillipsBrown2025.W.w7")).group prec✝

@[implicit_reducible]

instance PhillipsBrown2025.instInhabitedW : Inhabited W

Equations

• PhillipsBrown2025.instInhabitedW = { default := PhillipsBrown2025.instInhabitedW.default }

def PhillipsBrown2025.instInhabitedW.default : W

Equations

• PhillipsBrown2025.instInhabitedW.default = PhillipsBrown2025.W.w0

@[implicit_reducible]

instance PhillipsBrown2025.instFintypeW : Fintype W

Equations

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

§2. Propositions

World	nap	rested	pass
w0	T	T	T
w1	T	T	F
w2	T	F	T
w3	T	F	F
w4	F	T	T
w5	F	T	F
w6	F	F	T
w7	F	F	F

def PhillipsBrown2025.nap : Set W

Equations

• PhillipsBrown2025.nap PhillipsBrown2025.W.w0 = True
• PhillipsBrown2025.nap PhillipsBrown2025.W.w1 = True
• PhillipsBrown2025.nap PhillipsBrown2025.W.w2 = True
• PhillipsBrown2025.nap PhillipsBrown2025.W.w3 = True
• PhillipsBrown2025.nap x✝ = False

def PhillipsBrown2025.rested : Set W

Equations

• PhillipsBrown2025.rested PhillipsBrown2025.W.w0 = True
• PhillipsBrown2025.rested PhillipsBrown2025.W.w1 = True
• PhillipsBrown2025.rested PhillipsBrown2025.W.w4 = True
• PhillipsBrown2025.rested PhillipsBrown2025.W.w5 = True
• PhillipsBrown2025.rested x✝ = False

def PhillipsBrown2025.pass : Set W

Equations

• PhillipsBrown2025.pass PhillipsBrown2025.W.w0 = True
• PhillipsBrown2025.pass PhillipsBrown2025.W.w2 = True
• PhillipsBrown2025.pass PhillipsBrown2025.W.w4 = True
• PhillipsBrown2025.pass PhillipsBrown2025.W.w6 = True
• PhillipsBrown2025.pass x✝ = False

def PhillipsBrown2025.fail : Set W

Equations

• PhillipsBrown2025.fail w = ¬PhillipsBrown2025.pass w

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWNap : DecidablePred nap

Equations

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

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWRested : DecidablePred rested

Equations

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

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWPass : DecidablePred pass

Equations

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

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWFail : DecidablePred fail

Equations

• PhillipsBrown2025.instDecidablePredWFail w = id inferInstance

def PhillipsBrown2025.naturalProps : List (Semantics.Attitudes.Desire.DecProp W)

The natural propositions of the model (basic dimensions), used to feed isAntiDeckstacking. AD's quantifier is restricted to this test set — see Desire.isAntiDeckstacking docstring.

Equations

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

§3. Nap scenario

def PhillipsBrown2025.qNapRest : List (Semantics.Attitudes.Desire.DecProp W)

Q' = partition by nap × rested (4 cells).

Equations

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

def PhillipsBrown2025.qNapPass : List (Semantics.Attitudes.Desire.DecProp W)

Q'' = partition by nap × pass (4 cells).

Equations

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

def PhillipsBrown2025.belNapRest : Set W

Beliefs for Nap: nap ↔ rested. Bel = {w0, w1, w6, w7}.

Equations

• PhillipsBrown2025.belNapRest w = if PhillipsBrown2025.nap w then PhillipsBrown2025.rested w else ¬PhillipsBrown2025.rested w

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWBelNapRest : DecidablePred belNapRest

Equations

• PhillipsBrown2025.instDecidablePredWBelNapRest w = id inferInstance

def PhillipsBrown2025.belNapPass : Set W

Beliefs for Not-nap: pass ↔ ¬nap. Bel = {w1, w3, w4, w6}.

Equations

• PhillipsBrown2025.belNapPass w = if PhillipsBrown2025.nap w then ¬PhillipsBrown2025.pass w else PhillipsBrown2025.pass w

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWBelNapPass : DecidablePred belNapPass

Equations

• PhillipsBrown2025.instDecidablePredWBelNapPass w = id inferInstance

def PhillipsBrown2025.desRest : List (Semantics.Attitudes.Desire.DecProp W)

Equations

• PhillipsBrown2025.desRest = [Semantics.Attitudes.Desire.mkDec PhillipsBrown2025.rested]

def PhillipsBrown2025.desPass : List (Semantics.Attitudes.Desire.DecProp W)

Equations

• PhillipsBrown2025.desPass = [Semantics.Attitudes.Desire.mkDec PhillipsBrown2025.pass]

theorem PhillipsBrown2025.nap_true : Semantics.Attitudes.Desire.wantQuestionBased belNapRest desRest qNapRest nap

Nap is true relative to Q' with beliefs nap↔rested, desires [rested].

theorem PhillipsBrown2025.not_nap_true : Semantics.Attitudes.Desire.wantQuestionBased belNapPass desPass qNapPass fun (w : W) => ¬nap w

Not-nap is true relative to Q'' with beliefs pass↔¬nap, desires [pass].

theorem PhillipsBrown2025.fail_not_considered : ¬Semantics.Attitudes.Desire.isConsidered qNapRest fail

Fail is NOT considered relative to Q'.

theorem PhillipsBrown2025.fail_not_true : ¬Semantics.Attitudes.Desire.wantQuestionBased belNapRest desRest qNapRest fail

Fail is also not predicted true.

theorem PhillipsBrown2025.nap_diverse : Semantics.Attitudes.Desire.isDiverse qNapRest nap

Q' is diverse w.r.t. nap.

§4. Lobster scenario (paper §2.2)

The Lobster scenario reuses the Nap dimensions via abbrev: lobster := nap, gustatory := rested, die := fail. The two paper arguments use different questions over these dimensions — Q_{c''} (qLobGus) ignores death, Q_{c'''} (qLobDie) ignores taste.

@[reducible, inline]

abbrev PhillipsBrown2025.lobster : Set W

Equations

• PhillipsBrown2025.lobster = PhillipsBrown2025.nap

@[reducible, inline]

abbrev PhillipsBrown2025.gustatory : Set W

Equations

• PhillipsBrown2025.gustatory = PhillipsBrown2025.rested

@[reducible, inline]

abbrev PhillipsBrown2025.die : Set W

Equations

• PhillipsBrown2025.die = PhillipsBrown2025.fail

@[reducible, inline]

abbrev PhillipsBrown2025.qLobGus : List (Semantics.Attitudes.Desire.DecProp W)

Q_{c''} = partition by lobster × gustatory (= qNapRest).

Equations

• PhillipsBrown2025.qLobGus = PhillipsBrown2025.qNapRest

def PhillipsBrown2025.qLobDie : List (Semantics.Attitudes.Desire.DecProp W)

Q_{c'''} = partition by lobster × die.

Equations

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

def PhillipsBrown2025.belLobDie : Set W

Beliefs: die ↔ eat lobster. Bel = {w1, w3, w4, w6}.

Equations

• PhillipsBrown2025.belLobDie w = if PhillipsBrown2025.nap w then PhillipsBrown2025.fail w else ¬PhillipsBrown2025.fail w

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWBelLobDie : DecidablePred belLobDie

Equations

• PhillipsBrown2025.instDecidablePredWBelLobDie w = id inferInstance

def PhillipsBrown2025.desNotDie : List (Semantics.Attitudes.Desire.DecProp W)

Equations

• PhillipsBrown2025.desNotDie = [Semantics.Attitudes.Desire.mkDec fun (w : PhillipsBrown2025.W) => ¬PhillipsBrown2025.fail w]

theorem PhillipsBrown2025.lobster_true : Semantics.Attitudes.Desire.wantQuestionBased belNapRest desRest qLobGus lobster

Lobster is true in c'' (considering taste, ignoring death).

theorem PhillipsBrown2025.die_not_considered_in_qLobGus : ¬Semantics.Attitudes.Desire.isConsidered qLobGus die

Die is undefined in the Lobster context c'' (paper §2.2): in qLobGus = qNapRest, no cell settles die, so the Considering presupposition fails.

theorem PhillipsBrown2025.not_lobster_true : Semantics.Attitudes.Desire.wantQuestionBased belLobDie desNotDie qLobDie fun (w : W) => ¬nap w

Not-lobster is true in c''' (considering death, ignoring taste).

theorem PhillipsBrown2025.not_die_true : Semantics.Attitudes.Desire.wantQuestionBased belLobDie desNotDie qLobDie fun (w : W) => ¬fail w

Not-die is also true in c''' (best answer entails both ¬lobster and ¬die).

§5. Von Fintel comparison and the no-go theorem

The paper's central argument against belief-based semantics: vF cannot predict both want p and want ¬p simultaneously. Specialised here for the Nap example, then derived from the substrate's general wantVF_no_simultaneous_pq_and_negpq.

theorem PhillipsBrown2025.vf_nap_true : Semantics.Attitudes.Desire.wantVF belNapRest desRest nap

theorem PhillipsBrown2025.vf_not_nap_false : ¬Semantics.Attitudes.Desire.wantVF belNapRest desRest fun (w : W) => ¬nap w

theorem PhillipsBrown2025.vf_cannot_predict_both : ¬(Semantics.Attitudes.Desire.wantVF belNapRest desRest nap ∧ Semantics.Attitudes.Desire.wantVF belNapRest desRest fun (w : W) => ¬nap w)

vF cannot predict both Nap and Not-nap with the same parameter set (specific instance).

theorem PhillipsBrown2025.vf_no_conflict_nap : ¬(Semantics.Attitudes.Desire.wantVF belNapRest desRest nap ∧ Semantics.Attitudes.Desire.wantVF belNapRest desRest fun (w : W) => ¬nap w)

vF cannot predict both Nap and Not-nap (general no-go, delegates to the substrate). The witness is any belS-world that is Pareto-undominated under the desire ordering.

§6. Doxastic closure blocking (paper §4.1)

@cite{villalta-2008} identified the doxastic-closure problem for belief-based semantics: any proposition true at all best belief-worlds is predicted wanted, over-generating for coincidental propositions.

The question-based approach makes fail UNDEFINED rather than merely false: fail is not settled by Q' (the nap × rested partition), so the Considering presupposition blocks ⟦want(fail)⟧^{Q'} at definedness. With Q'' (the nap × pass partition), fail is settled — and the contrast is exactly the paper's point.

theorem PhillipsBrown2025.nap_considered_in_qNapPass : Semantics.Attitudes.Desire.isConsidered qNapPass nap

theorem PhillipsBrown2025.fail_considered_in_qNapPass : Semantics.Attitudes.Desire.isConsidered qNapPass fail

§7. Anti-deckstacking (paper §3.7)

Lu is unsure if it will rain, but is sure he'll feel happy no matter what. Q'''' (deck-stacked) = {r, ¬r∧h, ¬r∧¬h} asymmetrically cross-cuts rain with happiness; the r cell ignores h while the others distinguish it. Cell ¬r∧h predetermines h (entails it), but h is not considered by the question. AD fails on qDeckstacked with test set [r, h].

Q''''' (level playing field) = partition by rain × happy (4 cells). AD passes for the same [r, h] test set.

def PhillipsBrown2025.happy : Set W

Equations

• PhillipsBrown2025.happy PhillipsBrown2025.W.w0 = True
• PhillipsBrown2025.happy PhillipsBrown2025.W.w1 = True
• PhillipsBrown2025.happy PhillipsBrown2025.W.w4 = True
• PhillipsBrown2025.happy PhillipsBrown2025.W.w5 = True
• PhillipsBrown2025.happy x✝ = False

def PhillipsBrown2025.rain : Set W

Equations

• PhillipsBrown2025.rain PhillipsBrown2025.W.w0 = True
• PhillipsBrown2025.rain PhillipsBrown2025.W.w1 = True
• PhillipsBrown2025.rain PhillipsBrown2025.W.w2 = True
• PhillipsBrown2025.rain PhillipsBrown2025.W.w3 = True
• PhillipsBrown2025.rain x✝ = False

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWHappy : DecidablePred happy

Equations

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

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWRain : DecidablePred rain

Equations

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

def PhillipsBrown2025.naturalPropsLu : List (Semantics.Attitudes.Desire.DecProp W)

Test set of natural propositions for the Lu scenario.

Equations

• PhillipsBrown2025.naturalPropsLu = [Semantics.Attitudes.Desire.mkDec PhillipsBrown2025.rain, Semantics.Attitudes.Desire.mkDec PhillipsBrown2025.happy]

def PhillipsBrown2025.qDeckstacked : List (Semantics.Attitudes.Desire.DecProp W)

Q'''' (deck-stacked): {r, ¬r∧h, ¬r∧¬h}.

Equations

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

def PhillipsBrown2025.belLu : Set W

Lu's beliefs: happy unconditionally.

Equations

• PhillipsBrown2025.belLu = PhillipsBrown2025.happy

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWBelLu : DecidablePred belLu

Equations

• PhillipsBrown2025.instDecidablePredWBelLu = PhillipsBrown2025.instDecidablePredWBelLu._aux_1

def PhillipsBrown2025.desHappy : List (Semantics.Attitudes.Desire.DecProp W)

Equations

• PhillipsBrown2025.desHappy = [Semantics.Attitudes.Desire.mkDec PhillipsBrown2025.happy]

theorem PhillipsBrown2025.happy_not_considered_deckstacked : ¬Semantics.Attitudes.Desire.isConsidered qDeckstacked happy

happy is not considered in the deck-stacked Q'''' (the rain cell contains both happy and unhappy worlds).

theorem PhillipsBrown2025.happy_answer_exists_deckstacked : ∃ a ∈ qDeckstacked, ∀ (w : W), a.prop w → happy w

A happy-answer exists in qDeckstacked (the ¬r∧h cell entails happy) — the deck is stacked in favor of ¬rain.

theorem PhillipsBrown2025.not_rain_deckstacked_true : Semantics.Attitudes.Desire.wantQuestionBased belLu desHappy qDeckstacked fun (w : W) => ¬rain w

Without the constraint, the question-based semantics wrongly predicts Not-rain.

def PhillipsBrown2025.qRainHappy : List (Semantics.Attitudes.Desire.DecProp W)

Q''''' (level playing field): partition by rain × happy.

Equations

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

theorem PhillipsBrown2025.happy_considered_fair : Semantics.Attitudes.Desire.isConsidered qRainHappy happy

theorem PhillipsBrown2025.not_rain_false_fair : ¬Semantics.Attitudes.Desire.wantQuestionBased belLu desHappy qRainHappy fun (w : W) => ¬rain w

With the fair question, Not-rain is correctly predicted false.

theorem PhillipsBrown2025.qDeckstacked_fails_antideckstacking : ¬Semantics.Attitudes.Desire.isAntiDeckstacking naturalPropsLu qDeckstacked

The deck-stacked question fails Anti-deckstacking on test set [r, h] (h is predetermined by the ¬r∧h cell but not considered by Q'''').

theorem PhillipsBrown2025.qRainHappy_satisfies_antideckstacking : Semantics.Attitudes.Desire.isAntiDeckstacking naturalPropsLu qRainHappy

The fair (cross-product) question satisfies Anti-deckstacking — every basic proposition is settled by every cell.

theorem PhillipsBrown2025.qNapRest_satisfies_antideckstacking : Semantics.Attitudes.Desire.isAntiDeckstacking naturalProps qNapRest

Q' (qNapRest) satisfies Anti-deckstacking on the natural-prop test set [nap, rested, pass] — the cross-product over nap and rested settles nap and rested; no cell entails pass, so AD's antecedent is vacuous for pass.

§8. Finest-question simulation (paper §3.4)

When Q_c is the finest partition (singleton cells = individual worlds), the question-based semantics reduces to vF. The substrate provides finestPartition : List W → List (DecProp W); here we instantiate it on the explicit world list of the model.

def PhillipsBrown2025.allWorldsW : List W

Equations

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

def PhillipsBrown2025.qFinest : List (Semantics.Attitudes.Desire.DecProp W)

Equations

• PhillipsBrown2025.qFinest = Semantics.Attitudes.Desire.finestPartition PhillipsBrown2025.allWorldsW

theorem PhillipsBrown2025.allWorldsW_complete (w : W) : w ∈ allWorldsW

The 8-world list allWorldsW covers W. Hypothesis required by the substrate's general wantQuestionBased_finestPartition_iff_wantVF.

theorem PhillipsBrown2025.finest_simulates_vf_nap : Semantics.Attitudes.Desire.wantQuestionBased belNapRest desRest qFinest nap ↔ Semantics.Attitudes.Desire.wantVF belNapRest desRest nap

With the finest question, question-based want = standard vF want for nap. Derived from the substrate's general wantQuestionBased_finestPartition_iff_wantVF, not by decide.

theorem PhillipsBrown2025.finest_simulates_vf_not_nap : (Semantics.Attitudes.Desire.wantQuestionBased belNapRest desRest qFinest fun (w : W) => ¬nap w) ↔ Semantics.Attitudes.Desire.wantVF belNapRest desRest fun (w : W) => ¬nap w

With the finest question, question-based want = standard vF want for ¬nap.

theorem PhillipsBrown2025.finest_simulates_vf_not_lobster : (Semantics.Attitudes.Desire.wantQuestionBased belLobDie desNotDie qFinest fun (w : W) => ¬nap w) ↔ Semantics.Attitudes.Desire.wantVF belLobDie desNotDie fun (w : W) => ¬nap w

With the finest question, question-based want = standard vF want for ¬lobster in the Lobster context.

§9. Definedness via PrProp (paper §3.6)

theorem PhillipsBrown2025.nap_defined_in_qNapRest : Semantics.Attitudes.Desire.wantDefined belNapRest naturalProps qNapRest nap

theorem PhillipsBrown2025.fail_not_defined_in_qNapRest : ¬Semantics.Attitudes.Desire.wantDefined belNapRest naturalProps qNapRest fail

theorem PhillipsBrown2025.nap_prprop_holds : (Semantics.Attitudes.Desire.wantPrProp belNapRest desRest naturalProps qNapRest nap).presup W.w0 ∧ (Semantics.Attitudes.Desire.wantPrProp belNapRest desRest naturalProps qNapRest nap).assertion W.w0

theorem PhillipsBrown2025.fail_prprop_undefined : ¬(Semantics.Attitudes.Desire.wantPrProp belNapRest desRest naturalProps qNapRest fail).presup W.w0

§10. Belief-sensitivity: William III / nuclear war (paper §4.2)

William III wanted to avoid war. Avoiding war entails avoiding nuclear war. But we cannot conclude William III wanted to avoid nuclear war — he lacked the conceptual resources to grasp nuclear war.

Mechanism: William's beliefs are NOT sensitive to Q_nuc that distinguishes nuclear from conventional war. All Q_nuc answers are compatible with his beliefs (total uncertainty), so isBelSensitive returns false and wantDefined blocks the inference. A modern person whose beliefs rule out nuclear war DOES have belief-sensitive context, so the inference goes through.

Strawson upward monotonicity is the closure principle at issue; @cite{phillips-brown-2025} §4.2 argues that question-based semantics must be Strawson-but-not-naively upward monotonic, with definedness gating the inference. The substrate's wantQuestionBased_strawson_upward_monotonic captures the licit direction.

def PhillipsBrown2025.avoidWar : Set W

Equations

• PhillipsBrown2025.avoidWar = PhillipsBrown2025.nap

def PhillipsBrown2025.avoidNuclearWar : Set W

Equations

• PhillipsBrown2025.avoidNuclearWar w = (PhillipsBrown2025.nap w ∨ PhillipsBrown2025.rested w)

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWAvoidWar : DecidablePred avoidWar

Equations

• PhillipsBrown2025.instDecidablePredWAvoidWar = PhillipsBrown2025.instDecidablePredWAvoidWar._aux_1

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWAvoidNuclearWar : DecidablePred avoidNuclearWar

Equations

• PhillipsBrown2025.instDecidablePredWAvoidNuclearWar w = id inferInstance

def PhillipsBrown2025.qNuclear : List (Semantics.Attitudes.Desire.DecProp W)

Equations

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

def PhillipsBrown2025.naturalPropsNuclear : List (Semantics.Attitudes.Desire.DecProp W)

Natural-prop test set for the nuclear-war scenario. The Nap-vs-war distinction (nap) and the war-of-any-kind distinction (avoidNuclearWar) are the salient dimensions; rested and pass are not part of this scenario's vocabulary.

Equations

• PhillipsBrown2025.naturalPropsNuclear = [Semantics.Attitudes.Desire.mkDec PhillipsBrown2025.nap, Semantics.Attitudes.Desire.mkDec PhillipsBrown2025.avoidNuclearWar]

theorem PhillipsBrown2025.avoidWar_entails_avoidNuclearWar (w : W) : avoidWar w → avoidNuclearWar w

theorem PhillipsBrown2025.avoidNuclearWar_considered : Semantics.Attitudes.Desire.isConsidered qNuclear avoidNuclearWar

def PhillipsBrown2025.belWilliam : Set W

William III: total uncertainty (all worlds compatible).

Equations

• PhillipsBrown2025.belWilliam x✝ = True

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWBelWilliam : DecidablePred belWilliam

Equations

• PhillipsBrown2025.instDecidablePredWBelWilliam x✝ = isTrue trivial

theorem PhillipsBrown2025.william_insensitive : ¬Semantics.Attitudes.Desire.isBelSensitive belWilliam qNuclear

theorem PhillipsBrown2025.avoidNuclearWar_not_defined_william : ¬Semantics.Attitudes.Desire.wantDefined belWilliam naturalPropsNuclear qNuclear avoidNuclearWar

def PhillipsBrown2025.belModern : Set W

Modern person: beliefs rule out nuclear war (peace ∨ conventional).

Equations

• PhillipsBrown2025.belModern w = (PhillipsBrown2025.nap w ∨ PhillipsBrown2025.rested w)

@[implicit_reducible]

instance PhillipsBrown2025.instDecidablePredWBelModern : DecidablePred belModern

Equations

• PhillipsBrown2025.instDecidablePredWBelModern w = id inferInstance

theorem PhillipsBrown2025.modern_sensitive : Semantics.Attitudes.Desire.isBelSensitive belModern qNuclear

theorem PhillipsBrown2025.avoidNuclearWar_defined_modern : Semantics.Attitudes.Desire.wantDefined belModern naturalPropsNuclear qNuclear avoidNuclearWar

def PhillipsBrown2025.desAvoidWar : List (Semantics.Attitudes.Desire.DecProp W)

Equations

• PhillipsBrown2025.desAvoidWar = [Semantics.Attitudes.Desire.mkDec PhillipsBrown2025.nap]

theorem PhillipsBrown2025.modern_wants_avoidNuclearWar : Semantics.Attitudes.Desire.wantQuestionBased belModern desAvoidWar qNuclear avoidNuclearWar

§11. Cross-paper bridge: @cite{condoravdi-lauer-2016}

@cite{condoravdi-lauer-2016}'s effective-preferential wantEP carries a joint-belief-consistency theorem (wantEP_jointly_belief_consistent): if both wantEP EP a φ w and wantEP EP a ψ w hold, then (φ ∩ ψ) ∩ B(a, w) ≠ ∅. Specialized to ψ = φᶜ, the conclusion becomes ∅ ∩ B(a, w) ≠ ∅, which is contradictory. So C&L forbids simultaneous want(p) and want(¬p) against a single belief state and preference structure.

@cite{phillips-brown-2025} resolves the conflict by varying the contextual question Q_c (and the contextually-relevant belS) per ascription. C&L resolves it by varying the preference structure (per reading: wantPExact / wantPSuccess / wantPQH). The two resolutions are orthogonal — both can coexist in a unified theory of desire, but they make non-overlapping claims.

theorem PhillipsBrown2025.condoravdiLauer_blocks_simultaneous_pq_and_negpq {Agent W : Type} {B : Agent → W → Set W} (EP : Semantics.Attitudes.CondoravdiLauer.EffectivePreferentialBackground Agent W B) (a : Agent) (φ : Set W) (w : W) (hφ : Semantics.Attitudes.CondoravdiLauer.wantEP EP a φ w) (hnegφ : Semantics.Attitudes.CondoravdiLauer.wantEP EP a (fun (w : W) => ¬φ w) w) : False

C&L's joint-belief-consistency, specialized to ψ = φᶜ: no single EP-want can hold of both φ and ¬φ simultaneously, since their intersection is empty.

This is a paper-level contrast with PB §3: PB makes both nap_true and not_nap_true work by varying Q_c and belS; the C&L analysis would need different EP per ascription to reproduce the contrast.

§12. Heim foil and parametric no-go

@cite{heim-1992}'s comparative-belief semantics (wantHeim) is the other canonical belief-based account — formalized at Theories/Semantics/Attitudes/Desire.lean and exercised in Phenomena/Modality/Studies/Heim1992.lean. The substrate's BeliefBasedDesireSemantics typology packages vF, Heim, and (in principle) Levinson 2003 / sufficient-desirability accounts under a single structural property isConflictBlocking.

PB's argument against belief-based semantics generalizes from vf_no_conflict_nap (vF only) to:

• Heim 1992: blocked by wantHeim_no_simultaneous_pq_and_negpq under preference asymmetry. The (40) amendment makes definedness of wantHeim p and wantHeim ¬p simultaneously impossible when the agent's beliefs are consistent.
• vF: blocked by wantVF_no_simultaneous_pq_and_negpq.
• Any future BeliefBasedDesireSemantics instance: blocked by the parametric isConflictBlocking predicate (currently proved per instance in Theories/Semantics/Attitudes/Desire.lean).

PB's wantQuestionBased evades the no-go by selecting from Q-Bel_S rather than directly from Bel_S — it is not an instance of BeliefBasedDesireSemantics (the question parameter answers plays a non-trivial role outside the typeclass shape).

theorem PhillipsBrown2025.heim_no_go_covers_belief_based_family {W : Type} [Fintype W] [DecidableEq W] (params : Semantics.Attitudes.Desire.HeimDesireParams W) (w_eval : W) (hAsym : ∀ (x y : W), params.pref w_eval x y → params.pref w_eval y x → x = y) (belS : Set W) [DecidablePred belS] (p : Set W) [DecidablePred p] (h : Semantics.Attitudes.Desire.wantHeimDefined belS p) : ¬(Semantics.Attitudes.Desire.wantHeim belS params w_eval p ∧ Semantics.Attitudes.Desire.wantHeim belS params w_eval fun (w : W) => ¬p w)

theorem PhillipsBrown2025.lassiter_evades_no_go_via_grading : ∃ (W : Type) (x : Fintype W) (x_1 : DecidableEq W) (belS : Set W) (x_2 : DecidablePred belS) (pr : W → ℚ) (V : W → ℚ) (θ : ℚ) (p : Set W) (x_3 : DecidablePred p), Semantics.Attitudes.Desire.Lassiter.want belS pr V θ p ∧ Semantics.Attitudes.Desire.Lassiter.want belS pr V θ fun (w : W) => ¬p w

@cite{lassiter-2017} also evades the no-go but via numerical threshold + graded value rather than question-sensitivity. The Lassiter substrate's threshold_admits_conflict_witness exhibits a concrete configuration where both want(p) and want(¬p) fire on a single (belS, pr, V, θ) — falsifying isConflictBlocking.

Lassiter and PB are now formalized as two distinct non-instances of BeliefBasedDesireSemantics. PB's escape route: question parameter outside the BBS shape. Lassiter's: numerical threshold on graded expected value. The cross-paper picture: the typology correctly excludes both, and they evade via genuinely different mechanisms.

Summary

The 8-world model verifies all of the paper's quantitative predictions that fit the 3-binary-dimension encoding (Nap, Lobster-via-isomorphism, Lu/deck-stacking, William-III). The substrate carries the general arguments (no-go for vF, no-go for Heim, Strawson upward monotonicity, finest=vF direction, parametric BeliefBasedDesireSemantics typology). The §11 bridge makes the disagreement with C&L explicit; the §12 foil shows the no-go covers the whole belief-based family.

What's deferred:

• The general wantQuestionBased qFinest = wantVF ↔ identity is verified for the three named propositions in §8 by decide; lifting to the substrate as a universal ∀ p, ... theorem is sketched in Desire.lean as future work (the proof requires a structural lemma relating singleton-cell preference to single-world preference).

• The Lobster scenario reuses Nap's dimensions via abbrev — a 4-dimension model would let qLobGus and qLobDie be genuinely distinct in their underlying worlds. The current encoding is honest (qLobGus := qNapRest) and adequate for the structural argument.

• @cite{crnic-2014} is referenced in Desire.lean's docstring as the acknowledged precursor; a Crnič-2011 study file is the natural next paper.

• The CPR overgeneration argument (paper §2.2) is handled here via die_not_considered_in_qLobGus. A separate CPR formalization (paper §2.4) is not yet in linglib.