@cite{brandom-1994}: Scorekeeping Model of Assertion

@cite{brandom-1994} @cite{brandom-1983}Models assertion as a move in a normative scorekeeping game. Each participant tracks a "scorecard" for every other participant, recording two kinds of normative status:

• Commitments: what the agent has publicly committed to
• Entitlements: what the agent is entitled to assert (has reasons for)

The key insight: entitlements have no analog in Stalnaker's model. A speaker can be committed to p without being entitled to p (assertion without adequate grounds) or entitled to p without being committed (possessing evidence but not having asserted).

Scorekeeping

Each agent keeps a score for every other agent. Scores can DISAGREE: agent A might attribute commitment-to-p to agent B, while agent C does not. This means there is no single "common ground" — only an approximation derived from scorecard intersection.

Inferential Closure

If an agent is committed to p and p→q, they are inferentially committed to q (even if they haven't explicitly asserted q). This is Brandom's "material inference" — the content of a claim is determined by its inferential role.

structure Dialogue.Brandom.NormativeStatus (W : Type u_1) : Type u_1

The normative status attributed to an agent by a scorekeeper.

Brandom's central innovation: the deontic score has two independent dimensions. An agent can be committed-but-not-entitled (asserted without grounds), entitled-but-not-committed (has evidence, hasn't asserted), or both (well-grounded assertion).

• commitments : Core.Discourse.Commitment.CommitmentSlate W

  Propositions the agent is committed to

• entitlements : Core.Discourse.Commitment.CommitmentSlate W

  Propositions the agent is entitled to assert

def Dialogue.Brandom.NormativeStatus.empty {W : Type u_1} : NormativeStatus W

Empty normative status: no commitments, no entitlements.

Equations

• Dialogue.Brandom.NormativeStatus.empty = { commitments := Core.Discourse.Commitment.CommitmentSlate.empty, entitlements := Core.Discourse.Commitment.CommitmentSlate.empty }

def Dialogue.Brandom.NormativeStatus.addCommitment {W : Type u_1} (ns : NormativeStatus W) (p : Set W) : NormativeStatus W

Add a commitment (the agent publicly commits to p).

Equations

• ns.addCommitment p = { commitments := ns.commitments.add p, entitlements := ns.entitlements }

def Dialogue.Brandom.NormativeStatus.addEntitlement {W : Type u_1} (ns : NormativeStatus W) (p : Set W) : NormativeStatus W

Add an entitlement (the agent has grounds for p).

Equations

• ns.addEntitlement p = { commitments := ns.commitments, entitlements := ns.entitlements.add p }

inductive Dialogue.Brandom.BAgent : Type

Agent type for the scorekeeping model.

• speaker : BAgent
• addressee : BAgent

@[implicit_reducible]

instance Dialogue.Brandom.instDecidableEqBAgent : DecidableEq BAgent

Equations

• Dialogue.Brandom.instDecidableEqBAgent x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Dialogue.Brandom.instReprBAgent : Repr BAgent

Equations

• Dialogue.Brandom.instReprBAgent = { reprPrec := Dialogue.Brandom.instReprBAgent.repr }

def Dialogue.Brandom.instReprBAgent.repr : BAgent → ℕ → Std.Format

Equations

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

def Dialogue.Brandom.instInhabitedBAgent.default : BAgent

Equations

• Dialogue.Brandom.instInhabitedBAgent.default = Dialogue.Brandom.BAgent.speaker

@[implicit_reducible]

instance Dialogue.Brandom.instInhabitedBAgent : Inhabited BAgent

Equations

• Dialogue.Brandom.instInhabitedBAgent = { default := Dialogue.Brandom.instInhabitedBAgent.default }

structure Dialogue.Brandom.Scorecard (W : Type u_1) : Type u_1

A scorecard: what one agent attributes to another.

card a b is agent a's attribution of normative status to agent b. Crucially, card a b can differ from card c b — scorekeepers can disagree about what another agent is committed/entitled to.

• card : BAgent → BAgent → NormativeStatus W

  Agent a's view of agent b's normative status

def Dialogue.Brandom.Scorecard.empty {W : Type u_1} : Scorecard W

Initial scorecard: everyone attributes empty status to everyone.

Equations

• Dialogue.Brandom.Scorecard.empty = { card := fun (x x_1 : Dialogue.Brandom.BAgent) => Dialogue.Brandom.NormativeStatus.empty }

def Dialogue.Brandom.Scorecard.commitmentsOf {W : Type u_1} (sc : Scorecard W) (keeper scorer : BAgent) : Core.Discourse.Commitment.CommitmentSlate W

Get a specific agent's view of another agent's commitments.

Equations

• sc.commitmentsOf keeper scorer = (sc.card keeper scorer).commitments

def Dialogue.Brandom.Scorecard.entitlementsOf {W : Type u_1} (sc : Scorecard W) (keeper scorer : BAgent) : Core.Discourse.Commitment.CommitmentSlate W

Get a specific agent's view of another agent's entitlements.

Equations

• sc.entitlementsOf keeper scorer = (sc.card keeper scorer).entitlements

structure Dialogue.Brandom.BrandomState (W : Type u_1) : Type u_1

Brandom's discourse state: a scorecard tracking all agent attributions.

• scorecard : Scorecard W

  The scorecard recording normative status attributions

def Dialogue.Brandom.BrandomState.empty {W : Type u_1} : BrandomState W

Initial state: empty scorecard.

Equations

• Dialogue.Brandom.BrandomState.empty = { scorecard := Dialogue.Brandom.Scorecard.empty }

def Dialogue.Brandom.BrandomState.assert {W : Type u_1} (s : BrandomState W) (p : Set W) : BrandomState W

Assert: the speaker undertakes a commitment and authorizes the addressee to re-assert.

@cite{brandom-1994}: asserting p has two effects:

1. The speaker undertakes commitment to p
2. The speaker authorizes others to re-assert p (default entitlement)

Equations

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

def Dialogue.Brandom.BrandomState.effectiveContextSet {W : Type u_1} (s : BrandomState W) : Core.CommonGround.ContextSet W

Effective context set: intersection of all attributed commitments.

This is a LOSSY projection from Brandom → Stalnaker. Brandom's model has strictly more structure (entitlements, disagreement between scorekeepers), but for the AssertionTheory interface we need a single ContextSet.

Equations

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

def Dialogue.Brandom.BrandomState.isStable {W : Type u_1} (s : BrandomState W) : Prop

Stability: the state is stable when all commitments have matching entitlements (no ungrounded assertions).

Equations

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

@[implicit_reducible]

instance Dialogue.Brandom.BrandomState.instDecidableIsStable {W : Type u_1} (s : BrandomState W) : Decidable s.isStable

Equations

• s.instDecidableIsStable = Dialogue.Brandom.BrandomState.instDecidableIsStable._aux_1 s

structure Dialogue.Brandom.Challenge (W : Type u_1) : Type u_1

A challenge: the addressee demands reasons for a commitment.

@cite{brandom-1994}: challenges shift the burden of proof. If the speaker cannot provide entitlement for a commitment, the commitment is defeated (withdrawn from the scorecard).

• challenger : BAgent

  Who issues the challenge

• proposition : Set W

  The proposition challenged

def Dialogue.Brandom.inferentialClosure {W : Type u_1} (cs : Core.Discourse.Commitment.CommitmentSlate W) (rules : List (Set W × Set W)) : Core.Discourse.Commitment.CommitmentSlate W

Inferential closure: if committed to p and p→q, committed to q.

Brandom's "material inference" — the content of a concept is its inferential role, not its reference. An agent's commitments are closed under their acknowledged inferential connections.

TODO: full closure requires a fixpoint computation.

Equations

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

theorem Dialogue.Brandom.scorekeepers_can_disagree : ∃ (sc : Scorecard Unit), (sc.card BAgent.speaker BAgent.addressee).commitments.commitments.length ≠ (sc.card BAgent.addressee BAgent.addressee).commitments.commitments.length

Scorekeepers can disagree: agent A's view of B's status can differ from agent C's view of B's status.

Witnessed by a scorecard where the speaker attributes a commitment to the addressee, but the addressee does not self-attribute it.

@[implicit_reducible]

instance Dialogue.Brandom.instHasContextSetBrandomState {W : Type u_1} : Core.CommonGround.HasContextSet (BrandomState W) W

Brandom states project to a context set via effectiveContextSet (the lossy Brandom → Stalnaker projection: intersection of all self-attributed commitments). The lossy projection is the price of the typeclass — Brandom's per-scorekeeper disagreement is invisible at the HasContextSet API level (cf. scorekeepers_can_disagree).

Equations

• Dialogue.Brandom.instHasContextSetBrandomState = { toContextSet := Dialogue.Brandom.BrandomState.effectiveContextSet }