Alternatives and minimal worlds

A set of alternatives ALT : Set (Set World) preorders worlds by the alternatives they verify: u ≤[ALT] v when every alternative true at u is true at v. The minimal-world exhaustifier exhMW keeps the prejacent worlds that are minimal in this preorder; for finite ALT the strict order is well-founded, so a satisfiable prejacent has minimal worlds. A set of prejacent worlds is an IsMinimalCover when it represents the minimal worlds up to equivalence; the exhaustifiers of InnocentExclusion and InnocentInclusion are computed from one.

References

• [groenendijk-stokhof-1984]
• [Spe16]

def Exhaustification.leALT {World : Type u_1} (ALT : Set (Set World)) (u v : World) : Prop

u ≤[ALT] v when every alternative true at u is true at v.

Equations

• (u ≤[ALT] v) = ∀ a ∈ ALT, a u → a v

def Exhaustification.ltALT {World : Type u_1} (ALT : Set (Set World)) (u v : World) : Prop

u <[ALT] v when u verifies strictly fewer alternatives than v.

Equations

• (u <[ALT] v) = ((u ≤[ALT] v) ∧ ¬v ≤[ALT] u)

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

u ≤[ALT] v when every alternative true at u is true at v.

Equations

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

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

u <[ALT] v when u verifies strictly fewer alternatives than v.

Equations

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

theorem Exhaustification.leALT_refl {World : Type u_1} (ALT : Set (Set World)) (u : World) : u ≤[ALT] u

theorem Exhaustification.leALT_trans {World : Type u_1} (ALT : Set (Set World)) (u v w : World) (huv : u ≤[ALT] v) (hvw : v ≤[ALT] w) : u ≤[ALT] w

def Exhaustification.exhMW {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : Set World

The minimal-world exhaustifier: the prejacent worlds with no prejacent world strictly below them.

Equations

• Exhaustification.exhMW ALT φ u = (φ u ∧ ¬∃ (v : World), φ v ∧ v <[ALT] u)

def Exhaustification.IsMinimal {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (u : World) : Prop

A minimal prejacent world.

Equations

• Exhaustification.IsMinimal ALT φ u = (u ∈ Exhaustification.exhMW ALT φ)

theorem Exhaustification.exhMW_subset {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) : exhMW ALT φ ⊆ φ

theorem Exhaustification.ltALT_wf_of_finite {World : Type u_1} (ALT : Set (Set World)) (hfin : ALT.Finite) : WellFounded (ltALT ALT)

For finite ALT the strict order is well-founded: it is the pullback of strict inclusion along the finite set of alternatives a world verifies.

theorem Exhaustification.exists_minimal_of_finite {World : Type u_1} (ALT : Set (Set World)) (φ : Set World) (hfin : ALT.Finite) (hsat : ∃ (w : World), φ w) : ∃ (u : World), IsMinimal ALT φ u

A satisfiable prejacent has a minimal world when ALT is finite.

Representative minimal worlds

structure Exhaustification.IsMinimalCover {World : Type u_1} (ALT : Set (Set World)) (φ M : Set World) : Prop

A set of prejacent worlds represents the minimal worlds when every prejacent world lies above one of its members and no member lies strictly below another.

• mem (v : World) : v ∈ M → φ v
• le (w : World) : φ w → ∃ v ∈ M, v ≤[ALT] w
• antisymm (v : World) : v ∈ M → ∀ u ∈ M, (u ≤[ALT] v) → v ≤[ALT] u

theorem Exhaustification.IsMinimalCover.exhMW_eq {World : Type u_1} {ALT : Set (Set World)} {φ M : Set World} (hM : IsMinimalCover ALT φ M) : exhMW ALT φ = {u : World | φ u ∧ ∃ v ∈ M, (v ≤[ALT] u) ∧ u ≤[ALT] v}

The minimal worlds are the prejacent worlds equivalent to a representative.