Faller (2019): The discourse commitments of illocutionary reportatives

[Fal19] [FB10] [Sta78] [Wal96] [Kri14] [AB14] [Gun08] [Mur14] [Gof79]

Faller's discourse-update account of the Cuzco Quechua reportative =si. The puzzle (her display (1)): a speaker of a reportative declarative need not be committed to the reported proposition φ — they may even deny it (1a) — yet often intends φ to resolve the QUD (1b). Faller's solution splits Goffman's animator from principal: the reportative commits the animator only to having reportative evidence, while the distinct principal carries the truth commitment. The Collaborative Principle ([Wal96]) then derives the animator's dependent truth commitment when they do not disagree.

Main declarations

• GoffmanRole, RoleAssignment — animator / author / principal (her (30)).
• EvidenceType — adequate / reportative / bpg (her (24)–(25)), with an inferential extension.
• DiscourseState — the Farkas-Bruce table state extended with per-evidence-type commitment sets.
• PRESENT, reportativePRESENT — the speech-act operators (her (34), (35)).

Implementation notes

• Built over Discourse.Commitment.Table.DiscourseState A W (Set W): truth commitments live in the inherited per-agent slate dc, the Table is the proposition stack (I := Set W), and the common ground is cg. Only the evidence-type family evidCommit is Faller-specific.
• Faller numbers her framework as displays (24), (34), (35) — not equations.

Todo

• Model the (1b) half of the puzzle: the Collaborative Principle ([Wal96], her (29)) deriving the animator's dependent truth commitment when they do not disagree (her Figure 6). Only the (1a) Absence-of-Commitment half is formalized here.
• Promote GoffmanRole / EvidenceType to Discourse/ once a second consumer (e.g. [AB14], [Mur14]) imports them.

Goffman 1979 speaker roles

inductive Faller2019.GoffmanRole : Type

[Gof79] "Footing" distinguishes three roles within "speaker": the animator physically utters; the author chose the words; the principal is committed by the words. In standard cases all three coincide; reportatives, quotations, and messengers separate them.

• animator : GoffmanRole

  The individual physically producing the utterance (sound waves).

• author : GoffmanRole

  The individual who selected the words and sentiments expressed.

• principal : GoffmanRole

  The individual whose position is established by the words.

@[implicit_reducible]

instance Faller2019.instDecidableEqGoffmanRole : DecidableEq GoffmanRole

Equations

• Faller2019.instDecidableEqGoffmanRole x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Faller2019.instReprGoffmanRole : Repr GoffmanRole

Equations

• Faller2019.instReprGoffmanRole = { reprPrec := Faller2019.instReprGoffmanRole.repr }

def Faller2019.instReprGoffmanRole.repr : GoffmanRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Faller2019.instInhabitedGoffmanRole : Inhabited GoffmanRole

Equations

• Faller2019.instInhabitedGoffmanRole = { default := Faller2019.instInhabitedGoffmanRole.default }

structure Faller2019.RoleAssignment (E : Type u_1) : Type u_1

A Goffman-role assignment: who fills each role in an utterance. In default cases (animator = author = principal) it collapses to the standard speaker; reportatives require animator ≠ principal.

• animator : E
• author : E
• principal : E

def Faller2019.RoleAssignment.canonical {E : Type u_1} (e : E) : RoleAssignment E

The canonical-speaker assignment: animator = author = principal.

Equations

• Faller2019.RoleAssignment.canonical e = { animator := e, author := e, principal := e }

def Faller2019.RoleAssignment.messenger {E : Type u_1} (anim prin : E) : RoleAssignment E

A messenger-style assignment: animator and principal distinct. This is the configuration the CQ reportative =si requires (her (35ii)).

Equations

• Faller2019.RoleAssignment.messenger anim prin = { animator := anim, author := anim, principal := prin }

@[simp]

theorem Faller2019.RoleAssignment.canonical_animator {E : Type u_1} (e : E) : (canonical e).animator = e

@[simp]

theorem Faller2019.RoleAssignment.canonical_author {E : Type u_1} (e : E) : (canonical e).author = e

@[simp]

theorem Faller2019.RoleAssignment.canonical_principal {E : Type u_1} (e : E) : (canonical e).principal = e

@[simp]

theorem Faller2019.RoleAssignment.messenger_animator {E : Type u_1} (anim prin : E) : (messenger anim prin).animator = anim

@[simp]

theorem Faller2019.RoleAssignment.messenger_principal {E : Type u_1} (anim prin : E) : (messenger anim prin).principal = prin

Commitment-typed discourse state

inductive Faller2019.EvidenceType : Type

The evidence types Faller tracks in distinct commitment sets. Her (24)–(25) define exactly the first three (AeC, RepC, BpgC); inferential is an extension — Faller mentions inferential commitment in prose but defines no InfC set.

• adequate : EvidenceType

  Adequate evidence ([Fal19], after Grice): the default for unmarked assertions.

• reportative : EvidenceType

  Reportative evidence (hearsay). The CQ =si adds to this.

• bpg : EvidenceType

  Best possible grounds (strongest first-hand evidence). The CQ =mi adds to this.

• inferential : EvidenceType

  Inferential evidence (the CQ -chá conjectural). Extension; not one of Faller's defined commitment sets.

@[implicit_reducible]

instance Faller2019.instDecidableEqEvidenceType : DecidableEq EvidenceType

Equations

• Faller2019.instDecidableEqEvidenceType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Faller2019.instReprEvidenceType : Repr EvidenceType

Equations

• Faller2019.instReprEvidenceType = { reprPrec := Faller2019.instReprEvidenceType.repr }

def Faller2019.instReprEvidenceType.repr : EvidenceType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Faller2019.instInhabitedEvidenceType : Inhabited EvidenceType

Equations

• Faller2019.instInhabitedEvidenceType = { default := Faller2019.instInhabitedEvidenceType.default }

structure Faller2019.DiscourseState (A : Type u_1) (W : Type u_2) extends Discourse.Commitment.Table.DiscourseState A W (Set W) : Type (max u_1 u_2)

Faller's discourse structure: the Farkas-Bruce table state — truth commitments in the inherited slate dc, a proposition-stack Table, and a common ground — extended with per-evidence-type commitment sets.

• table : List (Set W)
• dc : A → TaggedSlate W
• cg : CommonGround W
• evidCommit : EvidenceType → A → Discourse.Commitment.CommitmentSlate W

  Per-evidence-type commitment sets per agent (AeC, RepC, BpgC, ...).

def Faller2019.DiscourseState.empty {A : Type u_1} {W : Type u_2} : DiscourseState A W

The empty discourse state: no commitments, empty Table, trivial CommonGround.

Equations

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

def Faller2019.DiscourseState.CommittedTrue {A : Type u_1} {W : Type u_2} (s : DiscourseState A W) (a : A) (φ : Set W) : Prop

Agent a is truth-committed to φ (φ ∈ TC_a).

Equations

• s.CommittedTrue a φ = (φ ∈ (s.dc a).toSlate.commitments)

def Faller2019.DiscourseState.CommittedEvid {A : Type u_1} {W : Type u_2} (s : DiscourseState A W) (et : EvidenceType) (a : A) (φ : Set W) : Prop

Agent a holds φ as evidence of type et (φ ∈ et-C_a).

Equations

• s.CommittedEvid et a φ = (φ ∈ (s.evidCommit et a).commitments)

def Faller2019.DiscourseState.pushTable {A : Type u_1} {W : Type u_2} (s : DiscourseState A W) (φ : Set W) : DiscourseState A W

Push a proposition onto the Table.

Equations

• s.pushTable φ = { toDiscourseState := s.pushItem φ, evidCommit := s.evidCommit }

def Faller2019.DiscourseState.addTruthCommit {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (a : A) (φ : Set W) (src : Discourse.Commitment.CommitmentSource := Discourse.Commitment.CommitmentSource.selfGenerated) : DiscourseState A W

Add φ to agent a's truth commitments (the inherited slate dc), with provenance src (default self-generated — the plain-assertion case; reportativePRESENT marks the principal's animator-introduced commitment other-generated, per [Fal19] fn. 30 / §6.1).

Equations

• s.addTruthCommit a φ src = { toDiscourseState := s.addCommit a φ src, evidCommit := s.evidCommit }

def Faller2019.DiscourseState.addEvidCommit {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (et : EvidenceType) (a : A) (φ : Set W) : DiscourseState A W

Add φ to agent a's type-et evidential commitments.

Equations

• s.addEvidCommit et a φ = { toDiscourseState := s.toDiscourseState, evidCommit := Function.update s.evidCommit et (Function.update (s.evidCommit et) a ((s.evidCommit et a).add φ)) }

Update API

Per-operator @[simp] lemmas, so the headline proofs reduce through this API rather than reaching into substrate slate internals.

@[simp]

theorem Faller2019.DiscourseState.pushTable_toDiscourseState {A : Type u_1} {W : Type u_2} (s : DiscourseState A W) (φ : Set W) : (s.pushTable φ).toDiscourseState = s.pushItem φ

@[simp]

theorem Faller2019.DiscourseState.addTruthCommit_toDiscourseState {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (a : A) (φ : Set W) (src : Discourse.Commitment.CommitmentSource) : (s.addTruthCommit a φ src).toDiscourseState = s.addCommit a φ src

@[simp]

theorem Faller2019.DiscourseState.addEvidCommit_toDiscourseState {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (et : EvidenceType) (a : A) (φ : Set W) : (s.addEvidCommit et a φ).toDiscourseState = s.toDiscourseState

@[simp]

theorem Faller2019.DiscourseState.addTruthCommit_evidCommit {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (a : A) (φ : Set W) (src : Discourse.Commitment.CommitmentSource) : (s.addTruthCommit a φ src).evidCommit = s.evidCommit

@[simp]

theorem Faller2019.DiscourseState.pushTable_evidCommit {A : Type u_1} {W : Type u_2} (s : DiscourseState A W) (φ : Set W) : (s.pushTable φ).evidCommit = s.evidCommit

@[simp]

theorem Faller2019.DiscourseState.addEvidCommit_evidCommit_self {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (et : EvidenceType) (a : A) (φ : Set W) : (s.addEvidCommit et a φ).evidCommit et a = (s.evidCommit et a).add φ

@[simp]

theorem Faller2019.DiscourseState.addEvidCommit_evidCommit_of_ne_agent {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (et : EvidenceType) {a b : A} (h : b ≠ a) (φ : Set W) : (s.addEvidCommit et a φ).evidCommit et b = s.evidCommit et b

@[simp]

theorem Faller2019.DiscourseState.addEvidCommit_evidCommit_of_ne_type {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) {et et' : EvidenceType} (h : et' ≠ et) (a : A) (φ : Set W) : (s.addEvidCommit et a φ).evidCommit et' = s.evidCommit et'

Commitment-membership API

@[simp]

theorem Faller2019.DiscourseState.committedTrue_addTruthCommit_self {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (a : A) (φ : Set W) (src : Discourse.Commitment.CommitmentSource) : (s.addTruthCommit a φ src).CommittedTrue a φ

@[simp]

theorem Faller2019.DiscourseState.committedTrue_addTruthCommit_of_ne {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) {a b : A} (h : b ≠ a) (φ ψ : Set W) (src : Discourse.Commitment.CommitmentSource) : (s.addTruthCommit a φ src).CommittedTrue b ψ ↔ s.CommittedTrue b ψ

@[simp]

theorem Faller2019.DiscourseState.committedTrue_pushTable {A : Type u_1} {W : Type u_2} (s : DiscourseState A W) (φ ψ : Set W) (a : A) : (s.pushTable φ).CommittedTrue a ψ ↔ s.CommittedTrue a ψ

@[simp]

theorem Faller2019.DiscourseState.committedTrue_addEvidCommit {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (et : EvidenceType) (a b : A) (φ ψ : Set W) : (s.addEvidCommit et a φ).CommittedTrue b ψ ↔ s.CommittedTrue b ψ

@[simp]

theorem Faller2019.DiscourseState.committedEvid_addEvidCommit_self {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (et : EvidenceType) (a : A) (φ : Set W) : (s.addEvidCommit et a φ).CommittedEvid et a φ

@[simp]

theorem Faller2019.DiscourseState.committedEvid_addTruthCommit {A : Type u_1} {W : Type u_2} [DecidableEq A] (s : DiscourseState A W) (et : EvidenceType) (a b : A) (φ ψ : Set W) (src : Discourse.Commitment.CommitmentSource) : (s.addTruthCommit b φ src).CommittedEvid et a ψ ↔ s.CommittedEvid et a ψ

@[simp]

theorem Faller2019.DiscourseState.committedEvid_pushTable {A : Type u_1} {W : Type u_2} (s : DiscourseState A W) (et : EvidenceType) (a : A) (φ ψ : Set W) : (s.pushTable φ).CommittedEvid et a ψ ↔ s.CommittedEvid et a ψ

@[simp]

theorem Faller2019.DiscourseState.not_committedTrue_empty {A : Type u_1} {W : Type u_2} (a : A) (φ : Set W) : ¬empty.CommittedTrue a φ

PRESENT and =si

Faller's final PRESENT, her display (34) (revising the initial three-clause (27), which committed the speaker's own TC and AeC):

PRESENT(φ, a, K_i) = K_{i+1} such that
  (i)   T_{i+1}   = push(φ, T_i)            -- always: scope on Table
  (ii)  TC_{p,i+1} = TC_{p,i} ∪ {φ}         -- principal commits to truth
  (iii) AeC_{a,i+1} = AeC_{a,i} ∪ {φ}       -- animator commits to evidence
  (iv)  a_{i+1}    = p_{i+1}                -- default: animator = principal

The reportative =si (her (35)) is a modifier on PRESENT:

=si(PRESENT)(φ, a, K_i) = PRESENT(φ, a, K_i) such that
  (i)  RepC_{a,i+1} = RepC_{a,i} ∪ {φ}      -- override (34iii): RepC, not AeC
  (ii) a_{i+1} ≠ p_{i+1}                    -- override (34iv): animator ≠ principal

def Faller2019.DiscourseState.PRESENT {A : Type u_1} {W : Type u_2} [DecidableEq A] (φ : Set W) (roles : RoleAssignment A) (s : DiscourseState A W) : DiscourseState A W

[Fal19] (34): with defaults active, PRESENT pushes φ to the Table, commits the principal to truth, and the animator to adequate evidence. The roles argument carries (34iv) flexibility: the canonical speaker uses RoleAssignment.canonical; a messenger uses the explicit assignment.

Equations

• Faller2019.DiscourseState.PRESENT φ roles s = ((s.pushTable φ).addTruthCommit roles.principal φ).addEvidCommit Faller2019.EvidenceType.adequate roles.animator φ

def Faller2019.DiscourseState.reportativePRESENT {A : Type u_1} {W : Type u_2} [DecidableEq A] (φ : Set W) (roles : RoleAssignment A) (s : DiscourseState A W) : DiscourseState A W

[Fal19] (35): the CQ =si modifier on PRESENT overrides (34iii) (commit to RepC, not AeC) and requires (35ii) (animator ≠ principal). The distinctness requirement is a precondition: the operator updates only when roles.animator ≠ roles.principal, else returns the input unchanged (a defective speech act).

Equations

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

Headline theorems

These lift Faller's verbal claims to provable statements over the substrate discourse state.

theorem Faller2019.DiscourseState.present_commits_principal_to_truth {A : Type u_1} {W : Type u_2} [DecidableEq A] (φ : Set W) (e : A) (s : DiscourseState A W) : (PRESENT φ (RoleAssignment.canonical e) s).CommittedTrue e φ

[Fal19] (34ii): default PRESENT puts φ in the principal's truth commitments.

theorem Faller2019.DiscourseState.present_commits_animator_to_adequate_evidence {A : Type u_1} {W : Type u_2} [DecidableEq A] (φ : Set W) (e : A) (s : DiscourseState A W) : (PRESENT φ (RoleAssignment.canonical e) s).CommittedEvid EvidenceType.adequate e φ

[Fal19] (34iii): default PRESENT puts φ in the animator's adequate-evidence commitments.

theorem Faller2019.DiscourseState.reportative_commits_animator_to_reportative_evidence {A : Type u_1} {W : Type u_2} [DecidableEq A] (φ : Set W) (anim prin : A) (h : anim ≠ prin) (s : DiscourseState A W) : (reportativePRESENT φ (RoleAssignment.messenger anim prin) s).CommittedEvid EvidenceType.reportative anim φ

[Fal19] (35i): =si adds φ to the animator's reportative commitments — the headline that reportatives flag the evidence type.

theorem Faller2019.DiscourseState.reportative_commits_principal_to_truth {A : Type u_1} {W : Type u_2} [DecidableEq A] (φ : Set W) (anim prin : A) (h : anim ≠ prin) (s : DiscourseState A W) : (reportativePRESENT φ (RoleAssignment.messenger anim prin) s).CommittedTrue prin φ

[Fal19] (35): =si commits the principal (not the animator) to truth — the reportative shifts truth-commitment to the third party.

theorem Faller2019.DiscourseState.reportative_does_not_commit_animator_to_truth {A : Type u_1} {W : Type u_2} [DecidableEq A] (φ : Set W) (anim prin : A) (h : anim ≠ prin) : ¬(reportativePRESENT φ (RoleAssignment.messenger anim prin) empty).CommittedTrue anim φ

[Fal19] Absence of Commitment (1a): after =si(PRESENT(φ)) with distinct animator and principal, the animator is not truth-committed to φ. Starting from empty, the animator's truth commitments stay empty because =si's truth update fires only on the principal.

theorem Faller2019.DiscourseState.reportative_evidence_without_truth {A : Type u_1} {W : Type u_2} [DecidableEq A] (φ : Set W) (anim prin : A) (h : anim ≠ prin) : (reportativePRESENT φ (RoleAssignment.messenger anim prin) empty).CommittedEvid EvidenceType.reportative anim φ ∧ ¬(reportativePRESENT φ (RoleAssignment.messenger anim prin) empty).CommittedTrue anim φ

[Fal19] (25): truth and evidential commitments are formally independent — witnessed by the reportative configuration, where the animator holds φ as reportative evidence yet is not truth-committed to it.