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

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

Equations

• Semantics.Modality.Desire.propEntails p q = Semantics.Attitudes.Intensional.allWorlds.all fun (w : Semantics.Attitudes.Intensional.World) => !p w || q w

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

Propositions overlap iff they share at least one world.

Equations

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

def Semantics.Modality.Desire.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.Desire.satisfiedBy GS a = List.filter (fun (p : BProp Semantics.Attitudes.Intensional.World) => Semantics.Modality.Desire.propEntails a p) GS

def Semantics.Modality.Desire.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.Desire.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.Desire.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

• Semantics.Modality.Desire.questionRelativeBelief answers belS = List.filter (fun (a : BProp Semantics.Attitudes.Intensional.World) => Semantics.Modality.Desire.propOverlap a belS) answers

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

Extensional equivalence of propositions.

Equations

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

def Semantics.Modality.Desire.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.Desire.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.

theorem Semantics.Modality.Desire.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.Desire.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.Desire.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.

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

Proposition ordering: a satisfies p iff a entails p.

Equations

• Semantics.Modality.Desire.propositionOrdering GS = { satisfies := fun (a p : BProp Semantics.Attitudes.Intensional.World) => Semantics.Modality.Desire.propEntails a p, criteria := GS }

theorem Semantics.Modality.Desire.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.Desire.propositionNormality (GS : List (BProp Attitudes.Intensional.World)) : Core.Order.NormalityOrder (BProp Attitudes.Intensional.World)

NormalityOrder derived from proposition ordering.

Equations

• Semantics.Modality.Desire.propositionNormality GS = (Semantics.Modality.Desire.propositionOrdering GS).toNormalityOrder

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.Desire.wantQuestionBased belS (self.desires w) question p

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

Preference ordering on propositions at world w.

Equations

• self.preferenceOrdering w = Semantics.Modality.Desire.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.Desire.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.Desire.questionRelativeBelief question belS

theorem Semantics.Modality.Desire.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.Desire.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

Key Properties

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

Metasemantic Constraints

Felicity conditions (Considering, Diversity, Anti-deckstacking) are defined in Phenomena.Modality.Studies.PhillipsBrown2025.

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