Satisfaction Ordering (Linguistic Instantiations)

Linguistic applications of Core.SatisfactionOrdering.SatisfactionOrdering:

• Kratzer's world ordering (worlds by propositions)
• Phillips-Brown's proposition ordering (propositions by desires)

def Semantics.Modality.worldOrdering (World : Type u_1) (props : List (World → Bool)) : SatisfactionOrdering World (World → Bool)

Kratzer's world ordering: w satisfies p iff p(w) = true.

Equations

• Semantics.Modality.worldOrdering World props = { satisfies := fun (w : World) (p : World → Bool) => p w, criteria := props }

def Semantics.Modality.propositionOrdering (World : Type u_1) [BEq World] (worlds : List World) (desires : List (World → Bool)) : SatisfactionOrdering (World → Bool) (World → Bool)

Phillips-Brown's proposition ordering: a satisfies p iff a entails p.

Equations

• Semantics.Modality.propositionOrdering World worlds desires = { satisfies := fun (a p : World → Bool) => worlds.all fun (w : World) => !a w || p w, criteria := desires }

def Semantics.Modality.propEntails {World : Type u_1} (worlds : List World) (a p : World → Bool) : Bool

Proposition entailment: a entails p iff every a-world is a p-world.

Equations

• Semantics.Modality.propEntails worlds a p = worlds.all fun (w : World) => !a w || p w