Rudin (2025): Embedded Intonation and Quotative Complements to Verbs of Speech

Rudin gives a double-Davidsonian semantics for quotative complements to verbs of speech and applies it to embedded rising declaratives. A quotation is a performance that the report refers to demonstratively, and the quotative complementizer relates it to the speech event by reenactment, so Ayka said "p" denotes the saying events that the performance reenacts. A verb of speech is fixed by a meaning postulate over reenactments, so quoting a performance under a verb is contradictory exactly when the performance lacks the verb's property: karate gestures under say, a whisper under yell, a rising declarative under assert. A rising declarative under ask is consistent, because its utterance raises an issue without a commitment that could resolve it, an asking in Farkas and Bruce's Table model, so embedded rising declaratives are no evidence that rising declaratives denote questions.

Main definitions

• speechVerb: a verb of speech under the paper's meaning-postulate template.
• quoteReport: a quotative speech report.
• Performance.Asking: a performance that raises an issue without commitment.

Main results

• exists_reenact_iff: a quotative report is satisfiable exactly when the performance has the verb's property.
• Performance.asking_iff: an asking is a rising declarative or an interrogative.
• ask_risingDeclarative: a rising declarative under ask is satisfiable.
• judgments: the paper's quotative judgments.

Implementation notes

Reenactment is a relation from events to performances, and the model is left free: a quotative report is consistent when some reenactment relation makes it true. A performance is its linguistic material, none for karate gestures, inarticulate for a howl or a random string, or the utterance of a sentence with its clause type, radical and tune, together with its volume. Its context update is the paper's: a falling declarative is a default assertion, a rising declarative places its proposition on the Table without commitment, and an interrogative is a default polar question. Askings and assertions are the paper's configurations of these primitives, quantified over contexts. The paper states the postulates for say and ask; the properties for yell, whisper, assert and claim are the ones its discussion of those verbs invokes. Interrogative grunts, which the paper takes to raise an issue without uttering a sentence, are not represented.

References

• [Rud25b]
• [FB10]
• [CG90]
• [Dav79]
• [Dav15]
• [Hac10]
• [FR17]

Quotative and ordinary complements

def Rudin2025b.speechVerb {E : Type u_1} {P : Type u_2} (reenact : E → P → Prop) (prop : P → Prop) (e : E) : Prop

A verb of speech under the paper's template holds of an event exactly when every performance reenacting it has the verb's characteristic property.

Equations

• Rudin2025b.speechVerb reenact prop e = ∀ (u : P), reenact e u → prop u

def Rudin2025b.quote {E : Type u_1} {P : Type u_2} (reenact : E → P → Prop) (u : P) (e : E) : Prop

The quotative complementizer holds of the events that the performance reenacts.

Equations

• Rudin2025b.quote reenact u e = reenact e u

def Rudin2025b.thatClause {E : Type u_1} {δ : Type u_3} (content : E → δ → Prop) (d : δ) (e : E) : Prop

An ordinary clausal complement holds of the events whose content is the clause's denotation.

Equations

• Rudin2025b.thatClause content d e = content e d

def Rudin2025b.quoteReport {E : Type u_1} {P : Type u_2} (reenact : E → P → Prop) (prop : P → Prop) (u : P) (e : E) : Prop

A quotative speech report holds, by predicate modification, of the verb's events that the performance reenacts.

Equations

• Rudin2025b.quoteReport reenact prop u e = (Rudin2025b.speechVerb reenact prop e ∧ Rudin2025b.quote reenact u e)

theorem Rudin2025b.not_quoteReport {E : Type u_1} {P : Type u_2} {reenact : E → P → Prop} {prop : P → Prop} {u : P} (h : ¬prop u) (e : E) : ¬quoteReport reenact prop u e

Quoting a performance that lacks the verb's property is contradictory.

theorem Rudin2025b.exists_reenact_iff {E : Type u_1} {P : Type u_2} (prop : P → Prop) (u : P) (e : E) : (∃ (reenact : E → P → Prop), quoteReport reenact prop u e) ↔ prop u

With the reenactment relation free, a quotative report of an event is satisfiable exactly when the performance has the verb's property.

def Rudin2025b.ContentSort {E : Type u_1} {δ : Type u_3} (V : E → Prop) (content : E → δ → Prop) (sort : δ → Prop) : Prop

A sortal restriction on content requires the content of every event of the verb to have the sort.

Equations

• Rudin2025b.ContentSort V content sort = ∀ (e : E) (d : δ), V e → content e d → sort d

theorem Rudin2025b.not_thatClause {E : Type u_1} {δ : Type u_3} {V : E → Prop} {content : E → δ → Prop} {sort : δ → Prop} (hV : ContentSort V content sort) {d : δ} (hd : ¬sort d) (e : E) : ¬(V e ∧ thatClause content d e)

An ordinary complement of the wrong sort, such as a proposition under ask, is contradictory.

Performances and their context updates

inductive Rudin2025b.Volume : Type

A Volume is the volume of a vocalization.

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

@[instance_reducible]

instance Rudin2025b.instDecidableEqVolume : DecidableEq Volume

Equations

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

structure Rudin2025b.Sentence (W : Type u_5) : Type u_5

A Sentence records an uttered sentence's clause type, the denotation of its radical, and its tune.

• type : Clause.SentenceType
• radical : Set W
• rising : Bool

inductive Rudin2025b.Material (W : Type u_5) : Type u_5

The linguistic material of a performance is none, inarticulate material, or the utterance of a sentence.

• none {W : Type u_5} : Material W
• inarticulate {W : Type u_5} : Material W
• utterance {W : Type u_5} (s : Sentence W) : Material W

structure Rudin2025b.Performance (W : Type u_5) : Type u_5

A performance consists of its linguistic material and its volume.

• material : Material W
• volume : Volume

def Rudin2025b.Material.Linguistic {W : Type u_4} : Material W → Prop

Material is linguistic when it produces linguistic material.

Equations

• Rudin2025b.Material.none.Linguistic = False
• x✝.Linguistic = True

def Rudin2025b.Material.Resp {W : Type u_4} : Material W → Prop

Material is response-eliciting when it is a rising declarative or an interrogative.

Equations

• (Rudin2025b.Material.utterance s).Resp = (s.type = Clause.SentenceType.declarative ∧ s.rising = true ∨ s.type = Clause.SentenceType.polar)
• x✝.Resp = False

def Rudin2025b.Material.Assertive {W : Type u_4} : Material W → Prop

Material is assertive when it is a falling declarative.

Equations

• (Rudin2025b.Material.utterance s).Assertive = (s.type = Clause.SentenceType.declarative ∧ s.rising = false)
• x✝.Assertive = False

@[instance_reducible]

instance Rudin2025b.instDecidablePredMaterialLinguistic {W : Type u_4} : DecidablePred Material.Linguistic

Equations

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

@[instance_reducible]

instance Rudin2025b.instDecidablePredMaterialResp {W : Type u_4} : DecidablePred Material.Resp

Equations

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

@[instance_reducible]

instance Rudin2025b.instDecidablePredMaterialAssertive {W : Type u_4} : DecidablePred Material.Assertive

Equations

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

def Rudin2025b.Sentence.update {W : Type u_4} : Sentence W → Commitment.Table Discourse.Role W → Commitment.Table Discourse.Role W

In the context update of an uttered sentence, a falling declarative is a default assertion, a rising declarative only places its proposition on the Table, and an interrogative is a default polar question.

Equations

• { type := Clause.SentenceType.declarative, radical := p, rising := false }.update x✝ = x✝.assert Discourse.Role.speaker p
• { type := Clause.SentenceType.declarative, radical := p, rising := true }.update x✝ = x✝.push (Question.ofSet p)
• { type := Clause.SentenceType.polar, radical := p, rising := rising }.update x✝ = x✝.polarQuestion p
• x✝¹.update x✝ = x✝

def Rudin2025b.Performance.update {W : Type u_4} : Performance W → Commitment.Table Discourse.Role W → Commitment.Table Discourse.Role W

The context update of a performance is that of the sentence it utters, if any.

Equations

• { material := Rudin2025b.Material.utterance s, volume := volume }.update x✝ = s.update x✝
• x✝¹.update x✝ = x✝

def Rudin2025b.Performance.Asking {W : Type u_4} (u : Performance W) : Prop

A performance is an asking when in every context it raises an issue without committing its speaker to any alternative of that issue.

Equations

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

def Rudin2025b.Performance.Assertion {W : Type u_4} (u : Performance W) : Prop

A performance is an assertion when in every context it raises an issue with a single alternative and commits its speaker to it.

Equations

• u.Assertion = ∀ (K : Commitment.Table Discourse.Role W), ∃ (q : Set W), (u.update K).stack = Question.ofSet q :: K.stack ∧ q ∈ (u.update K).discourseCommitments Discourse.Role.speaker

theorem Rudin2025b.Performance.asking_iff {W : Type u_4} (u : Performance W) : u.Asking ↔ u.material.Resp

A performance is an asking exactly when it utters a rising declarative or an interrogative.

theorem Rudin2025b.Performance.assertion_iff {W : Type u_4} (u : Performance W) : u.Assertion ↔ u.material.Assertive

A performance is an assertion exactly when it utters a falling declarative.

@[instance_reducible]

instance Rudin2025b.instDecidableAsking {W : Type u_4} (u : Performance W) : Decidable u.Asking

Equations

• Rudin2025b.instDecidableAsking u = decidable_of_iff u.material.Resp ⋯

@[instance_reducible]

instance Rudin2025b.instDecidableAssertion {W : Type u_4} (u : Performance W) : Decidable u.Assertion

Equations

• Rudin2025b.instDecidableAssertion u = decidable_of_iff u.material.Assertive ⋯

theorem Rudin2025b.Performance.not_asking_of_assertion {W : Type u_4} {u : Performance W} (h : u.Assertion) : ¬u.Asking

An assertion is not an asking, since it commits its speaker to a resolution of its issue.

The verbs of speech

inductive Rudin2025b.Verb : Type

A Verb is one of the verbs of speech the paper examines, or wonder, a species of asking.

• say : Verb
• assert : Verb
• claim : Verb
• ask : Verb
• wonder : Verb
• yell : Verb
• shout : Verb
• whisper : Verb

@[instance_reducible]

instance Rudin2025b.instDecidableEqVerb : DecidableEq Verb

Equations

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

@[instance_reducible]

instance Rudin2025b.instReprVerb : Repr Verb

Equations

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

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

Equations

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

def Rudin2025b.Verb.property {W : Type u_4} : Verb → Performance W → Prop

v.property is the property that the meaning postulate of v requires of the performances reenacting its events, linguistic material for say, an assertion for assert and claim, an asking for ask and wonder, loudness for yell and shout, a whisper for whisper.

Equations

• Rudin2025b.Verb.say.property = fun (u : Rudin2025b.Performance W) => u.material.Linguistic
• Rudin2025b.Verb.assert.property = Rudin2025b.Performance.Assertion
• Rudin2025b.Verb.claim.property = Rudin2025b.Performance.Assertion
• Rudin2025b.Verb.ask.property = Rudin2025b.Performance.Asking
• Rudin2025b.Verb.wonder.property = Rudin2025b.Performance.Asking
• Rudin2025b.Verb.yell.property = fun (u : Rudin2025b.Performance W) => u.volume = Rudin2025b.Volume.loud
• Rudin2025b.Verb.shout.property = fun (u : Rudin2025b.Performance W) => u.volume = Rudin2025b.Volume.loud
• Rudin2025b.Verb.whisper.property = fun (u : Rudin2025b.Performance W) => u.volume = Rudin2025b.Volume.whispered

@[instance_reducible]

instance Rudin2025b.instDecidableProperty {W : Type u_4} (v : Verb) (u : Performance W) : Decidable (v.property u)

Equations

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

theorem Rudin2025b.say_gesture {E : Type u_1} {W : Type u_4} {reenact : E → Performance W → Prop} {v : Volume} (e : E) : ¬quoteReport reenact Verb.say.property { material := Material.none, volume := v } e

Karate gestures under say are contradictory, since a saying is reenacted only by linguistic material.

theorem Rudin2025b.yell_whispered {E : Type u_1} {W : Type u_4} {reenact : E → Performance W → Prop} (e : E) (s : Material W) : ¬quoteReport reenact Verb.yell.property { material := s, volume := Volume.whispered } e

A whispered performance under yell is contradictory.

theorem Rudin2025b.assert_risingDeclarative {E : Type u_1} {W : Type u_4} {reenact : E → Performance W → Prop} {v : Volume} (p : Set W) (e : E) : ¬quoteReport reenact Verb.assert.property { material := Material.utterance { type := Clause.SentenceType.declarative, radical := p, rising := true }, volume := v } e

A rising declarative under assert is contradictory, since its utterance is no assertion.

theorem Rudin2025b.ask_risingDeclarative {E : Type u_1} {W : Type u_4} {v : Volume} (p : Set W) (e : E) : ∃ (reenact : E → Performance W → Prop), quoteReport reenact Verb.ask.property { material := Material.utterance { type := Clause.SentenceType.declarative, radical := p, rising := true }, volume := v } e

A rising declarative under ask is satisfiable, whatever proposition it denotes, since its utterance is an asking.

The paper's judgments

def Rudin2025b.verbs : List (String × Verb)

Equations

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

def Rudin2025b.volumes : List (String × Volume)

Equations

• Rudin2025b.volumes = [("neutral", Rudin2025b.Volume.neutral), ("loud", Rudin2025b.Volume.loud), ("whispered", Rudin2025b.Volume.whispered)]

def Rudin2025b.types : List (String × Clause.SentenceType)

types lists the sentence types the rows record; the paper's interrogatives are polar questions.

Equations

• Rudin2025b.types = [("declarative", Clause.SentenceType.declarative), ("interrogative", Clause.SentenceType.polar)]

def Rudin2025b.performance? (x : Datum) : Option (Performance Bool)

performance? x is the quoted performance of the row x, its sentence read as denoting a fixed proposition.

Equations

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

def Rudin2025b.datum (x : Datum) : Option (Verb × Performance Bool)

datum x reads the verb of speech and the quoted performance off the row x.

Equations

• Rudin2025b.datum x = do let __do_lift ← x.parse? "verb" Rudin2025b.verbs let __do_lift_1 ← Rudin2025b.performance? x pure (__do_lift, __do_lift_1)

def Rudin2025b.data : List (Datum × Verb × Performance Bool)

data lists the paper's quotative reports.

Equations

• Rudin2025b.data = List.filterMap (fun (x : Datum) => Option.map (fun (x_1 : Rudin2025b.Verb × Rudin2025b.Performance Bool) => (x, x_1)) (Rudin2025b.datum x)) Rudin2025b.Examples.all

def Rudin2025b.e₀ : Unit

e₀ is the one event of the reports.

Equations

• Rudin2025b.e₀ = ()

theorem Rudin2025b.judgments (d : Datum × Verb × Performance Bool) : d ∈ data → (d.1.judgment = Judgment.acceptable ↔ ∃ (reenact : Unit → Performance Bool → Prop), quoteReport reenact d.2.1.property d.2.2 e₀)

Each of the paper's quotative reports is judged acceptable exactly when it is satisfiable under the verb's meaning postulate.