Question — Hamblin constructions

[CGR18] [Pun19]

Two basic question-content constructions, both built from ofSet

• inquisitive disjunction:

• polar p — the polar interrogative ?p for proposition p. Defined as ofSet p ⊔ ofSet pᶜ, matching [Pun19]'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, ofSet (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_ofSet, and properties of the underlying Set operations.

Polar question via inquisitive disjunction

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

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

Equations

• Question.polar p = Question.ofSet p ⊔ Question.ofSet pᶜ

theorem Question.polar_eq_sup {W : Type u} (p : Set W) : polar p = ofSet p ⊔ ofSet 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 Question.mem_polar {W : Type u} {p σ : Set W} : σ ∈ polar p ↔ σ ⊆ p ∨ σ ⊆ pᶜ

Membership in polar p: a state resolves the polar question iff it is contained in p or in pᶜ (i.e. it settles the issue either way).

@[simp]

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

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

theorem 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 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 Question.polar_empty {W : Type u} : polar ∅ = ⊤

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

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

polar univ = ⊤: dual of polar_empty.

alt-characterization of polar (full)

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

@[reducible, inline]

abbrev 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, ofSet (P e).

Equations

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

theorem 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 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 Question.eq_empty_or_exists_of_mem_alt_which {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

An 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 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).

theorem Question.alt_which_of_antichain {W : Type u} {E : Type v} {D : Set E} {P : E → Set W} (hD : D.Nonempty) (hne : ∀ e ∈ D, (P e).Nonempty) (hA : IsAntichain (fun (x1 x2 : Set W) => x1 ⊆ x2) (P '' D)) : (which D P).alt = P '' D

For an antichain of nonempty per-element predicates, the alternatives of which D P are exactly the predicate family: the maximal elements of a lower closure of an antichain recover the antichain.

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

Variant of alt_which_of_antichain with a pointwise hypothesis: containment within the family collapses to equality of values.

theorem Question.which_univ {W : Type u} {ι : Type v} (P : ι → Set W) : which Set.univ P = ⨆ (i : ι), ofSet (P i)

which over the trivial domain is the indexed join of principal contents — a wh-question is the disjunction of its answers ([Ham73]).

theorem Question.mem_iSup_ofSet {W : Type u} {ι : Type v} {P : ι → Set W} {q : Set W} : q ∈ ⨆ (i : ι), ofSet (P i) ↔ q = ∅ ∨ ∃ (i : ι), q ⊆ P i

A state resolves the join of principal contents iff it is empty or contained in some P i.

theorem Question.alt_iSup_ofSet {W : Type u} {ι : Type v} [Nonempty ι] {P : ι → Set W} (hne : ∀ (i : ι), (P i).Nonempty) (hP : ∀ (i j : ι), P i ⊆ P j → P i = P j) : (⨆ (i : ι), ofSet (P i)).alt = Set.range P

For a nonempty pointwise antichain family, the alternatives of the join are exactly its range.

Hamblin construction from a finite alternative list

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

def 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, ofSet p. The underlying-set view of L is taken so the standard mem_biSup_iff API applies directly.

Equations

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

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

alt-characterization for ofList

Under an antichain condition (or the stronger pairwise disjointness) plus nonemptiness, the alternatives of ofList L are exactly the listed elements.

theorem 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}. The hypothesis is weaker than pairwise disjointness — cells may overlap as long as no cell is a 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 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: special case of alt_ofList_of_antichain_nonempty, since a nonempty cell disjoint from every other cell is contained in none of them.

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