@cite{rudin-2025b}: 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 @cite{rudin-2025b}'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.

inductive Phenomena.Quotation.Studies.Rudin2025LI.Verb : Type

Verbs of speech examined by @cite{rudin-2025b}.

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

@[implicit_reducible]

instance Phenomena.Quotation.Studies.Rudin2025LI.instDecidableEqVerb : DecidableEq Verb

Equations

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

@[implicit_reducible]

instance Phenomena.Quotation.Studies.Rudin2025LI.instReprVerb : Repr Verb

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.instReprVerb = { reprPrec := Phenomena.Quotation.Studies.Rudin2025LI.instReprVerb.repr }

def Phenomena.Quotation.Studies.Rudin2025LI.instReprVerb.repr : Verb → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedVerb : Inhabited Verb

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedVerb = { default := Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedVerb.default }

def Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedVerb.default : Verb

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedVerb.default = Phenomena.Quotation.Studies.Rudin2025LI.Verb.say

inductive Phenomena.Quotation.Studies.Rudin2025LI.Complement : Type

Complement types in the Rudin matrix.

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

@[implicit_reducible]

instance Phenomena.Quotation.Studies.Rudin2025LI.instDecidableEqComplement : DecidableEq Complement

Equations

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

@[implicit_reducible]

instance Phenomena.Quotation.Studies.Rudin2025LI.instReprComplement : Repr Complement

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.instReprComplement = { reprPrec := Phenomena.Quotation.Studies.Rudin2025LI.instReprComplement.repr }

def Phenomena.Quotation.Studies.Rudin2025LI.instReprComplement.repr : Complement → ℕ → Std.Format

Equations

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

def Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedComplement.default : Complement

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedComplement.default = Phenomena.Quotation.Studies.Rudin2025LI.Complement.quoteDecl

@[implicit_reducible]

instance Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedComplement : Inhabited Complement

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedComplement = { default := Phenomena.Quotation.Studies.Rudin2025LI.instInhabitedComplement.default }

def Phenomena.Quotation.Studies.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 → Semantics.Events.Event Time → Prop

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

Equations

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

def Phenomena.Quotation.Studies.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 : Semantics.Events.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

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

class Phenomena.Quotation.Studies.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 @cite{rudin-2025b}'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 Phenomena.Quotation.Studies.Rudin2025LI.E (n : ℕ) : Semantics.Events.Event ℕ

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

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.E n = { runtime := { start := n, finish := n, valid := ⋯ }, sort := Semantics.Events.EventSort.action }

def Phenomena.Quotation.Studies.Rudin2025LI.rudinReenact (e : Semantics.Events.Event ℕ) (u : Dialogue.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 Phenomena.Quotation.Studies.Rudin2025LI.rudinContent (e : Semantics.Events.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

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

def Phenomena.Quotation.Studies.Rudin2025LI.rudinSay (e : Semantics.Events.Event ℕ) : Prop

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

Equations

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

def Phenomena.Quotation.Studies.Rudin2025LI.rudinAssert (e : Semantics.Events.Event ℕ) : Prop

Equations

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

def Phenomena.Quotation.Studies.Rudin2025LI.rudinAsk (e : Semantics.Events.Event ℕ) : Prop

Equations

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

def Phenomena.Quotation.Studies.Rudin2025LI.rudinYell (e : Semantics.Events.Event ℕ) : Prop

Equations

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

def Phenomena.Quotation.Studies.Rudin2025LI.rudinWhisper (e : Semantics.Events.Event ℕ) : Prop

Equations

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

def Phenomena.Quotation.Studies.Rudin2025LI.respNonLingmat : Dialogue.QuotationFBOntology.FBPerformance Bool

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

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.respNonLingmat = { form := Dialogue.FarkasBruce.SentenceForm.interrogative, content := fun (x : Bool) => true = true, lingmat := false }

theorem Phenomena.Quotation.Studies.Rudin2025LI.respNonLingmat_resp : (Dialogue.QuotationFBOntology.fbOntology Bool).RESP respNonLingmat

theorem Phenomena.Quotation.Studies.Rudin2025LI.respNonLingmat_not_lingmat : ¬(Dialogue.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 Phenomena.Quotation.Studies.Rudin2025LI.committingDecl : Dialogue.QuotationFBOntology.FBPerformance Bool

A neutral committing declarative performance.

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.committingDecl = { form := Dialogue.FarkasBruce.SentenceForm.declarative, content := fun (x : Bool) => true = true }

theorem Phenomena.Quotation.Studies.Rudin2025LI.committingDecl_lingmat : (Dialogue.QuotationFBOntology.fbOntology Bool).LINGMAT committingDecl

theorem Phenomena.Quotation.Studies.Rudin2025LI.committingDecl_commits : (Dialogue.QuotationFBOntology.fbOntology Bool).Commits committingDecl

def Phenomena.Quotation.Studies.Rudin2025LI.committingLoud : Dialogue.QuotationFBOntology.FBPerformance Bool

A loud committing declarative performance.

Equations

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

theorem Phenomena.Quotation.Studies.Rudin2025LI.committingLoud_lingmat : (Dialogue.QuotationFBOntology.fbOntology Bool).LINGMAT committingLoud

theorem Phenomena.Quotation.Studies.Rudin2025LI.committingLoud_loud : (Dialogue.QuotationFBOntology.fbOntology Bool).Loud committingLoud

theorem Phenomena.Quotation.Studies.Rudin2025LI.committingLoud_commits : (Dialogue.QuotationFBOntology.fbOntology Bool).Commits committingLoud

def Phenomena.Quotation.Studies.Rudin2025LI.committingWhispered : Dialogue.QuotationFBOntology.FBPerformance Bool

A whispered committing declarative performance.

Equations

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

theorem Phenomena.Quotation.Studies.Rudin2025LI.committingWhispered_lingmat : (Dialogue.QuotationFBOntology.fbOntology Bool).LINGMAT committingWhispered

theorem Phenomena.Quotation.Studies.Rudin2025LI.committingWhispered_whispered : (Dialogue.QuotationFBOntology.fbOntology Bool).Whispered committingWhispered

theorem Phenomena.Quotation.Studies.Rudin2025LI.committingWhispered_commits : (Dialogue.QuotationFBOntology.fbOntology Bool).Commits committingWhispered

def Phenomena.Quotation.Studies.Rudin2025LI.risingDecl : Dialogue.QuotationFBOntology.FBPerformance Bool

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

Equations

• Phenomena.Quotation.Studies.Rudin2025LI.risingDecl = { form := Dialogue.FarkasBruce.SentenceForm.declarative, content := fun (x : Bool) => true = true, rising := true }

theorem Phenomena.Quotation.Studies.Rudin2025LI.risingDecl_rd : (Dialogue.QuotationFBOntology.fbOntology Bool).RisingDecl risingDecl

theorem Phenomena.Quotation.Studies.Rudin2025LI.risingDecl_resp : (Dialogue.QuotationFBOntology.fbOntology Bool).RESP risingDecl

def Phenomena.Quotation.Studies.Rudin2025LI.risingLoud : Dialogue.QuotationFBOntology.FBPerformance Bool

A loud rising-declarative performance.

Equations

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

theorem Phenomena.Quotation.Studies.Rudin2025LI.risingLoud_rd : (Dialogue.QuotationFBOntology.fbOntology Bool).RisingDecl risingLoud

theorem Phenomena.Quotation.Studies.Rudin2025LI.risingLoud_lingmat : (Dialogue.QuotationFBOntology.fbOntology Bool).LINGMAT risingLoud

theorem Phenomena.Quotation.Studies.Rudin2025LI.risingLoud_loud : (Dialogue.QuotationFBOntology.fbOntology Bool).Loud risingLoud

def Phenomena.Quotation.Studies.Rudin2025LI.risingWhispered : Dialogue.QuotationFBOntology.FBPerformance Bool

A whispered rising-declarative performance.

Equations

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

theorem Phenomena.Quotation.Studies.Rudin2025LI.risingWhispered_rd : (Dialogue.QuotationFBOntology.fbOntology Bool).RisingDecl risingWhispered

theorem Phenomena.Quotation.Studies.Rudin2025LI.risingWhispered_whispered : (Dialogue.QuotationFBOntology.fbOntology Bool).Whispered risingWhispered

def Phenomena.Quotation.Studies.Rudin2025LI.rudinModel : Semantics.Quotation.Demonstration.SpeechVerbs ℕ Bool (Dialogue.QuotationFBOntology.FBPerformance Bool) (Dialogue.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 Phenomena.Quotation.Studies.Rudin2025LI.instIsRudinModelNatBoolFBPerformanceRudinModel : IsRudinModel rudinModel

All 30 cells of @cite{rudin-2025b}'s empirical matrix are derived from the FB-grounded model + the SpeechVerbs postulates.

def Phenomena.Quotation.Studies.Rudin2025LI.fromEnglishVerb (v : Fragments.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