Question — Hamblin constructions

@cite{ciardelli-groenendijk-roelofsen-2018} @cite{puncochar-2019}

Two basic question-content constructions, both built from declarative

• inquisitive disjunction:

• polar p — the polar interrogative ?p for proposition p. Defined as declarative p ⊔ declarative pᶜ, matching @cite{puncochar-2019}'s ?α := α ⩒ ¬α (since the support clause for ¬α over an atom with truth set p reduces to q ⊆ pᶜ).
• which D P — the wh-question content "which e ∈ D satisfies P e?", built as a Hamblin disjunction ⨆ e ∈ D, declarative (P e). One alternative per element of D (modulo non-maximality of overlapping predicates).

Both constructions are defined in terms of the lattice operations rather than stipulated by a fresh props set with bridge theorems — informativity/inquisitivity facts then derive from info_sup, info_declarative, and properties of the underlying Set operations.

Polar question via inquisitive disjunction

def Core.Question.polar {W : Type u} (p : Set W) : Question W

The polar interrogative content of a proposition p, defined via @cite{puncochar-2019}'s ?α := α ⩒ ¬α. Alternatives are p and pᶜ; non-informative (info = univ); inquisitive iff p is non-trivial.

Equations

• Core.Question.polar p = Core.Question.declarative p ⊔ Core.Question.declarative pᶜ

theorem Core.Question.polar_eq_sup {W : Type u} (p : Set W) : polar p = declarative p ⊔ declarative pᶜ

polar is, by definition, the inquisitive disjunction of the two declaratives. Not @[simp]: polar p is a meaningful surface primitive (it's the polar interrogative), and unfolding it to its lattice definition disrupts simp lemmas like info_polar. Use explicitly when reasoning about the lattice structure.

@[simp]

theorem Core.Question.info_polar {W : Type u} (p : Set W) : (polar p).info = Set.univ

theorem Core.Question.not_isInformative_polar {W : Type u} (p : Set W) : ¬(polar p).isInformative

theorem Core.Question.isInquisitive_polar_iff {W : Type u} (p : Set W) : (polar p).isInquisitive ↔ p ≠ ∅ ∧ p ≠ Set.univ

A polar question is inquisitive iff its proposition is non-trivial (neither ∅ nor univ). The trivial cases collapse to declaratives because univ ⊆ p requires p = univ.

alt-characterization of polar

theorem Core.Question.alt_polar_of_nontrivial {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : (polar p).alt = {p, pᶜ}

Membership in a polar question's alternatives when p is non-trivial: the alternative set is exactly {p, pᶜ}. The two alternatives are the maximal subsets of polar p, with no intermediate maximal element. The non-triviality hypotheses rule out the degenerate cases (polar ∅ = polar univ = ⊤) where the two summands collapse and alt = {univ}.

Polar degenerate-case identities

theorem Core.Question.declarative_univ {W : Type u} : declarative Set.univ = ⊤

declarative univ = ⊤: the principal ideal of univ is the whole LowerSet.

theorem Core.Question.polar_empty {W : Type u} : polar ∅ = ⊤

polar ∅ = ⊤: a polar question with vacuous proposition collapses to the trivial issue.

theorem Core.Question.polar_univ {W : Type u} : polar Set.univ = ⊤

polar univ = ⊤: dual of polar_empty.

alt-characterization of polar (full)

theorem Core.Question.alt_polar_iff {W : Type u} (p q : Set W) : q ∈ (polar p).alt ↔ (p = ∅ ∨ p = Set.univ) ∧ q = Set.univ ∨ p ≠ ∅ ∧ p ≠ Set.univ ∧ (q = p ∨ q = pᶜ)

Membership in a polar question's alternatives — full characterization covering both the inquisitive case (p non-trivial) and the degenerate cases (p = ∅ or p = univ, which collapse the polar question to ⊤).

theorem Core.Question.mem_alt_polar_of_nontrivial {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) (q : Set W) : q ∈ (polar p).alt ↔ q = p ∨ q = pᶜ

Membership in alt (polar p) under the standard non-degenerate assumption — the convenient form for empirical study files.

Wh-question content via Hamblin alternatives

A wh-question Which x ∈ D satisfies P x? (Hamblin) has one alternative per element of D, given by the proposition P e for each e ∈ D. We define this as the inquisitive disjunction of the principal ideals generated by the per-element predicates.

def Core.Question.which {W : Type u} {E : Type v} (D : Set E) (P : E → Set W) : Question W

The wh-question content for "Which x ∈ D satisfies P x?". One alternative per element of D (modulo non-maximality of overlapping predicates). The Hamblin construction: which D P = ⨆ e ∈ D, declarative (P e).

Equations

• Core.Question.which D P = ⨆ e ∈ D, Core.Question.declarative (P e)

theorem Core.Question.mem_which {W : Type u} {E : Type v} {D : Set E} {P : E → Set W} {q : Set W} : q ∈ which D P ↔ q = ∅ ∨ ∃ e ∈ D, q ⊆ P e

A state resolves which D P iff it is empty or contained in some P e for an e ∈ D.

@[simp]

theorem Core.Question.info_which {W : Type u} {E : Type v} (D : Set E) (P : E → Set W) : (which D P).info = ⋃ e ∈ D, P e

The informative content of which D P is the union of the per-element predicates: a world is settled by the question iff it satisfies P e for some e ∈ D.

alt-characterization of which

theorem Core.Question.alt_which_iff_left {W : Type u} {E : Type v} {D : Set E} {P : E → Set W} {q : Set W} : q ∈ (which D P).alt → q = ∅ ∨ ∃ e ∈ D, q = P e ∧ ∀ e' ∈ D, P e ⊆ P e' → P e' = P e

A Q-alternative of which D P is necessarily either the empty set (in the degenerate "no inhabited witness" case) or some maximal P e for e ∈ D — i.e., a P e not properly contained in any other P e'.

theorem Core.Question.mem_alt_which_of_maximal {W : Type u} {E : Type v} {D : Set E} {P : E → Set W} (e : E) (heD : e ∈ D) (hne : (P e).Nonempty) (hmax : ∀ e' ∈ D, P e ⊆ P e' → P e' = P e) : P e ∈ (which D P).alt

The convenient direction: a maximal P e (in the antichain sense over D) that is nonempty is in alt (which D P).

Hamblin construction from a finite alternative list

Bridge primitive: ofList L packages a List (Set W) of alternatives into a Core.Question W, mediating between abstract Set-based issues and finite-presentation consumers (Roberts QUD relevance, Hamblin focus alternatives, etc.).

def Core.Question.ofList {W : Type u} (L : List (Set W)) : Question W

The Hamblin issue with alternatives drawn from a finite list L: ofList L = ⨆ p ∈ L, declarative p. The underlying-set view of L is taken so the standard mem_biSup_iff API applies directly.

Equations

• Core.Question.ofList L = ⨆ p ∈ {p : Set W | p ∈ L}, Core.Question.declarative p

theorem Core.Question.mem_ofList {W : Type u} {L : List (Set W)} {q : Set W} : q ∈ ofList L ↔ q = ∅ ∨ ∃ p ∈ L, q ⊆ p

A state resolves ofList L iff it is empty or contained in some listed alternative.

@[simp]

theorem Core.Question.info_ofList {W : Type u} (L : List (Set W)) : (ofList L).info = ⋃ p ∈ L, p

The informative content of ofList L is the union of its alternatives.

alt-characterization for ofList

Under pairwise disjointness, nonemptiness, and a nonempty list, the alternatives of ofList L are exactly the listed elements.

theorem Core.Question.alt_ofList_of_pairwise_disjoint_nonempty {W : Type u} (L : List (Set W)) (hL : L ≠ []) (hdisj : ∀ p₁ ∈ L, ∀ p₂ ∈ L, p₁ ≠ p₂ → Disjoint p₁ p₂) (hne : ∀ p ∈ L, p ≠ ∅) : (ofList L).alt = {p : Set W | p ∈ L}

Alternatives of ofList under pairwise disjoint + nonempty cells (and a nonempty list): alt (ofList L) = {p | p ∈ L}. The L ≠ [] hypothesis rules out the degenerate ofList [] = ⊥, where alt = {∅} rather than ∅.

theorem Core.Question.alt_ofList_of_antichain_nonempty {W : Type u} (L : List (Set W)) (hL : L ≠ []) (hac : ∀ p₁ ∈ L, ∀ p₂ ∈ L, p₁ ≠ p₂ → ¬p₁ ⊆ p₂) (hne : ∀ p ∈ L, p ≠ ∅) : (ofList L).alt = {p : Set W | p ∈ L}

Alternatives of ofList under the antichain condition (no cell is contained in another) plus nonemptiness: alt (ofList L) = {p | p ∈ L}. Weaker than alt_ofList_of_pairwise_disjoint_nonempty — cells may overlap as long as no cell is a (proper or improper) subset of any other distinct cell.

Use case: question alternatives like "Does shop A sell Italian?", "Does shop B sell Italian?" with truth-sets {A_only, both} and {B_only, both}. The two cells overlap on both but neither is a subset of the other, so they are still maximal alternatives in the Hamblin issue.

theorem Core.Question.mem_alt_ofList_of_disjoint_others {W : Type u} {L : List (Set W)} {p : Set W} (hp : p ∈ L) (hne : p ≠ ∅) (hdisj : ∀ p' ∈ L, p' ≠ p → Disjoint p p') : p ∈ (ofList L).alt

Membership in alt (ofList L) from per-cell disjointness: a nonempty cell p ∈ L is an alternative as long as it is disjoint from every other cell in L. Weaker than full pairwise disjointness — useful when only one cell's status is needed.

Lattice-entailment of polar from a classified ofList

When every cell of L is classified by p (each cell either lies in p or in pᶜ), the partition issue ofList L lattice-entails the polar question polar p. This subsumes both the partition-cell case (p ∈ L, classification by pairwise disjointness) and the finer-than-p case (p is a union of cells of L).

theorem Core.Question.ofList_le_polar_of_classified {W : Type u} (L : List (Set W)) {p : Set W} (hclass : ∀ p' ∈ L, p' ⊆ p ∨ p' ⊆ pᶜ) : ofList L ≤ polar p

Lattice entailment from cell classification: if every cell of L lies entirely in p or entirely in pᶜ, then ofList L ≤ polar p. Captures the Roberts subquestion relation in the common case where the wh-question's cells refine the polar question's cell.

Subsumes the older "p ∈ L + pairwise disjoint" formulation: pairwise disjointness lets the cell p ∈ L itself sit in p while every other cell is disjoint from p, hence in pᶜ.

Inf of two polar questions classified by a partition

When two polar questions polar p ⊓ polar q are answered together, the joint resolution carves the world space into the four "corners" p ∩ q, p ∩ qᶜ, pᶜ ∩ q, pᶜ ∩ qᶜ. Every state resolving both polars lies in some corner. A wh-question whose cells contain these corners therefore satisfies polar p ⊓ polar q ≤ ofList L.

theorem Core.Question.mem_polar_inf_polar_iff {W : Type u} {p q σ : Set W} : σ ∈ polar p ⊓ polar q ↔ σ ⊆ p ∩ q ∨ σ ⊆ p ∩ qᶜ ∨ σ ⊆ pᶜ ∩ q ∨ σ ⊆ pᶜ ∩ qᶜ

Membership in polar p ⊓ polar q: a state resolves both polar questions iff it is contained in one of the four corners p ∩ q, p ∩ qᶜ, pᶜ ∩ q, pᶜ ∩ qᶜ.

theorem Core.Question.polar_inf_polar_le_ofList_of_corners {W : Type u} (L : List (Set W)) {p q : Set W} (h1 : ∃ c ∈ L, p ∩ q ⊆ c) (h2 : ∃ c ∈ L, p ∩ qᶜ ⊆ c) (h3 : ∃ c ∈ L, pᶜ ∩ q ⊆ c) (h4 : ∃ c ∈ L, pᶜ ∩ qᶜ ⊆ c) : polar p ⊓ polar q ≤ ofList L

Two polar questions ≤ a covering ofList: if all four corners of polar p ⊓ polar q are contained in cells of L, then polar p ⊓ polar q ≤ ofList L. The Roberts completeness fact: pursuing both polar subquestions resolves the wh-question they jointly partition.