Partition as Inquiry — Setoid → Question embedding

[CGR18] [TRA18] [Pun19]

The faithful embedding of partition-based inquiry (Setoid W — what POSWQ.inquiry carries) into the more general inquisitive-content representation (Question W — downward-closed nonempty families of information states).

Architectural placement

This file implements the embedding direction prescribed in the "Architectural note: Setoid vs. Question" section of POSWQ.lean (added 0.229.922): we keep inquiry : Setoid W as the field of POSWQ (partitions are the right shape for the propositional- discourse use cases that currently exist), and provide a one-way embedding Setoid → Question. The embedding goes this way and not the other because every Setoid-based partition can be expressed as an Question (each equivalence class becomes a maximal proposition / alternative), but the reverse fails — mention-some, intermediate-exhaustive, and conditional question alternatives are non-disjoint or non-exhaustive and so are not representable as the classes of any equivalence relation (see [TRA18]).

This mirrors mathlib's Set.toFinset / Filter.principal / UniformSpace.toTopologicalSpace pattern: the "less general" structure sits inside the "more general" one via a faithful but not surjective forgetful map.

What this gives us

• fromSetoid r : Question W — the inquisitive content whose alternatives are the equivalence classes of r. Concretely, props = {q | q = ∅ ∨ ∃ c ∈ r.classes, q ⊆ c}: a non-empty information state q resolves the issue iff it is contained in some equivalence class (i.e., everything in q is r-equivalent).
• info_fromSetoid — informative content is Set.univ. Setoid-based inquiry is non-informative: it raises an issue but supplies no information. (This matches the standard partition-semantics view.)
• isInquisitive_fromSetoid_of_two_classes — if r has at least two distinct equivalence classes, the resulting content is inquisitive (in Question's sense: info ∉ props). The trivial partition (one class) yields a declarative.

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

The Question associated with a setoid r on W: a proposition q resolves the issue iff q = ∅ or q is contained in some r-equivalence class (i.e., everything in q agrees on the r-question). The maximal such propositions are the equivalence classes themselves.

Equations

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

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

The informative content of a partition-based inquiry is the whole universe: every world is in some equivalence class, so every world appears in some resolving proposition. Setoid-derived inquisitive contents are non-informative — they raise issues but provide no information.

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

If a setoid has two distinct equivalence classes, the resulting inquisitive content is inquisitive: Set.univ is not contained in any single equivalence class (it would have to coincide with both), so info ∉ props.

Setoid–Question bridge: refinement = entailment

The fromSetoid embedding is monotone in mathlib's lattice order on Setoid (where r₁ ≤ r₂ iff r₁ is finer: r₁.Rel x y → r₂.Rel x y) and the entailment order on Question (P ≤ Q iff P.props ⊆ Q.props). The bridge is moreover a lattice embedding: ≤ is reflected back.

This is the Set-based form of Groenendijk–Stokhof's "partition refinement = question entailment", formulated as a one-liner over Setoid and Question with no worlds : List W quantifier and no isPartition precondition.

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

The Setoid → Question embedding reflects the order: a setoid is finer than another iff its inquisitive content is entailed by the other's. The forward direction is monotonicity; the backward direction uses the fact that r-equivalent pairs are resolved by the two-element state {x, y}, which any cell-membership theorem can recover.

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

Monotonicity of the fromSetoid embedding (the easy direction of fromSetoid_le_iff).

Equivalence classes are alternatives

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

Conversely, every alternative of fromSetoid r is either the empty state or an equivalence class of r. The empty case can only occur when W is empty (otherwise some class is in props and strictly contains ∅, displacing it from maximality).

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

Each equivalence class of r is a maximal element (alternative) of fromSetoid r. The proof uses (i) classes are nonempty (so they aren't displaced by ∅), and (ii) classes are pairwise disjoint or equal — so a class can only be properly contained in itself.

POSWQ bridge

Lift the partition-based inquiry component of a POSWQ to its full Question. This makes every existing POSWQ-using study automatically a consumer of the inquisitive-content API: info, alt, isInquisitive, the lattice operations, and the mention-some/IE-question forcing arguments all become available without rewriting the underlying state.

def Semantics.Mood.POSWQ.inquiryContent {W : Type u} (c : POSWQ W) : Question W

The inquisitive content embedded in a POSWQ via its inquiry partition. Always non-informative (info = univ); inquisitive iff the partition has more than one cell.

Equations

• c.inquiryContent = Question.fromSetoid c.inquiry

@[simp]

theorem Semantics.Mood.POSWQ.inquiryContent_eq {W : Type u} (c : POSWQ W) : c.inquiryContent = Question.fromSetoid c.inquiry

@[simp]

theorem Semantics.Mood.POSWQ.info_inquiryContent {W : Type u} (c : POSWQ W) : c.inquiryContent.info = Set.univ