Evidential Illocutionary Operators

@cite{faller-2002} @cite{faller-2019a} @cite{murray-2014} @cite{murray-2017} @cite{krifka-2014} @cite{anderbois-brasoveanu-henderson-2015} @cite{martinez-vera-2024} @cite{martinez-vera-2026}

Two illocutionary operators consistently distinguish direct from indirect evidentials in the Faller / Murray tradition:

• assert (paired with direct evidentials, e.g. Cuzco Quechua -mi, Saraguro Kichwa -rka, Aymara direct -cha): the speaker commits to the scope proposition AND to the not-at-issue evidential proposition.
• present (paired with reportative/inferential evidentials, e.g. Cuzco Quechua -si, Saraguro Kichwa -shka): the speaker brings the scope to the addressee's attention WITHOUT committing to it; commits only to the not-at-issue evidential proposition.

Both operators are illocutionary in the sense of @cite{martinez-vera-2026} Composition Rule III: they consume the full ⟨at-issue, not-at-issue⟩ pair from Theories/Semantics/Composition/Layered and produce a discourse update.

What this module exposes

• EvidentialAct W — the act type produced by assert/present. The name disambiguates from Dialogue.Krifka.SpeechAct W (commitment-space framework, different shape) and Semantics.Modality.Assert.SpeechActEvent W (event-style speech-act primitive). All three are different formalisations of overlapping concepts; future bridge work would unify them through projection lemmas.
• EvidentialAct.raisedPropositions — the propositions the act puts forward to the addressee. This is the substrate-level projection that downstream highlighting consumers cite, rather than re-deriving from commitsToScope. assert raises just the scope; present raises both the scope and its complement (the polar issue), since the speaker is non-committal and both options are on the table.
• Substrate theorems present_raises_polar_negation, assert_raises_only_scope connect commitsToScope to the highlighting-relevant projection. Verum studies, biased polar question studies, and reportative-evidential studies all consume these instead of re-stipulating discourse-update behaviour.

Existing substrate:

• Core.Discourse.Commitment provides commitment slates and IndexedCommitment (Krifka 2015's S⊢φ); EvidentialAct here is a thinner illocutionary-output type that any of the larger discourse-state trackers can ingest.
• Features.Evidentiality.EvidentialSource provides the canonical Aikhenvald 3-way; this module supplies the typological default evidence-source-to-illocutionary-operator mapping.

structure Discourse.EvidentialIllocution.EvidentialAct (W : Type u_1) : Type u_1

The result of applying an illocutionary operator to a layered argument.

Records: speaker, addressee, the scope proposition (regardless of commitment), the not-at-issue evidential proposition, and the binary flag distinguishing assert-flavour (commits to scope) from present-flavour (does not). All four discourse-update tracker families (Krifka commitment-space, Farkas-Bruce table, Murray-style cards, Anderbois-Brasoveanu-Henderson AI-stack) can ingest this record by reading the relevant fields.

Named EvidentialAct to disambiguate from the existing Dialogue.Krifka.SpeechAct (CommitmentSpace.lean) and Semantics.Modality.Assert.SpeechActEvent — three different formalisations of overlapping concepts that should eventually be bridged.

• speaker : Core.Discourse.DiscourseRole

  Speaker of the act.

• addressee : Core.Discourse.DiscourseRole

  Addressee.

• scope : Set W

  The proposition under consideration (regardless of speaker commitment).

• evidentialContent : Set W

  The not-at-issue (evidential) proposition the speaker commits to.

• commitsToScope : Bool

  Whether the speaker publicly commits to scope (assert-flavour) or merely brings it to attention (present-flavour).

def Discourse.EvidentialIllocution.assert {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : EvidentialAct W

@cite{faller-2002}/@cite{faller-2019a}: assert(⟨A, N⟩) commits the speaker both to A (the scope proposition) and to N (the evidential proposition). Used with direct evidentials.

Equations

• Discourse.EvidentialIllocution.assert s a β = { speaker := s, addressee := a, scope := {w : W | β.atIssue w}, evidentialContent := {w : W | β.notAtIssue w}, commitsToScope := true }

def Discourse.EvidentialIllocution.present {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : EvidentialAct W

@cite{murray-2014}/@cite{faller-2019a}: present(⟨A, N⟩) brings A to the addressee's attention but does NOT commit the speaker to A; it commits only to N (the evidential proposition). Used with reportative/inferential evidentials.

Equations

• Discourse.EvidentialIllocution.present s a β = { speaker := s, addressee := a, scope := {w : W | β.atIssue w}, evidentialContent := {w : W | β.notAtIssue w}, commitsToScope := false }

@[simp]

theorem Discourse.EvidentialIllocution.assert_commitsToScope {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (assert s a β).commitsToScope = true

@[simp]

theorem Discourse.EvidentialIllocution.present_commitsToScope {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (present s a β).commitsToScope = false

@[simp]

theorem Discourse.EvidentialIllocution.assert_scope {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (assert s a β).scope = {w : W | β.atIssue w}

@[simp]

theorem Discourse.EvidentialIllocution.present_scope {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (present s a β).scope = {w : W | β.atIssue w}

@[simp]

theorem Discourse.EvidentialIllocution.assert_evidentialContent {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (assert s a β).evidentialContent = {w : W | β.notAtIssue w}

@[simp]

theorem Discourse.EvidentialIllocution.present_evidentialContent {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (present s a β).evidentialContent = {w : W | β.notAtIssue w}

theorem Discourse.EvidentialIllocution.assert_present_differ_only_in_scope_commitment {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (assert s a β).scope = (present s a β).scope ∧ (assert s a β).evidentialContent = (present s a β).evidentialContent ∧ (assert s a β).commitsToScope ≠ (present s a β).commitsToScope

The defining contrast between assert and present: they agree on speaker, addressee, scope, and evidential content, but disagree on whether the speaker commits to scope.

§ Raised propositions: the substrate-level highlighting projection

raisedPropositions is the propositions an act puts forward for the addressee to consider. The commitsToScope flag determines what's raised:

• commitsToScope = true (assert): the speaker has settled the issue; only the scope proposition is raised.
• commitsToScope = false (present): the speaker has NOT settled the issue; both the scope and its negation are raised — the polar issue is open.

This is the substrate-level claim about Faller/Murray's analysis. Verum studies (e.g. Phenomena/Verum/Studies/MartinezVera2026.lean) build their discourse-update maps by adding raisedPropositions to whatever salience tracker they use, rather than re-stipulating the match-on-commitsToScope.

def Discourse.EvidentialIllocution.EvidentialAct.raisedPropositions {W : Type u_1} (a : EvidentialAct W) : Set (Set W)

The propositions an act puts forward to the addressee.

assert raises just the scope (the speaker has committed; ¬scope is not on the table). present raises both scope and ¬scope (the speaker is non-committal, so both polar options are open).

This is the substrate-level projection that downstream highlighting consumers cite. The if is local here so future studies don't re-derive it.

Equations

• a.raisedPropositions = if a.commitsToScope = true then {a.scope} else {a.scope, a.scopeᶜ}

@[simp]

theorem Discourse.EvidentialIllocution.assert_raisedPropositions {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (assert s a β).raisedPropositions = {{w : W | β.atIssue w}}

assert raises only the scope.

@[simp]

theorem Discourse.EvidentialIllocution.present_raisedPropositions {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (present s a β).raisedPropositions = {{w : W | β.atIssue w}, {w : W | β.atIssue w}ᶜ}

present raises both the scope and its complement (the polar issue).

theorem Discourse.EvidentialIllocution.present_raises_polar_negation {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : {w : W | β.atIssue w}ᶜ ∈ (present s a β).raisedPropositions

present raises the negation of its scope as a salient alternative. This is the substrate fact verum studies cite to license a verum-marker follow-up after a reportative evidential.

theorem Discourse.EvidentialIllocution.assert_does_not_raise_polar_negation {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) (hne : ∃ (w : W), β.atIssue w) : {w : W | β.atIssue w}ᶜ ∉ (assert s a β).raisedPropositions

assert does NOT raise the negation of its scope, provided the scope is satisfiable (some world satisfies it). This rules out the degenerate empty-W case where every set equals its complement. The substrate fact verum studies cite to predict that a verum-marker follow-up is INFELICITOUS after a direct evidential.

§ Typological mapping from evidence source to illocutionary flavour

inductive Discourse.EvidentialIllocution.IllocutionaryFlavour : Type

Typological mapping from evidential source to illocutionary operator flavour. Direct evidence licenses assert; hearsay and inference license present (@cite{faller-2002}, @cite{faller-2019a}, @cite{murray-2014}, @cite{murray-2017}).

This is a typological generalisation, not a definitional truth. Footnote 7 of @cite{martinez-vera-2026} documents an Andean exception (a speaker authoritative about Inca history uses the direct -rka in the absence of direct perceptual evidence); per-construction analyses can override the default.

• assertFlavour : IllocutionaryFlavour
• presentFlavour : IllocutionaryFlavour

@[implicit_reducible]

instance Discourse.EvidentialIllocution.instDecidableEqIllocutionaryFlavour : DecidableEq IllocutionaryFlavour

Equations

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

@[implicit_reducible]

instance Discourse.EvidentialIllocution.instReprIllocutionaryFlavour : Repr IllocutionaryFlavour

Equations

• Discourse.EvidentialIllocution.instReprIllocutionaryFlavour = { reprPrec := Discourse.EvidentialIllocution.instReprIllocutionaryFlavour.repr }

def Discourse.EvidentialIllocution.instReprIllocutionaryFlavour.repr : IllocutionaryFlavour → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Discourse.EvidentialIllocution.instInhabitedIllocutionaryFlavour : Inhabited IllocutionaryFlavour

Equations

• Discourse.EvidentialIllocution.instInhabitedIllocutionaryFlavour = { default := Discourse.EvidentialIllocution.instInhabitedIllocutionaryFlavour.default }

def Discourse.EvidentialIllocution.instInhabitedIllocutionaryFlavour.default : IllocutionaryFlavour

Equations

• Discourse.EvidentialIllocution.instInhabitedIllocutionaryFlavour.default = Discourse.EvidentialIllocution.IllocutionaryFlavour.assertFlavour

def Discourse.EvidentialIllocution.IllocutionaryFlavour.ofEvidentialSource : Features.Evidentiality.EvidentialSource → IllocutionaryFlavour

Default mapping from evidential source to illocutionary flavour.

Equations

• Discourse.EvidentialIllocution.IllocutionaryFlavour.ofEvidentialSource Features.Evidentiality.EvidentialSource.direct = Discourse.EvidentialIllocution.IllocutionaryFlavour.assertFlavour
• Discourse.EvidentialIllocution.IllocutionaryFlavour.ofEvidentialSource Features.Evidentiality.EvidentialSource.hearsay = Discourse.EvidentialIllocution.IllocutionaryFlavour.presentFlavour
• Discourse.EvidentialIllocution.IllocutionaryFlavour.ofEvidentialSource Features.Evidentiality.EvidentialSource.inference = Discourse.EvidentialIllocution.IllocutionaryFlavour.presentFlavour

@[simp]

theorem Discourse.EvidentialIllocution.flavour_direct : IllocutionaryFlavour.ofEvidentialSource Features.Evidentiality.EvidentialSource.direct = IllocutionaryFlavour.assertFlavour

@[simp]

theorem Discourse.EvidentialIllocution.flavour_hearsay : IllocutionaryFlavour.ofEvidentialSource Features.Evidentiality.EvidentialSource.hearsay = IllocutionaryFlavour.presentFlavour

@[simp]

theorem Discourse.EvidentialIllocution.flavour_inference : IllocutionaryFlavour.ofEvidentialSource Features.Evidentiality.EvidentialSource.inference = IllocutionaryFlavour.presentFlavour

def Discourse.EvidentialIllocution.applyDefault {W : Type u_1} (src : Features.Evidentiality.EvidentialSource) (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : EvidentialAct W

Apply the typologically-default operator for a given evidential source.

Equations

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

@[simp]

theorem Discourse.EvidentialIllocution.applyDefault_direct {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : applyDefault Features.Evidentiality.EvidentialSource.direct s a β = assert s a β

@[simp]

theorem Discourse.EvidentialIllocution.applyDefault_hearsay {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : applyDefault Features.Evidentiality.EvidentialSource.hearsay s a β = present s a β

@[simp]

theorem Discourse.EvidentialIllocution.applyDefault_inference {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : applyDefault Features.Evidentiality.EvidentialSource.inference s a β = present s a β

theorem Discourse.EvidentialIllocution.direct_commits_indirect_does_not {W : Type u_1} (s a : Core.Discourse.DiscourseRole) (β : Semantics.Composition.Layered.BiLayered W) : (applyDefault Features.Evidentiality.EvidentialSource.direct s a β).commitsToScope = true ∧ (applyDefault Features.Evidentiality.EvidentialSource.hearsay s a β).commitsToScope = false ∧ (applyDefault Features.Evidentiality.EvidentialSource.inference s a β).commitsToScope = false

Direct evidentials commit the speaker to the scope proposition; indirect (hearsay/inference) evidentials do not. The headline typological generalisation.