def Semantics.Modality.Kratzer.propExtension (p : BProp Attitudes.Intensional.World) : List Attitudes.Intensional.World

Convert to list of worlds where proposition holds.

Equations

• Semantics.Modality.Kratzer.propExtension p = List.filter p Semantics.Attitudes.Intensional.allWorlds

def Semantics.Modality.Kratzer.propIntersection (props : List (BProp Attitudes.Intensional.World)) : List Attitudes.Intensional.World

The intersection of a set of propositions: worlds satisfying ALL.

Equations

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

def Semantics.Modality.Kratzer.followsFrom (p : BProp Attitudes.Intensional.World) (A : List (BProp Attitudes.Intensional.World)) : Bool

A proposition p follows from a set A iff ∩A ⊆ p (Kratzer p. 31)

In other words: every world satisfying all of A also satisfies p.

Equations

• Semantics.Modality.Kratzer.followsFrom p A = (Semantics.Modality.Kratzer.propIntersection A).all p

def Semantics.Modality.Kratzer.isConsistent (A : List (BProp Attitudes.Intensional.World)) : Bool

A set of propositions is consistent iff ∩A ≠ ∅ (Kratzer p. 31)

Equations

• Semantics.Modality.Kratzer.isConsistent A = !(Semantics.Modality.Kratzer.propIntersection A).isEmpty

def Semantics.Modality.Kratzer.isCompatibleWith (p : BProp Attitudes.Intensional.World) (A : List (BProp Attitudes.Intensional.World)) : Bool

A proposition p is compatible with A iff A ∪ {p} is consistent (Kratzer p. 31)

Equations

• Semantics.Modality.Kratzer.isCompatibleWith p A = Semantics.Modality.Kratzer.isConsistent (p :: A)

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.ConvBackground : Type

A conversational background maps worlds to sets of propositions.

This is Kratzer's key innovation: the modal base and ordering source are both conversational backgrounds, but play different roles.

Equations

• Semantics.Modality.Kratzer.ConvBackground = (Semantics.Attitudes.Intensional.World → List (BProp Semantics.Attitudes.Intensional.World))

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.ModalBase : Type

The modal base: determines which worlds are accessible.

Equations

• Semantics.Modality.Kratzer.ModalBase = Semantics.Modality.Kratzer.ConvBackground

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.OrderingSource : Type

The ordering source: determines how accessible worlds are ranked.

Equations

• Semantics.Modality.Kratzer.OrderingSource = Semantics.Modality.Kratzer.ConvBackground

def Semantics.Modality.Kratzer.isRealistic (f : ConvBackground) : Prop

A conversational background is realistic iff for all w: w ∈ ∩f(w).

This means the actual world satisfies all propositions in the modal base. Kratzer (p. 32): "For each world, there is a particular body of facts in w that has a counterpart in each world in ∩f(w)."

Equations

• Semantics.Modality.Kratzer.isRealistic f = ∀ (w : Semantics.Attitudes.Intensional.World), ((f w).all fun (p : BProp Semantics.Attitudes.Intensional.World) => p w) = true

def Semantics.Modality.Kratzer.isTotallyRealistic (f : ConvBackground) : Prop

A conversational background is totally realistic iff for all w: ∩f(w) = {w}.

This is the strongest form: only the actual world is accessible. Kratzer (p. 33): "A totally realistic conversational background is a function f such that for any world w, ∩f(w) = {w}."

Equations

• Semantics.Modality.Kratzer.isTotallyRealistic f = ∀ (w : Semantics.Attitudes.Intensional.World), Semantics.Modality.Kratzer.propIntersection (f w) = [w]

def Semantics.Modality.Kratzer.emptyBackground : ConvBackground

The empty conversational background: f(w) = ∅ for all w.

Kratzer (p. 33): "The empty conversational background is the function f such that for any w ∈ W, f(w) = ∅. Since ∩f(w) = W if f(w) = ∅, empty conversational backgrounds are also realistic."

Equations

• Semantics.Modality.Kratzer.emptyBackground x✝ = []