Resolution — answerhood predicates on Question

[CGR18] [TRA18] [Rob12] [GS84]

Canonical Prop-valued answerhood predicates over the inquisitive substrate (Question W), all in the Question namespace with the state argument first. One topical home for the "what does it mean for a state σ to answer a question Q?" question, with definitions chosen to match modern (CGR 2018) formal-semantics consensus rather than the historical Hamblin/Karttunen/G&S conventions.

The notions formalised

Given a state σ : Set W and a question Q : Question W:

• Resolves: σ settles at least one alternative — ∃ p ∈ alt Q, σ ⊆ p. This is the standard inquisitive resolution relation ([CGR18], [roelofsen-2013]). It is the natural notion of "σ answers Q" — even a singleton state can resolve a question by being contained in one of its alternatives.

• MentionSome: synonym of Resolves — the doctrinal "mention-some" reading of [GS84] Ch. VI §5 is just resolution by one alternative. Authors who add an extra "and not all alternatives" conjunct (forbidding mention-some answers from also being maximally informative) end up ruling out singleton-world states as mention-some answers to Where can I get coffee? — which is empirically wrong.

• MentionAll: σ decides every alternative — ∀ p ∈ alt Q, σ ⊆ p ∨ σ ⊆ pᶜ. Note this is not "σ ⊆ p for every p" (which collapses to σ ⊆ ⋂ alt Q and is incoherent for partition questions whose alternatives are disjoint). The "decides each alternative" form is what aligns with [GS84]-style strong exhaustivity on partition questions. See Exhaustivity.lean for the weak / intermediate / strong / relativized exhaustivity ladder ([Hei94b], [Geo11], [Xia22]).

• PartiallyAnswers ([Rob12] (3a), its non-contextual core — the paper relativizes entailment to the common ground): σ settles at least one alternative either positively (σ ⊆ p) or negatively (σ ⊆ pᶜ); ∅ vacuously answers everything, as there. Bridged by Resolves.partiallyAnswers.

The four form the quantifier × polarity square of answerhood: Resolves (∃, positive), PartiallyAnswers (∃, either), MentionAll (∀, either).

Why this file

A previous draft (deleted Core/Question/Answerhood.lean, audited 0.230.378) shipped isMentionSomeAnswer with the bad second conjunct and isMentionAllAnswer in the over-strong intersection form. Both have been corrected here. This file is the canonical home; the G&S mention-some data lives in Data.Examples.GroenendijkStokhof1984 (consumed by Studies/GroenendijkStokhof1984.lean), and Exhaustivity.lean (Karttunen / Dayal / Xiang / Fox) specializes these substrate predicates rather than defining parallel ones.

def Question.Resolves {W : Type u_1} (σ : Set W) (Q : Question W) : Prop

σ resolves Q if it settles at least one alternative. The standard inquisitive resolution relation ([CGR18]); the [GS84] "mention-some" notion is this same predicate.

Equations

• Question.Resolves σ Q = ∃ p ∈ Q.alt, σ ⊆ p

def Question.PartiallyAnswers {W : Type u_1} (σ : Set W) (Q : Question W) : Prop

σ partially answers Q if it settles some alternative positively (σ ⊆ p) or negatively (σ ⊆ pᶜ).

Equations

• Question.PartiallyAnswers σ Q = ∃ p ∈ Q.alt, σ ⊆ p ∨ σ ⊆ pᶜ

def Question.MentionAll {W : Type u_1} (σ : Set W) (Q : Question W) : Prop

σ mention-all answers Q if it decides every alternative, either entailing it or ruling it out.

Equations

• Question.MentionAll σ Q = ∀ p ∈ Q.alt, σ ⊆ p ∨ σ ⊆ pᶜ

Basic relationships

theorem Question.Resolves.partiallyAnswers {W : Type u_1} {σ : Set W} {Q : Question W} (h : Resolves σ Q) : PartiallyAnswers σ Q

Resolving implies partially answering: the positive disjunct fires.

theorem Question.partiallyAnswers_of_mem_alt {W : Type u_1} {Q : Question W} {p : Set W} (h : p ∈ Q.alt) : PartiallyAnswers p Q

Every alternative partially answers its own question.

theorem Question.partiallyAnswers_compl_of_mem_alt {W : Type u_1} {Q : Question W} {p : Set W} (h : p ∈ Q.alt) : PartiallyAnswers pᶜ Q

The complement of an alternative partially answers the question by ruling that alternative out.

Answerhood transmission

theorem Question.MentionAll.mono {W : Type u_1} {σ : Set W} {Q P : Question W} (h : MentionAll σ Q) (hsub : P.alt ⊆ Q.alt) : MentionAll σ P

MentionAll is antitone in the alternative set.

def Question.completeAnswers {W : Type u_1} (Q : Question W) : Set (Set W)

The set of complete answers to Q — [Rob12]'s Ans(q): the states that decide every alternative. Her question entailment (8), after [GS84], is completeAnswers P ⊆ completeAnswers Q, diverging from the alt-witnessed Entails off partition-shaped alternatives (see the fidelity note in Entailment.lean).

Equations

• Q.completeAnswers = {σ : Set W | Question.MentionAll σ Q}

@[simp]

theorem Question.mem_completeAnswers {W : Type u_1} {σ : Set W} {Q : Question W} : σ ∈ Q.completeAnswers ↔ MentionAll σ Q

theorem Question.completeAnswers_anti {W : Type u_1} {P Q : Question W} (h : Q.alt ⊆ P.alt) : P.completeAnswers ⊆ Q.completeAnswers

completeAnswers is antitone in the alternative set.

theorem Question.mentionAll_iff_of_alt_eq_range {W : Type u_1} {σ : Set W} {Q : Question W} {ι : Type u_2} {P : ι → Set W} (h : Q.alt = Set.range P) : MentionAll σ Q ↔ ∀ (i : ι), σ ⊆ P i ∨ σ ⊆ (P i)ᶜ

With the alternatives enumerated as a range, MentionAll quantifies over the index.

@[simp]

theorem Question.completeAnswers_top {W : Type u_1} : ⊤.completeAnswers = Set.univ

@[simp]

theorem Question.completeAnswers_bot {W : Type u_1} : ⊥.completeAnswers = Set.univ

theorem Question.mentionAll_ofSet_iff {W : Type u_1} {σ p : Set W} : MentionAll σ (ofSet p) ↔ σ ⊆ p ∨ σ ⊆ pᶜ

A state settles a single-alternative content iff it decides it.

theorem Question.completeAnswers_ofSet {W : Type u_1} (p : Set W) : (ofSet p).completeAnswers = {σ : Set W | σ ⊆ p ∨ σ ⊆ pᶜ}

theorem Question.completeAnswers_iSup_ofSet {W : Type u_1} {ι : Type u_2} [Nonempty ι] {P : ι → Set W} (hne : ∀ (i : ι), (P i).Nonempty) (hP : ∀ (i j : ι), P i ⊆ P j → P i = P j) : (⨆ (i : ι), ofSet (P i)).completeAnswers = ⋂ (i : ι), (ofSet (P i)).completeAnswers

The complete answers to a join of point-questions are the joint complete answers to each — [Rob12]'s (11) in general form.

Bridge to Question.Support

Resolves σ Q (alt-witnessed) and Support.supports σ Q := σ ∈ Q.props (CGR support, downward-closed) are two views on the same intuitive notion. The CGR side is the foundational definition; Resolves is the alt-witnessed corollary, equivalent under finiteness of Q.props.

theorem Question.Resolves.supports {W : Type u_1} {σ : Set W} {Q : Question W} (h : Resolves σ Q) : Support.supports σ Q

An alt witness is a resolving proposition, so any state below it is one by downward closure.

theorem Question.resolves_of_supports {W : Type u_1} {σ : Set W} {Q : Question W} (hFin : Q.props.Finite) (h : Support.supports σ Q) : Resolves σ Q

Under finiteness of Q.props, CGR support yields an alt witness via exists_alt_above.

theorem Question.resolves_iff_supports {W : Type u_1} {σ : Set W} {Q : Question W} (hFin : Q.props.Finite) : Resolves σ Q ↔ Support.supports σ Q

Resolves and Support.supports coincide under finiteness.

Polar reduction

Iff lemmas reducing the square on nontrivial polar p to plain Set inclusions — the joints consumer-side study files build on.

theorem Question.resolves_polar_iff {W : Type u_1} {σ p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : Resolves σ (polar p) ↔ σ ⊆ p ∨ σ ⊆ pᶜ

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

theorem Question.mentionAll_polar_iff {W : Type u_1} {σ p : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : MentionAll σ (polar p) ↔ σ ⊆ p ∨ σ ⊆ pᶜ

Decidability for polar questions

def Question.decidableResolvesPolar {W : Type u_1} {p σ : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) [Decidable (σ ⊆ p)] [Decidable (σ ⊆ pᶜ)] : Decidable (Resolves σ (polar p))

Resolves σ (polar p) is decidable when the two inclusions are.

Equations

• Question.decidableResolvesPolar hne hnu = decidable_of_iff (σ ⊆ p ∨ σ ⊆ pᶜ) ⋯

def Question.decidableMentionAllPolar {W : Type u_1} {p σ : Set W} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) [Decidable (σ ⊆ p)] [Decidable (σ ⊆ pᶜ)] : Decidable (MentionAll σ (polar p))

MentionAll σ (polar p) is decidable under the same hypotheses: on polar questions it coincides with Resolves.

Equations

• Question.decidableMentionAllPolar hne hnu = decidable_of_iff (σ ⊆ p ∨ σ ⊆ pᶜ) ⋯

Relevance to a question set

def Question.IsRelevantTo {W : Type u_1} (den : Question W) (qs : Set (Question W)) : Prop

A move with denotation den is relevant to the questions in qs when some alternative of den partially answers some question in qs — the assertion clause of [Rob12]'s Relevance, existentially weakened and extended to a question set (see Discourse/QUD/Basic.lean for the fidelity discussion).

Equations

• den.IsRelevantTo qs = ∃ a ∈ den.alt, ∃ q ∈ qs, Question.PartiallyAnswers a q

theorem Question.isRelevantTo_polar_iff {W : Type u_1} {p : Set W} {qs : Set (Question W)} (hne : p ≠ ∅) (hnu : p ≠ Set.univ) : (polar p).IsRelevantTo qs ↔ (∃ q ∈ qs, PartiallyAnswers p q) ∨ ∃ q ∈ qs, PartiallyAnswers pᶜ q

Polar reduction of IsRelevantTo to partial answerhood of p and pᶜ.