Documentation

Linglib.Phenomena.Modality.Studies.PhillipsBrown2025

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

Conflicting desire ascriptions — "S wants p" and "S wants ¬p" — falsify every belief-based semantics that is not question-sensitive. This study file verifies the core predictions from @cite{phillips-brown-2025} using an 8-world model (3 binary dimensions).

Results #

#	Prediction	Theorem
1	Nap is true (considering mood, ignoring exam)	`nap_true`
2	Not-nap is true (considering exam, ignoring mood)	`not_nap_true`
3	Fail is undefined in the Nap context	`fail_not_considered`
4	Lobster is true (considering taste, ignoring death)	`lobster_true`
5	Not-lobster is true (considering death, ignoring taste)	`not_lobster_true`
6	Not-die is also true in the Not-lobster context	`not_die_true`
7	Die is undefined in the Lobster context	`die_not_considered`
8	Standard vF cannot predict both Nap and Not-nap	`vf_cannot_predict_both`

inductive Phenomena.Modality.Studies.PhillipsBrown2025.W :

8 worlds encoding 3 binary dimensions (d₁ × d₂ × d₃). For Nap: d₁ = nap, d₂ = rested, d₃ = pass. For Lobster: d₁ = eat lobster, d₂ = gustatory, d₃ = ¬die.

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

Instances For

instance Phenomena.Modality.Studies.PhillipsBrown2025.instDecidableEqW :

Equations

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

def Phenomena.Modality.Studies.PhillipsBrown2025.instBEqW.beq :

W → W → Bool

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.instBEqW.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance Phenomena.Modality.Studies.PhillipsBrown2025.instBEqW :

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.instBEqW = { beq := Phenomena.Modality.Studies.PhillipsBrown2025.instBEqW.beq }

instance Phenomena.Modality.Studies.PhillipsBrown2025.instReprW :

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.instReprW = { reprPrec := Phenomena.Modality.Studies.PhillipsBrown2025.instReprW.repr }

def Phenomena.Modality.Studies.PhillipsBrown2025.instReprW.repr :

W → ℕ → Std.Format

Equations

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

Instances For

instance Phenomena.Modality.Studies.PhillipsBrown2025.instInhabitedW :

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.instInhabitedW = { default := Phenomena.Modality.Studies.PhillipsBrown2025.instInhabitedW.default }

def Phenomena.Modality.Studies.PhillipsBrown2025.instInhabitedW.default :

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.instInhabitedW.default = Phenomena.Modality.Studies.PhillipsBrown2025.W.w0

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.allW :

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.entails (a p : W → Bool) :

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.entails a p = Phenomena.Modality.Studies.PhillipsBrown2025.allW.all fun (w : Phenomena.Modality.Studies.PhillipsBrown2025.W) => !a w || p w

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.overlap (a q : W → Bool) :

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.overlap a q = Phenomena.Modality.Studies.PhillipsBrown2025.allW.any fun (w : Phenomena.Modality.Studies.PhillipsBrown2025.W) => a w && q w

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.satisfiedBy (GS : List (W → Bool)) (a : W → Bool) :

List (W → Bool)

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.propEquiv (p q : W → Bool) :

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.propEquiv p q = Phenomena.Modality.Studies.PhillipsBrown2025.allW.all fun (w : Phenomena.Modality.Studies.PhillipsBrown2025.W) => p w == q w

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.preferAnswer (GS : List (W → Bool)) (a a' : W → Bool) :

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.bestAnswers (GS answers : List (W → Bool)) :

List (W → Bool)

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.qBel (answers : List (W → Bool)) (belS : W → Bool) :

List (W → Bool)

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.want (belS : W → Bool) (GS answers : List (W → Bool)) (p : W → Bool) :

⟦S wants p⟧^c = all best answers in Q_c-Bel_S are p-answers.

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.isConsidered (answers : List (W → Bool)) (p : W → Bool) :

p is considered relative to Q iff every answer settles p. Considering Constraint: ⟦S wants p⟧^c is defined only if p is considered relative to Q_c.

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.isDiverse (answers : List (W → Bool)) (p : W → Bool) :

Diversity: Q_c must contain both p-answers and ¬p-answers.

Equations

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

Instances For

World assignment: | 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 Phenomena.Modality.Studies.PhillipsBrown2025.fail :

W → Bool

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.fail w = !Phenomena.Modality.Studies.PhillipsBrown2025.pass w

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.qNapRest :

List (W → Bool)

Q' = partition by nap × rested (4 cells, 2 worlds each).

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.qNapPass :

List (W → Bool)

Q'' = partition by nap × pass (4 cells, 2 worlds each).

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.belNapRest :

W → Bool

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

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.belNapPass :

W → Bool

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

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.desRest :

List (W → Bool)

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.desRest = [Phenomena.Modality.Studies.PhillipsBrown2025.rested ]

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.desPass :

List (W → Bool)

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.desPass = [Phenomena.Modality.Studies.PhillipsBrown2025.pass ]

Instances For

theorem Phenomena.Modality.Studies.PhillipsBrown2025.nap_true :

want belNapRest desRest qNapRest nap = true

Nap is true relative to Q' with beliefs nap↔rested, desires [rested]. Best in Q'-Bel: n∧r = {w0,w1} entails nap.

theorem Phenomena.Modality.Studies.PhillipsBrown2025.not_nap_true :

(want belNapPass desPass qNapPass fun (w : W) => !nap w) = true

Not-nap is true relative to Q'' with beliefs pass↔¬nap, desires [pass]. Best in Q''-Bel: ¬n∧p = {w4,w6} entails ¬nap.

theorem Phenomena.Modality.Studies.PhillipsBrown2025.fail_not_considered :

isConsidered qNapRest fail = false

Fail is NOT considered relative to Q': each cell contains both pass-worlds and fail-worlds, so no cell settles whether you fail.

theorem Phenomena.Modality.Studies.PhillipsBrown2025.fail_not_true :

want belNapRest desRest qNapRest fail = false

Fail is also not predicted true (best answers don't entail fail).

theorem Phenomena.Modality.Studies.PhillipsBrown2025.nap_diverse :

isDiverse qNapRest nap = true

Q' is diverse w.r.t. nap: both nap-answers and ¬nap-answers exist.

The Lobster scenario is structurally isomorphic to Nap:

dim1 = eat lobster = nap
dim2 = gustatory experience = rested
dim3 = ¬die = pass (so die = fail)

@[reducible, inline]

abbrev Phenomena.Modality.Studies.PhillipsBrown2025.lobster :

W → Bool

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.lobster = Phenomena.Modality.Studies.PhillipsBrown2025.nap

Instances For

@[reducible, inline]

abbrev Phenomena.Modality.Studies.PhillipsBrown2025.gustatory :

W → Bool

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.gustatory = Phenomena.Modality.Studies.PhillipsBrown2025.rested

Instances For

@[reducible, inline]

abbrev Phenomena.Modality.Studies.PhillipsBrown2025.die :

W → Bool

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.die = Phenomena.Modality.Studies.PhillipsBrown2025.fail

Instances For

theorem Phenomena.Modality.Studies.PhillipsBrown2025.lobster_true :

want belNapRest desRest qNapRest lobster = true

Lobster is true (same computation as Nap).

theorem Phenomena.Modality.Studies.PhillipsBrown2025.die_not_considered :

isConsidered qNapRest die = false

Die is not considered in the Lobster context (= Q').

def Phenomena.Modality.Studies.PhillipsBrown2025.qLobDie :

List (W → Bool)

Q_c''' = partition by lobster × die.

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.belLobDie :

W → Bool

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

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.desNotDie :

List (W → Bool)

Equations

Phenomena.Modality.Studies.PhillipsBrown2025.desNotDie = [fun (w : Phenomena.Modality.Studies.PhillipsBrown2025.W) => !Phenomena.Modality.Studies.PhillipsBrown2025.fail w]

Instances For

theorem Phenomena.Modality.Studies.PhillipsBrown2025.not_lobster_true :

(want belLobDie desNotDie qLobDie fun (w : W) => !nap w) = true

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

theorem Phenomena.Modality.Studies.PhillipsBrown2025.not_die_true :

(want belLobDie desNotDie qLobDie fun (w : W) => !fail w) = true

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

def Phenomena.Modality.Studies.PhillipsBrown2025.atLeastAsGood (GS : List (W → Bool)) (w z : W) :

Kratzer-style world ordering: w at least as good as z iff w satisfies every desire that z satisfies.

Equations

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

Instances For

def Phenomena.Modality.Studies.PhillipsBrown2025.wantVF (belS : W → Bool) (GS : List (W → Bool)) (p : W → Bool) :

Standard von Fintel semantics (not question-based): ⟦S wants p⟧ = all best worlds in Bel_S are p-worlds.

Equations

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

Instances For

theorem Phenomena.Modality.Studies.PhillipsBrown2025.vf_nap_true :

wantVF belNapRest desRest nap = true

VF correctly predicts Nap.

theorem Phenomena.Modality.Studies.PhillipsBrown2025.vf_not_nap_false :

(wantVF belNapRest desRest fun (w : W) => !nap w) = false

VF cannot also predict Not-nap (want is not context-sensitive).

theorem Phenomena.Modality.Studies.PhillipsBrown2025.vf_cannot_predict_both :

¬(wantVF belNapRest desRest nap = true ∧ (wantVF belNapRest desRest fun (w : W) => !nap w) = true)

VF cannot predict both Nap and Not-nap with any single parameter set.

On standard vF, want(nap) + Bel(nap ↔ fail) → want(fail): the best nap-worlds are also fail-worlds, so "all best are fail-worlds."

The question-based semantics blocks this: fail is not considered in Q', so ⟦want(fail)⟧^Q' is undefined. The block is fail_not_considered above.

theorem Phenomena.Modality.Studies.PhillipsBrown2025.nap_considered_in_qNapPass :

isConsidered qNapPass nap = true

In the Not-nap context Q'', nap IS considered (every cell settles nap).

theorem Phenomena.Modality.Studies.PhillipsBrown2025.fail_considered_in_qNapPass :

isConsidered qNapPass fail = true

Fail IS considered in Q'' (pass is a partition dimension, so fail = ¬pass is settled by every cell). But fail is NOT considered in Q' — and that is what blocks the doxastic closure inference in the Nap context.