Faller (2019): The discourse commitments of illocutionary reportatives

@cite{faller-2019a} @cite{farkas-bruce-2010} @cite{stalnaker-1978} @cite{walker-1996} @cite{krifka-2014} @cite{anderbois-2014} @cite{gunlogson-2008} @cite{murray-2014} @cite{goffman-1979}

Faller's discourse-update framework for the Cuzco Quechua reportative =si. The empirical puzzle (her eq. 1):

• (a) Speakers of CQ uttering a declarative with =si need NOT be committed to the reported proposition φ — they may even deny it.
• (b) Despite (a), they often INTEND φ to resolve the QUD.

Faller's solution: separate animator from principal (Goffman 1979). The reportative encodes that the animator's commitment is to HAVING REPORTATIVE EVIDENCE, while the principal — distinct from the animator — is the one committed to truth. The Collaborative Principle (Walker 1996) then derives the animator's dependent truth commitment when they don't immediately disagree.

Substrate consumed

• Core/Discourse/Roles.DiscourseRole for binary speaker/addressee (Faller adds Goffman's animator/author/principal — see § Goffman roles below; if a second study consumes these they graduate to substrate).
• Core/Question/Basic.Question is not directly used — Faller's Table is a stack of pushed propositions (her T_i), simpler than the inquisitive substrate.

What this file does NOT consume

• Theories/Dialogue/SAL/* (van der Leer 2026): SAL refines Faller by adding a Kripke layer inside each commitment-set. Faller's framework is the coarser set-of-propositions level. Faller and SAL relate by forgetful projection (SAL → Faller drops the Kripke structure inside states).
• Theories/Dialogue/CommitmentSpace.lean (Krifka 2015): a different framework (commitment-space tree of propositional states); Faller builds on Farkas-Bruce 2010 instead.

Notes for future substrate promotion

Three patterns arise in this file that may eventually graduate to substrate when a second consumer needs them:

1. Goffman roles (Animator/Author/Principal). Cited by AnderBois 2014, Murray 2014, Bary 2025, MV 2026. If/when a second study file imports them, promote to Core/Discourse/GoffmanRoles.lean.
2. Multi-typed commitment sets (TC, AeC, RepC, BpgC). The "open list of evidence-typed commitment sets per agent" pattern. Faller has 4 types; future papers may add more. If a second consumer wants the same shape, promote a generic EvidenceTypedCommitments to Theories/Discourse/.
3. Collaborative Principle as a defeasible discourse rule. Referenced by Walker 1996, Asher-Lascarides 2008, Geurts 2019, Bary 2025. Substrate candidate.

Each is currently inline in this study file.

§ Goffman 1979 speaker roles (inline; promote to substrate when 2nd consumer arrives)

inductive Phenomena.Assertion.Studies.Faller2019.GoffmanRole : Type

@cite{goffman-1979} Frame Analysis 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 (Faller 2019), quotations, messengers, and spokespersons 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 — whose commitment is conveyed.

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Faller2019.instDecidableEqGoffmanRole : DecidableEq GoffmanRole

Equations

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

def Phenomena.Assertion.Studies.Faller2019.instReprGoffmanRole.repr : GoffmanRole → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Faller2019.instReprGoffmanRole : Repr GoffmanRole

Equations

• Phenomena.Assertion.Studies.Faller2019.instReprGoffmanRole = { reprPrec := Phenomena.Assertion.Studies.Faller2019.instReprGoffmanRole.repr }

def Phenomena.Assertion.Studies.Faller2019.instInhabitedGoffmanRole.default : GoffmanRole

Equations

• Phenomena.Assertion.Studies.Faller2019.instInhabitedGoffmanRole.default = Phenomena.Assertion.Studies.Faller2019.GoffmanRole.animator

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Faller2019.instInhabitedGoffmanRole : Inhabited GoffmanRole

Equations

• Phenomena.Assertion.Studies.Faller2019.instInhabitedGoffmanRole = { default := Phenomena.Assertion.Studies.Faller2019.instInhabitedGoffmanRole.default }

structure Phenomena.Assertion.Studies.Faller2019.RoleAssignment (E : Type u_2) : Type u_2

A Goffman-role assignment: who fills each of the three roles in a given utterance. In default cases (a = author = principal), this collapses to the standard speaker. Reportatives require animator ≠ principal.

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

def Phenomena.Assertion.Studies.Faller2019.RoleAssignment.canonical {E : Type u_2} (e : E) : RoleAssignment E

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

Equations

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

@[simp]

theorem Phenomena.Assertion.Studies.Faller2019.canonical_animator {E : Type u_2} (e : E) : (RoleAssignment.canonical e).animator = e

@[simp]

theorem Phenomena.Assertion.Studies.Faller2019.canonical_principal {E : Type u_2} (e : E) : (RoleAssignment.canonical e).principal = e

@[simp]

theorem Phenomena.Assertion.Studies.Faller2019.canonical_author {E : Type u_2} (e : E) : (RoleAssignment.canonical e).author = e

def Phenomena.Assertion.Studies.Faller2019.RoleAssignment.messenger {E : Type u_2} (anim prin : E) : RoleAssignment E

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

Equations

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

§ Faller's commitment-typed discourse state

inductive Phenomena.Assertion.Studies.Faller2019.EvidenceType : Type

@cite{faller-2019a} eqs. 24-25: the per-agent commitment sets. Open-ended; Faller introduces TC, AeC, RepC, BpgC explicitly and notes "other types of evidential commitment sets" can be added.

A Set (Set W) per evidence type per agent: the set of propositions (modelled as Set W) the agent has committed to of that type.

truthCommit a = TC_a : "x is committed to the truth of φ" evidCommit .adequate a = AeC_a : "x has adequate evidence for φ" evidCommit .reportative a = RepC_a : "x has reportative evidence" evidCommit .bpg a = BpgC_a : "x has best possible grounds" Future cases extend EvidenceType.

• adequate : EvidenceType

  Adequate evidence (Grice 1989: p. 29). The default for unmarked assertions per Faller 2019 §4.2.

• reportative : EvidenceType

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

• bpg : EvidenceType

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

• inferential : EvidenceType

  Inferential evidence (the CQ -chá conjectural).

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Faller2019.instDecidableEqEvidenceType : DecidableEq EvidenceType

Equations

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

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Faller2019.instReprEvidenceType : Repr EvidenceType

Equations

• Phenomena.Assertion.Studies.Faller2019.instReprEvidenceType = { reprPrec := Phenomena.Assertion.Studies.Faller2019.instReprEvidenceType.repr }

def Phenomena.Assertion.Studies.Faller2019.instReprEvidenceType.repr : EvidenceType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Assertion.Studies.Faller2019.instInhabitedEvidenceType : Inhabited EvidenceType

Equations

• Phenomena.Assertion.Studies.Faller2019.instInhabitedEvidenceType = { default := Phenomena.Assertion.Studies.Faller2019.instInhabitedEvidenceType.default }

def Phenomena.Assertion.Studies.Faller2019.instInhabitedEvidenceType.default : EvidenceType

Equations

• Phenomena.Assertion.Studies.Faller2019.instInhabitedEvidenceType.default = Phenomena.Assertion.Studies.Faller2019.EvidenceType.adequate

structure Phenomena.Assertion.Studies.Faller2019.DiscourseState (W : Type u_2) (E : Type u_3) : Type (max u_2 u_3)

Faller 2019's discourse state: per-agent typed commitment sets plus a Table (stack of issues) and Common Ground.

Genericised over agent type E and world type W.

• truthCommit : E → Set (Set W)

  TC_x : truth commitments per agent.

• evidCommit : EvidenceType → E → Set (Set W)

  Per-evidence-type commitment sets per agent.

• table : List (Set W)

  Faller's Table T: a stack of propositions pushed by speech acts.

• commonGround : Set (Set W)

  Common Ground: jointly accepted propositions.

def Phenomena.Assertion.Studies.Faller2019.DiscourseState.empty {W : Type u_1} {E : Type u_2} : DiscourseState W E

The empty discourse state: no commitments, no table, no CG.

Equations

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

def Phenomena.Assertion.Studies.Faller2019.DiscourseState.addTruthCommit {W : Type u_1} {E : Type u_2} (s : DiscourseState W E) (a : E) (φ : Set W) : DiscourseState W E

Add a proposition to an agent's truth commitments.

Encoded propositionally (no if) to avoid requiring DecidableEq E: every other agent's commitments stay the same because the "added when a' = a" disjunct is only satisfied at the target agent.

Equations

• s.addTruthCommit a φ = { truthCommit := fun (a' : E) => {ψ : Set W | ψ ∈ s.truthCommit a' ∨ a' = a ∧ ψ = φ}, evidCommit := s.evidCommit, table := s.table, commonGround := s.commonGround }

def Phenomena.Assertion.Studies.Faller2019.DiscourseState.addEvidCommit {W : Type u_1} {E : Type u_2} (s : DiscourseState W E) (et : EvidenceType) (a : E) (φ : Set W) : DiscourseState W E

Add a proposition to an agent's typed evidential commitments. Same propositional encoding as addTruthCommit.

Equations

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

def Phenomena.Assertion.Studies.Faller2019.DiscourseState.pushTable {W : Type u_1} {E : Type u_2} (s : DiscourseState W E) (φ : Set W) : DiscourseState W E

Push a proposition on top of the Table.

Equations

• s.pushTable φ = { truthCommit := s.truthCommit, evidCommit := s.evidCommit, table := φ :: s.table, commonGround := s.commonGround }

@[simp]

theorem Phenomena.Assertion.Studies.Faller2019.DiscourseState.empty_truthCommit {W : Type u_1} {E : Type u_2} (a : E) : empty.truthCommit a = ∅

@[simp]

theorem Phenomena.Assertion.Studies.Faller2019.DiscourseState.empty_evidCommit {W : Type u_1} {E : Type u_2} (et : EvidenceType) (a : E) : empty.evidCommit et a = ∅

@[simp]

theorem Phenomena.Assertion.Studies.Faller2019.DiscourseState.empty_table {W : Type u_1} {E : Type u_2} : empty.table = []

§ PRESENT and =si

Faller 2019 eq. 27 (initial), revised at eq. 34 with role assignments:

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} ∪ {φ}        -- DEFAULT: principal commits to truth
  (iii) AeC_{a, i+1} = AeC_{a, i} ∪ {φ}      -- DEFAULT: animator commits to evidence
  (iv)  a_{i+1} = p_{i+1}                    -- DEFAULT: animator = principal

The reportative =si (Faller 2019 eq. 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 (iii): RepC, not AeC
  (ii) a_{i+1} ≠ p_{i+1}                    -- override (iv): animator ≠ principal

def Phenomena.Assertion.Studies.Faller2019.PRESENT {W : Type u_1} {E : Type u_2} (φ : Set W) (roles : RoleAssignment E) (s : DiscourseState W E) : DiscourseState W E

@cite{faller-2019a} eq. 34 (final PRESENT): with all defaults active, PRESENT updates Table + TC_principal + AeC_animator + sets animator = principal.

The roles : RoleAssignment E argument carries Faller's eq. 34.iv flexibility: the canonical speaker uses RoleAssignment.canonical; a messenger or reportative use the explicit assignment.

Equations

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

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

@cite{faller-2019a} eq. 35 (CQ =si modifier on PRESENT): override eq. 34.iii (commit to RepC instead of AeC) and require eq. 35.ii (animator ≠ principal).

The role-distinctness requirement is encoded as a precondition: the operator only updates the state when roles.animator ≠ roles.principal. Otherwise it returns the input state unchanged (a defective speech act, per Faller's analysis). Requires DecidableEq E to test the role-distinctness premise — agents in any concrete discourse model are decidable-equal.

Equations

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

§ Headline theorems

These lift Faller's verbal claims to provable statements.

theorem Phenomena.Assertion.Studies.Faller2019.present_commits_principal_to_truth {W : Type u_1} {E : Type u_2} (φ : Set W) (e : E) (s : DiscourseState W E) : φ ∈ (PRESENT φ (RoleAssignment.canonical e) s).truthCommit e

@cite{faller-2019a} default-PRESENT puts φ in the principal's TC. The headline (i) consequence of PRESENT — the speaker (=principal, canonically) commits to truth.

theorem Phenomena.Assertion.Studies.Faller2019.present_commits_animator_to_adequate_evidence {W : Type u_1} {E : Type u_2} (φ : Set W) (e : E) (s : DiscourseState W E) : φ ∈ (PRESENT φ (RoleAssignment.canonical e) s).evidCommit EvidenceType.adequate e

@cite{faller-2019a} default-PRESENT puts φ in the animator's AeC.

theorem Phenomena.Assertion.Studies.Faller2019.reportative_commits_animator_to_reportative_evidence {W : Type u_1} {E : Type u_2} [DecidableEq E] (φ : Set W) (anim prin : E) (h : anim ≠ prin) (s : DiscourseState W E) : φ ∈ (reportativePRESENT φ (RoleAssignment.messenger anim prin) s).evidCommit EvidenceType.reportative anim

@cite{faller-2019a} eq. 35.i: =si adds to RepC. The animator's RepC for φ DOES include φ after =si(PRESENT(φ)) — the headline finding that reportatives flag the evidence type.

theorem Phenomena.Assertion.Studies.Faller2019.reportative_commits_principal_to_truth {W : Type u_1} {E : Type u_2} [DecidableEq E] (φ : Set W) (anim prin : E) (h : anim ≠ prin) (s : DiscourseState W E) : φ ∈ (reportativePRESENT φ (RoleAssignment.messenger anim prin) s).truthCommit prin

@cite{faller-2019a} eq. 35: =si commits the principal (not the animator) to truth. The headline finding: the reportative shifts truth-commitment to the third-party principal.

theorem Phenomena.Assertion.Studies.Faller2019.reportative_does_not_commit_animator_to_truth {W : Type u_1} {E : Type u_2} [DecidableEq E] (φ : Set W) (anim prin : E) (h : anim ≠ prin) : φ ∉ (reportativePRESENT φ (RoleAssignment.messenger anim prin) DiscourseState.empty).truthCommit anim

@cite{faller-2019a} Absence of Commitment (eq. 1.a, headline): after =si(PRESENT(φ)) with distinct animator and principal, the ANIMATOR is NOT committed to truth of φ.

Formal version: starting from the empty state, =si(PRESENT(φ)) does not put φ in the animator's TC.