Polar and wh-questions

The two Hamblin constructions ([Ham73]) as inquisitive contents ([CGR18]): the polar question polar p, the join ofSet p ⊔ ofSet pᶜ, which is [Pun19]'s ?α := α ⩒ ¬α and the non-informative projection of the declarative (query_ofSet); and the wh-question which D P, the join of the declaratives of P e for e ∈ D. Both are generated by a family of states, so their alternatives are instances of alt_biSup_ofSet: a nontrivial polar question has the alternatives p and pᶜ (alt_polar_of_nontrivial), and a wh-question one alternative per instance when the instances form an antichain (alt_which_of_antichain).

References

• [CGR18]
• [Ham73]
• [Pun19]

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ᶜ

@[simp]

theorem Question.polar_compl {W : Type u} (p : Set W) : polar pᶜ = polar p

A polar question does not depend on which of p, pᶜ is asked about.

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

The polar question is the join of the declaratives of p and pᶜ.

theorem Question.polar_eq_iSup_orbit {W : Type u} (p : Set W) : polar p = ⨆ q ∈ MulAction.orbit Polarity p, ofSet q

The polar question is the Hamblin question over the polarity alternatives of its proposition.

@[simp]

theorem Question.polar_smul {W : Type u} (s : Polarity) (p : Set W) : polar (s • p) = polar p

A polar question depends only on the polarity alternatives of its proposition, so not on the polarity of the proposition asked about.

theorem Question.query_ofSet {W : Type u} (p : Set W) : (ofSet p).query = polar p

The query of a declarative is the polar question of its proposition.

@[simp]

theorem Question.mem_polar {W : Type u} {p σ : Set W} : σ ∈ polar p ↔ σ ⊆ p ∨ σ ⊆ pᶜ

A state resolves the polar question iff it is included in p or in pᶜ.

theorem Question.isNormal_polar {W : Type u} (p : Set W) : (polar p).IsNormal

A polar question is normal, whether or not p is trivial: p and pᶜ generate it.

@[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.coe_polar {W : Type u} (p : Set W) : ↑(polar p) = ↑(lowerClosure {p, pᶜ})

A polar question is generated by its two answers.

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

The alternatives of a polar question when p is non-trivial are its two answers, which then form an antichain. The non-triviality hypotheses rule out the degenerate cases (polar ∅ = polar univ = ⊤) where the two answers are nested and alt = {univ}.

theorem Question.alt_polar_eq_orbit {W : Type u} {p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : (polar p).alt = MulAction.orbit Polarity p

The alternatives of a polar question with a non-trivial proposition are its polarity alternatives.

Polar degenerate-case identities

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

The polar question of the contradiction is trivial.

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

The polar question of the tautology is trivial.

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 which e ∈ D is P? is the join of the declaratives of P e for e ∈ D.

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.which_eq_biSup_ofSet {W : Type u} {E : Type v} (D : Set E) (P : E → Set W) : which D P = ⨆ a ∈ P '' D, ofSet a

A wh-question is the question generated by its answers.

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

A maximal nonempty P e is an alternative of which D P, whether or not the other answers form an antichain.

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

Over a nonempty domain whose answers form an antichain, the alternatives of which D P are exactly the answers.

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

The alternatives of which D P are its instances when an instance included in another equals it.

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} (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.

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 ≤ which D P.

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ᶜ

A state resolves two polar questions iff it is included in one of the four corners p ∩ q, p ∩ qᶜ, pᶜ ∩ q, pᶜ ∩ qᶜ.