Discourse only

@cite{ippolito-kiss-williams-2025} @cite{merin-1999}

Part I: End-to-End Derivation Chains

Concrete instantiations of the discourse only theory (@cite{ippolito-kiss-williams-2025} Def. 16) that derive the acceptability of specific cross-linguistic examples.

Architecture

The discourse only theory (in Lexical/Particle/DiscourseOnly.lean) defines isDefined and ciContent as computable Bool functions over abstract types. This file instantiates those functions with a concrete 8-world model of the house-buying scenario used throughout IKW §7, then proves that the theory's predictions match the empirical data in Phenomena/Focus/DiscourseOnly.lean.

The House Model

8 worlds varying on three binary properties: beautiful, expensive, renovated. The QUD "Should we buy the house?" is answered affirmatively only when the house is beautiful, affordable, AND renovated (w₀). This ensures:

• "beautiful" supports buying (P(buy|beautiful) > P(buy))
• "expensive" anti-supports buying (P(buy|expensive) = 0)
• "renovated" is relevant to buying (P(buy|renovated) > P(buy))

Derivation Chains

Each derivation theorem proves:

1. isDefined = true (the presupposition is satisfied)
2. ciContent = true (the CI holds: S supports α but S' doesn't)
3. These match the datum's felicitous = true

For interrogative S' examples (30a, 31a, etc.), the derivation shows that the speaker's uncertainty about the answer blocks fullSupport for S' on all QUD answers, trivially satisfying the CI's condition (ii).

Part II: DTS Connection

Connects the CI of discourse only to @cite{merin-1999}'s Decision-Theoretic Semantics, specifically the notion of unexpectedness from the analysis of but.

Key Connection

Both but and discourse only express a form of evidential contrast:

• but: A is positively relevant and B is negatively relevant to H → B is unexpected given A (Theorem 8)
• discourse only: S supports α but S' does not support α → S' undermines the evidential direction

The but/only Asymmetry (@cite{ippolito-kiss-williams-2025} §6)

but requires negRelevant (BF < 1): the second clause must actively provide counter-evidence. Discourse only only requires ¬probSupports: the second clause merely fails to support the direction. Since negRelevant → ¬probSupports (anti-support implies non-support), but's condition is strictly stronger. This means every but context could license discourse only, but not vice versa.

@[reducible, inline]

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

8-world model for the house-buying scenario.

Encoding: w = 4b + 2e + r where

• b ∈ {0,1}: beauty (0 = beautiful)
• e ∈ {0,1}: expense (0 = affordable)
• r ∈ {0,1}: renovation (0 = renovated)

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

Equations

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

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.beautiful : W → Bool

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

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.beautiful w = decide (↑w < 4)

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.expensive : W → Bool

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

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.expensive w = (↑w / 2 % 2 == 1)

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.renovated : W → Bool

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

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.renovated w = (↑w % 2 == 0)

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.buy : W → Bool

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

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.buy w = (↑w == 0)

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.prior : Semantics.Questions.ProbabilisticAnswerhood.Prior W

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

Equations

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

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.worlds : List W

All worlds for doxastic subset checks.

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.worlds = List.finRange 8

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.qud : Discourse.Issue W

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

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.qud = Discourse.Issue.polar Phenomena.Focus.Studies.IppolitoKissWilliams2025.buy

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.sBeautiful : Discourse.Issue W

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

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.sBeautiful = { alternatives := [Phenomena.Focus.Studies.IppolitoKissWilliams2025.beautiful] }

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.s'Expensive : Discourse.Issue W

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

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.s'Expensive = { alternatives := [Phenomena.Focus.Studies.IppolitoKissWilliams2025.expensive] }

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.s'RenovatedQ : Discourse.Issue W

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

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.s'RenovatedQ = Discourse.Issue.polar Phenomena.Focus.Studies.IppolitoKissWilliams2025.renovated

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.doxBE : Discourse.InfoState W

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

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.doxBE w = (Phenomena.Focus.Studies.IppolitoKissWilliams2025.beautiful w && Phenomena.Focus.Studies.IppolitoKissWilliams2025.expensive w)

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.doxB : Discourse.InfoState W

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

Equations

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

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.coreCtx : Semantics.Lexical.Particle.DiscourseOnly.Context W

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.

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.clauseTypeCtx : Semantics.Lexical.Particle.DiscourseOnly.Context W

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.

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.declSentence : Semantics.Lexical.Particle.DiscourseOnly.Sentence W

"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 : Semantics.Lexical.Particle.DiscourseOnly.Sentence W

"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.

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

The presupposition is satisfied: S' is relevant and S supports an answer.

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

The CI holds: ∃α (= buy) s.t. all partial answers support α (vacuous), S supports α, and S' does not support α.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.core_atIssue_nonempty : declSentence.atIssueContent 2 = true

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 = true

S and S' disagree w.r.t. the QUD: S supports "buy" but S' supports "don't buy", and they don't agree on any single answer.

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

Per-datum connection: the theory predicts felicitous for the core examples.

Each core example (Italian 29a, Russian 29b, Hungarian 29c, Mandarin 29d, English 2) instantiates this same semantic scenario.

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

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

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

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

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

The presupposition is satisfied even with interrogative S': the polar Q "has it been renovated?" has alternatives [renovated, ¬renovated], and knowing whether the house is renovated is relevant to buying.

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

The CI holds: the speaker believes the house is beautiful, so S supports "buy". But the speaker doesn't know the answer to "has it been renovated?", so the doxastic condition of fullSupport fails for S' on every QUD answer. S' trivially fails to support the buying direction.

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

Per-datum: predicts felicitous for all polar Q S' examples.

Russian 30a, Hungarian 31a, and Mandarin 32a all instantiate this scenario.

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

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

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.interrogative_s'_ci_satisfied {W' : Type u_1} [Fintype W'] (sent : Semantics.Lexical.Particle.DiscourseOnly.Sentence W') (ctx : Semantics.Lexical.Particle.DiscourseOnly.Context W') (hSsupports : (ctx.qud.alternatives.any fun (α : Discourse.InfoState W') => Semantics.Questions.Support.fullSupport ctx.dox sent.sDen ctx.prior α ctx.worlds) = true) (hNoBelief : ∀ q ∈ sent.s'Den.alternatives, Discourse.supports ctx.dox q ctx.worlds = false) (hPartial : ctx.partialAnswers = []) : sent.ciContent ctx = true

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 fullSupport requires the doxastic condition (DOX_sp ⊆ q), which fails when the speaker doesn't believe any alternative of S'.

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

def Phenomena.Focus.Studies.IppolitoKissWilliams2025.dtsToInquisitive {W : Type u_1} (topic : BProp W) : Discourse.Issue W

Convert a DTS dichotomic issue {H, ¬H} to an inquisitive Issue.

A DTS Issue W is a single topic H (with ¬H implicit). The corresponding inquisitive issue has two alternatives: H and ¬H.

Equations

• Phenomena.Focus.Studies.IppolitoKissWilliams2025.dtsToInquisitive topic = Discourse.Issue.polar topic

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.dtsToInquisitive_alternatives {W : Type u_1} (topic : BProp W) : (dtsToInquisitive topic).alternatives = [topic, fun (w : W) => !topic w]

The DTS issue and inquisitive issue have matching alternatives.

structure Phenomena.Focus.Studies.IppolitoKissWilliams2025.DTSDiscourseOnlyWitness (W : Type u_1) [Fintype W] : Type u_1

A witness for the discourse only → DTS unexpectedness connection.

Bundles a DTS context, a discourse only configuration (as raw propositions for the binary case), and evidence that S is positively relevant to the topic H. Unlike the but witness, this does NOT require S' to be negatively relevant — discourse only only requires S' to fail to support, which is strictly weaker than negative relevance.

• dtsCtx : Theories.DTS.DTSContext W

  The DTS context (dichotomic issue H + prior)

• s : W → Bool

  Left clausal argument S (as a proposition for the binary case)

• s' : W → Bool

  Right clausal argument S' (as a proposition for the binary case)

• sPosRelevant : Theories.DTS.posRelevant self.dtsCtx self.s

  S is positively relevant to H

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.probSupports_implies_posRelevant_binary {W : Type u_1} [Fintype W] (prior : Semantics.Questions.ProbabilisticAnswerhood.Prior W) (topic : BProp W) (evidence : W → Bool) (hH_pos : Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior topic > 0) (hNH_pos : (Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior fun (w : W) => !topic w) > 0) (hS_pos : Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior evidence > 0) (hNonneg : ∀ (w : W), prior.mass w ≥ 0) (hNorm : (Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior fun (x : W) => true) = 1) : Semantics.Questions.Support.probSupports prior evidence topic = true → Theories.DTS.posRelevant { issue := { topic := topic }, prior := prior.mass } evidence

For binary issues, probabilistic probSupports (P(H|S) > P(H)) implies DTS posRelevant (BF_H(S) > 1).

Both capture the same intuition — S provides evidence for H — but via different formalizations: probSupports uses the absolute probability boost, while posRelevant uses the Bayes factor ratio.

The bridge is Bayes' theorem: P(H|S) > P(H) ↔ P(S∧H) > P(H)·P(S) (multiply by P(S) > 0) ↔ P(S∧H)·(1−P(H)) > P(H)·P(S∧¬H) (partition P(S), expand) ↔ P(S∧H)·P(¬H) > P(H)·P(S∧¬H) (normalization: P(¬H) = 1−P(H)) ↔ P(S|H) > P(S|¬H) (divide by P(H)P(¬H)) ↔ BF > 1.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.negRelevant_implies_not_probSupports {W : Type u_1} [Fintype W] (prior : Semantics.Questions.ProbabilisticAnswerhood.Prior W) (topic : BProp W) (evidence : W → Bool) (hH_pos : Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior topic > 0) (hNH_pos : (Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior fun (w : W) => !topic w) > 0) (hS_pos : Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior evidence > 0) (hNonneg : ∀ (w : W), prior.mass w ≥ 0) (hNorm : (Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior fun (x : W) => true) = 1) (hNeg : Theories.DTS.negRelevant { issue := { topic := topic }, prior := prior.mass } evidence) : Semantics.Questions.Support.probSupports prior evidence topic = false

Negative relevance (DTS) implies non-support (probabilistic).

If S' is negatively relevant to H (BF < 1, i.e., P(S'|H) < P(S'|¬H)), then S' does not probabilistically support H. This is the formal content of IKW's observation that but's condition on the second clause is strictly stronger than discourse only's.

By contrapositive: if probSupports were true, Bayes' theorem would give posRelevant (BF > 1), contradicting negRelevant (BF < 1).

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.but_sufficient_for_only {W : Type u_1} [Fintype W] (prior : Semantics.Questions.ProbabilisticAnswerhood.Prior W) (topic : BProp W) (s s' : W → Bool) (hH_pos : Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior topic > 0) (hNH_pos : (Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior fun (w : W) => !topic w) > 0) (_hS_pos : Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior s > 0) (hS'_pos : Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior s' > 0) (_hSpos : Theories.DTS.posRelevant { issue := { topic := topic }, prior := prior.mass } s) (hS'neg : Theories.DTS.negRelevant { issue := { topic := topic }, prior := prior.mass } s') (hNonneg : ∀ (w : W), prior.mass w ≥ 0) (hNorm : (Semantics.Questions.ProbabilisticAnswerhood.probOfProp prior fun (x : W) => true) = 1) : Semantics.Questions.Support.probSupports prior s' topic = false

Every but context can license discourse only.

When S is posRelevant and S' is negRelevant (the but condition), S' also fails to probabilistically support H (the only condition). This formalizes @cite{ippolito-kiss-williams-2025} §6's claim that discourse only is strictly weaker than but.

theorem Phenomena.Focus.Studies.IppolitoKissWilliams2025.discOnly_implies_unexpectedness_under_but {W : Type u_1} [Fintype W] (w : DTSDiscourseOnlyWitness W) (hS'neg : Theories.DTS.negRelevant w.dtsCtx w.s') (hPrior : ∀ (x : W), w.dtsCtx.prior x ≥ 0) (hNorm : Theories.DTS.probSum w.dtsCtx.prior (Core.Proposition.Decidable.top W) = 1) (hS_pos : 0 < Theories.DTS.probSum w.dtsCtx.prior w.s) (hH_pos : 0 < Theories.DTS.probSum w.dtsCtx.prior w.dtsCtx.issue.topic) (hNH_pos : 0 < Theories.DTS.probSum w.dtsCtx.prior (Core.Proposition.Decidable.pnot W w.dtsCtx.issue.topic)) (hCIP : Theories.DTS.CIP w.dtsCtx w.s w.s') : Theories.DTS.condProb w.dtsCtx.prior w.s' w.s < Theories.DTS.margProb w.dtsCtx.prior w.s'

Discourse only's CI implies unexpectedness when the QUD is binary, S' is negatively relevant, and CIP holds.

When S is posRelevant and S' is negRelevant (the stronger but condition), Merin's Theorem 8 gives P(S'|S) < P(S'): S' is unexpected given S.

Note: this theorem uses the stronger but condition (negRelevant) rather than the weaker discourse only condition (¬probSupports). Unexpectedness in Merin's sense requires active counter-relevance, not just failure to support. This means unexpectedness is a consequence when discourse only sentences happen to meet the stronger but threshold.