Conversational backgrounds

A premise set is a set of propositions A : Set (W → Prop). In the complete Boolean algebra W → Prop its infimum sInf A holds at the worlds verifying every premise, so p follows from A when sInf A ≤ p, and A is consistent when sInf A ≠ ⊥. A premise set also ranks worlds: w is at least as good as z when w verifies every premise z does, a preorder that is in general not total, whose minimal elements in a domain are its best worlds.

A conversational background assigns each world a premise set. Kratzer's modal base and ordering source are both conversational backgrounds, told apart only by their role: the premises of a modal base at w fix the worlds accessible from w, and those of an ordering source rank them.

Main definitions

• Background W: the backgrounds over W, a complete lattice pointwise, with ⊥ the empty background.
• Background.accessibleWorlds f w: the worlds verifying every premise of f w.
• Background.IsRealistic, Background.IsTotallyRealistic.
• Background.restrict f α: f with the premise α added at every world.
• premisePreorder A, w ≤[A] z, w <[A] z: the ordering a premise set induces.
• bestWorlds f g w: the minimal worlds accessible under f ranked by g.

Implementation notes

• w ≤[A] z and w <[A] z are notation for the order of premisePreorder A. A DecidableRel instance on that order would be keyed on every ≤-goal downstream, so a study that decides a premise ordering supplies a local instance for its own ordering source.

References

• [Kra77]
• [Kra81b]
• [Kra12b]

@[reducible, inline]

abbrev Modality.Background (W : Type u_2) : Type u_2

A conversational background assigns each world a premise set.

Equations

• Modality.Background W = (W → Set (W → Prop))

def Modality.Background.accessibleWorlds {W : Type u_1} (f : Background W) (w : W) : Set W

The worlds accessible from w under f are those verifying every premise of f w, Kratzer's ⋂f(w).

Equations

• f.accessibleWorlds w = {v : W | sInf (f w) v}

@[simp]

theorem Modality.Background.mem_accessibleWorlds {W : Type u_1} {f : Background W} {w v : W} : v ∈ f.accessibleWorlds w ↔ ∀ p ∈ f w, p v

theorem Modality.Background.accessibleWorlds_anti {W : Type u_1} {f f' : Background W} {w : W} (h : f w ⊆ f' w) : f'.accessibleWorlds w ⊆ f.accessibleWorlds w

More premises leave fewer accessible worlds.

@[simp]

theorem Modality.Background.accessibleWorlds_bot {W : Type u_1} (w : W) : ⊥.accessibleWorlds w = Set.univ

theorem Modality.Background.accessibleWorlds_sup {W : Type u_1} (f g : Background W) (w : W) : (f ⊔ g).accessibleWorlds w = {v : W | v ∈ f.accessibleWorlds w ∧ ∀ p ∈ g w, p v}

The worlds accessible under two backgrounds together are those accessible under the first that verify every premise of the second.

def Modality.Background.IsRealistic {W : Type u_1} (f : Background W) : Prop

A background is realistic when every world is accessible from itself, verifying its own premises.

Equations

• f.IsRealistic = ∀ (w : W), w ∈ f.accessibleWorlds w

def Modality.Background.IsTotallyRealistic {W : Type u_1} (f : Background W) : Prop

A background is totally realistic when its premises at a world single out that world.

Equations

• f.IsTotallyRealistic = ∀ (w : W), f.accessibleWorlds w = {w}

def Modality.Background.restrict {W : Type u_1} (f : Background W) (α : W → Prop) : Background W

The background f restricted by α, the premise a conditional antecedent adds, so that if α, must β is must_{f + α} β.

Equations

• f.restrict α w = insert α (f w)

@[simp]

theorem Modality.Background.mem_accessibleWorlds_restrict {W : Type u_1} {f : Background W} {w v : W} {α : W → Prop} : v ∈ (f.restrict α).accessibleWorlds w ↔ v ∈ f.accessibleWorlds w ∧ α v

theorem Modality.Background.accessibleWorlds_restrict {W : Type u_1} (f : Background W) (α : W → Prop) (w : W) : (f.restrict α).accessibleWorlds w = {v : W | v ∈ f.accessibleWorlds w ∧ α v}

theorem Modality.Background.accessibleWorlds_restrict_mono {W : Type u_1} {f : Background W} {w : W} {α₁ α₂ : W → Prop} (h : α₂ ≤ α₁) : (f.restrict α₂).accessibleWorlds w ⊆ (f.restrict α₁).accessibleWorlds w

A stronger antecedent leaves fewer accessible worlds.

The ordering

@[reducible, inline]

abbrev Modality.premisePreorder {W : Type u_1} (A : Set (W → Prop)) : Preorder W

The preorder that an ordering source induces ranks w below z when every proposition of A true at z is true at w. It is the criteria-derived preorder with truth as satisfaction.

Equations

• Modality.premisePreorder A = Preorder.ofCriteria (fun (w : W) (p : W → Prop) => p w) A

def Modality.«term_≤[_]_» : Lean.TrailingParserDescr

w ≤[A] z says that w is at least as good as z under the ordering source A, verifying every premise of A that z verifies.

Equations

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

def Modality.«term_<[_]_» : Lean.TrailingParserDescr

w <[A] z says that w is strictly better than z under the ordering source A.

Equations

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

Best worlds

def Modality.bestWorlds {W : Type u_1} (f g : Background W) (w : W) : Set W

The best accessible worlds from w are the minimal accessible worlds under the ordering source at w, the members that no other member strictly betters. The dominance form, at least as good as every member, is empty on an ordering that is not total, such as Kratzer's practical-inference example, so minimality is the faithful reading. Kratzer's official necessity is the limit-free humanNecessity, which quantifies over exactly this set under the Limit Assumption (humanNecessity_iff_necessity).

Equations

• Modality.bestWorlds f g w = (Modality.premisePreorder (g w)).minimals (f.accessibleWorlds w)

theorem Modality.mem_bestWorlds {W : Type u_1} {f g : Background W} {w u : W} : u ∈ bestWorlds f g w ↔ u ∈ f.accessibleWorlds w ∧ ∀ v ∈ f.accessibleWorlds w, v ≤ u → u ≤ v

@[simp]

theorem Modality.bestWorlds_bot {W : Type u_1} (f : Background W) (w : W) : bestWorlds f ⊥ w = f.accessibleWorlds w

With the empty ordering source the best worlds are the accessible ones.

theorem Modality.bestWorlds_eq_accessibleWorlds_sup {W : Type u_1} {f g : Background W} {w : W} (h : ((f ⊔ g).accessibleWorlds w).Nonempty) : bestWorlds f g w = (f ⊔ g).accessibleWorlds w

When some accessible world verifies every premise of the ordering source, the best worlds are the worlds accessible under the two backgrounds together.

theorem Modality.mem_bestWorlds_insert {W : Type u_1} {f g : Background W} {p q : W → Prop} {w u : W} (hq : q ∈ g w) (hpq : ∀ (v : W), q v → ¬p v) (hu : u ∈ bestWorlds f g w) (huq : q u) : u ∈ bestWorlds f (fun (v : W) => insert p (g v)) w

A best world verifying a member of the ordering source that excludes p stays best when p is added, because no p-world is at least as good, since it fails the member, and the other worlds are ordered as before.

theorem Modality.mem_bestWorlds_of_subset {W : Type u_1} {f f' g : Background W} {w u : W} (h : f'.accessibleWorlds w ⊆ f.accessibleWorlds w) (hu : u ∈ bestWorlds f g w) (hu' : u ∈ f'.accessibleWorlds w) : u ∈ bestWorlds f' g w

A best world of a modal base is a best world of any narrower modal base it is accessible under.