Roberts (2012) QUD relevance — Prop predicates on Core.Question

@cite{roberts-2012} @cite{groenendijk-stokhof-1984}

Mathlib-style Prop predicates with Decidable instances. Successor of an earlier Bool/List partiallyAnswers/questionEntails/isSubquestion/ moveRelevant API (now removed) that operated on a Hamblin list-of-alternatives Question type.

The predicates operate directly on Core.Question, ranging over alt P (the maximal-resolving propositions). For computability, an Question must expose a finite alternative-list witness via HasAltList. The canonical witness for a polar question is HasAltList.polar; for an arbitrary Hamblin issue, define a HasAltList instance via the ofList smart constructor (Core/Question/Hamblin.lean).

Decidability of σ ⊆ p for σ p : Set W is not automatic in mathlib (unlike Finset). The local instance Set.decidableSubsetOfFintype below plugs the gap: it derives Decidable (s ⊆ t) from [Fintype W] plus DecidablePred (· ∈ s) and DecidablePred (· ∈ t). Consumers building Set W from W → Bool predicates get the per-set DecidablePred for free.

Note that the [∀ p, Decidable (σ ⊆ p ∨ σ ⊆ pᶜ)] hypothesis on the instances below ranges over all p : Set W — Lean cannot synthesize this universally because DecidablePred (· ∈ p) is not derivable for arbitrary p. Consumers should either supply this hypothesis at the call site (typically via decide_partiallyAnswers_polar for polar questions) or invoke a specialized decision procedure tied to the specific alternative list.

def Core.Question.partiallyAnswers {W : Type u} (P : Question W) (σ : Set W) : Prop

σ partially answers P: settles at least one alternative either positively (σ ⊆ p) or negatively (σ ⊆ pᶜ). @cite{roberts-2012} Def. 3a.

Equations

• P.partiallyAnswers σ = ∃ p ∈ P.alt, σ ⊆ p ∨ σ ⊆ pᶜ

def Core.Question.questionEntails {W : Type u} (P Q : Question W) : Prop

Question entailment: every alternative of P entails some alternative of Q. @cite{roberts-2012} Def. 8 (after @cite{groenendijk-stokhof-1984}). At the partition level this is QUD.refines: P refines Q iff knowing P's answer determines Q's answer.

Equations

• P.questionEntails Q = ∀ p ∈ P.alt, ∃ q ∈ Q.alt, p ⊆ q

def Core.Question.isSubquestion {W : Type u} (q parent : Question W) : Prop

q is a subquestion of parent: answering parent settles q.

Equations

• q.isSubquestion parent = parent.questionEntails q

def Core.Question.moveRelevant {W : Type u} (den qud : Question W) (subquestions : List (Question W)) : Prop

A discourse move den is relevant to the QUD if some alternative partially answers the QUD or any of the subquestions. The QUD-relevance idea traces to @cite{roberts-2012}; the present formulation is the one @cite{ippolito-kiss-williams-2025} ex. (16) assumption iii uses for discourse only's definedness condition.

Equations

• den.moveRelevant qud subquestions = ∃ a ∈ den.alt, qud.partiallyAnswers a ∨ ∃ q ∈ subquestions, q.partiallyAnswers a

def Core.Question.CoversAltsOf {W : Type u} (P Q : Question W) : Prop

The dual of questionEntails: every nonempty alternative of Q is covered by a nonempty alternative of P.

On partition questions this is equivalent to questionEntails P Q; for general inquisitive Question W, the two directions are independent. The decision-relevance preservation theorem in Theories.Semantics.Questions.DecisionTheoretic requires this dual form, not questionEntails. The nonempty clause matches IsDecisionRelevant's requirement that witnessing alternatives be substantive — without it, ⊥-style questions trivially "cover" anything via the empty set.

Equations

• P.CoversAltsOf Q = ∀ q ∈ Q.alt, q.Nonempty → ∃ p ∈ P.alt, p.Nonempty ∧ p ⊆ q

Reflexivity / transitivity

theorem Core.Question.questionEntails_refl {W : Type u} (P : Question W) : P.questionEntails P

theorem Core.Question.questionEntails_trans {W : Type u} {P Q R : Question W} (hPQ : P.questionEntails Q) (hQR : Q.questionEntails R) : P.questionEntails R

Lattice → entailment

The workhorse: P ≤ Q in the inquisitive lattice (P.props ⊆ Q.props) implies questionEntails P Q. Every alternative of P resolves Q and therefore extends to a maximal Q-resolving proposition.

theorem Core.Question.questionEntails_of_le {W : Type u} {P Q : Question W} (h : P ≤ Q) (hQ : Q.props.Finite) : P.questionEntails Q

P ≤ Q (inquisitive entailment) implies questionEntails P Q (Roberts question entailment). The bridge from the lattice order to the alternative-set quantification. Requires Q.props.Finite to guarantee maximal extensions exist.

theorem Core.Question.questionEntails_of_le' {W : Type u} [Fintype W] [DecidableEq W] {P Q : Question W} (h : P ≤ Q) : P.questionEntails Q

Variant of questionEntails_of_le with [Fintype W] [DecidableEq W] discharging the finiteness hypothesis (via Fintype (Set W) then Set.toFinite). Convenient for finite-world studies.

theorem Core.Question.isSubquestion_refl {W : Type u} (P : Question W) : P.isSubquestion P

theorem Core.Question.isSubquestion_trans {W : Type u} {q r s : Question W} (hqr : q.isSubquestion r) (hrs : r.isSubquestion s) : q.isSubquestion s

theorem Core.Question.partiallyAnswers_imp_moveRelevant {W : Type u} {den qud : Question W} {a : Set W} (ha : a ∈ den.alt) (h : qud.partiallyAnswers a) : den.moveRelevant qud []

A move whose alternative directly partially answers the QUD is relevant (no subquestions needed).

Generic Set ⊆ Set decidability for finite types

Mathlib provides Set.Subset decidability only via Finset. For Question consumers that build alternatives as Set W from Bool-valued predicates, the gap is plugged by deriving from Fintype W plus per-set DecidablePred witnesses.

@[implicit_reducible]

instance Core.Question.Set.decidableSubsetOfFintype {α : Type u_1} [Fintype α] (s t : Set α) [DecidablePred fun (x : α) => x ∈ s] [DecidablePred fun (x : α) => x ∈ t] : Decidable (s ⊆ t)

Equations

• Core.Question.Set.decidableSubsetOfFintype s t = inferInstance

Decidability via HasAltList

class Core.Question.HasAltList {W : Type u} (P : Question W) : Type u

A finite-presentation witness for a Question's alternatives. The altList is a List (Set W) whose elements correspond bijectively (modulo set-equality) to alt P.

• altList : List (Set W)

  The finite list of alternatives.

• mem_altList (p : Set W) : p ∈ P.alt ↔ p ∈ altList P

  The list exhausts alt P.

@[implicit_reducible]

instance Core.Question.partiallyAnswers_decidable {W : Type u} (P : Question W) [HP : P.HasAltList] (σ : Set W) [(p : Set W) → Decidable (σ ⊆ p ∨ σ ⊆ pᶜ)] : Decidable (P.partiallyAnswers σ)

partiallyAnswers decides via the alternative list, given decidability of each alternative-subset / complement-subset check.

Equations

• P.partiallyAnswers_decidable σ = decidable_of_iff (∃ p ∈ Core.Question.HasAltList.altList P, σ ⊆ p ∨ σ ⊆ pᶜ) ⋯

@[implicit_reducible]

instance Core.Question.questionEntails_decidable {W : Type u} (P Q : Question W) [HP : P.HasAltList] [HQ : Q.HasAltList] [(p q : Set W) → Decidable (p ⊆ q)] : Decidable (P.questionEntails Q)

questionEntails decides via the alternative lists, given decidability of pairwise subset checks.

Equations

• P.questionEntails_decidable Q = decidable_of_iff (∀ p ∈ Core.Question.HasAltList.altList P, ∃ q ∈ Core.Question.HasAltList.altList Q, p ⊆ q) ⋯

@[implicit_reducible]

instance Core.Question.isSubquestion_decidable {W : Type u} (q parent : Question W) [q.HasAltList] [parent.HasAltList] [(p₁ p₂ : Set W) → Decidable (p₁ ⊆ p₂)] : Decidable (q.isSubquestion parent)

Equations

• q.isSubquestion_decidable parent = parent.questionEntails_decidable q

@[implicit_reducible]

instance Core.Question.moveRelevant_decidable {W : Type u} (den qud : Question W) (subquestions : List (Question W)) [HD : den.HasAltList] [(a : Set W) → Decidable (qud.partiallyAnswers a)] [(q : Question W) → (a : Set W) → Decidable (q.partiallyAnswers a)] : Decidable (den.moveRelevant qud subquestions)

moveRelevant decides via the move's alternative list, given decidability of partial answerhood against the QUD and each subquestion.

Equations

• den.moveRelevant_decidable qud subquestions = decidable_of_iff (∃ a ∈ Core.Question.HasAltList.altList den, qud.partiallyAnswers a ∨ ∃ q ∈ subquestions, q.partiallyAnswers a) ⋯

HasAltList constructors

@[reducible]

def Core.Question.HasAltList.polar {W : Type u} (p : Set W) [DecidablePred fun (x : W) => x ∈ p] (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : (Question.polar p).HasAltList

HasAltList witness for a polar question whose proposition is non-trivial (neither ∅ nor Set.univ). The two alternatives are p and pᶜ. Not an instance: nontriviality must be supplied.

Equations

• Core.Question.HasAltList.polar p hne hnu = { altList := [p, pᶜ], mem_altList := ⋯ }

@[reducible]

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

HasAltList witness for a Hamblin question built from an explicit alternative list under pairwise disjointness + nonempty cells. The Hamblin construction Question.ofList L has alt = {p | p ∈ L} by alt_ofList_of_pairwise_disjoint_nonempty. Not an instance: the structural hypotheses must be supplied at the call site.

Equations

• Core.Question.HasAltList.ofList L hL hdisj hne = { altList := L, mem_altList := ⋯ }

@[reducible]

def Core.Question.HasAltList.ofListAntichain {W : Type u} (L : List (Set W)) (hL : L ≠ []) (hac : ∀ p₁ ∈ L, ∀ p₂ ∈ L, p₁ ≠ p₂ → ¬p₁ ⊆ p₂) (hne : ∀ p ∈ L, p ≠ ∅) : (Question.ofList L).HasAltList

HasAltList witness for a Hamblin question built from an explicit alternative list under the antichain condition (no cell contained in another) + nonempty cells. Weaker than HasAltList.ofList — cells may overlap as long as none is a subset of another distinct cell. Useful for Hamblin alternatives whose truth-sets share worlds (e.g., two polar question alternatives with overlap).

Equations

• Core.Question.HasAltList.ofListAntichain L hL hac hne = { altList := L, mem_altList := ⋯ }

Iff-rewrite lemmas for polar

These reduce partiallyAnswers/questionEntails/moveRelevant on polar questions to plain Set operations, so consumers can rw and then decide (the residual Set subset checks fire from Set.decidableSubsetOfFintype plus per-set DecidablePred).

theorem Core.Question.partiallyAnswers_polar_iff {W : Type u} {p σ : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : (polar p).partiallyAnswers σ ↔ σ ⊆ p ∨ σ ⊆ pᶜ

theorem Core.Question.questionEntails_polar_polar_iff {W : Type u} {p q : Set W} (hne_p : p ≠ ∅) (hnu_p : p ≠ Set.univ) (hne_q : q ≠ ∅) (hnu_q : q ≠ Set.univ) : (polar p).questionEntails (polar q) ↔ (p ⊆ q ∨ p ⊆ qᶜ) ∧ (pᶜ ⊆ q ∨ pᶜ ⊆ qᶜ)

theorem Core.Question.moveRelevant_polar_iff {W : Type u} {p : Set W} {qud : Question W} {subquestions : List (Question W)} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : (polar p).moveRelevant qud subquestions ↔ (qud.partiallyAnswers p ∨ ∃ Q ∈ subquestions, Q.partiallyAnswers p) ∨ qud.partiallyAnswers pᶜ ∨ ∃ Q ∈ subquestions, Q.partiallyAnswers pᶜ