Roberts 2012: information structure in discourse

The worked D₀ discourse of [Rob12] (Semantics & Pragmatics 5(6)): two individuals, two foods, and seven questions forming a strategy tree —

q₁ = Who ate what?
├─ q_a = What did Hilary eat?  (q_ai: bagels?  q_aii: tofu?)
└─ q_b = What did Robin eat?   (q_bi: bagels?  q_bii: tofu?)

— with her entailment table, the answer-composition equations (11), the derived complete-answer partition (4), strategy completeness, and the QUD-stack trace with its (10g.iii) well-formedness invariant.

A world is the Finset of eating events that occurred, and a question is the join of its answers ([Ham73]): Question.ofSet of a single event for the yes/no questions, ⨆ over the open index for the wh-questions — her (1). Entailment (8) is inclusion of completeAnswers. The substrate's inquisitive Question.polar, with alternatives {p, pᶜ}, is the rival yes/no convention, not hers.

D₀ world space

inductive Roberts2012.Person : Type

The two individuals of D₀.

• hilary : Person
• robin : Person

@[instance_reducible]

instance Roberts2012.instDecidableEqPerson : DecidableEq Person

Equations

• Roberts2012.instDecidableEqPerson x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Roberts2012.instFintypePerson : Fintype Person

Equations

• Roberts2012.instFintypePerson = { elems := { val := ↑Roberts2012.Person.enumList, nodup := Roberts2012.Person.enumList_nodup }, complete := Roberts2012.instFintypePerson._proof_1 }

@[instance_reducible]

instance Roberts2012.instInhabitedPerson : Inhabited Person

Equations

• Roberts2012.instInhabitedPerson = { default := Roberts2012.instInhabitedPerson.default }

inductive Roberts2012.Food : Type

The two foods of D₀.

• bagels : Food
• tofu : Food

@[instance_reducible]

instance Roberts2012.instDecidableEqFood : DecidableEq Food

Equations

• Roberts2012.instDecidableEqFood x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Roberts2012.instFintypeFood : Fintype Food

Equations

• Roberts2012.instFintypeFood = { elems := { val := ↑Roberts2012.Food.enumList, nodup := Roberts2012.Food.enumList_nodup }, complete := Roberts2012.instFintypeFood._proof_1 }

@[instance_reducible]

instance Roberts2012.instInhabitedFood : Inhabited Food

Equations

• Roberts2012.instInhabitedFood = { default := Roberts2012.instInhabitedFood.default }

@[reducible, inline]

abbrev Roberts2012.World : Type

A world of Roberts' D₀ scenario: the set of eating events that occurred in it.

Equations

• Roberts2012.World = Finset (Roberts2012.Person × Roberts2012.Food)

@[reducible, inline]

abbrev Roberts2012.ate (u : Person) (f : Food) : Set World

u ate f — the worlds containing the event, i.e. the principal up-set of its minimal world {(u, f)}.

Equations

• Roberts2012.ate u f = Set.Ici {(u, f)}

Questions as q-alternative sets ((1), (2), (7))

@[reducible, inline]

abbrev Roberts2012.hilaryBagels : Set World

Hilary ate the bagels.

Equations

• Roberts2012.hilaryBagels = Roberts2012.ate Roberts2012.Person.hilary Roberts2012.Food.bagels

@[reducible, inline]

abbrev Roberts2012.hilaryTofu : Set World

Hilary ate the tofu.

Equations

• Roberts2012.hilaryTofu = Roberts2012.ate Roberts2012.Person.hilary Roberts2012.Food.tofu

@[reducible, inline]

abbrev Roberts2012.robinBagels : Set World

Robin ate the bagels.

Equations

• Roberts2012.robinBagels = Roberts2012.ate Roberts2012.Person.robin Roberts2012.Food.bagels

@[reducible, inline]

abbrev Roberts2012.robinTofu : Set World

Robin ate the tofu.

Equations

• Roberts2012.robinTofu = Roberts2012.ate Roberts2012.Person.robin Roberts2012.Food.tofu

@[reducible, inline]

abbrev Roberts2012.q_ai : Question World

"Did Hilary eat the bagels?"

Equations

• Roberts2012.q_ai = Question.ofSet Roberts2012.hilaryBagels

@[reducible, inline]

abbrev Roberts2012.q_aii : Question World

"Did Hilary eat the tofu?"

Equations

• Roberts2012.q_aii = Question.ofSet Roberts2012.hilaryTofu

@[reducible, inline]

abbrev Roberts2012.q_bi : Question World

"Did Robin eat the bagels?"

Equations

• Roberts2012.q_bi = Question.ofSet Roberts2012.robinBagels

@[reducible, inline]

abbrev Roberts2012.q_bii : Question World

"Did Robin eat the tofu?"

Equations

• Roberts2012.q_bii = Question.ofSet Roberts2012.robinTofu

@[reducible, inline]

abbrev Roberts2012.q_a : Question World

"What did Hilary eat?" — the join of its answers.

Equations

• Roberts2012.q_a = ⨆ (f : Roberts2012.Food), Question.ofSet (Roberts2012.ate Roberts2012.Person.hilary f)

@[reducible, inline]

abbrev Roberts2012.q_b : Question World

"What did Robin eat?"

Equations

• Roberts2012.q_b = ⨆ (f : Roberts2012.Food), Question.ofSet (Roberts2012.ate Roberts2012.Person.robin f)

@[reducible, inline]

abbrev Roberts2012.q_1 : Question World

"Who ate what?" — D₀'s move 1, joining answers over person–food pairs.

Equations

• Roberts2012.q_1 = ⨆ (uf : Roberts2012.Person × Roberts2012.Food), Question.ofSet (Roberts2012.ate uf.1 uf.2)

Alternative enumerations

Alternative inclusions

Subquestionhood in D₀ is alternative-set inclusion: each polar alternative is an alternative of its wh-question, and each wh alternative is an alternative of the big question.

The complete-answer partition ((4)), derived

theorem Roberts2012.mentionAll_wh_iff {σ : Set World} {u : Person} : Question.MentionAll σ (⨆ (f' : Food), Question.ofSet (ate u f')) ↔ σ ⊆ ate u Food.bagels ∩ ate u Food.tofu ∨ σ ⊆ ate u Food.bagels ∩ (ate u Food.tofu)ᶜ ∨ σ ⊆ (ate u Food.bagels)ᶜ ∩ ate u Food.tofu ∨ σ ⊆ (ate u Food.bagels)ᶜ ∩ (ate u Food.tofu)ᶜ

A state completely answers "What did u eat?" iff it lies within one cell of the partition the q-alternatives induce.

Question entailment ((3), (8))

Her (8) — answering q₁ yields a complete answer to q₂ — is completeAnswers q₁ ⊆ completeAnswers q₂; the î(1) table lists the entailments among D₀'s seven questions.

theorem Roberts2012.q1_entails_wh (u : Person) : q_1.completeAnswers ⊆ (⨆ (f' : Food), Question.ofSet (ate u f')).completeAnswers

"Who ate what?" entails "What did u eat?".

theorem Roberts2012.wh_entails_polar (u : Person) (f : Food) : (⨆ (f' : Food), Question.ofSet (ate u f')).completeAnswers ⊆ (Question.ofSet (ate u f)).completeAnswers

"What did u eat?" entails "Did u eat f?".

theorem Roberts2012.q1_entails_polar (u : Person) (f : Food) : q_1.completeAnswers ⊆ (Question.ofSet (ate u f)).completeAnswers

"Who ate what?" entails every polar subquestion.

theorem Roberts2012.qa_not_entails_q1 : ¬q_a.completeAnswers ⊆ q_1.completeAnswers

Subquestions do not entail their superquestions: "Hilary ate both" completely answers q_a but decides nothing about Robin.

theorem Roberts2012.qai_not_entails_qa : ¬q_ai.completeAnswers ⊆ q_a.completeAnswers

"Did Hilary eat the bagels?" does not entail "What did Hilary eat?": the positive answer leaves the tofu alternative open.

Answer composition ((11))

Her Ans(aᵢ) ∩ Ans(aᵢᵢ) = Ans(a) and Ans(a) ∩ Ans(b) = Ans(1): instances of completeAnswers_iSup_ofSet — the answers to a join are the meet of the answers. By iSup_prod, "Who ate what?" is itself the join of the per-person wh-questions, so (11c) is (11a) one level up. Partial answerhood is not transitive in general (chaining loses completeness at the middle link), which is why the stack invariant proofs below go direct rather than composing.

theorem Roberts2012.completeAnswers_wh (u : Person) : (⨆ (f' : Food), Question.ofSet (ate u f')).completeAnswers = ⋂ (f : Food), (Question.ofSet (ate u f)).completeAnswers

The complete answers to "What did u eat?" are the joint complete answers to its point questions.

theorem Roberts2012.completeAnswers_polar_inter (u : Person) : (Question.ofSet (ate u Food.bagels)).completeAnswers ∩ (Question.ofSet (ate u Food.tofu)).completeAnswers = (⨆ (f' : Food), Question.ofSet (ate u f')).completeAnswers

Jointly answering the polar subquestions is exactly answering "What did u eat?".

theorem Roberts2012.completeAnswers_wh_inter : (⨆ (f' : Food), Question.ofSet (ate Person.hilary f')).completeAnswers ∩ (⨆ (f' : Food), Question.ofSet (ate Person.robin f')).completeAnswers = q_1.completeAnswers

Jointly answering "What did Hilary eat?" and "What did Robin eat?" is exactly answering "Who ate what?".

Strategy of inquiry ((12))

def Roberts2012.strat_a : Discourse.Strategy World

Substrategy for q_a: pursue both polar subquestions about Hilary.

Equations

• Roberts2012.strat_a = RoseTree.node Roberts2012.q_a [RoseTree.leaf Roberts2012.q_ai, RoseTree.leaf Roberts2012.q_aii]

def Roberts2012.strat_b : Discourse.Strategy World

Substrategy for q_b: pursue both polar subquestions about Robin.

Equations

• Roberts2012.strat_b = RoseTree.node Roberts2012.q_b [RoseTree.leaf Roberts2012.q_bi, RoseTree.leaf Roberts2012.q_bii]

def Roberts2012.strat_1 : Discourse.Strategy World

Roberts' strategy for the D₀ scenario: answer q_1 by answering q_a and q_b; answer q_a by answering q_ai and q_aii; answer q_b by answering q_bi and q_bii.

Equations

• Roberts2012.strat_1 = RoseTree.node Roberts2012.q_1 [Roberts2012.strat_a, Roberts2012.strat_b]

theorem Roberts2012.strat_a_complete : strat_a.IsComplete

The Hilary substrategy is complete: jointly resolving q_ai and q_aii resolves q_a — already resolving q_ai does, since q_ai is one of q_a's disjuncts.

theorem Roberts2012.strat_b_complete : strat_b.IsComplete

The Robin substrategy is complete.

theorem Roberts2012.strat_1_complete : strat_1.IsComplete

The whole D₀ strategy is complete: joint resolutions of q_a and q_b resolve q_1, whose disjuncts include q_a's.

QUD stack traces ((10g), (17))

def Roberts2012.stack_0 : Discourse.QUDStack World

Initial state: accept move 1, "Who ate what?".

Equations

• Roberts2012.stack_0 = [Roberts2012.q_1]

def Roberts2012.stack_1 : Discourse.QUDStack World

Pursue Hilary's food: accept q_a.

Equations

• Roberts2012.stack_1 = Roberts2012.q_a :: Roberts2012.stack_0

def Roberts2012.stack_2 : Discourse.QUDStack World

Pursue Hilary+bagels: accept q_ai.

Equations

• Roberts2012.stack_2 = Roberts2012.q_ai :: Roberts2012.stack_1

theorem Roberts2012.stack_2_tail : List.tail stack_2 = stack_1

"Hilary ate the bagels" answers q_ai: retiring it returns the discourse to stack_1, so the immediate QUD is q_a again.

Stack well-formedness ((10g.iii))

theorem Roberts2012.stack_1_wellFormed : Discourse.QUDStack.WellFormed Set.univ stack_1

The stack [q_a, q_1] is well-formed in the trivial common ground: every complete answer to the subquestion partially answers the question below it.

theorem Roberts2012.stack_2_wellFormed : Discourse.QUDStack.WellFormed Set.univ stack_2

The full three-question stack [q_ai, q_a, q_1] is well-formed.

Answerhood ((3))

A partial answer evaluates at least one q-alternative, positively or negatively; the negative direction — ruling an alternative out — is her point against confirm-only answerhood.

theorem Roberts2012.neg_hilaryBagels_partiallyAnswers_qai : Question.PartiallyAnswers hilaryBagelsᶜ q_ai

"Hilary didn't eat bagels" negatively answers "Did Hilary eat the bagels?" — it falsifies its sole alternative.

theorem Roberts2012.neg_hilaryBagels_partiallyAnswers_qa : Question.PartiallyAnswers hilaryBagelsᶜ q_a

"Hilary didn't eat bagels" partially answers "What did Hilary eat?" — it rules out the bagels alternative.

theorem Roberts2012.hilaryBagels_partiallyAnswers_qai : Question.PartiallyAnswers hilaryBagels q_ai

"Hilary ate bagels" positively answers "Did Hilary eat the bagels?".

theorem Roberts2012.hilaryBagels_partiallyAnswers_q1 : Question.PartiallyAnswers hilaryBagels q_1

"Hilary ate bagels" partially answers "Who ate what?" — it confirms one of its four alternatives.

Relevance ((15))

Assertion-clause relevance throughout; Roberts' clause for interrogative moves is strategy membership, which qa_relevant_to_q1 proxies by partial answerhood.

def Roberts2012.hilaryBagels_assertion : Question World

The assertion "Hilary ate bagels": a declarative's q-alternative set is the singleton of its content.

Equations

• Roberts2012.hilaryBagels_assertion = Question.ofSet Roberts2012.hilaryBagels

theorem Roberts2012.hilaryBagels_relevant_to_q1 : hilaryBagels_assertion.IsRelevantTo {q_1}

"Hilary ate bagels" is relevant to move 1, "Who ate what?".

theorem Roberts2012.qa_relevant_to_q1 : q_a.IsRelevantTo {q_1}

The question q_a is relevant to q_1 under the assertion-clause proxy: its bagels alternative confirms an alternative of q_1.

theorem Roberts2012.hilaryBagels_relevant_to_strategy : hilaryBagels_assertion.IsRelevantTo {q : Question World | q ∈ RoseTree.values strat_1}

"Hilary ate bagels" is relevant to the entire D₀ strategy: it partially answers q_1 (the strategy's root).