Question — partition predicate, Setoid bridge, QUD bridge

@cite{groenendijk-stokhof-1984} @cite{roberts-2012} @cite{ciardelli-groenendijk-roelofsen-2018}

Bridge from Question W (downward-closed nonempty families of information states) to partition-style inquiry in mathlib's Setoid.IsPartition sense, plus a legacy bridge to the Bool-based QUD W.

Main definitions

• IsPartition P — Setoid.IsPartition (alt P). Mention-some, intermediate-exhaustive, and conditional-question alternative sets are not partitions and so fail this predicate.
• toSetoid h — the equivalence relation derived from a partition issue (two worlds equivalent iff they share an alternative cell).
• toQUD h — bridge to legacy Bool-based QUD W. noncomputable, uses classical decidability of the underlying equivalence.

Main theorems

• info_eq_univ, pairwiseDisjoint, nonempty_of_mem_alt, sUnion_alt_eq_univ — partition issues are non-informative and their alternative sets are partitions in the standard sense.
• isPartition_polar, isPartition_ofList — the basic Hamblin constructions yield partition issues under nontriviality / disjointness / cover hypotheses.
• toSetoid_fromSetoid — Setoid → Question → Setoid is the identity (round-trip with fromSetoid from Core/Mood/PartitionAsInquiry.lean).

IsPartition predicate

def Core.Question.IsPartition {W : Type u_1} (P : Question W) : Prop

An issue is a partition iff its alternative set is a partition of W in mathlib's Setoid.IsPartition sense: no empty alternative, and every world lies in a unique alternative. The Groenendijk–Stokhof partition shape.

Equations

• P.IsPartition = Setoid.IsPartition P.alt

@[simp]

theorem Core.Question.IsPartition.info_eq_univ {W : Type u_1} {P : Question W} (h : P.IsPartition) : P.info = Set.univ

Partition issues are non-informative: every world is covered by some alternative, hence by some resolving proposition, so info P = Set.univ.

theorem Core.Question.IsPartition.pairwiseDisjoint {W : Type u_1} {P : Question W} (h : P.IsPartition) : P.alt.PairwiseDisjoint id

Alternatives of a partition issue are pairwise disjoint. Direct inheritance from mathlib's Setoid.IsPartition.pairwiseDisjoint.

theorem Core.Question.IsPartition.nonempty_of_mem_alt {W : Type u_1} {P : Question W} (h : P.IsPartition) {p : Set W} (hp : p ∈ P.alt) : p.Nonempty

Alternatives of a partition issue are nonempty. Mathlib's Setoid.nonempty_of_mem_partition specialized to Question.

theorem Core.Question.IsPartition.sUnion_alt_eq_univ {W : Type u_1} {P : Question W} (h : P.IsPartition) : ⋃₀ P.alt = Set.univ

The union of a partition issue's alternatives is the whole universe.

toSetoid — equivalence relation from a partition issue

def Core.Question.toSetoid {W : Type u_1} {P : Question W} (h : P.IsPartition) : Setoid W

The setoid derived from a partition issue: two worlds are equivalent iff they lie in the same alternative cell. Built from mathlib's Setoid.mkClasses on the alternative set.

Equations

• Core.Question.toSetoid h = Setoid.mkClasses P.alt ⋯

@[simp]

theorem Core.Question.classes_toSetoid {W : Type u_1} {P : Question W} (h : P.IsPartition) : (toSetoid h).classes = P.alt

The equivalence classes of toSetoid h are exactly the alternatives of P. The defining roundtrip property of Setoid.mkClasses.

theorem Core.Question.toSetoid_rel_iff {W : Type u_1} {P : Question W} (h : P.IsPartition) (w v : W) : (toSetoid h) w v ↔ ∃ p ∈ P.alt, w ∈ p ∧ v ∈ p

Two worlds are related under toSetoid h iff they share an alternative cell — the linguistic reading of the underlying equivalence relation.

toQUD — bridge to the legacy Bool-based QUD

noncomputable def Core.Question.toQUD {W : Type u_1} {P : Question W} (h : P.IsPartition) : QUD W

Bridge to legacy Bool-based QUD W: two worlds get the same answer iff they share an alternative cell. noncomputable — decidability of the underlying equivalence is supplied classically.

Equations

• Core.Question.toQUD h = { toSetoid := Core.Question.toSetoid h, decR := fun (w v : W) => Classical.dec ((Core.Question.toSetoid h) w v) }

theorem Core.Question.toQUD_r_iff {W : Type u_1} {P : Question W} (h : P.IsPartition) (w v : W) : (toQUD h).r w v ↔ ∃ p ∈ P.alt, w ∈ p ∧ v ∈ p

toQUD's relation holds iff the two worlds share an alternative cell.

theorem Core.Question.toQUD_sameAnswer_iff {W : Type u_1} {P : Question W} (h : P.IsPartition) (w v : W) : (toQUD h).sameAnswer w v = true ↔ ∃ p ∈ P.alt, w ∈ p ∧ v ∈ p

toQUD's sameAnswer is true iff the two worlds share a cell.

theorem Core.Question.cell_toQUD_mem_alt {W : Type u_1} {P : Question W} (h : P.IsPartition) (w : W) : (toQUD h).cell w ∈ P.alt

The cell of a world under toQUD h is in alt P.

theorem Core.Question.mem_cell_toQUD {W : Type u_1} {P : Question W} (h : P.IsPartition) (w : W) : w ∈ (toQUD h).cell w

A world lies in its own toQUD cell.

theorem Core.Question.cell_toQUD_eq {W : Type u_1} {P : Question W} (h : P.IsPartition) {p : Set W} (hpAlt : p ∈ P.alt) {w : W} (hwp : w ∈ p) : (toQUD h).cell w = p

The toQUD cell of any world in an alternative p is exactly p.

Round-trip with fromSetoid

The Setoid → Question embedding (fromSetoid, in Core/Mood/PartitionAsInquiry.lean) and Question → Setoid projection (toSetoid) compose to the identity on partition-shaped issues.

theorem Core.Question.isPartition_fromSetoid {W : Type u_1} [Nonempty W] (r : Setoid W) : (fromSetoid r).IsPartition

Under Nonempty W, fromSetoid r is a partition issue. The nonemptiness assumption rules out the degenerate ∅-alternative that would otherwise appear when W is empty.

theorem Core.Question.toSetoid_fromSetoid {W : Type u_1} [Nonempty W] (r : Setoid W) : toSetoid ⋯ = r

Round-trip: the setoid derived from a partition issue built from a setoid recovers the original setoid. The Setoid → Question → Setoid direction of the partition–setoid correspondence.

IsPartition for the basic Hamblin constructions

theorem Core.Question.isPartition_polar {W : Type u_1} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : (polar p).IsPartition

Question.polar p is a partition issue when p is non-trivial: the two alternatives p and pᶜ partition W by LEM.

theorem Core.Question.isPartition_ofList {W : Type u_1} {L : List (Set W)} (hL : L ≠ []) (hdisj : ∀ p₁ ∈ L, ∀ p₂ ∈ L, p₁ ≠ p₂ → Disjoint p₁ p₂) (hne : ∀ p ∈ L, p ≠ ∅) (hcover : ∀ (w : W), ∃ p ∈ L, w ∈ p) : (ofList L).IsPartition

Question.ofList L is a partition issue when L is a nonempty list of pairwise-disjoint nonempty cells that exhaust W.