Partition questions as inquisitive contents

A partition question of [GS84], a Setoid W, is the inquisitive content whose alternatives are its cells ([CGR18]). The embedding is one-way: mention-some, intermediate-exhaustive and conditional questions have alternatives that overlap or fail to cover the worlds, and are not the classes of any equivalence relation.

Main definitions

• Question.fromSetoid r: the content whose alternatives are the cells of r, bundled as an order embedding by Question.fromSetoidEmbedding.
• Question.IsPartition P: the alternatives of P partition the worlds.
• Question.toSetoid h: the equivalence relation of a partition content.

Main statements

• Question.fromSetoid_eq_iSup_ofSet_classes: a partition content is the join of the declaratives of its cells.
• Question.fromSetoid_le_iff: refinement of partitions is entailment.
• Question.fromSetoid_sInf: the embedding preserves arbitrary meets, so the content of a family's partition is the meet of its polar questions (Question.fromSetoid_polar).
• Question.alt_fromSetoid, Question.info_fromSetoid: the alternatives are the cells, and partition contents are not informative.
• Question.toSetoid_fromSetoid, Question.fromSetoid_toSetoid: the correspondence between partition contents and setoids.

References

• [GS84]
• [CGR18]

The Setoid → Question embedding

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

A state resolves the issue of a setoid r iff it is empty or included in an r-class.

Equations

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

theorem Question.mem_fromSetoid {W : Type u_1} {r : Setoid W} {q : Set W} : q ∈ fromSetoid r ↔ ∀ x ∈ q, ∀ y ∈ q, r x y

A state resolves a partition issue exactly when all its worlds are related.

theorem Question.fromSetoid_sInf {W : Type u_1} (S : Set (Setoid W)) : fromSetoid (sInf S) = ⨅ r ∈ S, fromSetoid r

The embedding preserves arbitrary meets: a state resolves the issue of a meet of setoids when it resolves the issue of each.

theorem Question.fromSetoid_iInf {W : Type u_1} {ι : Sort u_2} (f : ι → Setoid W) : fromSetoid (⨅ (i : ι), f i) = ⨅ (i : ι), fromSetoid (f i)

theorem Question.fromSetoid_inf {W : Type u_1} (r₁ r₂ : Setoid W) : fromSetoid (r₁ ⊓ r₂) = fromSetoid r₁ ⊓ fromSetoid r₂

@[simp]

theorem Question.fromSetoid_top {W : Type u_1} : fromSetoid ⊤ = ⊤

The trivial partition raises no issue.

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 (IsNormal.eq_iSup_ofSet_alt) establishes for every normal question.

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.isNormal_fromSetoid {W : Type u_1} (r : Setoid W) : (fromSetoid r).IsNormal

A partition issue is normal: a resolving state lies in a cell, and the empty state lies in any cell, or is the only state 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 is an order embedding of the setoids into the questions.

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.

Polar questions and decided propositions

theorem Question.fromSetoid_polar {W : Type u_1} (p : Set W) : fromSetoid (Setoid.polar p) = polar p

The partition issue of the polar question whether p is the inquisitive polar question.

theorem Question.decides_iff_fromSetoid_le {W : Type u_1} (r : Setoid W) (p : Set W) : r.Decides p ↔ fromSetoid r ≤ polar p

A partition decides p iff its issue entails the polar question whether p.

IsPartition predicate

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

A question is a partition when its alternatives partition W: no alternative is empty, and every world lies in a unique one.

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 of a partition question relates two worlds iff they lie in the same alternative.

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.

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

The setoid of the partition question of r is r.

theorem Question.fromSetoid_toSetoid {W : Type u_1} {P : Question W} (h : P.IsPartition) (hN : P.IsNormal) : fromSetoid (toSetoid h) = P

A normal partition question is recovered from its setoid. Normality is needed: on ℕ, adding the finite states to the issue of the parity partition leaves its alternatives unchanged.

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.