Answerhood predicates on questions

This file defines the answerhood predicates over the inquisitive substrate Question W, with the question as subject so that dot notation reads in the right direction. Resolution is membership, σ ∈ Q, the support relation of [CGR18], which on normal questions is settling some alternative (mem_iff_exists_alt_subset), the mention-some reading of [GS84]. A state completely answers a question when it decides every alternative (CompletelyAnsweredBy), the mention-all reading, and partially answers it when it decides some alternative (PartiallyAnsweredBy), the non-contextual core of [Rob12]'s partial answer. The notions form the quantifier × polarity square of answerhood: resolution (∃, positive), PartiallyAnsweredBy (∃, either), CompletelyAnsweredBy (∀, either). A question is a contextual subquestion of another when its complete answers, cut to the context, partially answer it (IsSubquestionOf), and a move is relevant to a set of questions when some alternative of it partially answers one of them (IsRelevantTo).

Implementation notes

CompletelyAnsweredBy decides each alternative rather than entailing every one, which would collapse to σ ⊆ ⋂ alt Q and is incoherent for partition questions with disjoint alternatives; the decided form is [GS84]'s strong exhaustivity on partition questions, and Exhaustivity.lean builds the weak / intermediate / strong / relativized ladder on it ([Hei94b], [Geo11], [Xia22]). Mention-some answerhood is resolution itself: an added "and not all alternatives" conjunct would rule out singleton-world states as mention-some answers to Where can I get coffee?. ∅ vacuously answers everything, as in [Rob12].

References

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

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

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

Equations

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

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

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

Equations

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

def Question.IsSubquestionOf {W : Type u_1} (C : Set W) (P Q : Question W) : Prop

P is a subquestion of Q relative to the context C ([Rob12]): every complete answer to P contextually partially answers Q. The entailment is contextual, not question entailment, so the relation is not transitive in general.

Equations

• Question.IsSubquestionOf C P Q = ∀ a ∈ P.alt, Q.PartiallyAnsweredBy (C ∩ a)

theorem Question.isSubquestionOf_of_alt_subset {W : Type u_1} (C : Set W) {P Q : Question W} (h : P.alt ⊆ Q.alt) : IsSubquestionOf C P Q

A question whose alternatives are among another's is its subquestion in every context.

theorem Question.IsSubquestionOf.refl {W : Type u_1} (C : Set W) (P : Question W) : IsSubquestionOf C P P

theorem Question.isSubquestionOf_of_le {W : Type u_1} (C : Set W) {P Q : Question W} (hQ : Q.IsNormal) (h : P ≤ Q) : IsSubquestionOf C P Q

Entailment of a normal question gives subquestionhood in every context.

theorem Question.partiallyAnsweredBy_inter_iff {W : Type u_1} {Q : Question W} {C σ : Set W} : Q.PartiallyAnsweredBy (C ∩ σ) ↔ ∃ p ∈ Q.alt, σ ∈ (ofSet p).relativeTo C ∨ σ ∈ (ofSet pᶜ).relativeTo C

Contextual partial answerhood is partial answerhood of the relativized alternatives.

theorem Question.isSubquestionOf_iff {W : Type u_1} {C : Set W} {P Q : Question W} : IsSubquestionOf C P Q ↔ ∀ a ∈ P.alt, ∃ p ∈ Q.alt, a ∈ (ofSet p).relativeTo C ∨ a ∈ (ofSet pᶜ).relativeTo C

Subquestionhood in C is partial answerhood of the relativized alternatives.

Basic relationships

theorem Question.mem_of_exists_alt_subset {W : Type u_1} {σ : Set W} {Q : Question W} (h : ∃ p ∈ Q.alt, σ ⊆ p) : σ ∈ Q

A state under an alternative resolves the question, by downward closure.

theorem Question.mem_iff_exists_alt_subset {W : Type u_1} {σ : Set W} {Q : Question W} (hQ : Q.IsNormal) : σ ∈ Q ↔ ∃ p ∈ Q.alt, σ ⊆ p

Resolving a normal question is settling one of its alternatives.

theorem Question.partiallyAnsweredBy_of_mem {W : Type u_1} {σ : Set W} {Q : Question W} (hQ : Q.IsNormal) (h : σ ∈ Q) : Q.PartiallyAnsweredBy σ

Resolving a normal question partially answers it: the positive disjunct fires.

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

Every alternative partially answers its own question.

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

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

Answerhood transmission

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

CompletelyAnsweredBy 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 lattice order off partition-shaped alternatives (see Entailment.lean).

Equations

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

@[simp]

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

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.completelyAnsweredBy_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) : Q.CompletelyAnsweredBy σ ↔ ∀ (i : ι), σ ⊆ P i ∨ σ ⊆ (P i)ᶜ

With the alternatives enumerated as a range, CompletelyAnsweredBy 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.completelyAnsweredBy_ofSet_iff {W : Type u_1} {σ p : Set W} : (ofSet p).CompletelyAnsweredBy σ ↔ σ ⊆ 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} (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.

Polar reduction

Iff lemmas reducing the square on nontrivial polar p to plain Set inclusions — the joints consumer-side study files build on; resolution itself reduces without nontriviality, mem_polar.

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

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

Decidability for polar questions

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

CompletelyAnsweredBy (polar p) σ is decidable when the two inclusions are: on polar questions it coincides with resolution, mem_polar.

Equations

• Question.decidableCompletelyAnsweredByPolar 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, q.PartiallyAnsweredBy a

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, q.PartiallyAnsweredBy p) ∨ ∃ q ∈ qs, q.PartiallyAnsweredBy pᶜ

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