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

@cite{potts-2005} @cite{roberts-2012} @cite{thomas-2026}

Semantics of discourse only: a connective that takes two clausal arguments S and S' and contributes a conventional implicature (CI) that S' fails to support the evidential direction established by prior partial answers to the QUD.

The Puzzle

Cross-linguistically, some languages have a discourse particle glossed as "only" that conjoins two clauses while signaling that the second undermines the evidential trajectory of the first:

• Italian: solo che ("La casa è bella, solo che è costosissima")
• Russian: tol'ko ("Квартира большая, только кухня маленькая")
• Hungarian: csak ("A ház szép, csak drága")
• Mandarin: zhǐshì ("房子很好, 只是太贵了")

Definition 16

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

• At-issue: ⟨⟦S⟧^c, ⟦S'⟧^c⟩ (pair of denotations; for declaratives, modeled as conjunction of highlighted content)
• CI: ∃α ∈ QUD s.t. (i) every true partial answer p ∉ QUD supports α, and (ii) S' does not support α

Key Predictions

• 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_sp ⊆ q fails for all q, and SUPPORT fails. This falls out from fullSupport_fails_unbelieved in Support.lean — no stipulation needed.
• Biased/rhetorical questions CAN be left args (§5.2, exx. 20–21): These questions have a believed answer (DOX_sp ⊆ q for some q), so the doxastic condition is satisfied.
• Comparison with but (§6): Both express contrast, but only's right argument only needs to fail to support (¬SUPPORT), not actively counter-support (negRelevant). This makes only strictly weaker than but.

structure Semantics.Lexical.Particle.DiscourseOnly.Context (W : Type u_1) [Fintype W] : Type u_1

Discourse context for evaluating discourse only.

Includes the QUD, a prior distribution, the speaker's doxastic state, and a record of true partial answers to the QUD established in prior discourse.

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

• qud : Discourse.Issue W

  The QUD as an inquisitive issue

• prior : Questions.ProbabilisticAnswerhood.Prior W

  Prior probability distribution

• dox : Discourse.InfoState W

  Speaker's doxastic state DOX_sp

• worlds : List W

  Worlds for evaluating doxastic subset checks

• partialAnswers : List (W → Bool)

  True partial answers to the QUD established in prior discourse.

  @cite{ippolito-kiss-williams-2025} Def. 16 CI condition (i) quantifies universally over ALL true partial answers p ∉ QUD: each must support the same α. We track these explicitly so the CI can check the universal condition.

• subquestions : List (Discourse.Issue W)

  Subquestions of the QUD established by the discourse context.

  @cite{roberts-2012} Def. 8–9: q is a subquestion of Q iff answering Q (contextually) entails a complete answer to q. @cite{ippolito-kiss-williams-2025} §5.1: "Answering this question requires answering its plausible subquestions, such as Is the house beautiful? Is the house expensive?"

  These are provided by the discourse context, not computed: the contextual entailment relation depends on common ground assumptions (e.g., beauty is a criterion for buying).

structure Semantics.Lexical.Particle.DiscourseOnly.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'.

For declaratives, each Issue has a single alternative (the propositional content). For questions, each Issue has multiple alternatives. The denotation type is uniform — what varies is whether the doxastic condition of SUPPORT can be satisfied.

• sDen : Discourse.Issue W

  Inquisitive denotation of the left argument S

• s'Den : Discourse.Issue W

  Inquisitive denotation of the right argument S'

def Semantics.Lexical.Particle.DiscourseOnly.Sentence.atIssueContent {W : Type u_1} (d : Sentence W) : W → Bool

At-issue content of "S only S'".

@cite{ippolito-kiss-williams-2025} Def. 16: the at-issue content is the pair ⟨⟦S⟧, ⟦S'⟧⟩. For declarative arguments, we model this as conjunction of the highlighted (informational) content of each denotation: every world where both S and S' are informatively true.

Equations

• d.atIssueContent w = (d.sDen.highlighted w && d.s'Den.highlighted w)

def Semantics.Lexical.Particle.DiscourseOnly.Sentence.isDefined {W : Type u_1} [Fintype W] (d : Sentence W) (ctx : Context W) : Bool

Presupposition / definedness condition for discourse only.

@cite{ippolito-kiss-williams-2025} Def. 16: ⟦S [only S']⟧ is defined only if S and S' are "relevant" to the QUD and ∃α ∈ QUD s.t. S supports α.

Relevance is structural, following @cite{roberts-2012} Def. 15 and IKW assumption iii (p. 225): "S is relevant to QUD if S is either a subquestion of QUD or an answer to a subquestion q of QUD."

We decompose the presupposition into three conditions:

1. S is structurally relevant: some alternative of S partially answers the QUD or a subquestion of the QUD (via Discourse.moveRelevant).

2. S' is structurally relevant: same check for the right argument.

3. S supports some answer α via fullSupport (doxastic + probabilistic). This is where the interrogative left-argument restriction falls out: the doxastic condition (Def. 13) blocks info-seeking questions from supporting any answer.

Equations

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

def Semantics.Lexical.Particle.DiscourseOnly.Sentence.ciContent {W : Type u_1} [Fintype W] (d : Sentence W) (ctx : Context W) : Bool

CI content of discourse only.

@cite{ippolito-kiss-williams-2025} Def. 16 CI: ∃α ∈ QUD s.t. (i) ∀p ∈ partialAnswers, p supports α (all prior discourse points toward α) (ii) S' does not SUPPORT α (the right argument fails to support that direction)

Condition (i) captures the universal quantification over true partial answers. When partialAnswers is empty, condition (i) is vacuously true, which is correct: the CI only requires that no prior evidence contradicts the direction.

The "S supports α" condition is implicit in isDefined — if the CI is being evaluated, S already established the direction.

Equations

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

def Semantics.Lexical.Particle.DiscourseOnly.Sentence.meaning {W : Type u_1} [Fintype W] (d : Sentence W) (ctx : Context W) : Expressives.TwoDimProp W

Full two-dimensional meaning of "S only S'".

Combines at-issue content (conjunction of highlighted content) with CI content (S' fails to support an answer that S and prior discourse support). Uses @cite{potts-2005}'s TwoDimProp to keep the dimensions independent.

Equations

• d.meaning ctx = { atIssue := d.atIssueContent, ci := fun (x : W) => d.ciContent ctx }

def Semantics.Lexical.Particle.DiscourseOnly.Sentence.agree {W : Type u_1} [Fintype W] (d : Sentence W) (ctx : Context W) : Bool

Agreement: S and S' agree w.r.t. the QUD iff there is a proposition α ∈ QUD s.t. both S and S' fully support α.

@cite{ippolito-kiss-williams-2025} Def. 14a.

Equations

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

def Semantics.Lexical.Particle.DiscourseOnly.Sentence.disagree {W : Type u_1} [Fintype W] (d : Sentence W) (ctx : Context W) : Bool

Disagreement: S and S' disagree w.r.t. the QUD iff they each support some answer but do not agree on any single answer.

@cite{ippolito-kiss-williams-2025} Def. 14b.

Equations

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

theorem Semantics.Lexical.Particle.DiscourseOnly.atIssue_is_conjunction {W : Type u_1} (d : Sentence W) : d.atIssueContent = fun (w : W) => d.sDen.highlighted w && d.s'Den.highlighted w

At-issue content is conjunction of highlighted content.

theorem Semantics.Lexical.Particle.DiscourseOnly.ci_projects_neg {W : Type u_1} [Fintype W] (d : Sentence W) (ctx : Context W) : (d.meaning ctx).neg.ci = (d.meaning ctx).ci

CI projects through negation (inherited from TwoDimProp).

Negating "S only S'" negates the at-issue conjunction but the CI (S' fails to support the direction) still holds.

theorem Semantics.Lexical.Particle.DiscourseOnly.interrogative_blocks_support {W : Type u_1} [Fintype W] (dox : Discourse.InfoState W) (sentDen : Discourse.Issue W) (prior : Questions.ProbabilisticAnswerhood.Prior W) (answer : W → Bool) (worlds : List W) (hNoBelief : ∀ q ∈ sentDen.alternatives, Discourse.supports dox q worlds = false) : Questions.Support.fullSupport dox sentDen prior answer worlds = false

Interrogative left argument is blocked by the doxastic condition.

When the speaker doesn't believe any alternative of S (DOX_sp ⊄ q for all q ∈ ⟦S⟧), SUPPORT fails for every answer r. This blocks isDefined, because no α ∈ QUD can be supported.

This derives the restriction from the architecture of SUPPORT rather than stipulating it as a clause-type filter. Biased/rhetorical questions, where the speaker DOES believe an answer, correctly pass this check.

theorem Semantics.Lexical.Particle.DiscourseOnly.interrogative_prejacent_satisfies_ci_condition {W : Type u_1} [Fintype W] (dox : Discourse.InfoState W) (s'Den : Discourse.Issue W) (prior : Questions.ProbabilisticAnswerhood.Prior W) (α : W → Bool) (worlds : List W) (hNoBelief : ∀ q ∈ s'Den.alternatives, Discourse.supports dox q worlds = false) : (!decide (Questions.Support.fullSupport dox s'Den prior α worlds = true)) = true

Interrogative prejacents trivially satisfy the CI's condition (ii).

When S' is an info-seeking question whose speaker doesn't believe any answer, fullSupport fails for S', so ¬fullSupport ctx.dox d.s'Den... = true. The prejacent "automatically" fails to support any direction, which is why interrogative prejacents are typically fine cross-linguistically.

This captures IKW §5.2's observation that S' can be interrogative.

theorem Semantics.Lexical.Particle.DiscourseOnly.weak_non_agreement {W : Type u_1} [Fintype W] (d : Sentence W) (ctx : Context W) (hS'noSupport : ∀ α ∈ ctx.qud.alternatives, Questions.Support.fullSupport ctx.dox d.s'Den ctx.prior α ctx.worlds = false) : d.agree ctx = false ∧ d.disagree ctx = false

Weak non-agreement: when S' can't support any answer, S and S' neither agree nor disagree — they "merely don't agree" (@cite{ippolito-kiss-williams-2025} p. 227).

This captures a key prediction about interrogative prejacents. When S' is an info-seeking question, fullSupport fails for S' on every α (doxastic failure). So agree = false (S' can't jointly support any α with S) AND disagree = false (disagree requires S' to support some answer, which it can't). The result is non-agreement without disagreement — a weaker relation than the active clash seen with declarative S'.

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

theorem Semantics.Lexical.Particle.DiscourseOnly.disagree_implies_ciContent_empty_partial {W : Type u_1} [Fintype W] (d : Sentence W) (ctx : Context W) (hDisagree : d.disagree ctx = true) (hPartial : ctx.partialAnswers = []) : d.ciContent ctx = true

Disagreement implies CI content when partial answers are empty.

If S and S' disagree (each supports some answer but don't agree on any single answer) and there are no prior partial answers, then the CI is automatically satisfied.

Proof: disagree = true gives us (1) ∃α: fullSupport S α = true, (2) ∃β: fullSupport S' β = true, (3) ¬agree = for all γ, ¬(fullSupport S γ ∧ fullSupport S' γ). Taking α from (1), fullSupport S α is true. By (3), fullSupport S' α must be false. With empty partial answers, condition (i) is vacuous. So α witnesses the CI.

This captures the paper's core insight: when S and S' evidentially clash (disagree), the CI is inherently satisfied.