Conversational Backgrounds

[Kra81] [Kra12]

A conversational background maps worlds to sets of propositions. Two roles:

• Modal base (ModalBase) determines accessibility — R_f(w, w') ≡ w' ∈ ⋂f(w).
• Ordering source (OrderingSource) ranks accessible worlds by how many ordering propositions they satisfy.

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.ConvBackground (W : Type u_2) : Type u_2

A conversational background maps worlds to sets of propositions.

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

Equations

• Semantics.Modality.Kratzer.ConvBackground W = (W → List (W → Prop))

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.ModalBase (W : Type u_2) : Type u_2

The modal base: determines which worlds are accessible.

Equations

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

@[reducible, inline]

abbrev Semantics.Modality.Kratzer.OrderingSource (W : Type u_2) : Type u_2

The ordering source: determines how accessible worlds are ranked.

Equations

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

def Semantics.Modality.Kratzer.isRealistic {W : Type u_1} (f : ConvBackground W) : Prop

A conversational background is realistic iff for all w: w ∈ ⋂f(w). The actual world satisfies all propositions in the background.

[Kra81]: realistic conversational backgrounds make every fact about w part of ⋂f(w). UNVERIFIED page reference.

Equations

• Semantics.Modality.Kratzer.isRealistic f = ∀ (w : W), ∀ p ∈ f w, p w

def Semantics.Modality.Kratzer.isTotallyRealistic {W : Type u_1} (f : ConvBackground W) : Prop

A conversational background is totally realistic iff for all w: ⋂f(w) = {w}. The strongest form: only the actual world is accessible. UNVERIFIED page reference.

Equations

• Semantics.Modality.Kratzer.isTotallyRealistic f = ∀ (w : W), Intensional.Premise.propIntersection (f w) = {w}

def Semantics.Modality.Kratzer.emptyBackground {W : Type u_1} : ConvBackground W

The empty conversational background: f(w) = ∅ for all w. ⋂f(w) = W (vacuous intersection), so the empty background is itself trivially realistic. UNVERIFIED page reference.

Equations

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