Faller (2019): The Discourse Commitments of Illocutionary Reportatives

This file formalizes [Fal19]'s account of declaratives with the Cuzco Quechua reportative =si in a modified discourse structure of [FB10]. The puzzle is that the speaker of a reportative declarative need not be committed to the reported proposition φ and may deny it, yet φ is at issue and, unless it is denied, is taken to be proposed for the common ground. The account splits Goffman's animator from the principal ([Gof79]): the operator PRESENT of the declarative puts φ on the Table, commits the principal to its truth and the animator to adequate evidence, with animator and principal identified by default (her (34)); the reportative is an illocutionary modifier that adds φ to the animator's reportative commitments instead and requires the principal to be distinct (her (35)). The structure DS is the Table of Discourse/Commitment/Table.lean with a set of evidential commitments per participant for each evidence type (her (24) and (25)), and present carries the evidence type of its evidential as a parameter, so the plain declarative, the reportative and the best-possible-grounds evidential differ only there and in the distinctness requirement, which is the paper's uniform semantics of evidentials. accept is assertion acceptance (§4.3, Figure 2): the addressee commits on the strength of the assertion, so with reportative evidence, φ leaves the Table and enters the common ground.

The theorems are the paper's tableaux. Default assertion is Figure 1 (assert_discourseCommitments, assert_evid) and its acceptance Figure 2 (accept_discourseCommitments, accept_evid_addressee, mem_commonGround_accept, accept_stack). A reportative presentation is Figure 4: the principal is committed and the animator has reportative evidence (reportative_discourseCommitments_principal, reportative_evid), and Absence of Commitment is reportative_discourseCommitments_animator, the animator's truth commitments being untouched, with reportative_evid_adequate the override of the adequate-evidence default. The animator's denial (37) is Figure 5 (denial_discourseCommitments, denial_evid), and her acceptance under the Collaborative Principle ([Wal96]) Figure 6 (figure6_discourseCommitments, figure6_discourseCommitments_eq_assert). §6.3 draws the upshot with [Gun08]'s distinction: a truth commitment is Dependent when backed by reportative evidence and IsSource when backed by adequate evidence or best possible grounds, so the animator of Figure 6 is committed as after an assertion but only dependently (figure6_dependent, figure6_not_isSource), where the asserter and the denier commit as sources (assert_isSource, denial_isSource) and the English hearsay parenthetical commits dependently (present_reportative_dependent).

Implementation notes

• Goffman's author plays no part in the operators, which take the animator and the principal as participants; the paper treats the principal as a free variable that need not be a participant, and the acceptance of Figure 2 is the addressee's Table.commit, with the Gunlogson distinction carried by the evidential commitments rather than by the Table.
• The Collaborative Principle is pragmatic, so Figure 6 is the animator performing accept on her own reportative presentation rather than an operator of its own.
• The denial is the animator's best-possible-grounds presentation of φᶜ; the Table then carries φᶜ above φ where the paper's tableau shows φ replaced.
• Acceptance keeps φ in the truth commitments when it enters the common ground, as the paper's tableaux do, rather than stripping it as Table.settle does.

References

• [Fal19]
• [FB10]
• [Gof79]
• [Gun08]
• [Wal96]

inductive Faller2019.EvidenceType : Type

The evidence types whose commitments are tracked in distinct sets: adequate evidence in Grice's sense, the default of assertion (24b); reportative evidence, which the reportative =si contributes (25a); best possible grounds, which =mi contributes (25b).

• adequate : EvidenceType
• reportative : EvidenceType
• bpg : EvidenceType

@[instance_reducible]

instance Faller2019.instDecidableEqEvidenceType : DecidableEq EvidenceType

Equations

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

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

Equations

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

@[instance_reducible]

instance Faller2019.instReprEvidenceType : Repr EvidenceType

Equations

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

structure Faller2019.DS (A : Type u_1) (W : Type u_2) extends Commitment.Table A W : Type (max u_1 u_2)

A discourse structure: the Table, with its truth commitments and common ground, and the evidential commitment sets AeC, RepC and BpgC of each participant.

• stack : List (Question W)
• commitments : State A W
• commonGround : Filter W
• evid : EvidenceType → A → Set (Set W)

  The propositions a is committed to having evidence of type e for.

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

The initial structure: the empty Table and no evidential commitments.

Equations

• Faller2019.DS.empty = { toTable := Commitment.Table.empty, evid := fun (x : Faller2019.EvidenceType) (x_1 : A) => ∅ }

def Faller2019.DS.addEvid {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) (e : EvidenceType) : DS A W

Add φ to a's evidential commitments of type e.

Equations

• K.addEvid φ a e = { toTable := K.toTable, evid := Function.update K.evid e (Function.update (K.evid e) a (insert φ (K.evid e a))) }

def Faller2019.DS.present {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) (e : EvidenceType) : DS A W

(34) with an evidential: φ goes on the Table, the principal p commits to its truth and the animator a to evidence of type e.

Equations

• K.present φ a p e = { toTable := K.assert p φ, evid := (K.addEvid φ a e).evid }

def Faller2019.DS.assert {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) : DS A W

Default assertion: the animator is the principal and the evidence is adequate.

Equations

• K.assert φ a = K.present φ a a Faller2019.EvidenceType.adequate

def Faller2019.DS.reportative {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : DS A W

(35): the reportative presents with reportative evidence; that animator and principal are distinct is its requirement, a hypothesis of the theorems below.

Equations

• K.reportative φ a p = K.present φ a p Faller2019.EvidenceType.reportative

def Faller2019.DS.accept {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (b : A) : DS A W

Acceptance of φ by b (§4.3): b commits to φ on the strength of the assertion, so with reportative evidence, φ leaves the Table and enters the common ground.

Equations

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

def Faller2019.DS.Dependent {A : Type u_1} {W : Type u_2} (K : DS A W) (φ : Set W) (a : A) : Prop

A dependent truth commitment ([Gun08]): φ in TC_a ∩ RepC_a (§6.3).

Equations

• K.Dependent φ a = (φ ∈ K.discourseCommitments a ∧ φ ∈ K.evid Faller2019.EvidenceType.reportative a)

def Faller2019.DS.IsSource {A : Type u_1} {W : Type u_2} (K : DS A W) (φ : Set W) (a : A) : Prop

A source commitment: φ in TC_a ∩ AeC_a or in TC_a ∩ BpgC_a (§6.3).

Equations

• K.IsSource φ a = (φ ∈ K.discourseCommitments a ∧ (φ ∈ K.evid Faller2019.EvidenceType.adequate a ∨ φ ∈ K.evid Faller2019.EvidenceType.bpg a))

@[simp]

theorem Faller2019.DS.addEvid_toTable {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) (e : EvidenceType) : (K.addEvid φ a e).toTable = K.toTable

@[simp]

theorem Faller2019.DS.addEvid_evid_self {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) (e : EvidenceType) : (K.addEvid φ a e).evid e a = insert φ (K.evid e a)

theorem Faller2019.DS.addEvid_evid_of_ne {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) (e : EvidenceType) {b : A} (h : b ≠ a) : (K.addEvid φ a e).evid e b = K.evid e b

theorem Faller2019.DS.addEvid_evid_of_ne_type {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) (e : EvidenceType) {e' : EvidenceType} (h : e' ≠ e) : (K.addEvid φ a e).evid e' = K.evid e'

@[simp]

theorem Faller2019.DS.present_toTable {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) (e : EvidenceType) : (K.present φ a p e).toTable = K.assert p φ

@[simp]

theorem Faller2019.DS.present_evid {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) (e : EvidenceType) : (K.present φ a p e).evid = (K.addEvid φ a e).evid

@[simp]

theorem Faller2019.DS.accept_toTable {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (b : A) : (K.accept φ b).toTable = have __src := (K.commit b φ).pop; { stack := __src.stack, commitments := __src.commitments, commonGround := K.commonGround ⊓ Filter.principal φ }

@[simp]

theorem Faller2019.DS.accept_evid {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (b : A) : (K.accept φ b).evid = (K.addEvid φ b EvidenceType.reportative).evid

Figures 1 and 2: default assertion and its acceptance

theorem Faller2019.DS.assert_discourseCommitments {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) : φ ∈ (K.assert φ a).discourseCommitments a

theorem Faller2019.DS.assert_evid {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) : φ ∈ (K.assert φ a).evid EvidenceType.adequate a

theorem Faller2019.DS.assert_stack {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) : (K.assert φ a).stack = Question.ofSet φ :: K.stack

theorem Faller2019.DS.assert_commonGround {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) : (K.assert φ a).commonGround = K.commonGround

theorem Faller2019.DS.accept_discourseCommitments {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a b : A) : φ ∈ ((K.assert φ a).accept φ b).discourseCommitments b

theorem Faller2019.DS.accept_discourseCommitments_speaker {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a b : A) : φ ∈ ((K.assert φ a).accept φ b).discourseCommitments a

theorem Faller2019.DS.accept_evid_addressee {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a b : A) : φ ∈ ((K.assert φ a).accept φ b).evid EvidenceType.reportative b

theorem Faller2019.DS.mem_commonGround_accept {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a b : A) : φ ∈ ((K.assert φ a).accept φ b).commonGround

theorem Faller2019.DS.accept_stack {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a b : A) : ((K.assert φ a).accept φ b).stack = K.stack

Acceptance resolves the issue: the Table is as before the assertion.

Figure 4: reportative presentation and Absence of Commitment

theorem Faller2019.DS.reportative_discourseCommitments_principal {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : φ ∈ (K.reportative φ a p).discourseCommitments p

theorem Faller2019.DS.reportative_evid {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : φ ∈ (K.reportative φ a p).evid EvidenceType.reportative a

theorem Faller2019.DS.reportative_discourseCommitments_animator {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) (h : a ≠ p) : (K.reportative φ a p).discourseCommitments a = K.discourseCommitments a

Absence of Commitment: with a distinct principal the animator's truth commitments are untouched.

theorem Faller2019.DS.reportative_evid_adequate {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : (K.reportative φ a p).evid EvidenceType.adequate = K.evid EvidenceType.adequate

(35i) overrides (34iii): no adequate-evidence commitment is added.

theorem Faller2019.DS.reportative_stack {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : (K.reportative φ a p).stack = Question.ofSet φ :: K.stack

theorem Faller2019.DS.not_discourseCommitments_reportative_empty {A : Type u_1} {W : Type u_2} [DecidableEq A] (φ : Set W) (a p : A) (h : a ≠ p) : φ ∉ (empty.reportative φ a p).discourseCommitments a

Figure 5: the animator's denial

def Faller2019.DS.denial {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : DS A W

The denial (37): the animator presents φᶜ on best possible grounds.

Equations

• K.denial φ a p = (K.reportative φ a p).present φᶜ a a Faller2019.EvidenceType.bpg

theorem Faller2019.DS.denial_discourseCommitments {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) (h : a ≠ p) : φ ∈ (K.denial φ a p).discourseCommitments p ∧ φᶜ ∈ (K.denial φ a p).discourseCommitments a

theorem Faller2019.DS.denial_discourseCommitments_animator {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) (h : a ≠ p) : (K.denial φ a p).discourseCommitments a = insert φᶜ (K.discourseCommitments a)

φ stays out of the animator's truth commitments; only φᶜ enters.

theorem Faller2019.DS.denial_stack {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : (K.denial φ a p).stack = Question.ofSet φᶜ :: Question.ofSet φ :: K.stack

theorem Faller2019.DS.denial_evid {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : φ ∈ (K.denial φ a p).evid EvidenceType.reportative a ∧ φᶜ ∈ (K.denial φ a p).evid EvidenceType.bpg a

theorem Faller2019.DS.denial_isSource {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : (K.denial φ a p).IsSource φᶜ a

Figure 6: the animator's acceptance under the Collaborative Principle

theorem Faller2019.DS.figure6_discourseCommitments {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) (h : a ≠ p) : φ ∈ ((K.reportative φ a p).accept φ a).discourseCommitments a ∧ φ ∈ ((K.reportative φ a p).accept φ a).discourseCommitments p

theorem Faller2019.DS.figure6_discourseCommitments_eq_assert {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) (h : a ≠ p) : ((K.reportative φ a p).accept φ a).discourseCommitments a = (K.assert φ a).discourseCommitments a

The animator's truth commitments are those of an assertion of φ.

theorem Faller2019.DS.figure6_dependent {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) : ((K.reportative φ a p).accept φ a).Dependent φ a

theorem Faller2019.DS.figure6_not_isSource {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a p : A) (h1 : φ ∉ K.evid EvidenceType.adequate a) (h2 : φ ∉ K.evid EvidenceType.bpg a) : ¬((K.reportative φ a p).accept φ a).IsSource φ a

Weaker than an assertion: the animator is not committed as a source unless she already had adequate evidence or best possible grounds for φ.

theorem Faller2019.DS.assert_isSource {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) : (K.assert φ a).IsSource φ a

theorem Faller2019.DS.present_reportative_dependent {A : Type u_1} {W : Type u_2} [DecidableEq A] (K : DS A W) (φ : Set W) (a : A) : (K.present φ a a EvidenceType.reportative).Dependent φ a

The English Juan has a tractor, I hear: an animator who is her own principal but specifies reportative evidence commits dependently.