@cite{roberts-2012} — Information Structure in Discourse

@cite{roberts-2012} "Information structure in discourse: Towards an integrated formal theory of pragmatics" (Semantics & Pragmatics 5(6): 1–69).

Core Contributions Formalized

1. QUD stack — discourse state is an ordered stack of accepted, unanswered questions (QUDStack), not a single QUD.
2. Strategy of inquiry — recursive question decomposition (Strategy): answering all subquestions answers the parent.
3. Negative partial answerhood — a proposition partially answers a question by ruling out an alternative, not just confirming one (partiallyAnswers).
4. Q-A congruence — the focus alternatives of an answer equal the QUD alternatives (grounded by the Rooth–Hamblin type identity).

D₀ Worked Example (Roberts §1.2)

The Big Question: "What did each person eat?"

• 4 Boolean dimensions: Hannah-beans, Hannah-tofu, Roger-beans, Roger-tofu
• 16 possible worlds
• 7 questions forming a strategy tree

         q₁ (What did everyone eat?)
        /                            \
    q_a (What did Hannah eat?)    q_b (What did Roger eat?)
    /        \                    /        \
q_ai (H beans?) q_aii (H tofu?) q_bi (R beans?) q_bii (R tofu?)

Representation

This file uses Core.Question (Set-based, with Prop + Decidable Roberts QUD predicates from Core/Question/Relevance.lean). Non-polar issues are built via Question.ofList and ⊓; entailment for these uses the HasAltList infrastructure from Core/Question/Hamblin.lean. Set-based partitions live in Core/Question/Partition.lean (Core.Question.IsPartition, backed by Setoid.IsPartition).

structure Roberts2012.D0World : Type

A world in the D₀ scenario: 4 independent Boolean facts.

• hb : Bool
• ht : Bool
• rb : Bool
• rt : Bool

def Roberts2012.instDecidableEqD0World.decEq (x✝ x✝¹ : D0World) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Roberts2012.instDecidableEqD0World : DecidableEq D0World

Equations

• Roberts2012.instDecidableEqD0World = Roberts2012.instDecidableEqD0World.decEq

def Roberts2012.instBEqD0World.beq : D0World → D0World → Bool

Equations

• Roberts2012.instBEqD0World.beq { hb := a, ht := a_1, rb := a_2, rt := a_3 } { hb := b, ht := b_1, rb := b_2, rt := b_3 } = (a == b && (a_1 == b_1 && (a_2 == b_2 && a_3 == b_3)))
• Roberts2012.instBEqD0World.beq x✝¹ x✝ = false

@[implicit_reducible]

instance Roberts2012.instBEqD0World : BEq D0World

Equations

• Roberts2012.instBEqD0World = { beq := Roberts2012.instBEqD0World.beq }

def Roberts2012.instReprD0World.repr : D0World → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance Roberts2012.instReprD0World : Repr D0World

Equations

• Roberts2012.instReprD0World = { reprPrec := Roberts2012.instReprD0World.repr }

@[implicit_reducible]

instance Roberts2012.instFintypeD0World : Fintype D0World

Finite enumeration of D0World via the canonical equivalence with Bool × Bool × Bool × Bool.

Equations

• One or more equations did not get rendered due to their size.

theorem Roberts2012.card_D0World : Fintype.card D0World = 16

def Roberts2012.hannahBeans : Set D0World

Hannah ate the beans.

Equations

• Roberts2012.hannahBeans = {w : Roberts2012.D0World | w.hb = true}

def Roberts2012.hannahTofu : Set D0World

Hannah ate the tofu.

Equations

• Roberts2012.hannahTofu = {w : Roberts2012.D0World | w.ht = true}

def Roberts2012.rogerBeans : Set D0World

Roger ate the beans.

Equations

• Roberts2012.rogerBeans = {w : Roberts2012.D0World | w.rb = true}

def Roberts2012.rogerTofu : Set D0World

Roger ate the tofu.

Equations

• Roberts2012.rogerTofu = {w : Roberts2012.D0World | w.rt = true}

@[implicit_reducible]

instance Roberts2012.instDecidablePredD0WorldMemSetHannahBeans : DecidablePred fun (x : D0World) => x ∈ hannahBeans

Equations

• Roberts2012.instDecidablePredD0WorldMemSetHannahBeans w = inferInstance

@[implicit_reducible]

instance Roberts2012.instDecidablePredD0WorldMemSetComplHannahBeans : DecidablePred fun (x : D0World) => x ∈ hannahBeansᶜ

Equations

• Roberts2012.instDecidablePredD0WorldMemSetComplHannahBeans w = inferInstance

@[implicit_reducible]

instance Roberts2012.instDecidablePredD0WorldMemSetHannahTofu : DecidablePred fun (x : D0World) => x ∈ hannahTofu

Equations

• Roberts2012.instDecidablePredD0WorldMemSetHannahTofu w = inferInstance

@[implicit_reducible]

instance Roberts2012.instDecidablePredD0WorldMemSetComplHannahTofu : DecidablePred fun (x : D0World) => x ∈ hannahTofuᶜ

Equations

• Roberts2012.instDecidablePredD0WorldMemSetComplHannahTofu w = inferInstance

@[implicit_reducible]

instance Roberts2012.instDecidablePredD0WorldMemSetRogerBeans : DecidablePred fun (x : D0World) => x ∈ rogerBeans

Equations

• Roberts2012.instDecidablePredD0WorldMemSetRogerBeans w = inferInstance

@[implicit_reducible]

instance Roberts2012.instDecidablePredD0WorldMemSetComplRogerBeans : DecidablePred fun (x : D0World) => x ∈ rogerBeansᶜ

Equations

• Roberts2012.instDecidablePredD0WorldMemSetComplRogerBeans w = inferInstance

@[implicit_reducible]

instance Roberts2012.instDecidablePredD0WorldMemSetRogerTofu : DecidablePred fun (x : D0World) => x ∈ rogerTofu

Equations

• Roberts2012.instDecidablePredD0WorldMemSetRogerTofu w = inferInstance

@[implicit_reducible]

instance Roberts2012.instDecidablePredD0WorldMemSetComplRogerTofu : DecidablePred fun (x : D0World) => x ∈ rogerTofuᶜ

Equations

• Roberts2012.instDecidablePredD0WorldMemSetComplRogerTofu w = inferInstance

Nontriviality lemmas (manual, one per atomic proposition)

theorem Roberts2012.hb_ne_empty : hannahBeans ≠ ∅

theorem Roberts2012.hb_ne_univ : hannahBeans ≠ Set.univ

theorem Roberts2012.ht_ne_empty : hannahTofu ≠ ∅

theorem Roberts2012.ht_ne_univ : hannahTofu ≠ Set.univ

theorem Roberts2012.rb_ne_empty : rogerBeans ≠ ∅

theorem Roberts2012.rb_ne_univ : rogerBeans ≠ Set.univ

theorem Roberts2012.rt_ne_empty : rogerTofu ≠ ∅

theorem Roberts2012.rt_ne_univ : rogerTofu ≠ Set.univ

@[reducible, inline]

abbrev Roberts2012.q_ai : Core.Question D0World

"Did Hannah eat the beans?"

Equations

• Roberts2012.q_ai = Core.Question.polar Roberts2012.hannahBeans

@[reducible, inline]

abbrev Roberts2012.q_aii : Core.Question D0World

"Did Hannah eat the tofu?"

Equations

• Roberts2012.q_aii = Core.Question.polar Roberts2012.hannahTofu

@[reducible, inline]

abbrev Roberts2012.q_bi : Core.Question D0World

"Did Roger eat the beans?"

Equations

• Roberts2012.q_bi = Core.Question.polar Roberts2012.rogerBeans

@[reducible, inline]

abbrev Roberts2012.q_bii : Core.Question D0World

"Did Roger eat the tofu?"

Equations

• Roberts2012.q_bii = Core.Question.polar Roberts2012.rogerTofu

def Roberts2012.q_a : Core.Question D0World

"What did Hannah eat?" — partition into 4 cells by ⟨hb, ht⟩. Beans-only, tofu-only, both, neither.

Equations

• One or more equations did not get rendered due to their size.

def Roberts2012.q_b : Core.Question D0World

"What did Roger eat?" — partition by ⟨rb, rt⟩.

Equations

• One or more equations did not get rendered due to their size.

def Roberts2012.q_1 : Core.Question D0World

"What did everyone eat?" — the Big Question, the lattice meet of q_a and q_b (knowing what everyone ate = knowing what Hannah ate AND what Roger ate).

Equations

• Roberts2012.q_1 = Roberts2012.q_a ⊓ Roberts2012.q_b

theorem Roberts2012.qai_entails_qai : q_ai.questionEntails q_ai

q_ai entails itself (sanity check).

theorem Roberts2012.qai_not_entails_qbi : ¬q_ai.questionEntails q_bi

q_ai does NOT entail q_bi: knowing whether Hannah ate beans tells you nothing about whether Roger ate beans (orthogonal polar questions).

theorem Roberts2012.q1_entails_qa : q_1.questionEntails q_a

The Big Question entails "What did Hannah eat?"

theorem Roberts2012.q1_entails_qb : q_1.questionEntails q_b

The Big Question entails "What did Roger eat?"

theorem Roberts2012.qa_entails_qai : q_a.questionEntails q_ai

"What did Hannah eat?" entails "Did Hannah eat the beans?"

theorem Roberts2012.qa_entails_qaii : q_a.questionEntails q_aii

"What did Hannah eat?" entails "Did Hannah eat the tofu?"

theorem Roberts2012.qb_entails_qbi : q_b.questionEntails q_bi

"What did Roger eat?" entails "Did Roger eat the beans?"

theorem Roberts2012.qb_entails_qbii : q_b.questionEntails q_bii

"What did Roger eat?" entails "Did Roger eat the tofu?"

theorem Roberts2012.qa_not_entails_q1 : ¬q_a.questionEntails q_1

q_a does NOT entail q_1. The witness qa_c1 ∈ alt q_a (Hannah-beans-only) contains worlds with all four (rb, rt) combinations; no single q_b cell contains them all, so no alt q_1 (which lies in some q_b cell) can extend qa_c1.

theorem Roberts2012.qai_not_entails_qa : ¬q_ai.questionEntails q_a

q_ai does NOT entail q_a. The witness hannahBeans ∈ alt q_ai contains worlds with both ht = true and ht = false; no q_a cell (each fixing ht) can extend hannahBeans.

theorem Roberts2012.qa_sub_q1 : q_a.isSubquestion q_1

q_a is a subquestion of q_1.

theorem Roberts2012.qb_sub_q1 : q_b.isSubquestion q_1

q_b is a subquestion of q_1.

def Roberts2012.strat_1 : Discourse.Strategy D0World

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

• One or more equations did not get rendered due to their size.

theorem Roberts2012.strat_1_count : strat_1.allQuestions.length = 7

The strategy has 7 questions total.

theorem Roberts2012.strat_1_root_complete : strat_1.isComplete

The root of the strategy is complete: answering "What did Hannah eat?" and "What did Roger eat?" answers "What did everyone eat?" Reduces by top_inf_eq to questionEntails (q_a ⊓ q_b) q_1 = reflexivity.

theorem Roberts2012.strat_1_qa_complete : (Discourse.Strategy.branch q_a [Discourse.Strategy.leaf q_ai, Discourse.Strategy.leaf q_aii]).isComplete

The q_a sub-strategy is complete: pursuing both polar subquestions q_ai and q_aii resolves the wh-question q_a they jointly partition. Closes via polar_inf_polar_le_ofList_of_corners: the four corners (Hannah's beans × tofu) are exactly the cells of q_a.

theorem Roberts2012.strat_1_qb_complete : (Discourse.Strategy.branch q_b [Discourse.Strategy.leaf q_bi, Discourse.Strategy.leaf q_bii]).isComplete

The q_b sub-strategy is complete (mirror of strat_1_qa_complete for Roger).

def Roberts2012.stack_0 : Discourse.QUDStack D0World

Initial state: push the Big Question.

Equations

• Roberts2012.stack_0 = Discourse.QUDStack.empty.push Roberts2012.q_1

def Roberts2012.stack_1 : Discourse.QUDStack D0World

Pursue Hannah's food: push q_a.

Equations

• Roberts2012.stack_1 = Roberts2012.stack_0.push Roberts2012.q_a

def Roberts2012.stack_2 : Discourse.QUDStack D0World

Pursue Hannah+beans: push q_ai.

Equations

• Roberts2012.stack_2 = Roberts2012.stack_1.push Roberts2012.q_ai

def Roberts2012.stack_3 : Discourse.QUDStack D0World

"Hannah ate the beans" answers q_ai: pop.

Equations

• Roberts2012.stack_3 = Roberts2012.stack_2.pop

theorem Roberts2012.stack_depths : stack_0.depth = 1 ∧ stack_1.depth = 2 ∧ stack_2.depth = 3 ∧ stack_3.depth = 2

Stack depths trace the discourse.

theorem Roberts2012.stack_3_qud : stack_3.immediateQUD = some q_a

After popping q_ai, the immediate QUD is q_a.

theorem Roberts2012.neg_hb_partially_answers_qai : q_ai.partiallyAnswers hannahBeansᶜ

"Hannah didn't eat beans" (hannahBeansᶜ) negatively partially answers "Did Hannah eat beans?" — it rules out the hannahBeans alternative.

theorem Roberts2012.neg_hb_partially_answers_qa : q_a.partiallyAnswers hannahBeansᶜ

"Hannah didn't eat beans" also partially answers "What did Hannah eat?" — it rules out the qa_c1 (Hannah-beans-only) alternative.

theorem Roberts2012.hb_partially_answers_qai : q_ai.partiallyAnswers hannahBeans

"Hannah ate beans" positively partially answers q_ai.

theorem Roberts2012.hb_partially_answers_q1 : q_1.partiallyAnswers hannahBeans

"Hannah ate beans" partially answers the Big Question — it rules out the {w_zero} (all-false) alternative.

def Roberts2012.hannahBeans_assertion : Core.Question D0World

"Hannah ate beans" as a single-alternative declarative issue.

Equations

• Roberts2012.hannahBeans_assertion = Core.Question.declarative Roberts2012.hannahBeans

theorem Roberts2012.hannahBeans_relevant_to_q1 : hannahBeans_assertion.moveRelevant q_1 []

"Hannah ate beans" is relevant to q_1 (the Big Question).

theorem Roberts2012.qa_relevant_to_q1 : q_a.moveRelevant q_1 []

q_a is relevant to q_1 as a subquestion: the qa_c1 alternative rules out the {w_zero} alternative of q_1 (since w_zero ∉ qa_c1).

theorem Roberts2012.hannahBeans_relevant_to_strategy : Discourse.moveRelevantToStrategy hannahBeans_assertion strat_1

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

theorem Roberts2012.focus_value_is_propositional_set : Semantics.FocusInterpretation.PropFocusValue D0World = Set (Set D0World)

Q-A congruence in Rooth's framework rests on the type identity PropFocusValue W = Set (Set W): focus values and question denotations are both flat sets of propositions over W. The substrate-level bridge to Core.Question W (inquisitive, downward-closed) lives in the focus-as-issue lift; see Focus/Interpretation.lean.