def Semantics.Modality.PhillipsBrown.propEntails (p q : BProp Attitudes.Intensional.World) : Bool

p entails q iff every p-world is a q-world.

Equations

• Semantics.Modality.PhillipsBrown.propEntails p q = Semantics.Modality.propEntails Semantics.Attitudes.Intensional.allWorlds p q

def Semantics.Modality.PhillipsBrown.propOverlap (p q : BProp Attitudes.Intensional.World) : Bool

Propositions overlap iff they share at least one world.

Equations

• Semantics.Modality.PhillipsBrown.propOverlap p q = Semantics.Attitudes.Intensional.allWorlds.any fun (w : Semantics.Attitudes.Intensional.World) => p w && q w

def Semantics.Modality.PhillipsBrown.satisfiedBy (GS : List (BProp Attitudes.Intensional.World)) (a : BProp Attitudes.Intensional.World) : List (BProp Attitudes.Intensional.World)

Desires from G_S that proposition a satisfies (a entails p).

Equations

• Semantics.Modality.PhillipsBrown.satisfiedBy GS a = List.filter (fun (p : BProp Semantics.Attitudes.Intensional.World) => Semantics.Modality.PhillipsBrown.propEntails a p) GS

def Semantics.Modality.PhillipsBrown.preferAnswer (GS : List (BProp Attitudes.Intensional.World)) (a a' : BProp Attitudes.Intensional.World) : Bool

S prefers a to a' iff a satisfies strictly more desires.

Equations

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

def Semantics.Modality.PhillipsBrown.atLeastAsPreferred (GS : List (BProp Attitudes.Intensional.World)) (a a' : BProp Attitudes.Intensional.World) : Bool

a ≥ a' iff a satisfies all desires that a' satisfies.

Equations

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

def Semantics.Modality.PhillipsBrown.questionRelativeBelief (answers : List (BProp Attitudes.Intensional.World)) (belS : BProp Attitudes.Intensional.World) : List (BProp Attitudes.Intensional.World)

Q-Bel_S: answers compatible with S's beliefs.

Equations

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

def Semantics.Modality.PhillipsBrown.propEquiv (p q : BProp Attitudes.Intensional.World) : Bool

Extensional equivalence of propositions.

Equations

• Semantics.Modality.PhillipsBrown.propEquiv p q = Semantics.Attitudes.Intensional.allWorlds.all fun (w : Semantics.Attitudes.Intensional.World) => p w == q w

def Semantics.Modality.PhillipsBrown.bestAnswers (GS answers : List (BProp Attitudes.Intensional.World)) : List (BProp Attitudes.Intensional.World)

Best answers: those not strictly dominated by any other.

Equations

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

def Semantics.Modality.PhillipsBrown.wantQuestionBased (belS : BProp Attitudes.Intensional.World) (GS answers : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) : Bool

⟦S wants p⟧ = all best answers in Q-Bel_S entail p.

Equations

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

def Semantics.Modality.PhillipsBrown.wantBouletic (belS : BProp Attitudes.Intensional.World) (flavor : Kratzer.BouleticFlavor) (w : Attitudes.Intensional.World) (answers : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) : Bool

Convenience: extract desires from BouleticFlavor.

Equations

• Semantics.Modality.PhillipsBrown.wantBouletic belS flavor w answers p = Semantics.Modality.PhillipsBrown.wantQuestionBased belS (flavor.desires w) answers p

def Semantics.Modality.PhillipsBrown.considering (answers : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) : Bool

Considering: Q must have both p-answers and ¬p-answers.

Equations

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

def Semantics.Modality.PhillipsBrown.diversity (answers : List (BProp Attitudes.Intensional.World)) (belS : BProp Attitudes.Intensional.World) : Bool

Diversity: |Q-Bel_S| ≥ 2.

Equations

• Semantics.Modality.PhillipsBrown.diversity answers belS = decide ((Semantics.Modality.PhillipsBrown.questionRelativeBelief answers belS).length ≥ 2)

def Semantics.Modality.PhillipsBrown.antiDeckstacking (answers : List (BProp Attitudes.Intensional.World)) (belS : BProp Attitudes.Intensional.World) (GS : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) : Bool

Anti-deckstacking: question shouldn't trivially favor p.

This prevents "rigged" questions that make the desire ascription vacuously true.

Equations

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

def Semantics.Modality.PhillipsBrown.beliefSensitive (answers GS : List (BProp Attitudes.Intensional.World)) (p belS belS' : BProp Attitudes.Intensional.World) : Bool

Belief-sensitivity: S's beliefs affect the truth value.

This is built into the semantics via Q-Bel_S, but we can test whether the desire ascription is sensitive to belief changes.

Equations

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

theorem Semantics.Modality.PhillipsBrown.prefer_answer_transitive (GS : List (BProp Attitudes.Intensional.World)) (a a' a'' : BProp Attitudes.Intensional.World) (h1 : atLeastAsPreferred GS a a' = true) (h2 : atLeastAsPreferred GS a' a'' = true) : atLeastAsPreferred GS a a'' = true

Theorem: Preference between answers is transitive.

If S prefers a to a' and a' to a'', then S prefers a to a''.

theorem Semantics.Modality.PhillipsBrown.empty_desires_indifferent (a a' : BProp Attitudes.Intensional.World) : atLeastAsPreferred [] a a' = true

Theorem: Empty desires make all answers equivalent.

When G_S = ∅, no answer is preferred over another, so the agent is indifferent.

theorem Semantics.Modality.PhillipsBrown.empty_desires_belief_only (belS : BProp Attitudes.Intensional.World) (answers : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) : wantQuestionBased belS [] answers p = (questionRelativeBelief answers belS).all fun (a : BProp Attitudes.Intensional.World) => propEntails a p

Theorem: With empty desires, want reduces to belief compatibility.

If G_S = ∅, then ⟦S wants p⟧ = 1 iff every answer in Q-Bel_S entails p.

C-distributivity

A key diagnostic for question-sensitivity: whether ⟦x V Q⟧ ↔ ∃p ∈ Q. ⟦x V p⟧.

"Want" is NOT c-distributive in Phillips-Brown's analysis, while "know" and "wonder" are.

def Semantics.Modality.PhillipsBrown.isCDistributive (semantics : List (BProp Attitudes.Intensional.World) → BProp Attitudes.Intensional.World → Bool) (answers : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) : Bool

Test whether a predicate is c-distributive for a given scenario.

Returns true iff semantics(Q, p) = ∃a ∈ Q. semantics({a}, p)

Equations

• Semantics.Modality.PhillipsBrown.isCDistributive semantics answers p = (semantics answers p == answers.any fun (a : BProp Semantics.Attitudes.Intensional.World) => semantics [a] p)

def Semantics.Modality.PhillipsBrown.propositionOrdering (GS : List (BProp Attitudes.Intensional.World)) : SatisfactionOrdering (BProp Attitudes.Intensional.World) (BProp Attitudes.Intensional.World)

Proposition ordering: a satisfies p iff a entails p.

Equations

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

theorem Semantics.Modality.PhillipsBrown.satisfiedBy_eq_generic (GS : List (BProp Attitudes.Intensional.World)) (a : BProp Attitudes.Intensional.World) : satisfiedBy GS a = (propositionOrdering GS).satisfiedBy a

satisfiedBy matches SatisfactionOrdering.satisfiedBy.

def Semantics.Modality.PhillipsBrown.propositionPreorder (GS : List (BProp Attitudes.Intensional.World)) : Preorder (BProp Attitudes.Intensional.World)

Preorder derived from proposition ordering.

Equations

• Semantics.Modality.PhillipsBrown.propositionPreorder GS = (Semantics.Modality.PhillipsBrown.propositionOrdering GS).toPreorder

def Semantics.Modality.Kratzer.BouleticFlavor.evalWant (self : BouleticFlavor) (w : Attitudes.Intensional.World) (belS : BProp Attitudes.Intensional.World) (question : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) : Bool

Question-based desire: ⟦S wants p⟧ = all best answers in Q-Bel_S entail p.

Equations

• self.evalWant w belS question p = Semantics.Modality.PhillipsBrown.wantQuestionBased belS (self.desires w) question p

def Semantics.Modality.Kratzer.BouleticFlavor.preferenceOrdering (self : BouleticFlavor) (w : Attitudes.Intensional.World) : SatisfactionOrdering (BProp Attitudes.Intensional.World) (BProp Attitudes.Intensional.World)

Preference ordering on propositions at world w.

Equations

• self.preferenceOrdering w = Semantics.Modality.PhillipsBrown.propositionOrdering (self.desires w)

def Semantics.Modality.Kratzer.BouleticFlavor.getBestAnswers (self : BouleticFlavor) (w : Attitudes.Intensional.World) (answers : List (BProp Attitudes.Intensional.World)) : List (BProp Attitudes.Intensional.World)

Best answers according to S's desires at world w.

Equations

• self.getBestAnswers w answers = Semantics.Modality.PhillipsBrown.bestAnswers (self.desires w) answers

def Semantics.Modality.Kratzer.BouleticFlavor.liveAnswers (_self : BouleticFlavor) (question : List (BProp Attitudes.Intensional.World)) (belS : BProp Attitudes.Intensional.World) : List (BProp Attitudes.Intensional.World)

Answers compatible with S's beliefs.

Equations

• _self.liveAnswers question belS = Semantics.Modality.PhillipsBrown.questionRelativeBelief question belS

theorem Semantics.Modality.PhillipsBrown.bouletic_evalWant_eq (flavor : Kratzer.BouleticFlavor) (w : Attitudes.Intensional.World) (belS : BProp Attitudes.Intensional.World) (question : List (BProp Attitudes.Intensional.World)) (p : BProp Attitudes.Intensional.World) : flavor.evalWant w belS question p = wantQuestionBased belS (flavor.desires w) question p

Theorem: BouleticFlavor.evalWant = wantQuestionBased.

The extension is definitionally equal to the standalone function.

theorem Semantics.Modality.PhillipsBrown.empty_bouletic_indifferent (w : Attitudes.Intensional.World) (a a' : BProp Attitudes.Intensional.World) : preferAnswer (Kratzer.emptyBackground w) a a' = false

Corollary: Empty bouletic desires → agent is indifferent.

Summary: @cite{phillips-brown-2025} Integration

Core Functions

• satisfiedBy GS a: desires that proposition a satisfies
• preferAnswer GS a a': S prefers a to a'
• bestAnswers GS answers: optimal answers under preference
• questionRelativeBelief answers belS: Q-Bel_S, live answers
• wantQuestionBased belS GS answers p: main semantics
• wantBouletic: convenience wrapper using BouleticFlavor

Metasemantic Constraints

• considering: prejacent under consideration
• diversity: multiple live answers
• antiDeckstacking: question not rigged
• beliefSensitive: beliefs affect truth

Key Properties

• Preference is transitive (prefer_answer_transitive)
• Empty desires → indifference (empty_desires_indifferent)
• Automatically inherits from Kratzer's BouleticFlavor

The Unified Framework

Concept	Kratzer (Worlds)	Phillips-Brown (Props)	Generic
Type	World	BProp World	α
Ideals	List (BProp World)	List (BProp World)	List Ideal
Satisfies	p w	propEntails a p	o.satisfies
Ordering	atLeastAsGoodAs	atLeastAsPreferred	atLeastAsGood
Best	bestWorlds	bestAnswers	best