Farkas-Bruce Performance Ontology Bridge

@cite{rudin-2025b} @cite{farkas-bruce-2010}

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 askPolarQuestions 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 @cite{rudin-2025b}'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 FarkasBruce.lean § Bridge theorems) 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 Dialogue.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

@[implicit_reducible]

instance Dialogue.QuotationFBOntology.instDecidableEqVolume : DecidableEq Volume

Equations

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

@[implicit_reducible]

instance Dialogue.QuotationFBOntology.instReprVolume : Repr Volume

Equations

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

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

Equations

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

@[implicit_reducible]

instance Dialogue.QuotationFBOntology.instInhabitedVolume : Inhabited Volume

Equations

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

def Dialogue.QuotationFBOntology.instInhabitedVolume.default : Volume

Equations

• Dialogue.QuotationFBOntology.instInhabitedVolume.default = Dialogue.QuotationFBOntology.Volume.neutral

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

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

• form : FarkasBruce.SentenceForm

  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 Dialogue.QuotationFBOntology.FBPerformance.update {W : Type u_1} (u : FBPerformance W) (s : FarkasBruce.DiscourseState W) : FarkasBruce.DiscourseState W

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

• non-rising declarative: assertDeclarative (commits + pushes issue)
• interrogative: askPolarQuestion (pushes issue, no commit)
• rising declarative: pushes issue without commit (the intermediate prosodic case @cite{rudin-2025b} relies on)

Equations

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

def Dialogue.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 Dialogue.QuotationFBOntology.FBPerformance.Loud {W : Type u_1} (u : FBPerformance W) : Prop

Loud: structural property of Volume.

Equations

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

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

Whispered: structural property of Volume.

Equations

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

def Dialogue.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 = Dialogue.FarkasBruce.SentenceForm.declarative)

def Dialogue.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 assertDeclarative branch adds, the rising and interrogative branches do not — so this matches the structural classification "non-rising declarative".

Equations

• u.Commits = (u.content ∈ (u.update Dialogue.FarkasBruce.DiscourseState.empty).dcS)

def Dialogue.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 Dialogue.FarkasBruce.DiscourseState.empty).table ≠ [])

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

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

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

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

def Dialogue.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 Dialogue.QuotationFBOntology.FBPerformance.commits_iff {W : Type u_1} (u : FBPerformance W) : u.Commits ↔ u.rising = false ∧ u.form = FarkasBruce.SentenceForm.declarative

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

theorem Dialogue.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 Dialogue.QuotationFBOntology.FBPerformance.update_decl_eq_assert {W : Type u_1} (u : FBPerformance W) (hr : u.rising = false) (hf : u.form = FarkasBruce.SentenceForm.declarative) (s : FarkasBruce.DiscourseState W) : u.update s = s.assertDeclarative u.content

Bridge to FarkasBruce: when the performance is a non-rising declarative, its update equals assertDeclarative content, so Dialogue.FarkasBruce.assert_adds_to_dcS applies directly.