@cite{ippolito-kiss-williams-2025}: Discourse only

@cite{ippolito-kiss-williams-2022} @cite{potts-2005} @cite{roberts-2012} @cite{thomas-2026}

Formalisation of @cite{ippolito-kiss-williams-2025} "Discourse only" (WCCFL 41 proceedings, pp. 222–231). Discourse only is a clausal connective taking two clausal arguments S and S' and contributing a conventional implicature (CI) of lack of agreement between S and S' w.r.t. a QUD.

The doxastic-evidential apparatus (Supports, Agree, Disagree) that the paper's §4 statement uses is attributed by the paper itself to the predecessor @cite{ippolito-kiss-williams-2022} ("Following Ippolito et al. (2022) we define…"); it lives in Phenomena/Focus/Studies/IppolitoKissWilliams2022.lean and is imported here. This file owns the paper-specific bundling — Sentence, Context, the felicity conditions of ex. (16), the architectural derivations of §5.2, and the worked house-buying example of §7.

A previous "Part II: Bayesian-to-DTS bridge" was removed in 0.230.502: @cite{merin-1999} is not cited in the paper's reference list, and the §6 only-vs-but discussion grounds itself in @cite{anscombre-ducrot-1977} and IKW 2022's notion of semantic equality of but's arguments — not in decision-theoretic semantics. The bridge was the formaliser's editorial overlay; the substrate-internal Bayesian theorems it contained (probSupports_implies_posRelevant_binary, negRelevant_implies_not_probSupports) moved to Theories/Pragmatics/DecisionTheoretic/Core.lean where they belong.

The puzzle

Cross-linguistically, some languages have a discourse particle glossed as "only" that conjoins two clauses while signalling that the second undermines the evidential trajectory of the first. Paper (29a-d) all use a single house-buying frame:

• Italian solo che ("La casa è bella, solo che è costosissima")
• Russian tol'ko ("Dom krasivyj, tol'ko ochen' dorogoj")
• Hungarian csak ("Szép a ház, csak nagyon drága")
• Mandarin zhǐshì ("Zhège fángzi hěn piàoliang, zhǐshì yǒudiǎr guì")

Paper ex. (16) — the proposal

⟦S [only S']⟧^c is defined only if S and S' are relevant to the QUD in c and ∃ α ∈ QUD, S supports α. If defined:

• At-issue: highlighted content of S intersected with that of S' — every world where both are informatively true.
• CI: ∃ α ∈ QUD such that (i) every true partial answer p ∉ QUD is positive evidence for α; (ii) S' does not support α.

The Lean ciContent (i) restricts to partial answers p ∉ alt qud to match the paper's p ∉ QUD exclusion; the "p supports α" gloss is implemented as IsPositiveEvidence p α rather than fully-doxastic Supports, since established partial answers are presumed already common-ground. A doxastic-gated variant is straightforward but deferred.

Architectural derivations

• Interrogative left-arg restriction (§5.2). Canonical info-seeking questions cannot be the left argument because the speaker doesn't believe any answer, so dox ⊆ q fails for all q ∈ alt S, so Supports fails. This falls out from Supports.of_no_belief_fails in IppolitoKissWilliams2022.lean — no clause-type filter required.
• Biased / rhetorical questions can be left-args (§5.2 ex. (20)–(21)). These have a believed answer (dox ⊆ q for some q), so the doxastic condition is satisfied.

Layout

• Substrate (Sentence, Context, isDefined, ciContent, agree, disagree) and architectural theorems (interrogative_blocks_support, weak_non_agreement, disagree_imp_ciContent_of_empty_partials).
• Part I: end-to-end derivation chains for the house-buying scenario (§7), instantiating the substrate on a concrete 8-world model and connecting the predictions to the cross-linguistic data in the sibling Data.lean.

Discourse context

structure Phenomena.Focus.Studies.IppolitoKissWilliams2025.Context (W : Type u_1) : Type u_1

Discourse context for evaluating discourse only.

The doxastic state is what makes the interrogative restriction fall out naturally: canonical info-seeking questions fail the doxastic condition of Supports (the speaker doesn't believe any answer).

• qud : Core.Question W

  The QUD as an inquisitive issue.

• prior : PMF W

  Prior probability distribution.

• dox : Set W

  Speaker's doxastic state dox_sp.

• partialAnswers : List (Set W)

  True partial answers to the QUD established in prior discourse. @cite{ippolito-kiss-williams-2025} ex. (16) CI clause (i) quantifies universally over all true partial answers p ∉ QUD.

• subquestions : List (Core.Question W)

  Subquestions of the QUD established by the discourse context. @cite{roberts-2012} (subquestion strategy); IKW §5.1: provided by the context, not computed.

Sentence

structure Phenomena.Focus.Studies.IppolitoKissWilliams2025.Sentence (W : Type u_1) : Type u_1

A discourse only sentence with two clausal arguments.

sDen is the inquisitive denotation of the left argument S, s'Den is the inquisitive denotation of the right argument S'. The denotation type is uniform — what varies between declarative and interrogative arguments is whether Supports can be satisfied.

• sDen : Core.Question W

  Inquisitive denotation of the left argument S.

• s'Den : Core.Question W

  Inquisitive denotation of the right argument S'.

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.Sentence.atIssueContent {W : Type u_1} (d : Sentence W) : Set W

At-issue content of S only S': every world where both S and S' are informatively true. @cite{ippolito-kiss-williams-2025} ex. (16).

Equations

• d.atIssueContent = d.sDen.info ∩ d.s'Den.info

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.Sentence.isDefined {W : Type u_1} (d : Sentence W) (ctx : Context W) : Prop

Presupposition / definedness condition for discourse only. @cite{ippolito-kiss-williams-2025} ex. (16):

1. S is structurally relevant to the QUD;
2. S' is structurally relevant to the QUD;
3. S supports some answer α ∈ QUD via Supports.

Equations

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

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.Sentence.ciContent {W : Type u_1} (d : Sentence W) (ctx : Context W) : Prop

CI content of discourse only. @cite{ippolito-kiss-williams-2025} ex. (16): ∃ α ∈ QUD such that (i) every true partial answer p with p ∉ QUD is positive evidence for α; (ii) S itself supports α; (iii) S' does not support α.

The p ∉ alt ctx.qud exclusion in (i) matches the paper's p ∉ QUD restriction. The "p supports α" gloss is read here as raw IsPositiveEvidence (presuming established partial answers are common-ground); a doxastic-gated variant using the IKW 2022 Supports predicate is straightforward but not currently used.

When partialAnswers is empty, condition (i) is vacuously true: no prior evidence contradicts the direction.

Equations

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

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.Sentence.agree {W : Type u_1} (d : Sentence W) (ctx : Context W) : Prop

S and S' agree on the QUD: there is some α ∈ QUD that both Supports. Lifted from IKW2022.Agree. @cite{ippolito-kiss-williams-2025} ex. (14a).

Equations

• d.agree ctx = Phenomena.Focus.Studies.IppolitoKissWilliams2022.Agree ctx.dox d.sDen d.s'Den ctx.qud ctx.prior

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.Sentence.disagree {W : Type u_1} (d : Sentence W) (ctx : Context W) : Prop

S and S' disagree on the QUD. Lifted from IKW2022.Disagree. @cite{ippolito-kiss-williams-2025} ex. (14b).

Equations

• d.disagree ctx = Phenomena.Focus.Studies.IppolitoKissWilliams2022.Disagree ctx.dox d.sDen d.s'Den ctx.qud ctx.prior

Architectural derivations

@[simp]

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.atIssue_eq_inter {W : Type u_1} (d : Sentence W) : d.atIssueContent = d.sDen.info ∩ d.s'Den.info

At-issue content unfolds as the intersection of informational content.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.interrogative_blocks_support {W : Type u_1} {dox : Set W} {S : Core.Question W} {μ : PMF W} {α : Set W} (h : ∀ q ∈ S.alt, ¬dox ⊆ q) : ¬IppolitoKissWilliams2022.Supports dox S α μ

@cite{ippolito-kiss-williams-2025} §5.2: an info-seeking interrogative cannot be the left argument because the speaker doesn't believe any of its alternatives, so Supports fails for every answer. Direct re-export of Supports.of_no_belief_fails.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.interrogative_satisfies_ci_clause {W : Type u_1} {dox : Set W} {S' : Core.Question W} {μ : PMF W} {α : Set W} (h : ∀ q ∈ S'.alt, ¬dox ⊆ q) : ¬IppolitoKissWilliams2022.Supports dox S' α μ

@cite{ippolito-kiss-williams-2025} §5.2: an info-seeking interrogative S' trivially satisfies the CI's condition (ii) — Supports fails for every α, so ¬ Supports … holds.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.weak_non_agreement {W : Type u_1} (d : Sentence W) (ctx : Context W) (hS' : ∀ α ∈ ctx.qud.alt, ¬IppolitoKissWilliams2022.Supports ctx.dox d.s'Den α ctx.prior) : ¬d.agree ctx ∧ ¬d.disagree ctx

Weak non-agreement (@cite{ippolito-kiss-williams-2025} §5.2 prose around ex. (18)): when S' cannot support any QUD answer, S and S' neither agree nor disagree. Both relations require S' to support something.

Example IKW ex. (18): "The house is beautiful, only can we afford it?" — S supports "buy the house", S' supports nothing. Not agreement, not disagreement: weak non-agreement.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.disagree_imp_ciContent_of_empty_partials {W : Type u_1} (d : Sentence W) (ctx : Context W) (hDisagree : d.disagree ctx) (hPartial : ctx.partialAnswers = []) : d.ciContent ctx

@cite{ippolito-kiss-williams-2025} core insight: when S and S' evidentially clash (disagree) and there are no prior partial answers, the CI is automatically satisfied.

Proof: pick the witness α from S's support side; by ¬agree, S' cannot support that same α; the empty-partial-answers hypothesis discharges (i) vacuously.

Part I: End-to-End Derivation Chains

Concrete instantiations on a 8-world model of the house-buying scenario (@cite{ippolito-kiss-williams-2025} §7). Connects the substrate predictions to the empirical data in the sibling Data.lean under this study's subdirectory.

§ 1: World Type and Propositions

8-world model. Encoding w = 4b + 2e + r where:

World	Beautiful	Expensive	Renovated	Buy?
w₀	✓		✓	✓
w₁	✓
w₂	✓	✓	✓
w₃	✓	✓
w₄			✓
w₅
w₆		✓	✓
w₇		✓

@[reducible, inline]

abbrev Phenomena.Focus.Studies.IppolitoKissWilliams2025.World : Type

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.World = Fin 8

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.beautiful : Set World

The house is beautiful (w₀–w₃).

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.beautiful = {w : Phenomena.Focus.Studies.IppolitoKissWilliams2025.World | ↑w < 4}

@[implicit_reducible]

instance Phenomena.Focus.Studies.IppolitoKissWilliams2025.instDecidablePredWorldMemSetBeautiful : DecidablePred fun (x : World) => x ∈ beautiful

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.instDecidablePredWorldMemSetBeautiful w = (↑w).decLt 4

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.expensive : Set World

The house is expensive (w₂, w₃, w₆, w₇).

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.expensive = {w : Phenomena.Focus.Studies.IppolitoKissWilliams2025.World | ↑w / 2 % 2 = 1}

@[implicit_reducible]

instance Phenomena.Focus.Studies.IppolitoKissWilliams2025.instDecidablePredWorldMemSetExpensive : DecidablePred fun (x : World) => x ∈ expensive

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.instDecidablePredWorldMemSetExpensive x✝ = (↑x✝ / 2 % 2).decEq 1

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.renovated : Set World

The house has been renovated (w₀, w₂, w₄, w₆).

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.renovated = {w : Phenomena.Focus.Studies.IppolitoKissWilliams2025.World | ↑w % 2 = 0}

@[implicit_reducible]

instance Phenomena.Focus.Studies.IppolitoKissWilliams2025.instDecidablePredWorldMemSetRenovated : DecidablePred fun (x : World) => x ∈ renovated

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.instDecidablePredWorldMemSetRenovated x✝ = (↑x✝ % 2).decEq 0

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.buy : Set World

Should we buy the house? Only if beautiful, affordable, and renovated (w₀).

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.buy = {w : Phenomena.Focus.Studies.IppolitoKissWilliams2025.World | ↑w = 0}

@[implicit_reducible]

instance Phenomena.Focus.Studies.IppolitoKissWilliams2025.instDecidablePredWorldMemSetBuy : DecidablePred fun (x : World) => x ∈ buy

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.instDecidablePredWorldMemSetBuy x✝ = (↑x✝).decEq 0

noncomputable def Phenomena.Focus.Studies.IppolitoKissWilliams2025.prior : PMF World

Uniform prior: P(w) = 1/8 for each world.

Equations

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

§ 2: QUD and Denotations

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.qud : Core.Question World

QUD: "Should we buy the house?" — binary issue.

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.qud = Core.Question.polar Phenomena.Focus.Studies.IppolitoKissWilliams2025.buy

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.sBeautiful : Core.Question World

Declarative S: "The house is beautiful" — one alternative.

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.sBeautiful = Core.Question.polar Phenomena.Focus.Studies.IppolitoKissWilliams2025.beautiful

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.s'Expensive : Core.Question World

Declarative S': "It's (very) expensive" — one alternative.

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.s'Expensive = Core.Question.polar Phenomena.Focus.Studies.IppolitoKissWilliams2025.expensive

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.s'RenovatedQ : Core.Question World

Polar Q S': "Has it been renovated?" — two alternatives.

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.s'RenovatedQ = Core.Question.polar Phenomena.Focus.Studies.IppolitoKissWilliams2025.renovated

§ 3: Doxastic States

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.doxBE : Set World

Speaker who asserts "beautiful" and "expensive": believes both. dox = {w₂, w₃} (beautiful ∧ expensive).

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.doxBE = Phenomena.Focus.Studies.IppolitoKissWilliams2025.beautiful ∩ Phenomena.Focus.Studies.IppolitoKissWilliams2025.expensive

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.doxB : Set World

Speaker who asserts "beautiful" but asks about renovation: believes beautiful, uncertain about expense and renovation. dox = {w₀, w₁, w₂, w₃} (beautiful).

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.doxB = Phenomena.Focus.Studies.IppolitoKissWilliams2025.beautiful

§ 4: Contexts

noncomputable def Phenomena.Focus.Studies.IppolitoKissWilliams2025.coreCtx : Context World

Context for core examples: S = "beautiful", S' = "expensive". No prior partial answers — fresh discourse.

Subquestions per IKW §5.1 ("Answering this question requires answering its plausible subquestions, such as Is the house beautiful? Is the house expensive?"). We also include renovation since it appears in the polar Q examples.

Equations

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

noncomputable def Phenomena.Focus.Studies.IppolitoKissWilliams2025.clauseTypeCtx : Context World

Context for clause-type examples: S = "beautiful", S' = interrogative. Speaker believes S but doesn't know the answer to S'. Same subquestions as core context — the QUD structure doesn't change with clause type.

Equations

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

§ 5: Sentences

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.declSentence : Sentence World

"The house is beautiful, only it's expensive" (core declarative-declarative).

Equations

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

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.polarQSentence : Sentence World

"The house is beautiful, only has it been renovated?" (polar Q as S').

Equations

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

§ 6: Core Derivation: Declarative S + Declarative S'

The five sorries discharged in §6 and §7 establish the §7 cross-linguistic predictions on a concrete 8-world model with uniform prior. The PMF arithmetic reduces to four base probabilities (beautiful, expensive, their intersections with buy/buyᶜ) computed via PMF.probOfSet_apply + Fin.sum_univ_eight. The doxastic ⊆ checks and the moveRelevant reductions (via moveRelevant_polar_iff) are pure Set arithmetic discharged by decide.

Bayesian-evidence facts and Supports witnesses

Discharged theorems

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.core_isDefined : declSentence.isDefined coreCtx

The presupposition is satisfied: both arguments are relevant via the explicit subquestion list, and S supports buy from doxBE.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.core_ciContent : declSentence.ciContent coreCtx

The CI holds: ∃α (= buy) s.t. all partial answers are positive evidence for α (vacuous, since coreCtx.partialAnswers = []), S supports α, and S' does not.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.core_atIssue_nonempty : 2 ∈ declSentence.atIssueContent

The at-issue content is non-trivial: there exist worlds where both S and S' hold (e.g., w₂: beautiful ∧ expensive).

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.core_disagree : declSentence.disagree coreCtx

S and S' disagree w.r.t. the QUD: S supports "buy", S' supports "don't buy", no shared answer is supported by both.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.core_predicted : declSentence.isDefined coreCtx ∧ declSentence.ciContent coreCtx ∧ Data.italian_house.felicitous = true

Per-datum: predicts felicitous for the core declarative-declarative examples (Italian 29a, Russian 29b, Hungarian 29c, Mandarin 29d, English 2).

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.russian_house_predicted : declSentence.isDefined coreCtx ∧ declSentence.ciContent coreCtx ∧ Data.russian_house.felicitous = true

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.hungarian_house_predicted : declSentence.isDefined coreCtx ∧ declSentence.ciContent coreCtx ∧ Data.hungarian_house.felicitous = true

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.mandarin_house_predicted : declSentence.isDefined coreCtx ∧ declSentence.ciContent coreCtx ∧ Data.mandarin_house.felicitous = true

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.english_house_predicted : declSentence.isDefined coreCtx ∧ declSentence.ciContent coreCtx ∧ Data.english_house.felicitous = true

§ 7: Clause-Type Derivation: Declarative S + Polar Q S'

doxB-specific helpers (for the polar-Q derivation)

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.polarQ_isDefined : polarQSentence.isDefined clauseTypeCtx

The presupposition is satisfied even with interrogative S'. The polar renovated subquestion in clauseTypeCtx.subquestions discharges the relevance of s'RenovatedQ.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.polarQ_ciContent : polarQSentence.ciContent clauseTypeCtx

The CI holds: clause (ii) by sBeautiful_supports_buy_doxB; clause (iii) reduces to Supports.of_no_belief_fails since the speaker (who knows the house is beautiful but not whether renovated) doesn't believe any answer to "has it been renovated?".

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.russian_polarQ_predicted : polarQSentence.isDefined clauseTypeCtx ∧ polarQSentence.ciContent clauseTypeCtx ∧ Data.russian_s'_polarQ.felicitous = true

Per-datum: predicts felicitous for the polar-Q-as-S' examples (Russian 30a, Hungarian 31a, Mandarin 32a).

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.hungarian_polarQ_predicted : polarQSentence.isDefined clauseTypeCtx ∧ polarQSentence.ciContent clauseTypeCtx ∧ Data.hungarian_s'_polarQ.felicitous = true

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.mandarin_polarQ_predicted : polarQSentence.isDefined clauseTypeCtx ∧ polarQSentence.ciContent clauseTypeCtx ∧ Data.mandarin_s'_polarQ.felicitous = true

§ 8: Abstract theorem — interrogative S' trivially satisfies CI

For any context where S supports some QUD answer and S' is an interrogative whose answer the speaker doesn't know, the CI's condition (ii) is satisfied: S' trivially fails to support any answer because Supports requires the doxastic condition (dox ⊆ q), which fails when the speaker doesn't believe any alternative of S'.

This generalises the polar-Q derivation to all interrogative S' examples (30a-d, 31a-d, 32a-d): the specific question content doesn't matter for the CI — only that the speaker doesn't know the answer.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.interrogative_s'_ci_satisfied {W' : Type u_1} (sent : Sentence W') (ctx : Context W') (hSsupports : ∃ α ∈ ctx.qud.alt, IppolitoKissWilliams2022.Supports ctx.dox sent.sDen α ctx.prior) (hNoBelief : ∀ q ∈ sent.s'Den.alt, ¬ctx.dox ⊆ q) (hPartial : ctx.partialAnswers = []) : sent.ciContent ctx