Farkas & Roelofsen (2017): Division of Labor in Declaratives and Interrogatives

@cite{farkas-roelofsen-2017}

A formalization of the sentence-type taxonomy and commitment table from "Division of Labor in the Interpretation of Declaratives and Interrogatives" (J. Semantics 34(2): 237–289). The paper builds on @cite{farkas-bruce-2010}'s commitment-based discourse contexts and inquisitive semantics (@cite{ciardelli-groenendijk-roelofsen-2018}) to give a uniform account of the six sentence types in (3)–(8):

• (3) Amalia left↓. [falling declarative]
• (4) Amalia left↑? [rising declarative]
• (5) Did Amalia leave↓? [falling polar interrogative]
• (6) Did Amalia leave↑? [rising polar interrogative]
• (7) Amalia left↓, didn't she↓? [falling tag interrogative]
• (8) Amalia left↓, didn't she↑? [rising tag interrogative]

What this study formalizes

1. Clause-type markers (§4.1, eq. (26), p. 257): the two binary axes DEC/INT (declarative vs interrogative word order) and CLOSED/OPEN (falling vs rising intonation), composed with an optional tag. Implemented as MarkerTriple (renamed from the earlier SentenceForm, which collided with FarkasBruce.SentenceForm).
2. Markedness classification (§3 eq. (21) "Division of labor principle", p. 250; eq. (47) classification, p. 265). Falling declaratives + polar interrogatives are unmarked; rising declaratives + tag interrogatives are marked. The polar-interrogative classification rests on the paper's "equal weight" reading of formal-simplicity vs communicative-success (p. 264, last paragraph): "We leave open here how the factors are ranked in American English, and will not distinguish rising and falling polar interrogatives in terms of markedness." The flat verdict here therefore matches eq. (47) but inherits that disambiguation.
3. Commitment table (p. 240, the unnumbered table immediately preceding example (13)): the four-row taxonomy — full / bias / neutral.
4. Basic convention of use F_b (§5.1 eq. (48), p. 265): two clauses — (1) the proposition is added to the table, (2) its informative content is added to the speaker's commitments. F_b is the single convention that replaces Frege's two force operators (Assertion / Question); §7 defines it explicitly over FarkasBruce.DiscourseState and proves the structural division-of-labor claim that for unmarked forms, the discourse-effect update reduces to F_b alone (p. 266: "the conventional discourse effects of unmarked sentence types ... are fully determined by (48)").
5. Credence intervals (§3.2, p. 256): rising declaratives signal credence at most low; rising tag interrogatives signal moderate-to-high; falling tag interrogatives signal high. The four-level scale zero < low < moderate < high is F&R's own (p. 256).
6. Felicity contrasts (13)/(14), p. 240 — repeated as (24)/(25) on p. 256 — illustrating the rising-declarative ↔ tag-interrogative complementary distribution.
7. Highlighting integration (§5b): the felicity-in-context predicate threads Semantics.Highlighting.HighlightingContext, retiring the earlier "placeholder propositions" caveat. F&R's "highlighted alternative" (p. 256) is exactly the substrate's Highlighted predicate, anchored on the same Roelofsen-Farkas line of work (@cite{roelofsen-farkas-2015}, two years prior to F&R 2017).
8. Cross-framework divergences (§8): formal contrasts with Theories/Dialogue/Gunlogson.lean on rising declaratives (different substrate, different state predictions) and Krifka 2015 on tag interrogatives (sequential composition vs conjunction/disjunction; see also Phenomena/Assertion/Studies/Krifka2015.lean §5).

What's out of scope

• Full inquisitive-semantic compositional machinery of §4.2 (how clause-type markers combine with sentence radicals at the type level). The proposition-as-set-of-alternatives apparatus is available in Core/Question/; this study uses bare Set W for content because the paper-anchored felicity claims do not require alternative-set arithmetic.
• Sections 6–7 of the paper (extensions: alternative-question marking, comparison to other accounts).

Substrate consumed

• Theories/Dialogue/FarkasBruce.lean — DiscourseState, assertDeclarative, askPolarQuestion, pushIssue, addToDcS.
• Theories/Semantics/Highlighting.lean — HighlightingContext, Highlighted, AddressesQUD. Anchored on Roelofsen & Farkas (2015), which F&R 2017 cites and builds on.
• Theories/Dialogue/Gunlogson.lean — the divergence in §8 (rising declarative writes to addressee slate vs. F&R + F&B's "no commitment write" prediction).

Literature pointers (post-F&R 2017, not consumed by this file)

The dialogue commitment / rising-intonation literature has continued since 2017. Pointers for downstream readers:

• @cite{rudin-2018}, @cite{rudin-2019} on rising declaratives
• @cite{goodhue-2022a}, @cite{goodhue-2022b} on bias in polar questions
• @cite{krifka-2015} (≤ 2017) on tag interrogatives in Commitment Space Semantics — see Phenomena/Assertion/Studies/Krifka2015.lean for the formalization

inductive Phenomena.Dialogue.Studies.FarkasRoelofsen2017.ClauseType : Type

DEC/INT axis: declarative vs interrogative word order (@cite{farkas-roelofsen-2017} §4.1 eq. (26a), p. 257). In English root clauses, DEC = declarative word order, INT = interrogative word order.

• dec : ClauseType
• int : ClauseType

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqClauseType : DecidableEq ClauseType

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprClauseType : Repr ClauseType

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprClauseType = { reprPrec := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprClauseType.repr }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

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

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedClauseType.default : ClauseType

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedClauseType.default = Phenomena.Dialogue.Studies.FarkasRoelofsen2017.ClauseType.dec

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedClauseType : Inhabited ClauseType

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedClauseType = { default := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedClauseType.default }

inductive Phenomena.Dialogue.Studies.FarkasRoelofsen2017.Intonation : Type

CLOSED/OPEN axis: falling vs rising intonation (@cite{farkas-roelofsen-2017} §4.1 eq. (26b), p. 257). CLOSED = ↓ (falling); OPEN = ↑ (rising).

• closed : Intonation
• rising : Intonation

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqIntonation : DecidableEq Intonation

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqIntonation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprIntonation.repr : Intonation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprIntonation : Repr Intonation

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprIntonation = { reprPrec := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprIntonation.repr }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedIntonation.default : Intonation

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedIntonation.default = Phenomena.Dialogue.Studies.FarkasRoelofsen2017.Intonation.closed

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedIntonation : Inhabited Intonation

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedIntonation = { default := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedIntonation.default }

structure Phenomena.Dialogue.Studies.FarkasRoelofsen2017.MarkerTriple : Type

A MarkerTriple is a triple of clause-type marker, intonation marker, and tag-presence flag (@cite{farkas-roelofsen-2017} §4.1; tags are introduced after eq. (27), p. 258).

The 6 sentence types of (3)–(8):

• ⟨.dec, .closed, false⟩ — falling declarative
• ⟨.dec, .rising, false⟩ — rising declarative
• ⟨.int, .closed, false⟩ — falling polar interrogative
• ⟨.int, .rising, false⟩ — rising polar interrogative
• ⟨.dec, .closed, true⟩ — falling tag interrogative (declarative anchor + tag with falling intonation)
• ⟨.dec, .rising, true⟩ — rising tag interrogative (declarative anchor + tag with rising intonation)

Tags assumed to be reverse-polarity per F&R 2017 footnote 15 (p. 259); same-polarity tags ("Amalia left, did she?", their (9)) are explicitly out of scope.

Renamed from SentenceForm to avoid namespace collision with FarkasBruce.SentenceForm (.declarative | .interrogative), which is a coarser classification this triple refines.

• clauseType : ClauseType
• intonation : Intonation
• hasTag : Bool

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqMarkerTriple : DecidableEq MarkerTriple

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqMarkerTriple = Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqMarkerTriple.decEq

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqMarkerTriple.decEq (x✝ x✝¹ : MarkerTriple) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprMarkerTriple : Repr MarkerTriple

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprMarkerTriple = { reprPrec := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprMarkerTriple.repr }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprMarkerTriple.repr : MarkerTriple → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedMarkerTriple : Inhabited MarkerTriple

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedMarkerTriple = { default := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedMarkerTriple.default }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedMarkerTriple.default : MarkerTriple

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedMarkerTriple.default = { clauseType := default, intonation := default, hasTag := default }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.MarkerTriple.fallingDeclarative : MarkerTriple

Falling declarative (3) "Amalia left↓."

Equations

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

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.MarkerTriple.risingDeclarative : MarkerTriple

Rising declarative (4) "Amalia left↑?"

Equations

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

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.MarkerTriple.fallingPolarInterrogative : MarkerTriple

Falling polar interrogative (5) "Did Amalia leave↓?"

Equations

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

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.MarkerTriple.risingPolarInterrogative : MarkerTriple

Rising polar interrogative (6) "Did Amalia leave↑?"

Equations

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

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.MarkerTriple.fallingTagInterrogative : MarkerTriple

Falling tag interrogative (7) "Amalia left↓, didn't she↓?"

Equations

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

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.MarkerTriple.risingTagInterrogative : MarkerTriple

Rising tag interrogative (8) "Amalia left↓, didn't she↑?"

Equations

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

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.MarkerTriple.isMarked : MarkerTriple → Prop

Markedness predicate (@cite{farkas-roelofsen-2017} §3 eq. (21) "Division of labor principle", p. 250; classification eq. (47), p. 265):

Per (21): (a) The discourse effects of unmarked forms should be fully determined by their semantic content and the basic convention of use, F_b. (b) The discourse effects of marked forms should always include the discourse effects dictated by F_b. In addition, they may include special discourse effects connected to the particular sentence type involved.

Classification per eq. (47):

• Optimal, unmarked: falling declaratives, polar interrogatives (BOTH intonations, under the equal-weight reading discussed at p. 264, last paragraph).
• Marked: rising declaratives, tag interrogatives.

Caveat: F&R explicitly leave open whether English ranks formal simplicity above communicative success or vice versa (p. 264); if one is ranked higher, rising and falling polar interrogatives differ in markedness. The Lean classification adopts the equal-weight reading and so does not split rising vs. falling polars.

Equations

• One or more equations did not get rendered due to their size.
• { clauseType := clauseType, intonation := intonation, hasTag := true }.isMarked = True
• x✝.isMarked = False

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableIsMarked (mt : MarkerTriple) : Decidable mt.isMarked

Equations

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

inductive Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CommitmentType : Type

Three commitment-types from the unnumbered "Type of commitment" table on p. 240 (@cite{farkas-roelofsen-2017}):

• fullCommitment — the speaker is fully committed to one alternative (falling declaratives).
• bias — the speaker is biased toward one alternative but not fully committed (rising declaratives + tag interrogatives).
• neutral — the speaker remains neutral between alternatives (polar interrogatives, both intonations).

• fullCommitment : CommitmentType
• bias : CommitmentType
• neutral : CommitmentType

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqCommitmentType : DecidableEq CommitmentType

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqCommitmentType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCommitmentType : Repr CommitmentType

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCommitmentType = { reprPrec := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCommitmentType.repr }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCommitmentType.repr : CommitmentType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCommitmentType : Inhabited CommitmentType

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCommitmentType = { default := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCommitmentType.default }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCommitmentType.default : CommitmentType

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCommitmentType.default = Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CommitmentType.fullCommitment

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.commitmentType : MarkerTriple → CommitmentType

Map each marker triple to its commitment type (@cite{farkas-roelofsen-2017}, p. 240 unnumbered table).

Equations

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

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.commitment_table : commitmentType MarkerTriple.fallingDeclarative = CommitmentType.fullCommitment ∧ commitmentType MarkerTriple.risingDeclarative = CommitmentType.bias ∧ commitmentType MarkerTriple.fallingTagInterrogative = CommitmentType.bias ∧ commitmentType MarkerTriple.risingTagInterrogative = CommitmentType.bias ∧ commitmentType MarkerTriple.fallingPolarInterrogative = CommitmentType.neutral ∧ commitmentType MarkerTriple.risingPolarInterrogative = CommitmentType.neutral

Headline theorem: the commitment table from p. 240. Each of the 6 sentence types is assigned the commitment type the paper claims it has.

inductive Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceLevel : Type

Credence levels (@cite{farkas-roelofsen-2017} §3.2 p. 256): "If the speaker considers the highlighted alternative α to be much more likely than ᾱ, we say her credence in α is high; if she only considers it to be somewhat more likely than ᾱ, we say her credence in α is moderate; in cases that fall in between these two extremes that the speaker's credence in α is low; and finally, if the speaker does not consider α more likely than ᾱ at all, we say her credence in α is zero."

The four levels are linearly ordered: zero < low < moderate < high.

• zero : CredenceLevel
• low : CredenceLevel
• moderate : CredenceLevel
• high : CredenceLevel

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqCredenceLevel : DecidableEq CredenceLevel

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqCredenceLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCredenceLevel.repr : CredenceLevel → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCredenceLevel : Repr CredenceLevel

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCredenceLevel = { reprPrec := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCredenceLevel.repr }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceLevel.default : CredenceLevel

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceLevel.default = Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceLevel.zero

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceLevel : Inhabited CredenceLevel

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceLevel = { default := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceLevel.default }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceLevel.toNat : CredenceLevel → ℕ

Total order on CredenceLevel: zero < low < moderate < high.

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceLevel.zero.toNat = 0
• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceLevel.low.toNat = 1
• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceLevel.moderate.toNat = 2
• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceLevel.high.toNat = 3

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instLECredenceLevel : LE CredenceLevel

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instLECredenceLevel = { le := fun (a b : Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceLevel) => a.toNat ≤ b.toNat }

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableLeCredenceLevel (a b : CredenceLevel) : Decidable (a ≤ b)

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableLeCredenceLevel a b = a.toNat.decLe b.toNat

structure Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceInterval : Type

A credence interval is a pair of lower and upper bounds on a speaker's credence in the highlighted alternative (@cite{farkas-roelofsen-2017} §3.2, p. 256: "i is a credence interval, capturing the amount of credence x signals that she has in p").

• lower : CredenceLevel
• upper : CredenceLevel

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqCredenceInterval.decEq (x✝ x✝¹ : CredenceInterval) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqCredenceInterval : DecidableEq CredenceInterval

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqCredenceInterval = Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableEqCredenceInterval.decEq

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCredenceInterval.repr : CredenceInterval → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCredenceInterval : Repr CredenceInterval

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCredenceInterval = { reprPrec := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instReprCredenceInterval.repr }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceInterval.default : CredenceInterval

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceInterval.default = { lower := default, upper := default }

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceInterval : Inhabited CredenceInterval

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceInterval = { default := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instInhabitedCredenceInterval.default }

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.CredenceInterval.contains (i : CredenceInterval) (c : CredenceLevel) : Prop

A credence level falls within a credence interval.

Equations

• i.contains c = (i.lower ≤ c ∧ c ≤ i.upper)

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableContains (i : CredenceInterval) (c : CredenceLevel) : Decidable (i.contains c)

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableContains i c = Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableContains._aux_1 i c

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.signaledCredence : MarkerTriple → CredenceInterval

The credence interval signaled by each marker triple (@cite{farkas-roelofsen-2017} §3.2, p. 256, last paragraph before §4: "for rising declaratives the credence interval will be [zero, low], for rising tag interrogatives [moderate, high], and for falling tag interrogatives just [high]"):

• Rising declaratives → [zero, low]
• Rising tag interrogatives → [moderate, high]
• Falling tag interrogatives → [high, high] (F&R's "[high]")
• Other forms (unmarked) → no signal; the trivial interval [zero, high] which contains every level vacuously. The "no signal" reading is intended: F&R's credence-interval machinery applies only to marked forms (§3.2 prose).

Equations

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

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.felicitous (form : MarkerTriple) (speakerCredence : CredenceLevel) : Prop

A speaker is felicitous in uttering form in a context where her credence in the highlighted alternative is c iff c falls within the form's signaled credence interval (@cite{farkas-roelofsen-2017} §3.2 prose around examples (24)/(25), p. 256).

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.felicitous form speakerCredence = (Phenomena.Dialogue.Studies.FarkasRoelofsen2017.signaledCredence form).contains speakerCredence

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableFelicitous (form : MarkerTriple) (c : CredenceLevel) : Decidable (felicitous form c)

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableFelicitous form c = Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableFelicitous._aux_1 form c

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.example_24_rising_felicitous : felicitous MarkerTriple.risingDeclarative CredenceLevel.zero

Example (24) (@cite{farkas-roelofsen-2017} p. 256): "Belinda is going through a pile of job applications. Chris has not seen any of them yet. Belinda hands Chris the application that she just finished reading, and tells him to have a look at it. Chris to Belinda: a. This is a good one↑? [rising declarative, ✓ felicitous] b. #This is a good one, isn't it? [tag, # infelicitous]"

In this context, Chris has NO prior evidence — credence = zero. Rising declarative requires [zero, low] → felicitous (zero ∈ [zero, low]). Tag interrogative requires [moderate, high] → infelicitous.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.example_24_tag_infelicitous : ¬felicitous MarkerTriple.risingTagInterrogative CredenceLevel.zero

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.example_24_tag_infelicitous_falling : ¬felicitous MarkerTriple.fallingTagInterrogative CredenceLevel.zero

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.example_25_rising_infelicitous : ¬felicitous MarkerTriple.risingDeclarative CredenceLevel.high

Example (25) (@cite{farkas-roelofsen-2017} p. 256): "Belinda and Chris are looking at a sunset together. Belinda to Chris: a. #It's a beautiful sunset↑? [rising declarative, # infelicitous] b. It's a beautiful sunset, isn't it? [tag, ✓ felicitous]"

In this context, Belinda is looking at the sunset directly — credence = high. Rising declarative requires [zero, low] → infelicitous (high ∉ [zero, low]). The paper does not specify the intonation on the tag in (25b); F&R's signaled-credence assignment is "[high]" for falling-tag specifically (p. 256). The Lean encoding proves felicity for both intonations: rising-tag's [moderate, high] contains high, and falling-tag's [high, high] trivially contains high.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.example_25_tag_felicitous_rising : felicitous MarkerTriple.risingTagInterrogative CredenceLevel.high

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.example_25_tag_felicitous_falling : felicitous MarkerTriple.fallingTagInterrogative CredenceLevel.high

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.rising_dec_and_falling_tag_disjoint (c : CredenceLevel) : ¬(felicitous MarkerTriple.risingDeclarative c ∧ felicitous MarkerTriple.fallingTagInterrogative c)

The complementary-distribution claim of (24)/(25): rising declaratives and tag interrogatives are NEVER both felicitous in the same speaker-credence context (their signaled-credence intervals are disjoint).

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.rising_dec_and_rising_tag_disjoint (c : CredenceLevel) : ¬(felicitous MarkerTriple.risingDeclarative c ∧ felicitous MarkerTriple.risingTagInterrogative c)

Rising declarative + rising tag are also disjoint in signaled-credence (rising-dec ⊆ [zero, low] vs rising-tag ⊆ [moderate, high]).

F&R 2017's signaled-credence claims are explicitly about "the highlighted alternative" (p. 256). The substrate Theories/Semantics/Highlighting.lean (anchored on @cite{roelofsen-farkas-2015}, the same author line two years prior to F&R 2017) supplies the HighlightingContext/Highlighted predicate. This section threads it through felicitous, retiring the study's earlier "placeholder propositions" caveat.

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.felicitousInContext {W : Type u_1} (form : MarkerTriple) (c : Semantics.Highlighting.HighlightingContext W) (p : Set W) (speakerCredence : CredenceLevel) : Prop

Felicity of a marker form in a highlighting context: the proposition p must actually be highlighted in the context, AND the speaker's credence in p must fall in the form's signaled interval (@cite{farkas-roelofsen-2017} §3.2 p. 256, "the highlighted alternative" prose).

Equations

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

@[implicit_reducible]

instance Phenomena.Dialogue.Studies.FarkasRoelofsen2017.instDecidableFelicitousInContextOfHighlighted {W : Type u_1} (form : MarkerTriple) (c : Semantics.Highlighting.HighlightingContext W) (p : Set W) (cr : CredenceLevel) [Decidable (Semantics.Highlighting.Highlighted c p)] : Decidable (felicitousInContext form c p cr)

Equations

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

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.felicitousInContext_imp_highlighted {W : Type u_1} {form : MarkerTriple} {c : Semantics.Highlighting.HighlightingContext W} {p : Set W} {cr : CredenceLevel} (h : felicitousInContext form c p cr) : Semantics.Highlighting.Highlighted c p

Felicity-in-context implies the proposition is highlighted.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.felicitousInContext_imp_felicitous {W : Type u_1} {form : MarkerTriple} {c : Semantics.Highlighting.HighlightingContext W} {p : Set W} {cr : CredenceLevel} (h : felicitousInContext form c p cr) : felicitous form cr

Felicity-in-context implies the bare felicity (forgetting the highlighting witness).

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.rising_dec_and_falling_tag_disjoint_in_context {W : Type u_1} (c : Semantics.Highlighting.HighlightingContext W) (p : Set W) (cr : CredenceLevel) : ¬(felicitousInContext MarkerTriple.risingDeclarative c p cr ∧ felicitousInContext MarkerTriple.fallingTagInterrogative c p cr)

The complementary-distribution result lifts to the contextual setting: if p is highlighted in c, rising-dec and falling-tag cannot both be felicitous-in-context at any credence level.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.felicitousInContext_imp_addressesQUD {W : Type u_1} {form : MarkerTriple} {c : Semantics.Highlighting.HighlightingContext W} {p : Set W} {cr : CredenceLevel} (h : felicitousInContext form c p cr) : Semantics.Highlighting.AddressesQUD c.qud p

Felicity-in-context implies the proposition addresses the current QUD. Routes through Highlighting.highlighted_imp_addressesQUD — making the integration with Theories/Semantics/Highlighting.lean load-bearing (the substrate's AddressesQUD API is invoked, not just its Highlighted predicate's existence).

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.felicitousInContext_imp_salient {W : Type u_1} {form : MarkerTriple} {c : Semantics.Highlighting.HighlightingContext W} {p : Set W} {cr : CredenceLevel} (h : felicitousInContext form c p cr) : p ∈ c.salient

Felicity-in-context implies the proposition is in the salient set (made salient by recent utterance). Routes through Highlighting.highlighted_imp_salient.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.not_felicitousInContext_empty {W : Type u_1} (form : MarkerTriple) (p : Set W) (cr : CredenceLevel) : ¬felicitousInContext form Semantics.Highlighting.empty p cr

In the empty highlighting context (no salient propositions, trivial QUD), no proposition is felicitous-in-context for any marker form. The Highlighted check fails on the empty salient set.

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.signaledCredenceFor {W : Type u_1} (form : MarkerTriple) (c : Semantics.Highlighting.HighlightingContext W) (p : Set W) [Decidable (Semantics.Highlighting.Highlighted c p)] : Option CredenceInterval

The credence interval signaled by form for a specific proposition p in highlighting context c: some (signaledCredence form) if p is highlighted in c, otherwise none. F&R's signaled-credence machinery applies only when there IS a highlighted alternative (p. 256).

Equations

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

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.signaledCredenceFor_some_of_highlighted {W : Type u_1} {form : MarkerTriple} {c : Semantics.Highlighting.HighlightingContext W} {p : Set W} [Decidable (Semantics.Highlighting.Highlighted c p)] (h : Semantics.Highlighting.Highlighted c p) : signaledCredenceFor form c p = some (signaledCredence form)

When the proposition is highlighted, signaledCredenceFor projects to the bare signaledCredence.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.signaledCredenceFor_none_of_not_addressesQUD {W : Type u_1} {form : MarkerTriple} {c : Semantics.Highlighting.HighlightingContext W} {p : Set W} [Decidable (Semantics.Highlighting.Highlighted c p)] (h : ¬Semantics.Highlighting.AddressesQUD c.qud p) : signaledCredenceFor form c p = none

A proposition that does not address the current QUD has no signaled credence interval — signaledCredenceFor returns none. This is the load-bearing use of AddressesQUD: the F&R signaled-credence machinery is gated on the highlighted alternative actually addressing the QUD, not merely being made salient.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.signaledCredenceFor_none_of_not_salient {W : Type u_1} {form : MarkerTriple} {c : Semantics.Highlighting.HighlightingContext W} {p : Set W} [Decidable (Semantics.Highlighting.Highlighted c p)] (h : p ∉ c.salient) : signaledCredenceFor form c p = none

A proposition not in the salient set has no signaled credence interval. Load-bearing use of c.salient.

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.paperSentenceForms : List MarkerTriple

The six sentence forms the paper considers (3)–(8). Tags only combine with declarative anchors, so ⟨.int, _, true⟩ is not a valid F&R sentence form.

Equations

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

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.unmarked_iff_full_or_neutral_paper (mt : MarkerTriple) (h : mt ∈ paperSentenceForms) : ¬mt.isMarked ↔ commitmentType mt ∈ [CommitmentType.fullCommitment, CommitmentType.neutral]

A consequence of the framework restricted to the 6 paper-valid sentence forms: every UNMARKED form is either fullCommitment (falling declarative) or neutral (polar interrogatives). Bias commitments are reserved for marked forms (rising declaratives

• tag interrogatives).

This is the "Division of Labor" principle's structural signature: unmarked forms have either full commitment or no commitment, never partial bias.

F&R 2017's central architectural move (p. 265 eq. (48), p. 266 prose) is replacing Frege's two illocutionary force operators (Assertion + Question) with a single basic convention of use F_b. F_b is then augmented with sentence-type-specific special effects for marked forms.

This section formalizes F_b over FarkasBruce.DiscourseState and proves that for the unmarked forms (falling declaratives + both polar interrogatives), the per-form discourse-effect update reduces to F_b alone — the structural Division of Labor (eq. (21a) + p. 266).

The earlier landing of this study (CHANGELOG 0.230.675) imported FarkasBruce but never used it; the re-audit (CHANGELOG 0.230.677) flagged the hollow import; subsequent work added per-form update operators. The present revision adds explicit F_b and proves the unmarked-equals-F_b reduction, structurally enforcing what was previously documented in prose only.

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.F_b_dec {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : Dialogue.FarkasBruce.DiscourseState W

F_b — F&R 2017's "basic convention of use" (eq. (48), p. 265). Per F&R: "If a discourse participant x utters a declarative or interrogative sentence φ, the discourse context is affected as follows: (1) The proposition expressed by φ, [[φ]], is added to the table. (2) The informative content of φ, ⋃[[φ]], is added to commitments(x)."

F&R parameterize the proposition's alternatives at the type of inquisitive content. For the F&B substrate, we expose F_b in two forms: a single-alternative version (declarative content; one proposition α) and a two-alternative version (polar content; α and αᶜ).

The polar case follows F&R's eq. (50) (p. 267) verbatim: even though ⋃{α, αᶜ} = W is the trivial commitment, F&R explicitly add it to commitments(x). F&R's prose (p. 267): "the commitment entered on the speaker's discourse commitment list is the trivial commitment that w_a is an element of α∪ᾱ, which is the set of all possible worlds, W. In this case then, the speaker makes a trivial commitment and she remains neutral." This is distinct from F&B's askPolarQuestion, which omits the trivial-commitment step. The vacuity is genuine — see F_b_int_dcS_growth_is_vacuous below.

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.F_b_dec content ds = ds.assertDeclarative content

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.F_b_int {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : Dialogue.FarkasBruce.DiscourseState W

F_b for two-alternative (polar) content: alternatives = {α, αᶜ}, informative content = α ∪ αᶜ = Set.univ. Per F&R eq. (50) p. 267, this trivial commitment IS added to dcS — diverging from the F&B-substrate convention used by MarkerTriple.update for polar interrogatives, which skips the vacuous step. The two predictions differ in dcS shape but agree on toContextSet (the Set.univ commit doesn't constrain anything; see the vacuity theorem below).

Equations

• Phenomena.Dialogue.Studies.FarkasRoelofsen2017.F_b_int content ds = (ds.askPolarQuestion content).addToDcS Set.univ

def Phenomena.Dialogue.Studies.FarkasRoelofsen2017.MarkerTriple.update {W : Type u_2} (form : MarkerTriple) (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : Dialogue.FarkasBruce.DiscourseState W

Update a F&B discourse state by uttering content with marker form form. Follows F&B substrate conventions, which differ from F&R's verbatim eq. (48)/(50) on polar interrogatives — see update_int_vs_F_b_int_diverge_on_dcS below for the divergence and F_b_int_dcS_growth_is_vacuous for why the divergence is observably inert (toContextSet-preserving).

Mapping:

• Falling declarative (unmarked) → F_b_dec (= assertDeclarative): writes to dcS, pushes a one-alternative issue.
• Rising or falling polar interrogative (unmarked) → askPolarQuestion (NOT F_b_int): pushes a {p, ¬p} issue, omits the trivial Set.univ commit. Differs from F&R verbatim by the trivial commit; agrees on observable context.
• Rising declarative (marked, bias) → push a one-alternative issue WITHOUT writing dcS. F&B has no built-in operator for this; we construct the RaisedIssue directly.
• Tag interrogative (marked, bias) → declarative anchor commits via assertDeclarative AND a polar issue is raised by the tag.

Non-paper-canonical forms (interrogative + tag) are no-ops.

Equations

• One or more equations did not get rendered due to their size.
• { clauseType := Phenomena.Dialogue.Studies.FarkasRoelofsen2017.ClauseType.int, intonation := intonation, hasTag := false }.update content ds = ds.askPolarQuestion content
• form.update content ds = ds

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.update_eq_F_b_dec_falling {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : MarkerTriple.fallingDeclarative.update content ds = F_b_dec content ds

Division of Labor (eq. (21a) + p. 266 prose), unmarked falling declarative case: the per-form update IS F_b for falling declaratives. Note this remains rfl-vacuous because update for this case is defined to call F_b_dec. The substantive content is in §3 of the paper (that no special effects are needed for this form); the Lean encoding records that consensus.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.update_int_vs_F_b_int_diverge_on_dcS {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : (MarkerTriple.fallingPolarInterrogative.update content ds).dcS = ds.dcS ∧ (F_b_int content ds).dcS = Set.univ :: ds.dcS

Substrate divergence on polar interrogatives: F&B's askPolarQuestion (used by MarkerTriple.update for both polar interrogatives) skips the trivial Set.univ commit that F&R's eq. (50) requires. Concretely, F&R-verbatim F_b adds Set.univ to dcS; F&B's askPolarQuestion does not.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.F_b_int_dcS_growth_is_vacuous {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : (F_b_int content ds).toContextSet = (ds.askPolarQuestion content).toContextSet

The divergence in update_int_vs_F_b_int_diverge_on_dcS is observably inert: F&R's verbatim F_b for polar adds Set.univ to dcS, but Set.univ is the identity for context-set intersection, so the toContextSet projection of F_b_int agrees with that of askPolarQuestion. F&R prose (p. 267): "the speaker makes a trivial commitment and she remains neutral."

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.fallingDec_writes_dcS {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : (MarkerTriple.fallingDeclarative.update content ds).dcS = content :: ds.dcS

Falling declarative writes to dcS (full commitment, p. 240 table).

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.polarInt_doesnt_write_dcS_falling {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : (MarkerTriple.fallingPolarInterrogative.update content ds).dcS = ds.dcS

Polar interrogatives (either intonation) do NOT write to dcS (neutral, p. 240 table).

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.polarInt_doesnt_write_dcS_rising {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : (MarkerTriple.risingPolarInterrogative.update content ds).dcS = ds.dcS

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.risingDec_doesnt_write_dcS {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : (MarkerTriple.risingDeclarative.update content ds).dcS = ds.dcS

Rising declarative does NOT write to dcS (bias, no full commitment; matches p. 240 table classification).

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.tag_writes_dcS_falling {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : (MarkerTriple.fallingTagInterrogative.update content ds).dcS = content :: ds.dcS

Tag interrogatives DO write to dcS (the declarative anchor commits; the tag separately raises an issue). The "bias" classification on p. 240 thus has TWO structurally distinct realizations in F&B terms: rising declaratives don't commit, tags do.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.tag_writes_dcS_rising {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : (MarkerTriple.risingTagInterrogative.update content ds).dcS = content :: ds.dcS

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.all_paper_forms_push_issue {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) (form : MarkerTriple) (h : form ∈ paperSentenceForms) : (form.update content ds).table.length > ds.table.length

All sentence types push at least one issue onto the table. The structural common ground per F&B: every utterance is table-bearing.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.fullCommitment_iff_dcS_grows {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) (form : MarkerTriple) (h : form ∈ paperSentenceForms) : commitmentType form = CommitmentType.fullCommitment → (form.update content ds).dcS = content :: ds.dcS

The commitment-table classification corresponds to F&B-side behavior for the two "extreme" cases:

• fullCommitment ↔ writes to dcS via assertDeclarative
• neutral ↔ does not write to dcS (only pushes an issue)

The bias middle case is NOT structurally uniform: rising declaratives don't write dcS (like neutral), tag interrogatives DO write dcS (like full). This is an honest finding — the p. 240 commitment table abstracts over a structural distinction that F&B's substrate makes visible.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.neutral_iff_dcS_unchanged {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) (form : MarkerTriple) (h : form ∈ paperSentenceForms) : commitmentType form = CommitmentType.neutral → (form.update content ds).dcS = ds.dcS

Complement direction: neutral commitment type ↔ no dcS write.

F&R 2017 sits in a crowded field of commitment-based dialogue frameworks, each making different structural predictions for the contested cases (rising declaratives, tag interrogatives). This section makes two divergences Lean-checkable.

@cite{gunlogson-2008} (and earlier @cite{gunlogson-2001}, the work F&R 2017's footnote 13 cites), formalized in Theories/Dialogue/Gunlogson.lean, records rising-declarative information by writing to the addressee's slate as an other-generated commitment. F&R 2017 (threaded through F&B substrate) writes nothing to the speaker's dcS (only pushes an issue).

These two facts look like a contradiction, but F&R themselves frame the relationship more carefully. Footnote 13 (p. 257) reads: "Our account is similar to Gunlogson's in separating the two components but while for Gunlogson they only come into play at the discourse level, for us they have semantic import." So the difference is in which layer of analysis carries the rising-vs-falling distinction (discourse-level for Gunlogson; semantic-level for F&R), not whether the addressee has anything attributed to them.

The Lean witness in this section records the difference in state shapes — F&R + F&B's DiscourseState does not even have a slot for "other-generated addressee commitment" (only dcL for self-generated listener commitments), so F&B's silence on rising-dec addressee attribution is type-level silence, not an empirical prediction. The substrates differ in what they record, not in what they claim happens.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.fr_rising_dec_no_speaker_commitment {W : Type u_2} (content : Set W) (ds : Dialogue.FarkasBruce.DiscourseState W) : (MarkerTriple.risingDeclarative.update content ds).dcS = ds.dcS

F&R + F&B prediction for rising declarative: dcS is unchanged.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.gunlogson_rising_dec_writes_addressee {W : Type u_2} (content : Set W) : (Dialogue.Gunlogson.GunlogsonState.empty.risingDeclarative content).addresseeSlate.commitments.length = 1

Gunlogson 2008 prediction for rising declarative from the empty state: the addressee's slate gains exactly one commitment (other-generated). Restated from Theories/Dialogue/Gunlogson.lean for the cross-framework comparison.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.fr_vs_gunlogson_rising_dec_state_shape {W : Type u_2} (content : Set W) : (MarkerTriple.risingDeclarative.update content Dialogue.FarkasBruce.DiscourseState.empty).dcS = [] ∧ (Dialogue.Gunlogson.GunlogsonState.empty.risingDeclarative content).addresseeSlate.commitments ≠ []

Cross-framework state-shape divergence: F&R + F&B record the rising-declarative effect in different state slots than Gunlogson. F&R + F&B's dcS (speaker's commitments) is unchanged; Gunlogson's addresseeSlate gains an other-generated commitment. Per F&R's own footnote 13 (p. 257), this is a layer-of-analysis difference rather than an empirical contradiction — F&R simply factor the addressee- attribution into the semantic component (out of scope for this discourse-state formalization), where Gunlogson factors it into the discourse component (which the substrate makes visible). The theorem witnesses the structural divergence; it does not adjudicate which framework better captures the phenomenon.

@cite{krifka-2015} §5 (eqs. 44–45), with substrate in Theories/Dialogue/CommitmentSpace.lean, argues that tag interrogatives are a SINGLE complex speech act — matchingTag is a ComplexSpeechAct.conj of an assertion and a monopolar question (sharing content φ), reverseTag is a ComplexSpeechAct.disj. Krifka explicitly contrasts this with the sequential reading: per CommitmentSpace.lean line ~688, "this is not a move in which the speaker first makes an assertion and then asks the addressee to make the same assertion. Rather, the two speech acts are first conjoined, and then applied as one complex speech act."

The F&B-threaded F&R update in this file uses sequential composition (assertDeclarative |> askPolarQuestion), producing two independent issues on the table. This is exactly the structural shape Krifka rejects. The contrast theorem below pulls in Krifka's matchingTag substrate so the divergence is Lean-checkable on both sides — F&R's two-issue sequential signature vs Krifka's single-conjunction signature.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.fr_tag_pushes_two_issues {W : Type u_2} (content : Set W) : (MarkerTriple.fallingTagInterrogative.update content Dialogue.FarkasBruce.DiscourseState.empty).table.length = 2

F&R + F&B prediction for tag interrogative: the table gains TWO issues — one interrogative (from the tag's polar question), one declarative (from the assertion anchor), sequentially stacked.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.fr_tag_table_forms {W : Type u_2} (content : Set W) : List.map Dialogue.FarkasBruce.RaisedIssue.form (MarkerTriple.fallingTagInterrogative.update content Dialogue.FarkasBruce.DiscourseState.empty).table = [Dialogue.FarkasBruce.SentenceForm.interrogative, Dialogue.FarkasBruce.SentenceForm.declarative]

The two issues F&R + F&B place on the table for a tag are of DIFFERENT forms — one interrogative (from the tag's polar question), one declarative (from the assertion anchor).

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.krifka_matching_tag_is_single_conjunction {W : Type u_2} (φ : W → Prop) : ∃ (a : Dialogue.Krifka.SpeechAct W) (b : Dialogue.Krifka.SpeechAct W), Dialogue.Krifka.matchingTag φ = Dialogue.Krifka.ComplexSpeechAct.conj a b

Krifka 2015 prediction for a matching tag: a SINGLE ComplexSpeechAct.conj wrapper around two component speech acts. Restated from Theories/Dialogue/CommitmentSpace.lean for the cross-framework comparison.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.krifka_matching_tag_shared_content {W : Type u_2} (φ : W → Prop) : List.map Dialogue.Krifka.SpeechAct.content (Dialogue.Krifka.matchingTag φ).components = [φ, φ]

In Krifka's matching tag, the two components share content φ (matching the assertion + monopolar-question semantics of "I have won the race, have I?"). Restated from CommitmentSpace.lean.

theorem Phenomena.Dialogue.Studies.FarkasRoelofsen2017.fr_vs_krifka_tag_structural_divergence {W : Type u_2} (φ : W → Prop) : List.map Dialogue.FarkasBruce.RaisedIssue.form (MarkerTriple.fallingTagInterrogative.update φ Dialogue.FarkasBruce.DiscourseState.empty).table = [Dialogue.FarkasBruce.SentenceForm.interrogative, Dialogue.FarkasBruce.SentenceForm.declarative] ∧ (∃ (a : Dialogue.Krifka.SpeechAct W) (b : Dialogue.Krifka.SpeechAct W), Dialogue.Krifka.matchingTag φ = Dialogue.Krifka.ComplexSpeechAct.conj a b) ∧ List.map Dialogue.Krifka.SpeechAct.content (Dialogue.Krifka.matchingTag φ).components = [φ, φ]

Cross-framework structural divergence on tag interrogatives: F&R + F&B produces a sequence of TWO distinct issues with DIFFERENT forms; Krifka 2015 produces ONE complex speech act wrapping two components with the SAME content. The two signatures cannot be re-reconciled by changing input content — they encode tag interrogatives as fundamentally different mathematical objects.