Scoreboard: Unified Discourse State

@cite{roberts-2023} @cite{roberts-2012} @cite{lewis-1979} @cite{portner-2004}

The scoreboard K for a language game at time t is a tuple ⟨I, M, ≺, CG, QUD, G⟩ (@cite{roberts-2023} §2.1.1), tracking:

• I: the set of interlocutors
• M: illocutionary moves made so far (with subsets A, Q, D, Acc)
• ≺: temporal order on moves
• CG: the common ground (propositions treated as mutually believed)
• QUD: the ordered set of questions under discussion
• G: the interlocutors' publicly evident goals, plans, and priorities

The three central elements — CG, QUD, G — are updated by the three canonical speech acts via the Illocutionary Force Linking Principle (@cite{roberts-2023} (56)):

Clause type	Semantic type	Default force	Updates
declarative	proposition	assertion	CG
interrogative	set of propositions	interrogation	QUD
imperative	indexed property	direction	G

Relation to Prior Work

@cite{lewis-1979}'s "scorekeeping in a language game" introduced the metaphor. @cite{roberts-2012} formalized CG + QUD. @cite{portner-2004} added the addressee's ToDo list. @cite{roberts-2023} unifies all three into a single scoreboard and gives G richer internal structure (conditional goals with hierarchical priorities, following @cite{bratman-1987}).

inductive Core.Discourse.SemanticType : Type

The semantic type of a clause, determining its default illocutionary force.

@cite{roberts-2023} (56): propositions → assertion, sets of propositions → interrogation, indexed properties → direction.

• proposition : SemanticType

  Type ⟨s, t⟩: a proposition (set of worlds)

• setOfPropositions : SemanticType

  Type ⟨⟨s, t⟩, t⟩: a set of propositions (Hamblin question denotation)

• indexedProperty : SemanticType

  Type ⟨s, ⟨e, t⟩⟩: a property indexed to the addressee

@[implicit_reducible]

instance Core.Discourse.instDecidableEqSemanticType : DecidableEq SemanticType

Equations

• Core.Discourse.instDecidableEqSemanticType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.Discourse.instReprSemanticType : Repr SemanticType

Equations

• Core.Discourse.instReprSemanticType = { reprPrec := Core.Discourse.instReprSemanticType.repr }

def Core.Discourse.instReprSemanticType.repr : SemanticType → ℕ → Std.Format

Equations

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

def Core.Discourse.forceLinkingPrinciple : SemanticType → Mood.IllocutionaryMood

Illocutionary Force Linking Principle (@cite{roberts-2023} (56)): the default illocutionary force of a root sentence is determined by its semantic type.

(a) proposition → assertion (b) set of propositions → interrogation (c) indexed property → direction

Equations

• Core.Discourse.forceLinkingPrinciple Core.Discourse.SemanticType.proposition = Core.Mood.IllocutionaryMood.declarative
• Core.Discourse.forceLinkingPrinciple Core.Discourse.SemanticType.setOfPropositions = Core.Mood.IllocutionaryMood.interrogative
• Core.Discourse.forceLinkingPrinciple Core.Discourse.SemanticType.indexedProperty = Core.Mood.IllocutionaryMood.imperative

@[simp]

theorem Core.Discourse.forceLinkingPrinciple_proposition : forceLinkingPrinciple SemanticType.proposition = Mood.IllocutionaryMood.declarative

@[simp]

theorem Core.Discourse.forceLinkingPrinciple_setOfPropositions : forceLinkingPrinciple SemanticType.setOfPropositions = Mood.IllocutionaryMood.interrogative

@[simp]

theorem Core.Discourse.forceLinkingPrinciple_indexedProperty : forceLinkingPrinciple SemanticType.indexedProperty = Mood.IllocutionaryMood.imperative

def Core.Discourse.defaultSemanticType : Mood.IllocutionaryMood → SemanticType

The default semantic type for each illocutionary mood (inverse of IFLP).

Equations

• Core.Discourse.defaultSemanticType Core.Mood.IllocutionaryMood.declarative = Core.Discourse.SemanticType.proposition
• Core.Discourse.defaultSemanticType Core.Mood.IllocutionaryMood.interrogative = Core.Discourse.SemanticType.setOfPropositions
• Core.Discourse.defaultSemanticType Core.Mood.IllocutionaryMood.imperative = Core.Discourse.SemanticType.indexedProperty
• Core.Discourse.defaultSemanticType Core.Mood.IllocutionaryMood.promissive = Core.Discourse.SemanticType.indexedProperty
• Core.Discourse.defaultSemanticType Core.Mood.IllocutionaryMood.exclamative = Core.Discourse.SemanticType.proposition

@[simp]

theorem Core.Discourse.defaultSemanticType_declarative : defaultSemanticType Mood.IllocutionaryMood.declarative = SemanticType.proposition

@[simp]

theorem Core.Discourse.defaultSemanticType_interrogative : defaultSemanticType Mood.IllocutionaryMood.interrogative = SemanticType.setOfPropositions

@[simp]

theorem Core.Discourse.defaultSemanticType_imperative : defaultSemanticType Mood.IllocutionaryMood.imperative = SemanticType.indexedProperty

theorem Core.Discourse.iflp_roundtrip_decl : forceLinkingPrinciple (defaultSemanticType Mood.IllocutionaryMood.declarative) = Mood.IllocutionaryMood.declarative

IFLP round-trips for the three core moods.

theorem Core.Discourse.iflp_roundtrip_interrog : forceLinkingPrinciple (defaultSemanticType Mood.IllocutionaryMood.interrogative) = Mood.IllocutionaryMood.interrogative

theorem Core.Discourse.iflp_roundtrip_imp : forceLinkingPrinciple (defaultSemanticType Mood.IllocutionaryMood.imperative) = Mood.IllocutionaryMood.imperative

The Scoreboard

structure Core.Discourse.Move (W : Type u_2) : Type u_2

An illocutionary move on the scoreboard.

@cite{roberts-2023} §2.1.1: M is the set of moves, with distinguished subsets A (assertions), Q (questions), D (directions), Acc (accepted).

• mood : Mood.IllocutionaryMood

  Which kind of speech act

• content : W → Prop

  Propositional content (for assertions and questions; for directions, the propositional closure of the targeted property)

• agent : ℕ

  Who made the move

• accepted : Bool

  Whether this move has been accepted by the interlocutors

def Core.Discourse.instInhabitedMove.default {a✝ : Type u_2} : Move a✝

Equations

• Core.Discourse.instInhabitedMove.default = { mood := default, content := default, agent := default, accepted := default }

@[implicit_reducible]

instance Core.Discourse.instInhabitedMove {a✝ : Type u_2} : Inhabited (Move a✝)

Equations

• Core.Discourse.instInhabitedMove = { default := Core.Discourse.instInhabitedMove.default }

structure Core.Discourse.Scoreboard (W : Type u_2) : Type u_2

The scoreboard K for a language game.

@cite{roberts-2023} §2.1.1: K = ⟨I, M, ≺, CG, QUD, G⟩. We represent ≺ implicitly via list order in moves.

• numInterlocutors : ℕ

  I: the interlocutors (by index)

• moves : List (Move W)

  M: illocutionary moves in temporal order (≺ = list position)

• cg : List (W → Prop)

  CG: the common ground — propositions treated as mutually believed. Represented as a list of propositions; the context set is their intersection.

• qud : List (W → Prop)

  QUD: questions under discussion (as a stack of proposition-sets). Simplified from the full QUDStack for composability.

• goals : List (GoalSet W)

  G: per-agent goal sets. goals[i] is G_i. Length should equal numInterlocutors.

def Core.Discourse.instInhabitedScoreboard.default {a✝ : Type u_2} : Scoreboard a✝

Equations

• Core.Discourse.instInhabitedScoreboard.default = { numInterlocutors := default, moves := default, cg := default, qud := default, goals := default }

@[implicit_reducible]

instance Core.Discourse.instInhabitedScoreboard {a✝ : Type u_2} : Inhabited (Scoreboard a✝)

Equations

• Core.Discourse.instInhabitedScoreboard = { default := Core.Discourse.instInhabitedScoreboard.default }

def Core.Discourse.Scoreboard.contextSet {W : Type u_1} (K : Scoreboard W) : W → Prop

The context set: worlds compatible with all CG propositions.

Equations

• K.contextSet w = ∀ p ∈ K.cg, p w

def Core.Discourse.Scoreboard.agentGoals {W : Type u_1} (K : Scoreboard W) (i : ℕ) : GoalSet W

An agent's goal set. Returns empty if index out of bounds.

Equations

• K.agentGoals i = K.goals.getD i Core.Discourse.GoalSet.empty

def Core.Discourse.Scoreboard.assertionUpdate {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (agent : ℕ) : Scoreboard W

Assertion update (@cite{roberts-2023} (57), following @cite{stalnaker-1978}): If a proposition is asserted and accepted, it is added to CG_K.

Equations

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

def Core.Discourse.Scoreboard.interrogationUpdate {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (agent : ℕ) : Scoreboard W

Interrogation update (@cite{roberts-2023} (58), following @cite{roberts-2012}): If a question is posed and accepted, it is added to QUD_K.

Equations

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

def Core.Discourse.Scoreboard.addGoalAt {W : Type u_1} : List (GoalSet W) → ℕ → ℕ → Goal W → List (GoalSet W)

Replace the target-th goal set in xs (walking from index i) by adding g. Returns xs unchanged if target is out of range (no implicit list extension). Used by directionUpdate and reasoned about by addGoalAt_out_of_range and mem_addGoalAt_flatMap.

Equations

• Core.Discourse.Scoreboard.addGoalAt [] x✝² x✝¹ x✝ = []
• Core.Discourse.Scoreboard.addGoalAt (gs :: rest) x✝² x✝¹ x✝ = (if (x✝¹ == x✝²) = true then gs.add x✝ else gs) :: Core.Discourse.Scoreboard.addGoalAt rest x✝² (x✝¹ + 1) x✝

theorem Core.Discourse.Scoreboard.addGoalAt_out_of_range {W : Type u_1} (xs : List (GoalSet W)) (target i : ℕ) (g : Goal W) (h : target < i) : addGoalAt xs target i g = xs

If the walk is past target, addGoalAt is the identity.

def Core.Discourse.Scoreboard.directionUpdate {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (speaker target : ℕ) (priority : ℕ := 0) : Scoreboard W

Direction update (@cite{roberts-2023} (59)): If a targeted property is issued to addressee i and accepted, G_i is revised to include the realization of the property in any applicable circumstances.

Equations

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

@[simp]

theorem Core.Discourse.Scoreboard.assertion_adds_to_cg {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).cg = p :: K.cg

Assertion update adds to CG.

@[simp]

theorem Core.Discourse.Scoreboard.assertion_preserves_qud {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).qud = K.qud

Assertion update preserves QUD.

@[simp]

theorem Core.Discourse.Scoreboard.assertion_preserves_goals {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).goals = K.goals

Assertion update preserves G.

@[simp]

theorem Core.Discourse.Scoreboard.interrogation_adds_to_qud {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).qud = q :: K.qud

Interrogation update adds to QUD.

@[simp]

theorem Core.Discourse.Scoreboard.interrogation_preserves_cg {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).cg = K.cg

Interrogation update preserves CG.

@[simp]

theorem Core.Discourse.Scoreboard.interrogation_preserves_goals {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).goals = K.goals

Interrogation update preserves G.

@[simp]

theorem Core.Discourse.Scoreboard.direction_preserves_cg {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) : (K.directionUpdate p s t pr).cg = K.cg

Direction update preserves CG.

@[simp]

theorem Core.Discourse.Scoreboard.direction_preserves_qud {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) : (K.directionUpdate p s t pr).qud = K.qud

Direction update preserves QUD.

POSW Substrate Bridge

The scoreboard's CG and G components project jointly into a Core.Mood.POSW substrate (@cite{portner-2018}, eq. 1):

• The cs component is the scoreboard contextSet (∩ of CG).
• The le component is the goal-induced preference ordering: w is at least as good as v iff every active goal content (across every agent) that holds at v also holds at w. Equivalently, w violates no goal that v doesn't already violate.

This makes the two scoreboard updates that target the POSW substrate correspond, by construction, to the two POSW updates of @cite{portner-2018}:

scoreboard	POSW	informational consequence
assertionUpdate	plus	boxCs_plus_self (Stalnakerian principle)
directionUpdate	star	le-refinement: p-violators demoted

We derive both consequences from POSW.boxCs_plus_self and the star-refinement via the bridge theorems below — not re-stipulate them.

def Core.Discourse.Scoreboard.goalContents {W : Type u_1} (K : Scoreboard W) : List (W → Prop)

The flat list of goal contents across all agents. The substrate of the goal-induced preference ordering on toPOSW.

Equations

• K.goalContents = List.flatMap Core.Discourse.GoalSet.toPropertyList K.goals

@[simp]

theorem Core.Discourse.Scoreboard.goalContents_def {W : Type u_1} (K : Scoreboard W) : K.goalContents = List.flatMap GoalSet.toPropertyList K.goals

@[simp]

theorem Core.Discourse.Scoreboard.assertion_preserves_goalContents {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).goalContents = K.goalContents

Assertion update preserves goal contents (since it doesn't touch G).

theorem Core.Discourse.Scoreboard.mem_addGoalAt_flatMap {W : Type u_1} (xs : List (GoalSet W)) (target i : ℕ) (g : Goal W) (hin : i ≤ target) (hbd : target < i + xs.length) (q : W → Prop) : q ∈ List.flatMap GoalSet.toPropertyList (addGoalAt xs target i g) ↔ q = g.content ∨ q ∈ List.flatMap GoalSet.toPropertyList xs

Membership in the flat goal-content list of a directionUpdate-modified scoreboard: the directive's content is added; everything else is preserved. Requires the target to be in bounds.

theorem Core.Discourse.Scoreboard.mem_directionUpdate_goalContents {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) (hin : t < K.goals.length) (q : W → Prop) : q ∈ (K.directionUpdate p s t pr).goalContents ↔ q = p ∨ q ∈ K.goalContents

Membership in the flat goal-content list after directionUpdate: the new directive's content joins the existing goal contents.

def Core.Discourse.Scoreboard.toPOSW {W : Type u_1} (K : Scoreboard W) : Mood.POSW W

Project the scoreboard into a POSW substrate. cs is the scoreboard's contextSet; le is the goal-induced ordering — w is at least as good as v iff w satisfies every goal v satisfies. The two POSW updates of @cite{portner-2018} target these two components (cf. toPOSW_assertion_eq_plus and toPOSW_direction_eq_star).

Equations

• K.toPOSW = { cs := K.contextSet, le := fun (w v : W) => ∀ p ∈ K.goalContents, p v → p w, le_refl := ⋯, le_trans := ⋯ }

@[simp]

theorem Core.Discourse.Scoreboard.toPOSW_cs {W : Type u_1} (K : Scoreboard W) : K.toPOSW.cs = K.contextSet

@[simp]

theorem Core.Discourse.Scoreboard.toPOSW_le {W : Type u_1} (K : Scoreboard W) (w v : W) : K.toPOSW.le w v ↔ ∀ p ∈ K.goalContents, p v → p w

theorem Core.Discourse.Scoreboard.toPOSW_assertion_eq_plus {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) (w : W) : (K.assertionUpdate p a).toPOSW.cs w ↔ (K.toPOSW.plus p).cs w

Assertion-as-+-update bridge (@cite{stalnaker-1978}, @cite{portner-2018} eq. 2a). Asserting p against scoreboard K refines the projected POSW exactly the way POSW.plus does: the new context set is the conjunction of the old context set with p. The bridge is definitional — assertionUpdate is +-update on the cs side.

theorem Core.Discourse.Scoreboard.boxCs_after_assertion {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (a : ℕ) : (K.assertionUpdate p a).toPOSW.boxCs p

Stalnakerian assertion principle (@cite{stalnaker-1978}): after asserting p, p is informationally necessary on the projected POSW. Derived from POSW.boxCs_plus_self via the toPOSW_assertion_eq_plus bridge — not re-stipulated.

theorem Core.Discourse.Scoreboard.toPOSW_direction_eq_star {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) (hin : t < K.goals.length) (w v : W) : (K.directionUpdate p s t pr).toPOSW.le w v ↔ (K.toPOSW.star p).le w v

Direction-as-⋆-update bridge (@cite{portner-2018} eq. 2b, following @cite{portner-2004}). Issuing the directive p to a target in bounds refines the projected POSW exactly the way POSW.star does: the new ordering keeps the old ordering and additionally requires that whenever the dominated world satisfies p, the dominating world does too. The bridge mirrors the assertion bridge — directionUpdate is ⋆-update on the le side, modulo the t < K.goals.length precondition (out-of-range targets silently drop the directive; that's a stipulated property of directionUpdate, not of POSW).

theorem Core.Discourse.Scoreboard.direction_demotes_violators {W : Type u_1} (K : Scoreboard W) (p : W → Prop) (s t pr : ℕ) (hin : t < K.goals.length) (w v : W) (hpv : p v) (hpw : ¬p w) : ¬(K.directionUpdate p s t pr).toPOSW.le w v

Goal-violator demotion (corollary of the ⋆-bridge): after directing p, no p-violator can dominate a p-satisfier in the goal-induced ordering. The directive update genuinely refines the preference relation — the analogue, on the le side, of boxCs_after_assertion on the cs side.

POSWQ Substrate Bridge

The scoreboard's QUD component projects into the third POSW component of @cite{portner-2018} — the inquiry partition of Core.Mood.POSWQ. Each yes/no question q : W → Prop on the QUD stack induces a binary partition (q-true worlds vs. q-false worlds); the joint inquiry is the meet of these binary partitions in the Setoid W lattice.

scoreboard	POSWQ	informational consequence
assertionUpdate	plus	boxCs_plus_self
directionUpdate	star	le-refinement
interrogationUpdate	inquire (?)	boxAns-strengthening

Together these three bridges complete the @cite{portner-2018} 3×3 unification on the discourse-update side.

def Core.Discourse.Scoreboard.qudInquiry {W : Type u_1} (K : Scoreboard W) : Setoid W

The inquiry partition projected from the QUD stack: the meet of the polar Setoids of every question on the stack, with the trivial inquiry (⊤) as identity. The fold convention places the new head's polar Setoid on the right of ⊓ so that consing reduces definitionally to the inquire update on POSWQ. polarSetoid lives in Core/Mood/POSWQ.lean (the natural primitive site — it is the partition substrate).

Equations

• K.qudInquiry = List.foldr (fun (q : W → Prop) (s : Setoid W) => s ⊓ Core.Mood.POSWQ.polarSetoid q) ⊤ K.qud

@[simp]

theorem Core.Discourse.Scoreboard.qudInquiry_nil {W : Type u_1} (K : Scoreboard W) (h : K.qud = []) : K.qudInquiry = ⊤

@[simp]

theorem Core.Discourse.Scoreboard.qudInquiry_cons {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (rest : List (W → Prop)) (h : K.qud = q :: rest) : K.qudInquiry = List.foldr (fun (q : W → Prop) (s : Setoid W) => s ⊓ Mood.POSWQ.polarSetoid q) ⊤ rest ⊓ Mood.POSWQ.polarSetoid q

@[simp]

theorem Core.Discourse.Scoreboard.interrogation_preserves_goalContents {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).goalContents = K.goalContents

Interrogation update preserves goal contents (since it doesn't touch G). Needed for the POSWQ bridge — toPOSWQ projects both le (from goalContents) and inquiry (from qud), and the interrogation update only refines the latter.

def Core.Discourse.Scoreboard.toPOSWQ {W : Type u_1} (K : Scoreboard W) : Mood.POSWQ W

Project the scoreboard into a POSWQ substrate: the underlying POSW plus the QUD-induced inquiry partition. The third row of the @cite{portner-2018} unification table.

Equations

• K.toPOSWQ = { toPOSW := K.toPOSW, inquiry := K.qudInquiry }

@[simp]

theorem Core.Discourse.Scoreboard.toPOSWQ_toPOSW {W : Type u_1} (K : Scoreboard W) : K.toPOSWQ.toPOSW = K.toPOSW

@[simp]

theorem Core.Discourse.Scoreboard.toPOSWQ_inquiry {W : Type u_1} (K : Scoreboard W) : K.toPOSWQ.inquiry = K.qudInquiry

theorem Core.Discourse.Scoreboard.toPOSWQ_interrogation_eq_inquire {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).toPOSWQ.inquiry = (K.toPOSWQ.inquire (Mood.POSWQ.polarSetoid q)).inquiry

Interrogation-as-?-update bridge (@cite{portner-2018} on questions; @cite{groenendijk-stokhof-1984} partitions). Posing a question q against scoreboard K refines the projected POSWQ exactly the way POSWQ.inquire does on the polar Setoid of q: the new inquiry partition is the meet of the old inquiry with the polar partition of q. The bridge is definitional — interrogationUpdate is ?-update on the inquiry side.

theorem Core.Discourse.Scoreboard.boxAns_polar_after_interrogation {W : Type u_1} (K : Scoreboard W) (q : W → Prop) (a : ℕ) : (K.interrogationUpdate q a).toPOSWQ.boxAns q

Question-strengthening principle (the inquiry analogue of boxCs_after_assertion and direction_demotes_violators): after posing q, every proposition that is settled by q and compatible with the prior inquiry is settled by the new POSWQ. Concretely, the polar partition of q itself is settled. Derived from POSWQ.boxAns over the meet — not re-stipulated.