Partition questions

The correspondence between partition-style inquiry ([GS84]'s question semantics, a Setoid W) and the more general inquisitive content Question W ([CGR18]). The embedding is one-way: every partition is an issue whose alternatives are its cells, but mention-some, intermediate-exhaustive, and conditional-question alternative sets are non-disjoint or non-exhaustive and are not the classes of any equivalence relation.

Main definitions

• fromSetoid r — the issue whose alternatives are the cells of r.
• fromSetoidEmbedding — fromSetoid bundled as an order embedding Setoid W ↪o Question W.
• IsPartition P — Setoid.IsPartition (alt P).
• toSetoid h — the equivalence relation of a partition issue.
• QUD.toQuestion q — the issue whose alternatives are a QUD's cells.

Main theorems

• fromSetoid_eq_iSup_ofSet_classes — a partition issue is the Hamblin disjunction of the declaratives generated by its cells.
• fromSetoid_le_iff — partition refinement is issue entailment.
• alt_fromSetoid, info_fromSetoid — the alternatives are the cells; partition issues are non-informative.
• isPartition_polar, isPartition_ofList — the basic Hamblin constructions yield partition issues under nontriviality / disjointness / cover hypotheses.
• toSetoid_fromSetoid, fromSetoid_toSetoid — the two round-trip directions of the partition–setoid correspondence.

The Setoid → Question embedding

def Question.fromSetoid {W : Type u_1} (r : Setoid W) : Question W

The issue raised by a setoid r: a state q resolves it iff q is empty or contained in an r-equivalence class.

Equations

• Question.fromSetoid r = Question.ofLowerSet {q : Set W | q = ∅ ∨ ∃ c ∈ r.classes, q ⊆ c} ⋯ ⋯

theorem Question.fromSetoid_eq_iSup_ofSet_classes {W : Type u_1} (r : Setoid W) : fromSetoid r = ⨆ c ∈ r.classes, ofSet c

A partition issue is the Hamblin disjunction of the declaratives generated by its cells — the fromSetoid instance of the shape the Resolutions Theorem (eq_iSup_ofSet_alt) establishes in general.

theorem Question.info_fromSetoid {W : Type u_1} (r : Setoid W) : (fromSetoid r).info = Set.univ

Partition-derived issues are non-informative: they raise an issue but supply no information.

Alternatives of fromSetoid

theorem Question.mem_alt_fromSetoid_of_mem_classes {W : Type u_1} (r : Setoid W) {c : Set W} (hc : c ∈ r.classes) : c ∈ (fromSetoid r).alt

Each cell of r is an alternative of fromSetoid r.

theorem Question.eq_empty_or_mem_classes_of_mem_alt_fromSetoid {W : Type u_1} (r : Setoid W) {p : Set W} (hp : p ∈ (fromSetoid r).alt) : p = ∅ ∨ p ∈ r.classes

Every alternative of fromSetoid r is the empty state or a cell of r (the empty case only when W is empty).

@[simp]

theorem Question.alt_fromSetoid {W : Type u_1} [Nonempty W] (r : Setoid W) : (fromSetoid r).alt = r.classes

The alternatives of fromSetoid r are exactly the cells of r. Nonemptiness rules out the degenerate ∅-alternative that appears when W is empty.

theorem Question.isInquisitive_fromSetoid_of_two_classes {W : Type u_1} (r : Setoid W) (w₁ w₂ : W) (hne : ¬r w₁ w₂) : (fromSetoid r).isInquisitive

A setoid with two distinct cells yields an inquisitive content.

Refinement is entailment

theorem Question.fromSetoid_le_iff {W : Type u_1} (r₁ r₂ : Setoid W) : fromSetoid r₁ ≤ fromSetoid r₂ ↔ r₁ ≤ r₂

The embedding reflects the order: a setoid is finer than another iff its issue entails the other's — Groenendijk–Stokhof's "partition refinement is question entailment".

def Question.fromSetoidEmbedding {W : Type u_1} : Setoid W ↪o Question W

fromSetoid as an order embedding: the Groenendijk–Stokhof partition order sits order-faithfully inside the inquisitive algebra. Companion of ofSetEmbedding, which embeds the declaratives.

Equations

• Question.fromSetoidEmbedding = OrderEmbedding.ofMapLEIff Question.fromSetoid ⋯

theorem Question.fromSetoid_mono {W : Type u_1} {r₁ r₂ : Setoid W} (h : r₁ ≤ r₂) : fromSetoid r₁ ≤ fromSetoid r₂

Monotonicity of the embedding.

theorem Question.fromSetoid_entails_iff {W : Type u_1} [Finite W] (r₁ r₂ : Setoid W) : (fromSetoid r₁).Entails (fromSetoid r₂) ↔ r₁ ≤ r₂

Under finiteness, question entailment between partition issues is the Setoid refinement order: the Question-level and Setoid-level encodings of refinement coincide.

IsPartition predicate

def 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

theorem 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.

theorem 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.

theorem 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.

theorem 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 lies in some alternative, hence in some resolving proposition.

toSetoid — equivalence relation from a partition issue

def 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

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

@[simp]

theorem 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 round-trip property of Setoid.mkClasses.

theorem 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.

Bridge to the Bool-based QUD

def QUD.toQuestion {W : Type u_1} (q : QUD W) : Question W

The issue raised by a QUD: its alternatives are exactly the QUD's equivalence classes. The bridge is one-way: not every Question arises from a QUD (mention-some, intermediate-exhaustive, and conditional-question alternatives are non-disjoint or non-exhaustive and so are not the cells of any equivalence relation — [TRA18]).

Equations

• q.toQuestion = Question.fromSetoid q.toSetoid

theorem QUD.refines_iff_toQuestion_entails {M : Type u_2} [Finite M] (q q' : QUD M) : q.refines q' ↔ q.toQuestion.Entails q'.toQuestion

QUD refinement is question entailment of the induced partition issues: the Bool-layer ⊑ agrees with the Question-layer entailment order.

Round-trips with fromSetoid

fromSetoid and toSetoid compose to the identity in both directions: on setoids whenever W is inhabited, and on partition issues whenever every resolving state extends to an alternative. The latter hypothesis is essential: over infinite W a partition issue may contain resolving states that extend to no alternative.

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

Under Nonempty W, fromSetoid r is a partition issue.

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

Round-trip, Setoid → Question → Setoid: the setoid derived from the partition issue of r is r itself.

theorem Question.fromSetoid_toSetoid {W : Type u_1} {P : Question W} (h : P.IsPartition) (hExt : ∀ p ∈ P.props, ∃ q ∈ P.alt, p ⊆ q) : fromSetoid (toSetoid h) = P

Round-trip, Question → Setoid → Question: a partition issue whose resolving states all extend to alternatives is recovered from its setoid. The extension hypothesis is discharged by exists_alt_above when P.props is finite.

IsPartition for the basic Hamblin constructions

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

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

theorem 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

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