[Rud25b]: Embedded Intonation and Quotative Complements

Rudin, Deniz (2025/2026). "Embedded Intonation and Quotative Complements to Verbs of Speech." Linguistic Inquiry, early access. doi:10.1162/ling.a.554.

Empirical Generalizations

The paper's central observation: verbs of speech systematically split on whether they accept rising-declarative ("quotative") complements:

Verb	"p"	"p?"	"p" loud	"p" whisp	that p	that wh / Q
say	✓	✓	✓	✓	✓	✗
assert	✓	✗	✓	✓	✓	✗
yell	✓	✓	✓	✗	✓	✗
whisper	✓	✓	✗	✓	✓	✗
ask	✗	✓	✗	✗	✗	✓

Architecture: One Definition, Not Three

Following mathlib practice, this file has no parallel formalizations.

• Felicitous M V c is the single, model-parameterized definition of felicity: a complement is felicitous with a verb predicate iff there exists a witness (event + performance/proposition) with the right ontological properties.
• IsRudinModel M is a class with 30 fields, one per cell. This is the statement of [Rud25b]'s empirical claim — any model is tested against it.
• rudinModel is the concrete SpeechVerbs ℕ Bool (FBPerformance Bool) (fbOntology Bool) instantiation — Farkas-Bruce-grounded, with verb predicates defined as the postulate RHS so the meaning postulates hold by rfl.
• instance : IsRudinModel rudinModel discharges the 30 cells from the postulates + FB ontology axioms.

There is no separate empirical : Verb → Complement → Felicity function and no separate predicted decision function. The empirical matrix and its derivation are the same proposition.

Demonstration Semantics for Quotative Complements

[Rud25b] [davidson-2015] [eckardt-2014] [maier-2017]

A double-Davidsonian analysis of quotative complements to verbs of speech, following [Rud25b]'s "Embedded Intonation and Quotative Complements to Verbs of Speech" (Linguistic Inquiry).

The Core Shift

Standard analysis of Sara said "Aaron likes apples":

• say is a 2-place predicate of events and propositions
• The quote denotes a proposition (or content individual)
• say introduces a CONTENT relation between the event and the proposition

[Rud25b]'s proposal: verbs of speech are uniformly 1-place event predicates. The complementizer — overt that or covert QUOTE — supplies the relation:

⟦say⟧ = λe. SAY(e) ⟦that⟧ introduces CONTENT(e, p) for propositional δ ⟦QUOTE⟧ introduces REENACT(e, u) for a paratactic performance u

A quotative complement is a covert demonstrative pthat whose referent is the cotemporaneous performance u itself. Composition is via predicate modification, not function application.

Architecture

We split the formalization in two layers:

1. PerformanceOntology Perf — properties of utterance-events (LINGMAT, Loud, Whispered, RisingDecl, Commits, RaisesIssue) and the cross-property axioms that drive verb-class postulates.
2. SpeechVerbs Time SemObj Perf [Ω] — verb predicates (SAY, ASK, ASSERT, YELL, WHISPER), event relations (CONTENT, REENACT), and meaning postulates that connect verbs to performances via the ontology.

This split mirrors mathlib practice: a small "data" structure exposing properties + axioms, separated from the larger structure that consumes them. It also makes the Farkas-Bruce bridge possible: a discourse-state adapter can supply a PerformanceOntology instance whose Commits and RaisesIssue are derived from F&B dcS / table operations rather than stipulated (see Pragmatics/Assertion/QuotationFBOntology.lean).

Meaning Postulates

The verb-class differences are captured by meaning postulates constraining the relation between verbal predicates and properties of performances:

SAY(e) ↔ ∀u. REENACT(e,u) → LINGMAT(u) (Rudin §3.3.4) ASK(e) ↔ ∀u. REENACT(e,u) → RESP(u) (Rudin §4.4.1) ASSERT(e) ↔ SAY(e) ∧ ∀u. REENACT(e,u) → Commits(u) [extrapolation] YELL(e) ↔ SAY(e) ∧ ∀u. REENACT(e,u) → Loud(u) [extrapolation] WHISPER(e) ↔ SAY(e) ∧ ∀u. REENACT(e,u) → Whispered(u) [extrapolation]

where RESP(u) := RaisesIssue(u) ∧ ¬ Commits(u) is the "response-eliciting" property characterized by [Rud25b].

These postulates derive [Rud25b]'s empirical generalizations:

• yell is consistent with quotative complements requiring loud performances; whisper is not (incompatible with loud quotation).
• assert requires the speaker to commit to the content; rising declaratives don't commit; therefore assert "p?" is infelicitous while say "p?" is fine.
• ask requires the absence of commitment AND issue-raising; rising declaratives are exactly that; therefore ask "p?" is fine even though propositional ask that p is not.

The ASSERT/YELL/WHISPER postulates are formal extrapolations of the informal generalizations in [Rud25b] (the paper states the empirical generalization but does not provide a formal postulate for each verb). The SAY and ASK postulates are explicit in the paper.

Anchoring

Performances are events in their own right — utterance-events paratactically associated with the speech-event. We model Performance as a type synonym Event Time, following [Rud25b]'s remark that performances are special-purpose events. But the SpeechVerbs structure is parameterized over an arbitrary Perf type, so alternative ontologies (e.g., a Farkas-Bruce-derived discourse adapter) can supply their own performance type.

@[reducible, inline]

abbrev Semantics.Quotation.Demonstration.Performance (Time : Type u_1) [LinearOrder Time] : Type u_1

Default performance type: an Event Time, since performances have temporal extent and ontological status as events (per [Rud25b], fn 21). The SpeechVerbs structure is parameterized over Perf, so users may instantiate Perf with other types (e.g., a discourse-state-derived performance type).

Equations

• Semantics.Quotation.Demonstration.Performance Time = Event Time

structure Semantics.Quotation.Demonstration.PerformanceOntology (Perf : Type u_1) : Type u_1

The ontology of performance properties.

Bundles the basic properties of utterance-events that the verb-class meaning postulates appeal to, plus the cross-property axioms that [Rud25b] relies on (loud/whispered exclusion, rising declaratives' non-commitment, etc.).

Parameterized over Perf so that downstream modules can supply alternative performance ontologies (e.g., one whose Commits is derived from a Farkas-Bruce discourse-state update).

• LINGMAT : Perf → Prop

  LINGMAT: the performance is linguistic material ([Rud25b] §3.3.4).

• Loud : Perf → Prop

  Loud: the performance is loud.

• Whispered : Perf → Prop

  Whispered: the performance is whispered (sub-vocal).

• RisingDecl : Perf → Prop

  RisingDecl: the performance has rising declarative intonation ([Rud25b] §4.1, the empirical engine of the paper).

• Commits : Perf → Prop

  Commits: the performance commits its speaker to its content (Farkas-Bruce dcS update; [FB10]).

• RaisesIssue : Perf → Prop

  RaisesIssue: the performance raises an issue (Farkas-Bruce table push; [FB10]).

• loud_not_whispered (u : Perf) : self.Loud u → ¬self.Whispered u

  Loud and whispered performances are mutually exclusive.

• rd_not_commits (u : Perf) : self.RisingDecl u → ¬self.Commits u

  Rising declaratives don't commit ([Rud25b] §4.1, §4.4.1: the load-bearing fact).

• rd_raises_issue (u : Perf) : self.RisingDecl u → self.RaisesIssue u

  Rising declaratives raise issues (rising intonation flags openness; the issue-raising side of the RESP property).

• rd_is_lingmat (u : Perf) : self.RisingDecl u → self.LINGMAT u

  Rising declaratives are linguistic material.

def Semantics.Quotation.Demonstration.PerformanceOntology.RESP {Perf : Type u_1} (Ω : PerformanceOntology Perf) (u : Perf) : Prop

RESP (response-eliciting): the performance raises an issue without committing to its resolution. ([Rud25b] §4.4.1, eq. for the property characterizing ASK-quotative performances.)

Equations

• Ω.RESP u = (Ω.RaisesIssue u ∧ ¬Ω.Commits u)

theorem Semantics.Quotation.Demonstration.PerformanceOntology.rd_is_resp {Perf : Type u_1} (Ω : PerformanceOntology Perf) (u : Perf) : Ω.RisingDecl u → Ω.RESP u

Rising declaratives are RESP. Follows from rd_raises_issue and rd_not_commits.

structure Semantics.Quotation.Demonstration.SpeechVerbs (Time : Type u_1) (SemObj : Type u_2) (Perf : Type u_3) [LinearOrder Time] (Ω : PerformanceOntology Perf) : Type (max (max u_1 u_2) u_3)

A model of verbs of speech and their thematic complements, parameterized over a performance ontology Ω.

Bundles:

• Verb predicates (1-place predicates of events): SAY, ASSERT, ASK, YELL, WHISPER
• Event relations: CONTENT (event to semantic object) and REENACT (event to performance)
• Sortal predicates on semantic objects: isProposition, isQuestion
• Meaning postulates as fields, connecting the verbs to Ω

Each meaning postulate carries an annotation indicating whether it is explicit in [Rud25b] or an extrapolation (formal rendering of an informal generalization in the paper).

• SAY : Event Time → Prop

  say: linguistic-material producing event

• ASSERT : Event Time → Prop

  assert: SAY + commitment

• ASK : Event Time → Prop

  ask: REENACT pole forces RESP performances

• YELL : Event Time → Prop

  yell: SAY + loud performance

• WHISPER : Event Time → Prop

  whisper: SAY + whispered performance

• CONTENT : ArgumentStructure.EventRel Time SemObj

  CONTENT: event-to-content (proposition or question denotation)

• REENACT : ArgumentStructure.EventRel Time Perf

  REENACT: event-to-performance ([Rud25b] §3.2).

• isProposition : SemObj → Prop

  The semantic object is a proposition.

• isQuestion : SemObj → Prop

  The semantic object is a question denotation.

• say_iff_lingmat (e : Event Time) : self.SAY e ↔ ∀ (u : Perf), self.REENACT e u → Ω.LINGMAT u

  Explicit in [Rud25b] (§3.3.4): SAY-events ↔ all reenacted performances are linguistic material.

• ask_iff_resp (e : Event Time) : self.ASK e ↔ ∀ (u : Perf), self.REENACT e u → Ω.RESP u

  Explicit in [Rud25b] (§4.4.1): ASK-events ↔ all reenacted performances are response-eliciting (raise an issue without committing). Crucial: this is not merely the absence of commitment — it also requires issue-raising, which is what makes rising declaratives (a RESP performance) a felicitous ASK complement while a silent grunt (no issue raised) would not be.

• assert_iff_say_and_commits (e : Event Time) : self.ASSERT e ↔ self.SAY e ∧ ∀ (u : Perf), self.REENACT e u → Ω.Commits u

  Extrapolation of the informal generalization in [Rud25b] (§4.5: assert requires speaker commitment). The paper does not provide a formal postulate; this is the natural rendering.

• yell_iff_say_and_loud (e : Event Time) : self.YELL e ↔ self.SAY e ∧ ∀ (u : Perf), self.REENACT e u → Ω.Loud u

  Extrapolation of the informal generalization in [Rud25b] (§3.3.6, §4.7: yell requires loud performances).

• whisper_iff_say_and_whispered (e : Event Time) : self.WHISPER e ↔ self.SAY e ∧ ∀ (u : Perf), self.REENACT e u → Ω.Whispered u

  Extrapolation dual to yell_iff_say_and_loud.

• content_say_propositional (e : Event Time) (δ : SemObj) : self.SAY e → self.CONTENT e δ → self.isProposition δ

  Explicit in [Rud25b] (§3.3.4): sortal restriction on SAY's CONTENT — propositional content of a SAY-event must be a proposition.

• content_ask_question (e : Event Time) (δ : SemObj) : self.ASK e → self.CONTENT e δ → self.isQuestion δ

  Explicit in [Rud25b] (§4.3): sortal restriction on ASK's CONTENT — propositional content of an ASK-event must be a question.

• prop_not_question (δ : SemObj) : self.isProposition δ → ¬self.isQuestion δ

  Sortal disjointness: a semantic object is not simultaneously a proposition and a question. Used to derive *say that <question>* infelicity from the SAY/ASK content sortal restrictions.

def Semantics.Quotation.Demonstration.SpeechVerbs.thatComp {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (V : Event Time → Prop) (p : SemObj) (e : Event Time) : Prop

Propositional complement composition: V that p asserts a CONTENT relation between the verb-event and the propositional denotation.

Equations

• M.thatComp V p e = (V e ∧ M.CONTENT e p)

def Semantics.Quotation.Demonstration.SpeechVerbs.quoteComp {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (V : Event Time → Prop) (u : Perf) (e : Event Time) : Prop

Quotative complement composition: V "u" asserts a REENACT relation between the verb-event and the cotemporaneous performance u (the referent of covert pthat; [Rud25b] §3).

Equations

• M.quoteComp V u e = (V e ∧ M.REENACT e u)

def Semantics.Quotation.Demonstration.SpeechVerbs.quoteCompEx {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (V : Event Time → Prop) (P : Perf → Prop) (e : Event Time) : Prop

Quotative composition existentially closed over the performance. This is what shows up in actual sentence meanings: at the sentence level the performance is introduced as an existential when QUOTE attaches, then constrained by descriptive content (a proposition over performances, e.g., "this rising-declarative tokening of Aaron likes apples?").

Equations

• M.quoteCompEx V P e = (V e ∧ ∃ (u : Perf), M.REENACT e u ∧ P u)

theorem Semantics.Quotation.Demonstration.SpeechVerbs.say_quote_lingmat {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) (u : Perf) : M.quoteComp M.SAY u e → Ω.LINGMAT u

Prediction: a say event with REENACT to u requires u to be linguistic material. (Rules out #Sara said {grunt} in the absence of LINGMAT.)

theorem Semantics.Quotation.Demonstration.SpeechVerbs.assert_quote_rd_empty {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) (u : Perf) : Ω.RisingDecl u → ¬M.quoteComp M.ASSERT u e

Prediction: an assert event with a rising-declarative performance is impossible ([Rud25b] §4.5: #Sara asserted "Aaron likes apples?" with rising intonation).

theorem Semantics.Quotation.Demonstration.SpeechVerbs.ask_quote_rd_consistent {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) (u : Perf) : M.ASK e → M.REENACT e u → Ω.RisingDecl u → Ω.RESP u

Prediction: an ask event with a rising-declarative performance is consistent. The reenacted performance is RESP (rising declaratives raise an issue and don't commit), satisfying ASK's postulate. ([Rud25b] §4.4.1: derives the felicity of Sara asked "Aaron likes apples?".)

theorem Semantics.Quotation.Demonstration.SpeechVerbs.ask_quote_no_issue_empty {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) (u : Perf) : ¬Ω.RaisesIssue u → ¬M.quoteComp M.ASK u e

Prediction: an ask event quoting a non-issue-raising performance is impossible. The ASK postulate requires RESP, which requires RaisesIssue. (Rules out e.g. #Sara asked "Aaron likes apples" with falling, declarative intonation that commits the original speaker rather than raising an open question.)

theorem Semantics.Quotation.Demonstration.SpeechVerbs.yell_quote_loud {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) (u : Perf) : M.quoteComp M.YELL u e → Ω.Loud u

Prediction: a yell event with REENACT to u makes u loud.

theorem Semantics.Quotation.Demonstration.SpeechVerbs.whisper_quote_loud_empty {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) (u : Perf) : Ω.Loud u → ¬M.quoteComp M.WHISPER u e

Prediction: a whisper event with a loud performance is impossible. Loud and whispered are mutually exclusive, but whisper requires whispered performances.

theorem Semantics.Quotation.Demonstration.SpeechVerbs.ask_that_question {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) (δ : SemObj) : M.thatComp M.ASK δ e → M.isQuestion δ

Sortal prediction: an ask-event with propositional CONTENT requires that CONTENT be a question. Combined with disjointness of isProposition and isQuestion in concrete models, this rules out #ask that p with declarative p.

theorem Semantics.Quotation.Demonstration.SpeechVerbs.assert_implies_say {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) : M.ASSERT e → M.SAY e

ASSERT ⊆ SAY: an assertion is a saying. Direct from the postulate.

theorem Semantics.Quotation.Demonstration.SpeechVerbs.yell_implies_say {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) : M.YELL e → M.SAY e

YELL ⊆ SAY: yelling is a manner-of-saying.

theorem Semantics.Quotation.Demonstration.SpeechVerbs.whisper_implies_say {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) : M.WHISPER e → M.SAY e

WHISPER ⊆ SAY: whispering is a manner-of-saying.

theorem Semantics.Quotation.Demonstration.SpeechVerbs.assert_ask_incompatible_at_perf {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e e' : Event Time) (u : Perf) : M.ASSERT e → M.REENACT e u → M.ASK e' → M.REENACT e' u → False

ASSERT and ASK are incompatible at a single performance: ASSERT forces commitment, ASK forces non-commitment. (Captures the say/ask polar split — Sara said "p" may overlap with Sara asked "p?" via different performances, but a single performance can satisfy at most one.)

theorem Semantics.Quotation.Demonstration.SpeechVerbs.say_non_lingmat_impossible {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : PerformanceOntology Perf} (M : SpeechVerbs Time SemObj Perf Ω) (e : Event Time) (u : Perf) : M.SAY e → M.REENACT e u → ¬Ω.LINGMAT u → False

karate gestures contradiction (motivation for LINGMAT in [Rud25b]): a SAY-event whose REENACTed performance is not linguistic material is impossible. The postulate enforces LINGMAT, so a non-LINGMAT witness gives an immediate contradiction.

Farkas-Bruce Performance Ontology Bridge

[Rud25b] [FB10]

Provides a PerformanceOntology instance whose Commits and RaisesIssue are derived from Farkas-Bruce discourse-state updates, rather than stipulated as primitive properties.

The Bridge

A performance in F&B terms is a discourse-state update determined by its sentence form (declarative/interrogative), its propositional content, and its prosodic profile (rising or not, loud/whispered/ neutral). The FBPerformance record bundles exactly the data needed to compute its discourse effect:

• a non-rising declarative asserts its content (adds to dcS, pushes issue)
• an interrogative polarQuestions its content (pushes issue, no dcS commit)
• a rising declarative pushes its content as an issue (no dcS commit) — the intermediate prosodic case that drives [Rud25b]'s empirical engine

Commits and RaisesIssue are then F&B-grounded predicates: a performance Commits iff its update adds its content to dcS; it RaisesIssue iff its update grows the table. Verb-class meaning postulates in SpeechVerbs see the same Commits / RaisesIssue that the F&B bridge theorems (in Discourse/Commitment/Table.lean) reason about — the connection is true by construction, not provable as an equivalence.

Why this matters

Without the bridge, Commits is an axiomatic property of performances in PerformanceOntology — we'd have to say that rising declaratives don't commit. With the bridge, the F&B update semantics makes them not commit (the update doesn't touch dcS), and the Demonstration postulates inherit that fact directly.

Anti-correspondences

A FBPerformance whose lingmat field is false and rising is false represents a non-linguistic performance (e.g., karate gestures). We choose LingMat to disjoin lingmat = true ∨ rising = true so that every rising-declarative performance is automatically linguistic material — a structural rather than axiomatic fact.

The Volume enumeration (neutral, loud, whispered) makes loud_not_whispered true by construction: a single field cannot simultaneously be both values.

inductive Discourse.QuotationFBOntology.Volume : Type

Volume profile of a performance. The 3-way enumeration ensures that Loud and Whispered are mutually exclusive by construction.

• neutral : Volume
• loud : Volume
• whispered : Volume

@[instance_reducible]

instance Discourse.QuotationFBOntology.instDecidableEqVolume : DecidableEq Volume

Equations

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

def Discourse.QuotationFBOntology.instReprVolume.repr : Volume → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Discourse.QuotationFBOntology.instReprVolume : Repr Volume

Equations

• Discourse.QuotationFBOntology.instReprVolume = { reprPrec := Discourse.QuotationFBOntology.instReprVolume.repr }

@[instance_reducible]

instance Discourse.QuotationFBOntology.instInhabitedVolume : Inhabited Volume

Equations

• Discourse.QuotationFBOntology.instInhabitedVolume = { default := Discourse.QuotationFBOntology.instInhabitedVolume.default }

structure Discourse.QuotationFBOntology.FBPerformance (W : Type u_1) : Type u_1

A Farkas-Bruce performance: minimal data to compute its discourse update.

• form : Mood.Illocutionary

  Sentence form (declarative / interrogative).

• content : Set W

  Propositional content.

• lingmat : Bool

  Whether the performance is linguistic material. False allows modeling non-linguistic gestures (the karate-gestures contrast that motivates LINGMAT).

• volume : Volume

  Volume profile.

• rising : Bool

  Rising-declarative intonation (only meaningful with declarative form, but field is independent for simplicity).

def Discourse.QuotationFBOntology.FBPerformance.update {W : Type u_1} (u : FBPerformance W) (s : Commitment.Table.State W) : Commitment.Table.State W

The F&B-grounded discourse update for the performance.

• non-rising declarative: assert (commits + pushes issue)
• interrogative: polarQuestion (pushes issue, no commit)
• rising declarative: pushes issue without commit (the intermediate prosodic case [Rud25b] relies on)

Equations

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

def Discourse.QuotationFBOntology.FBPerformance.LingMat {W : Type u_1} (u : FBPerformance W) : Prop

Linguistic-material. Disjoins explicit lingmat = true with rising = true: a rising-declarative performance is linguistic material by virtue of being a structured intonation pattern.

Equations

• u.LingMat = (u.lingmat = true ∨ u.rising = true)

def Discourse.QuotationFBOntology.FBPerformance.Loud {W : Type u_1} (u : FBPerformance W) : Prop

Loud: structural property of Volume.

Equations

• u.Loud = (u.volume = Discourse.QuotationFBOntology.Volume.loud)

def Discourse.QuotationFBOntology.FBPerformance.Whispered {W : Type u_1} (u : FBPerformance W) : Prop

Whispered: structural property of Volume.

Equations

• u.Whispered = (u.volume = Discourse.QuotationFBOntology.Volume.whispered)

def Discourse.QuotationFBOntology.FBPerformance.RisingDecl {W : Type u_1} (u : FBPerformance W) : Prop

Rising declarative: rising intonation on declarative form.

Equations

• u.RisingDecl = (u.rising = true ∧ u.form = Mood.Illocutionary.declarative)

def Discourse.QuotationFBOntology.FBPerformance.Commits {W : Type u_1} (u : FBPerformance W) : Prop

F&B-derived Commits: the performance's update adds its content to dcS (computed from the empty initial state). The assert branch adds, the rising and interrogative branches do not — so this matches the structural classification "non-rising declarative".

Equations

• u.Commits = (u.content ∈ Discourse.Commitment.Table.DiscourseState.dcS (u.update Discourse.Commitment.Table.DiscourseState.empty))

def Discourse.QuotationFBOntology.FBPerformance.RaisesIssue {W : Type u_1} (u : FBPerformance W) : Prop

F&B-derived RaisesIssue: the performance's update grows the table. All three branches push to the table, so any well-formed speech act raises an issue. (RESP's discriminating power comes from ¬ Commits, not from RaisesIssue.)

Equations

• u.RaisesIssue = ((u.update Discourse.Commitment.Table.DiscourseState.empty).table ≠ [])

theorem Discourse.QuotationFBOntology.FBPerformance.loud_not_whispered {W : Type u_1} (u : FBPerformance W) : u.Loud → ¬u.Whispered

theorem Discourse.QuotationFBOntology.FBPerformance.rd_not_commits {W : Type u_1} (u : FBPerformance W) : u.RisingDecl → ¬u.Commits

theorem Discourse.QuotationFBOntology.FBPerformance.rd_raises_issue {W : Type u_1} (u : FBPerformance W) : u.RisingDecl → u.RaisesIssue

theorem Discourse.QuotationFBOntology.FBPerformance.rd_is_lingmat {W : Type u_1} (u : FBPerformance W) : u.RisingDecl → u.LingMat

def Discourse.QuotationFBOntology.fbOntology (W : Type u_1) : Semantics.Quotation.Demonstration.PerformanceOntology (FBPerformance W)

The Farkas-Bruce-grounded performance ontology. Plug into a SpeechVerbs to get verb-class semantics whose Commits / RaisesIssue facts come from the F&B discourse-state machinery rather than free axioms.

Equations

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

theorem Discourse.QuotationFBOntology.FBPerformance.commits_iff {W : Type u_1} (u : FBPerformance W) : u.Commits ↔ u.rising = false ∧ u.form = Mood.Illocutionary.declarative

Structural characterization of Commits: a performance commits iff it is a non-rising declarative. Derives directly from the F&B update semantics.

theorem Discourse.QuotationFBOntology.FBPerformance.raises_issue_always {W : Type u_1} (u : FBPerformance W) : u.RaisesIssue

Structural characterization of RaisesIssue: every performance raises an issue (declarative or interrogative; rising or non-rising). The discriminating empirical content lives in Commits, not here.

theorem Discourse.QuotationFBOntology.FBPerformance.update_decl_eq_assert {W : Type u_1} (u : FBPerformance W) (hr : u.rising = false) (hf : u.form = Mood.Illocutionary.declarative) (s : Commitment.Table.State W) : u.update s = Commitment.Table.assert s u.content

Bridge: when the performance is a non-rising declarative, its update equals assert s content, so assert_dc_speaker_doxasticContents applies directly.

inductive Rudin2025LI.Verb : Type

Verbs of speech examined by [Rud25b].

• say : Verb
• assert : Verb
• yell : Verb
• whisper : Verb
• ask : Verb

@[instance_reducible]

instance Rudin2025LI.instDecidableEqVerb : DecidableEq Verb

Equations

• Rudin2025LI.instDecidableEqVerb x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Rudin2025LI.instReprVerb : Repr Verb

Equations

• Rudin2025LI.instReprVerb = { reprPrec := Rudin2025LI.instReprVerb.repr }

def Rudin2025LI.instReprVerb.repr : Verb → ℕ → Std.Format

Equations

• Rudin2025LI.instReprVerb.repr Rudin2025LI.Verb.say prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rudin2025LI.Verb.say")).group prec✝
• Rudin2025LI.instReprVerb.repr Rudin2025LI.Verb.assert prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rudin2025LI.Verb.assert")).group prec✝
• Rudin2025LI.instReprVerb.repr Rudin2025LI.Verb.yell prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rudin2025LI.Verb.yell")).group prec✝
• Rudin2025LI.instReprVerb.repr Rudin2025LI.Verb.whisper prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rudin2025LI.Verb.whisper")).group prec✝
• Rudin2025LI.instReprVerb.repr Rudin2025LI.Verb.ask prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Rudin2025LI.Verb.ask")).group prec✝

@[instance_reducible]

instance Rudin2025LI.instInhabitedVerb : Inhabited Verb

Equations

• Rudin2025LI.instInhabitedVerb = { default := Rudin2025LI.instInhabitedVerb.default }

inductive Rudin2025LI.Complement : Type

Complement types in the Rudin matrix.

• quoteDecl : Complement
• quoteRising : Complement
• quoteLoud : Complement
• quoteWhispered : Complement
• thatProp : Complement
• thatQuestion : Complement

@[instance_reducible]

instance Rudin2025LI.instDecidableEqComplement : DecidableEq Complement

Equations

• Rudin2025LI.instDecidableEqComplement x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Rudin2025LI.instReprComplement : Repr Complement

Equations

• Rudin2025LI.instReprComplement = { reprPrec := Rudin2025LI.instReprComplement.repr }

def Rudin2025LI.instReprComplement.repr : Complement → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Rudin2025LI.instInhabitedComplement : Inhabited Complement

Equations

• Rudin2025LI.instInhabitedComplement = { default := Rudin2025LI.instInhabitedComplement.default }

def Rudin2025LI.Verb.toPred {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : Semantics.Quotation.Demonstration.PerformanceOntology Perf} (M : Semantics.Quotation.Demonstration.SpeechVerbs Time SemObj Perf Ω) : Verb → Event Time → Prop

Selector: map a Verb enum to the corresponding model predicate.

Equations

• Rudin2025LI.Verb.toPred M Rudin2025LI.Verb.say = M.SAY
• Rudin2025LI.Verb.toPred M Rudin2025LI.Verb.assert = M.ASSERT
• Rudin2025LI.Verb.toPred M Rudin2025LI.Verb.yell = M.YELL
• Rudin2025LI.Verb.toPred M Rudin2025LI.Verb.whisper = M.WHISPER
• Rudin2025LI.Verb.toPred M Rudin2025LI.Verb.ask = M.ASK

def Rudin2025LI.Felicitous {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : Semantics.Quotation.Demonstration.PerformanceOntology Perf} (M : Semantics.Quotation.Demonstration.SpeechVerbs Time SemObj Perf Ω) (V : Event Time → Prop) : Complement → Prop

A complement is felicitous with a verb predicate in a given model iff there exists a witness — an event-and-performance pair (for quotative complements) or an event-and-content pair (for that-clauses) — satisfying the ontological constraints encoded by the complement type.

Quotative complements constrain the REENACTed performance: quoteDecl requires a committing linguistic performance, quoteRising a rising declarative, quoteLoud/quoteWhispered a committing performance with the marked volume.

Propositional complements constrain the CONTENT denotation: thatProp requires propositional content, thatQuestion requires question content.

Verb-class felicity is then derived: a verb's postulates impose constraints on REENACTed performances (or CONTENT denotations); if those constraints conflict with the complement's, no witness exists and the cell is infelicitous.

Equations

• Rudin2025LI.Felicitous M V Rudin2025LI.Complement.quoteDecl = ∃ (e : Event Time) (u : Perf), V e ∧ M.REENACT e u ∧ Ω.LINGMAT u ∧ Ω.Commits u
• Rudin2025LI.Felicitous M V Rudin2025LI.Complement.quoteRising = ∃ (e : Event Time) (u : Perf), V e ∧ M.REENACT e u ∧ Ω.RisingDecl u
• Rudin2025LI.Felicitous M V Rudin2025LI.Complement.quoteLoud = ∃ (e : Event Time) (u : Perf), V e ∧ M.REENACT e u ∧ Ω.LINGMAT u ∧ Ω.Commits u ∧ Ω.Loud u
• Rudin2025LI.Felicitous M V Rudin2025LI.Complement.quoteWhispered = ∃ (e : Event Time) (u : Perf), V e ∧ M.REENACT e u ∧ Ω.LINGMAT u ∧ Ω.Commits u ∧ Ω.Whispered u
• Rudin2025LI.Felicitous M V Rudin2025LI.Complement.thatProp = ∃ (e : Event Time) (p : SemObj), V e ∧ M.CONTENT e p ∧ M.isProposition p
• Rudin2025LI.Felicitous M V Rudin2025LI.Complement.thatQuestion = ∃ (e : Event Time) (q : SemObj), V e ∧ M.CONTENT e q ∧ M.isQuestion q

class Rudin2025LI.IsRudinModel {Time : Type u_1} {SemObj : Type u_2} {Perf : Type u_3} [LinearOrder Time] {Ω : Semantics.Quotation.Demonstration.PerformanceOntology Perf} (M : Semantics.Quotation.Demonstration.SpeechVerbs Time SemObj Perf Ω) : Prop

A SpeechVerbs model satisfies [Rud25b]'s empirical claims about English speech verbs. The 30 fields are exactly the cells of the verb × complement felicity matrix.

This class IS the empirical claim. There is no separate empirical function whose values must be reconciled with model predictions — a model satisfies these facts or it does not.

• say_quoteDecl : Felicitous M M.SAY Complement.quoteDecl
• say_quoteRising : Felicitous M M.SAY Complement.quoteRising
• say_quoteLoud : Felicitous M M.SAY Complement.quoteLoud
• say_quoteWhispered : Felicitous M M.SAY Complement.quoteWhispered
• say_thatProp : Felicitous M M.SAY Complement.thatProp
• say_thatQuestion : ¬Felicitous M M.SAY Complement.thatQuestion
• assert_quoteDecl : Felicitous M M.ASSERT Complement.quoteDecl
• assert_quoteRising : ¬Felicitous M M.ASSERT Complement.quoteRising
• assert_quoteLoud : Felicitous M M.ASSERT Complement.quoteLoud
• assert_quoteWhispered : Felicitous M M.ASSERT Complement.quoteWhispered
• assert_thatProp : Felicitous M M.ASSERT Complement.thatProp
• assert_thatQuestion : ¬Felicitous M M.ASSERT Complement.thatQuestion
• yell_quoteDecl : Felicitous M M.YELL Complement.quoteDecl
• yell_quoteRising : Felicitous M M.YELL Complement.quoteRising
• yell_quoteLoud : Felicitous M M.YELL Complement.quoteLoud
• yell_quoteWhispered : ¬Felicitous M M.YELL Complement.quoteWhispered
• yell_thatProp : Felicitous M M.YELL Complement.thatProp
• yell_thatQuestion : ¬Felicitous M M.YELL Complement.thatQuestion
• whisper_quoteDecl : Felicitous M M.WHISPER Complement.quoteDecl
• whisper_quoteRising : Felicitous M M.WHISPER Complement.quoteRising
• whisper_quoteLoud : ¬Felicitous M M.WHISPER Complement.quoteLoud
• whisper_quoteWhispered : Felicitous M M.WHISPER Complement.quoteWhispered
• whisper_thatProp : Felicitous M M.WHISPER Complement.thatProp
• whisper_thatQuestion : ¬Felicitous M M.WHISPER Complement.thatQuestion
• ask_quoteDecl : ¬Felicitous M M.ASK Complement.quoteDecl
• ask_quoteRising : Felicitous M M.ASK Complement.quoteRising
• ask_quoteLoud : ¬Felicitous M M.ASK Complement.quoteLoud
• ask_quoteWhispered : ¬Felicitous M M.ASK Complement.quoteWhispered
• ask_thatProp : ¬Felicitous M M.ASK Complement.thatProp
• ask_thatQuestion : Felicitous M M.ASK Complement.thatQuestion

We now build a concrete SpeechVerbs model over FBPerformance Bool with fbOntology as its performance ontology, and show it satisfies IsRudinModel. The model uses ℕ as the time type and Bool as the semantic-object type (true ↦ proposition, false ↦ question).

Verb predicates are defined as the postulate RHS, so the meaning postulates hold by rfl. The discriminator for verb classes is runtime.start (0 = SAY, 1 = ASSERT, 2 = YELL, 3 = WHISPER, 4 = ASK). REENACT and CONTENT are defined per verb class to give the right witnesses and exclusions.

def Rudin2025LI.E (n : ℕ) : Event ℕ

A canonical event for each verb class, indexed by runtime.start.

Equations

• Rudin2025LI.E n = { runtime := { fst := n, snd := n, fst_le_snd := ⋯ }, sort := Features.Dynamicity.dynamic }

def Rudin2025LI.rudinReenact (e : Event ℕ) (u : Discourse.QuotationFBOntology.FBPerformance Bool) : Prop

The REENACT relation: per verb-class events have different REENACT targets, chosen so the postulates' universal quantifiers reduce to obvious tautologies (e.g., for SAY events, REENACT only relates to LINGMAT performances, so SAY's postulate ∀u, REENACT → LINGMAT is vacuously true).

Equations

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

def Rudin2025LI.rudinContent (e : Event ℕ) (b : Bool) : Prop

The CONTENT relation: SAY-class events take propositional (true) content; ASK-class events take question (false) content; other events have no propositional content.

Equations

• Rudin2025LI.rudinContent e b = match e.runtime.toProd.1 with | 0 => b = true | 1 => b = true | 2 => b = true | 3 => b = true | 4 => b = false | x => False

def Rudin2025LI.rudinSay (e : Event ℕ) : Prop

Verb predicates: defined as the postulate RHS so the iff-axioms hold by rfl.

Equations

• Rudin2025LI.rudinSay e = ∀ (u : Discourse.QuotationFBOntology.FBPerformance Bool), Rudin2025LI.rudinReenact e u → (Discourse.QuotationFBOntology.fbOntology Bool).LINGMAT u

def Rudin2025LI.rudinAssert (e : Event ℕ) : Prop

Equations

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

def Rudin2025LI.rudinAsk (e : Event ℕ) : Prop

Equations

• Rudin2025LI.rudinAsk e = ∀ (u : Discourse.QuotationFBOntology.FBPerformance Bool), Rudin2025LI.rudinReenact e u → (Discourse.QuotationFBOntology.fbOntology Bool).RESP u

def Rudin2025LI.rudinYell (e : Event ℕ) : Prop

Equations

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

def Rudin2025LI.rudinWhisper (e : Event ℕ) : Prop

Equations

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

def Rudin2025LI.respNonLingmat : Discourse.QuotationFBOntology.FBPerformance Bool

A non-LINGMAT RESP performance: a non-linguistic, non-rising interrogative (e.g., a wordless interrogative gesture). Its update is polarQuestion, which pushes an issue without committing. Used to falsify SAY for ASK-class events.

Equations

• Rudin2025LI.respNonLingmat = { form := Mood.Illocutionary.interrogative, content := fun (x : Bool) => true = true, lingmat := false }

theorem Rudin2025LI.respNonLingmat_resp : (Discourse.QuotationFBOntology.fbOntology Bool).RESP respNonLingmat

theorem Rudin2025LI.respNonLingmat_not_lingmat : ¬(Discourse.QuotationFBOntology.fbOntology Bool).LINGMAT respNonLingmat

Witness performances

Concrete FBPerformance witnesses with named property proofs. Each witness pins down the exact field configuration that makes a particular cell of the matrix felicitous, and is referenced both in rudinModel's postulate proofs and in the IsRudinModel instance discharge.

def Rudin2025LI.committingDecl : Discourse.QuotationFBOntology.FBPerformance Bool

A neutral committing declarative performance.

Equations

• Rudin2025LI.committingDecl = { form := Mood.Illocutionary.declarative, content := fun (x : Bool) => true = true }

theorem Rudin2025LI.committingDecl_lingmat : (Discourse.QuotationFBOntology.fbOntology Bool).LINGMAT committingDecl

theorem Rudin2025LI.committingDecl_commits : (Discourse.QuotationFBOntology.fbOntology Bool).Commits committingDecl

def Rudin2025LI.committingLoud : Discourse.QuotationFBOntology.FBPerformance Bool

A loud committing declarative performance.

Equations

• Rudin2025LI.committingLoud = { form := Mood.Illocutionary.declarative, content := fun (x : Bool) => true = true, volume := Discourse.QuotationFBOntology.Volume.loud }

theorem Rudin2025LI.committingLoud_lingmat : (Discourse.QuotationFBOntology.fbOntology Bool).LINGMAT committingLoud

theorem Rudin2025LI.committingLoud_loud : (Discourse.QuotationFBOntology.fbOntology Bool).Loud committingLoud

theorem Rudin2025LI.committingLoud_commits : (Discourse.QuotationFBOntology.fbOntology Bool).Commits committingLoud

def Rudin2025LI.committingWhispered : Discourse.QuotationFBOntology.FBPerformance Bool

A whispered committing declarative performance.

Equations

• Rudin2025LI.committingWhispered = { form := Mood.Illocutionary.declarative, content := fun (x : Bool) => true = true, volume := Discourse.QuotationFBOntology.Volume.whispered }

theorem Rudin2025LI.committingWhispered_lingmat : (Discourse.QuotationFBOntology.fbOntology Bool).LINGMAT committingWhispered

theorem Rudin2025LI.committingWhispered_whispered : (Discourse.QuotationFBOntology.fbOntology Bool).Whispered committingWhispered

theorem Rudin2025LI.committingWhispered_commits : (Discourse.QuotationFBOntology.fbOntology Bool).Commits committingWhispered

def Rudin2025LI.risingDecl : Discourse.QuotationFBOntology.FBPerformance Bool

A rising-declarative performance (RESP, not committing).

Equations

• Rudin2025LI.risingDecl = { form := Mood.Illocutionary.declarative, content := fun (x : Bool) => true = true, rising := true }

theorem Rudin2025LI.risingDecl_rd : (Discourse.QuotationFBOntology.fbOntology Bool).RisingDecl risingDecl

theorem Rudin2025LI.risingDecl_resp : (Discourse.QuotationFBOntology.fbOntology Bool).RESP risingDecl

def Rudin2025LI.risingLoud : Discourse.QuotationFBOntology.FBPerformance Bool

A loud rising-declarative performance.

Equations

• Rudin2025LI.risingLoud = { form := Mood.Illocutionary.declarative, content := fun (x : Bool) => true = true, volume := Discourse.QuotationFBOntology.Volume.loud, rising := true }

theorem Rudin2025LI.risingLoud_rd : (Discourse.QuotationFBOntology.fbOntology Bool).RisingDecl risingLoud

theorem Rudin2025LI.risingLoud_lingmat : (Discourse.QuotationFBOntology.fbOntology Bool).LINGMAT risingLoud

theorem Rudin2025LI.risingLoud_loud : (Discourse.QuotationFBOntology.fbOntology Bool).Loud risingLoud

def Rudin2025LI.risingWhispered : Discourse.QuotationFBOntology.FBPerformance Bool

A whispered rising-declarative performance.

Equations

• Rudin2025LI.risingWhispered = { form := Mood.Illocutionary.declarative, content := fun (x : Bool) => true = true, volume := Discourse.QuotationFBOntology.Volume.whispered, rising := true }

theorem Rudin2025LI.risingWhispered_rd : (Discourse.QuotationFBOntology.fbOntology Bool).RisingDecl risingWhispered

theorem Rudin2025LI.risingWhispered_whispered : (Discourse.QuotationFBOntology.fbOntology Bool).Whispered risingWhispered

def Rudin2025LI.rudinModel : Semantics.Quotation.Demonstration.SpeechVerbs ℕ Bool (Discourse.QuotationFBOntology.FBPerformance Bool) (Discourse.QuotationFBOntology.fbOntology Bool)

The Rudin model: a concrete SpeechVerbs instantiation over FBPerformance Bool with fbOntology as its performance ontology. Each meaning postulate holds by rfl since the verb predicates are defined as the postulate RHS.

Equations

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

instance Rudin2025LI.instIsRudinModelNatBoolFBPerformanceRudinModel : IsRudinModel rudinModel

All 30 cells of [Rud25b]'s empirical matrix are derived from the FB-grounded model + the SpeechVerbs postulates.

def Rudin2025LI.fromEnglishVerb (v : English.Predicates.Verbal.VerbEntry) : Option Verb

Classify an English VerbEntry into the Rudin verb taxonomy. Returns none for verbs that don't fall into the matrix (e.g., tell requires a recipient; think is not a speech act).

Reads directly off Fragment fields — speechActVerb, takesQuestionBase, levinClass, and surface form — so the classification stays in sync with Fragment edits.

Equations

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

Per-entry classification witnesses

These examples pin individual Fragment verbs to the Rudin taxonomy. Renaming or reclassifying any of these verbs in the Fragment will break exactly the relevant witness, surfacing the inconsistency.

Negative cases — verbs outside the Rudin matrix