[PB25] — 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 [PB25], plus a §11 cross-paper bridge to [CL16] (an effective-preferential alternative that refuses simultaneous want(p) and want(¬p)).

The substrate is Semantics/Attitudes/Desire/. 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 (BestWorlds.Want.not_compl, toPartialProp_strawsonEntails, …).

§-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 [Car13]'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 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

@[instance_reducible]

instance PhillipsBrown2025.instDecidableEqW : DecidableEq W

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instFintypeW : Fintype W

Equations

• PhillipsBrown2025.instFintypeW = { elems := { val := ↑PhillipsBrown2025.W.enumList, nodup := PhillipsBrown2025.W.enumList_nodup }, complete := PhillipsBrown2025.instFintypeW._proof_1 }

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✝

@[instance_reducible]

instance PhillipsBrown2025.instReprW : Repr W

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instInhabitedW : Inhabited W

Equations

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

§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 = PhillipsBrown2025.passᶜ

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetNap : DecidablePred fun (x : W) => x ∈ nap

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetRested : DecidablePred fun (x : W) => x ∈ rested

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetPass : DecidablePred fun (x : W) => x ∈ pass

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetFail : DecidablePred fun (x : W) => x ∈ fail

Equations

• PhillipsBrown2025.instDecidablePredWMemSetFail = PhillipsBrown2025.instDecidablePredWMemSetFail._aux_1

def PhillipsBrown2025.naturalProps : List (Finset W)

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

Equations

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

§3. Nap scenario

def PhillipsBrown2025.qNapRest : List (Finset 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 (Finset 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 : PhillipsBrown2025.W | if w ∈ PhillipsBrown2025.nap then w ∈ PhillipsBrown2025.rested else w ∉ PhillipsBrown2025.rested}

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetBelNapRest : DecidablePred fun (x : W) => x ∈ belNapRest

Equations

• PhillipsBrown2025.instDecidablePredWMemSetBelNapRest w = PhillipsBrown2025.instDecidablePredWMemSetBelNapRest._aux_1 w

def PhillipsBrown2025.belNapPass : Set W

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

Equations

• PhillipsBrown2025.belNapPass = {w : PhillipsBrown2025.W | if w ∈ PhillipsBrown2025.nap then w ∉ PhillipsBrown2025.pass else w ∈ PhillipsBrown2025.pass}

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetBelNapPass : DecidablePred fun (x : W) => x ∈ belNapPass

Equations

• PhillipsBrown2025.instDecidablePredWMemSetBelNapPass w = PhillipsBrown2025.instDecidablePredWMemSetBelNapPass._aux_1 w

def PhillipsBrown2025.desRest : List (Finset W)

Equations

• PhillipsBrown2025.desRest = [{x : PhillipsBrown2025.W | x ∈ PhillipsBrown2025.rested}]

def PhillipsBrown2025.desPass : List (Finset W)

Equations

• PhillipsBrown2025.desPass = [{x : PhillipsBrown2025.W | x ∈ PhillipsBrown2025.pass}]

theorem PhillipsBrown2025.nap_true : Desire.QuestionBased.Want desRest qNapRest belNapRest nap

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

theorem PhillipsBrown2025.not_nap_true : Desire.QuestionBased.Want desPass qNapPass belNapPass napᶜ

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

theorem PhillipsBrown2025.fail_not_considered : ¬Desire.QuestionBased.IsConsidered qNapRest fail

Fail is NOT considered relative to Q'.

theorem PhillipsBrown2025.fail_not_true : ¬Desire.QuestionBased.Want desRest qNapRest belNapRest fail

Fail is also not predicted true.

theorem PhillipsBrown2025.nap_diverse : Desire.QuestionBased.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 (Finset W)

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

Equations

• PhillipsBrown2025.qLobGus = PhillipsBrown2025.qNapRest

def PhillipsBrown2025.qLobDie : List (Finset 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 : PhillipsBrown2025.W | if w ∈ PhillipsBrown2025.nap then w ∈ PhillipsBrown2025.fail else w ∉ PhillipsBrown2025.fail}

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetBelLobDie : DecidablePred fun (x : W) => x ∈ belLobDie

Equations

• PhillipsBrown2025.instDecidablePredWMemSetBelLobDie w = PhillipsBrown2025.instDecidablePredWMemSetBelLobDie._aux_1 w

def PhillipsBrown2025.desNotDie : List (Finset W)

Equations

• PhillipsBrown2025.desNotDie = [{x : PhillipsBrown2025.W | x ∉ PhillipsBrown2025.fail}]

theorem PhillipsBrown2025.lobster_true : Desire.QuestionBased.Want desRest qLobGus belNapRest lobster

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

theorem PhillipsBrown2025.die_not_considered_in_qLobGus : ¬Desire.QuestionBased.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 : Desire.QuestionBased.Want desNotDie qLobDie belLobDie napᶜ

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

theorem PhillipsBrown2025.not_die_true : Desire.QuestionBased.Want desNotDie qLobDie belLobDie failᶜ

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 BestWorlds.Want.not_compl.

theorem PhillipsBrown2025.vf_nap_true : Desire.BestWorlds.Want desRest belNapRest nap

theorem PhillipsBrown2025.vf_not_nap_false : ¬Desire.BestWorlds.Want desRest belNapRest napᶜ

theorem PhillipsBrown2025.vf_cannot_predict_both : ¬(Desire.BestWorlds.Want desRest belNapRest nap ∧ Desire.BestWorlds.Want desRest belNapRest napᶜ)

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

theorem PhillipsBrown2025.vf_no_conflict_nap : ¬(Desire.BestWorlds.Want desRest belNapRest nap ∧ Desire.BestWorlds.Want desRest belNapRest napᶜ)

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)

[Vil08] 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 : Desire.QuestionBased.IsConsidered qNapPass nap

theorem PhillipsBrown2025.fail_considered_in_qNapPass : Desire.QuestionBased.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

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetHappy : DecidablePred fun (x : W) => x ∈ happy

Equations

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

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetRain : DecidablePred fun (x : W) => x ∈ rain

Equations

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

def PhillipsBrown2025.naturalPropsLu : List (Finset W)

Test set of natural propositions for the Lu scenario.

Equations

• PhillipsBrown2025.naturalPropsLu = [{x : PhillipsBrown2025.W | x ∈ PhillipsBrown2025.rain}, {x : PhillipsBrown2025.W | x ∈ PhillipsBrown2025.happy}]

def PhillipsBrown2025.qDeckstacked : List (Finset 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

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetBelLu : DecidablePred fun (x : W) => x ∈ belLu

Equations

• PhillipsBrown2025.instDecidablePredWMemSetBelLu = PhillipsBrown2025.instDecidablePredWMemSetBelLu._aux_1

def PhillipsBrown2025.desHappy : List (Finset W)

Equations

• PhillipsBrown2025.desHappy = [{x : PhillipsBrown2025.W | x ∈ PhillipsBrown2025.happy}]

theorem PhillipsBrown2025.happy_not_considered_deckstacked : ¬Desire.QuestionBased.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 ∈ a, w ∈ happy

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 : Desire.QuestionBased.Want desHappy qDeckstacked belLu rainᶜ

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

def PhillipsBrown2025.qRainHappy : List (Finset 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 : Desire.QuestionBased.IsConsidered qRainHappy happy

theorem PhillipsBrown2025.not_rain_false_fair : ¬Desire.QuestionBased.Want desHappy qRainHappy belLu rainᶜ

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

theorem PhillipsBrown2025.qDeckstacked_fails_antideckstacking : ¬Desire.QuestionBased.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 : Desire.QuestionBased.IsAntiDeckstacking naturalPropsLu qRainHappy

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

theorem PhillipsBrown2025.qNapRest_satisfies_antideckstacking : Desire.QuestionBased.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 finest : List W → List (Finset 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 (Finset W)

Equations

• PhillipsBrown2025.qFinest = Desire.QuestionBased.finest PhillipsBrown2025.allWorldsW

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

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

theorem PhillipsBrown2025.finest_simulates_vf_nap : Desire.QuestionBased.Want desRest qFinest belNapRest nap ↔ Desire.BestWorlds.Want desRest belNapRest nap

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

theorem PhillipsBrown2025.finest_simulates_vf_not_nap : Desire.QuestionBased.Want desRest qFinest belNapRest napᶜ ↔ Desire.BestWorlds.Want desRest belNapRest napᶜ

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

theorem PhillipsBrown2025.finest_simulates_vf_not_lobster : Desire.QuestionBased.Want desNotDie qFinest belLobDie napᶜ ↔ Desire.BestWorlds.Want desNotDie belLobDie napᶜ

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

§9. Definedness via PartialProp (paper §3.6)

theorem PhillipsBrown2025.nap_defined_in_qNapRest : Desire.QuestionBased.Defined naturalProps qNapRest belNapRest nap

theorem PhillipsBrown2025.fail_not_defined_in_qNapRest : ¬Desire.QuestionBased.Defined naturalProps qNapRest belNapRest fail

theorem PhillipsBrown2025.nap_prprop_holds : (Desire.QuestionBased.toPartialProp desRest naturalProps qNapRest belNapRest nap).presup W.w0 ∧ (Desire.QuestionBased.toPartialProp desRest naturalProps qNapRest belNapRest nap).assertion W.w0

theorem PhillipsBrown2025.fail_prprop_undefined : ¬(Desire.QuestionBased.toPartialProp desRest naturalProps qNapRest belNapRest 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 Defined 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; [PB25] §4.2 argues that question-based semantics must be Strawson-but-not-naively upward monotonic, with definedness gating the inference. The substrate's toPartialProp_strawsonEntails captures the licit direction.

def PhillipsBrown2025.avoidWar : Set W

Equations

• PhillipsBrown2025.avoidWar = PhillipsBrown2025.nap

def PhillipsBrown2025.avoidNuclearWar : Set W

Equations

• PhillipsBrown2025.avoidNuclearWar = PhillipsBrown2025.nap ∪ PhillipsBrown2025.rested

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetAvoidWar : DecidablePred fun (x : W) => x ∈ avoidWar

Equations

• PhillipsBrown2025.instDecidablePredWMemSetAvoidWar = PhillipsBrown2025.instDecidablePredWMemSetAvoidWar._aux_1

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetAvoidNuclearWar : DecidablePred fun (x : W) => x ∈ avoidNuclearWar

Equations

• PhillipsBrown2025.instDecidablePredWMemSetAvoidNuclearWar = PhillipsBrown2025.instDecidablePredWMemSetAvoidNuclearWar._aux_1

def PhillipsBrown2025.qNuclear : List (Finset W)

Equations

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

def PhillipsBrown2025.naturalPropsNuclear : List (Finset 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 = [{x : PhillipsBrown2025.W | x ∈ PhillipsBrown2025.nap}, {x : PhillipsBrown2025.W | x ∈ PhillipsBrown2025.avoidNuclearWar}]

theorem PhillipsBrown2025.avoidWar_entails_avoidNuclearWar : avoidWar ⊆ avoidNuclearWar

theorem PhillipsBrown2025.avoidNuclearWar_considered : Desire.QuestionBased.IsConsidered qNuclear avoidNuclearWar

def PhillipsBrown2025.belWilliam : Set W

William III: total uncertainty (all worlds compatible).

Equations

• PhillipsBrown2025.belWilliam = Set.univ

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetBelWilliam : DecidablePred fun (x : W) => x ∈ belWilliam

Equations

• PhillipsBrown2025.instDecidablePredWMemSetBelWilliam x✝ = isTrue trivial

theorem PhillipsBrown2025.william_insensitive : ¬Desire.QuestionBased.IsBelSensitive qNuclear belWilliam

theorem PhillipsBrown2025.avoidNuclearWar_not_defined_william : ¬Desire.QuestionBased.Defined naturalPropsNuclear qNuclear belWilliam avoidNuclearWar

def PhillipsBrown2025.belModern : Set W

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

Equations

• PhillipsBrown2025.belModern = PhillipsBrown2025.nap ∪ PhillipsBrown2025.rested

@[instance_reducible]

instance PhillipsBrown2025.instDecidablePredWMemSetBelModern : DecidablePred fun (x : W) => x ∈ belModern

Equations

• PhillipsBrown2025.instDecidablePredWMemSetBelModern = PhillipsBrown2025.instDecidablePredWMemSetBelModern._aux_1

theorem PhillipsBrown2025.modern_sensitive : Desire.QuestionBased.IsBelSensitive qNuclear belModern

theorem PhillipsBrown2025.avoidNuclearWar_defined_modern : Desire.QuestionBased.Defined naturalPropsNuclear qNuclear belModern avoidNuclearWar

def PhillipsBrown2025.desAvoidWar : List (Finset W)

Equations

• PhillipsBrown2025.desAvoidWar = [{x : PhillipsBrown2025.W | x ∈ PhillipsBrown2025.nap}]

theorem PhillipsBrown2025.modern_wants_avoidNuclearWar : Desire.QuestionBased.Want desAvoidWar qNuclear belModern avoidNuclearWar

§11. Cross-paper bridge: [CL16]

[CL16]'s exact-match want over an effective — pointwise consistent — preferential background is jointly belief-consistent (PreferenceStructure.maxElts_pair_belief_compatible): if both Preferential.Want P a φ w and Preferential.Want P 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.

[PB25] 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: Preferential.Want / WantSufficient / WantNecessary). 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} (P : Agent → W → PreferenceStructure W) (hC : ∀ (a : Agent) (w : W), (P a w).consistent (B a w)) (a : Agent) (φ : Set W) (w : W) (hφ : Desire.Preferential.Want P a φ w) (hnegφ : Desire.Preferential.Want P a φᶜ w) : False

C&L's joint-belief-consistency, specialized to ψ = φᶜ: no single exact-match want over a consistent background 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 a different background per ascription to reproduce the contrast.

The belief-based class and its no-go (paper §2)

The paper's §2 thesis is class-level: conflicting desire ascriptions falsify every semantics on the orthodox belief-based approach — [Hei92], [vF99a], Levinson 2003, and their descendants. BeliefBasedDesireSemantics formalizes the class: a desire-semantic device over (Bel_S, parameters, evaluation world, proposition) with no contextual question parameter outside that shape. Both von Fintel and Heim are instances (vonFintelSemantics, heimSemantics), each proved conflict-blocking by delegation to the substrate's per-account no-go theorems (BestWorlds.Want.not_compl, Conditional.Want.not_compl).

PB's QuestionBased.Want 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 shape).

structure PhillipsBrown2025.BeliefBasedDesireSemantics (W : Type u_1) : Type (max u_1 (u_2 + 1))

A belief-based desire semantics on world type W: defined is the presuppositional definedness condition, want the truth condition. Decidability inside instances is supplied classically — the structure is for Prop-level reasoning, not for decide.

• Param : Type u_2

  Type of additional parameters (desire list for von Fintel, similarity + pref for Heim, etc.).

• defined : Set W → self.Param → Set W → Prop

  Definedness condition: the presupposition that ⟦S wants p⟧^c is defined at the configuration.

• want : Set W → self.Param → W → Set W → Prop

  Truth condition: when defined, the prediction of ⟦S wants p⟧^c.

def PhillipsBrown2025.BeliefBasedDesireSemantics.IsConflictBlocking {W : Type u_1} (F : BeliefBasedDesireSemantics W) : Prop

A semantics is conflict-blocking if no parameters/world make want(p) and want(¬p) both true when both are defined — the paper's §2 no-go in slogan form.

Equations

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

def PhillipsBrown2025.vonFintelSemantics {W : Type u_1} : BeliefBasedDesireSemantics W

von Fintel as a BeliefBasedDesireSemantics instance. defined requires both p- and ¬p-witnesses in belS — strong enough that some belS-world is necessarily undominated, which the no-go needs.

Equations

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

def PhillipsBrown2025.heimSemantics {W : Type u_1} : BeliefBasedDesireSemantics W

Heim as a BeliefBasedDesireSemantics instance: definedness is her (40) amendment.

Equations

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

theorem PhillipsBrown2025.vonFintelSemantics_IsConflictBlocking {W : Type u_1} [Finite W] : vonFintelSemantics.IsConflictBlocking

von Fintel is conflict-blocking (BestWorlds.Want.not_compl).

theorem PhillipsBrown2025.heimSemantics_IsConflictBlocking {W : Type u_1} [Finite W] (F : Desire.Conditional.Frame W) (w_eval : W) [Std.Antisymm (F.pref w_eval)] (belS p : Set W) : heimSemantics.defined belS F p → heimSemantics.defined belS F pᶜ → ¬(heimSemantics.want belS F w_eval p ∧ heimSemantics.want belS F w_eval pᶜ)

Heim is conflict-blocking at any frame and evaluation world with antisymmetric desirability (Conditional.Want.not_compl).

theorem PhillipsBrown2025.lassiter_evades_no_go_via_grading : ∃ (W : Type) (x : Fintype W) (pr : W → ℚ) (V : W → ℚ) (θ : ℚ) (bel : Set W) (p : Set W) (x_1 : DecidablePred fun (x : W) => x ∈ bel) (x_2 : DecidablePred fun (x : W) => x ∈ p), Desire.ExpectedValue.Want pr V θ bel p ∧ Desire.ExpectedValue.Want pr V θ bel pᶜ

[Las17a] also evades the no-go but via numerical threshold + graded value rather than question-sensitivity. The Lassiter substrate's exists_want_and_want_compl 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, and the universal finest-question identity want_finest_iff); the belief-based-class typology — the paper's own §2 packaging — is formalized above. The §11 bridge makes the disagreement with C&L explicit; heimSemantics_IsConflictBlocking shows the no-go covers Heim as well.

What's deferred:

• 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.

• [Crn14] is the acknowledged precursor of the question-based semantics; 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.