Docs / Semantics / Exhaustification / MinimalWorlds

Minimal-world exhaustification

import Linglib.Semantics.Exhaustification.MinimalWorlds · namespace Exhaustification

This file defines Spector's minimal-world exhaustifier exhMW ALT φ, the worlds of the prejacent φ whose set of true alternatives, Preorder.satisfied (· ∈ ·) ALT, is minimal among the prejacent's worlds. These are Kratzer's best worlds, with the prejacent as modal base and the negated alternatives as ordering source. Over finitely many alternatives every world of the prejacent lies above a minimal one, so a satisfiable prejacent has minimal worlds. An IsMinimalCover is a set of prejacent worlds representing the minimal worlds up to sharing their true alternatives; the exhaustifiers of InnocentExclusion and InnocentInclusion are computed from one.

Main statements

Exhaustification.exhMW_eq_minimals: minimal worlds are the minimal elements of the criteria preorder with the negated alternatives as criteria.
Exhaustification.exists_mem_exhMW_le: over finitely many alternatives, every world of the prejacent lies above a minimal world.

References

Groenendijk & Stokhof 1984, Studies on the Semantics of Questions and the Pragmatics of Answers formalized
Spector 2016, Comparing Exhaustivity Operators formalized
Kratzer 1981, The Notional Category of Modality formalized

Declarations

The minimal-world exhaustifier keeps the prejacent worlds whose set of true alternatives is minimal among the prejacent's worlds.

def exhMW L40–42

{W : Type u_1} (ALT : Set (Set W)) (φ : Set W) :

Set W

exhMW ALT φ = {u : W | MinimalFor (fun (x : W) => x ∈ φ) (Preorder.satisfied (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) ALT) u}

Used by mem_exhMW, exhMW_subset, mem_exhMW_iff_minimal, exhMW_eq_minimals, exists_mem_exhMW_le, exhMW_nonempty, exhMW_univ, instDecidablePredMemSetExhMWRangeOfFintype, instDecidablePredMemSetExhMWImageOfFintype, IsMinimalCover.exhMW_eq

Used in Semantics/Exhaustification/Disjunctive, Semantics/Exhaustification/InnocentExclusion, Denic2023, Enguehard2025, Fagen2026 and 4 more

L46–47

L49

L51–55

Minimal worlds are Kratzer's best worlds: the minimal elements of the criteria preorder whose criteria are the negated alternatives.

theorem exhMW_eq_minimals L58–67

{W : Type u_1} (ALT : Set (Set W)) (φ : Set W) :

exhMW ALT φ = (Preorder.ofCriteria (fun (w : W) (a : Set W) => w ∉ a) ALT).minimals φ

Built from

Over finitely many alternatives, every world of the prejacent lies above a minimal world.

theorem exists_mem_exhMW_le L69–75

{W : Type u_1} {ALT : Set (Set W)} {φ : Set W} {w : W} (hfin : ALT.Finite) (hw : w ∈ φ) :

∃ u ∈ exhMW ALT φ, Preorder.satisfied (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) ALT u ⊆ Preorder.satisfied (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) ALT w

Built from

Representative minimal worlds

A set of prejacent worlds represents the minimal worlds when every prejacent world lies above one of its members and no member's true alternatives strictly include another's.

structure IsMinimalCover L108–115

{W : Type u_1} (ALT : Set (Set W)) (φ M : Set W) :

Prop

mem (v : W) : v ∈ M → v ∈ φ
le (w : W) : w ∈ φ → ∃ v ∈ M, Preorder.satisfied (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) ALT v ⊆ Preorder.satisfied (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) ALT w
antisymm (v : W) : v ∈ M → ∀ u ∈ M, Preorder.satisfied (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) ALT u ⊆ Preorder.satisfied (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) ALT v → Preorder.satisfied (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) ALT v ⊆ Preorder.satisfied (fun (x1 : W) (x2 : Set W) => x1 ∈ x2) ALT u

Used by IsMinimalCover.exhMW_eq

Used in Semantics/Exhaustification/InnocentExclusion, Semantics/Exhaustification/InnocentInclusion, BarLevFox2020, Fox2007

L119–127