Conversational Backgrounds

@cite{kratzer-1981} @cite{kratzer-2012}

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.

Despite being introduced by Kratzer for natural-language modality, these are generic IL primitives — no Kratzer-specific commitments live here. The Kratzer-flavored modality theory in Theories/Semantics/Modality/Kratzer/ re-exports these so that consumers can keep using either namespace.

@[reducible, inline]

abbrev Core.Logic.Intensional.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

• Core.Logic.Intensional.ConvBackground W = (W → List (W → Prop))

@[reducible, inline]

abbrev Core.Logic.Intensional.ModalBase (W : Type u_2) : Type u_2

The modal base: determines which worlds are accessible.

Equations

• Core.Logic.Intensional.ModalBase W = Core.Logic.Intensional.ConvBackground W

@[reducible, inline]

abbrev Core.Logic.Intensional.OrderingSource (W : Type u_2) : Type u_2

The ordering source: determines how accessible worlds are ranked.

Equations

• Core.Logic.Intensional.OrderingSource W = Core.Logic.Intensional.ConvBackground W

def Core.Logic.Intensional.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.

@cite{kratzer-1981}: realistic conversational backgrounds make every fact about w part of ⋂f(w). UNVERIFIED page reference.

Equations

• Core.Logic.Intensional.isRealistic f = ∀ (w : W), ∀ p ∈ f w, p w

def Core.Logic.Intensional.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

• Core.Logic.Intensional.isTotallyRealistic f = ∀ (w : W), Core.Logic.Intensional.Premise.propIntersection (f w) = {w}

def Core.Logic.Intensional.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

• Core.Logic.Intensional.emptyBackground x✝ = []