[IKW25]: Discourse only

[IKW22] [Pot05] [Rob12]

Formalisation of [IKW25] "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 [IKW22] ("Following Ippolito et al. (2022) we define…"); it lives in 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: [Mer99] is not cited in the paper's reference list, and the §6 only-vs-but discussion grounds itself in [AD77] 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 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 ez 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: the pair ⟨⟦S⟧^c, ⟦S'⟧^c⟩ — the pair structure is what lets interrogative arguments in at all. atIssueContent here is the derived declarative-case notion (intersection of informative content), not the pair itself.
• 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. ciContent also conjoins "S supports α" — a strengthening of the paper's two-clause CI that identifies the CI's α with the answer whose existence the definedness condition requires.

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.
• Rhetorically-interpreted questions can be left-args (§5.2 ex. (20)–(21)). These commit the speaker to an answer (dox ⊆ q for some q), so the doxastic condition is satisfied. Bias alone is not enough: the genuinely biased but still info-seeking high-negation question in ex. (22) is infelicitous as S.

Layout

• Substrate (Sentence, Context, isDefined, ciContent, agree, disagree) and architectural theorems (interrogative_blocks_support, weak_non_agreement, disagree_imp_ciContent_of_empty_partials).
• Account (ClauseType, Interp, Particle, predictLeft, Particle.predictPrejacent): the §7 typology as a derived prediction function — doxastic derivation in left position, per-particle morphosyntactic parameters over the prejacent.
• Examples: the paper's stimuli as LinguisticExamples, imported from the generated Data.Examples.IppolitoKissWilliams2025 module (source of truth: Data/Examples/IppolitoKissWilliams2025.json).
• Part I: end-to-end derivation chains for the house-buying scenario (§7), instantiating the substrate on a concrete 8-world model; these discharge the account's clauses.
• Matrix (Row, matrixRows, misses): the fit theorem misses_eq — the account's only miss across all 40 rows is the %-marked Mandarin (32a).

Discourse context

structure 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 : 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. [IKW25] ex. (16) CI clause (i) quantifies universally over all true partial answers p ∉ QUD.

• subquestions : List (Question W)

  Subquestions of the QUD established by the discourse context. [Rob12] (subquestion strategy); IKW §5.1: provided by the context, not computed.

Sentence

structure 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 : Question W

  Inquisitive denotation of the left argument S.

• s'Den : Question W

  Inquisitive denotation of the right argument S'.

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

Informational at-issue content of S only S': every world where both S and S' are informatively true.

[IKW25] ex. (16) defines the at-issue denotation as the pair ⟨⟦S⟧^c, ⟦S'⟧^c⟩; the intersection here is the derived declarative-case notion, not the paper's pair.

Equations

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

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

Presupposition / definedness condition for discourse only. [IKW25] 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 IppolitoKissWilliams2025.Sentence.ciContent {W : Type u_1} (d : Sentence W) (ctx : Context W) : Prop

CI content of discourse only. [IKW25] ex. (16): ∃ α ∈ QUD such that (i) every true partial answer p with p ∉ QUD is positive evidence for α; (ii) S' does not support α.

The middle conjunct below — S itself supports α — is not in the paper's (16); it is the formaliser's strengthening identifying the CI's α with the answer whose existence the definedness condition already requires. The verbatim version is ciContentPaper; ciContent_imp_ciContentPaper records the entailment.

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 IppolitoKissWilliams2025.Sentence.ciContentPaper {W : Type u_1} (d : Sentence W) (ctx : Context W) : Prop

The paper's ex. (16) CI verbatim: two clauses — (i) every established true partial answer outside the QUD is positive evidence for α; (ii) S' does not support α. ciContent strengthens this with "S supports α"; ciContent_imp_ciContentPaper records the entailment.

Equations

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

theorem IppolitoKissWilliams2025.Sentence.ciContent_imp_ciContentPaper {W : Type u_1} {d : Sentence W} {ctx : Context W} (h : d.ciContent ctx) : d.ciContentPaper ctx

The formaliser's strengthened CI entails the paper's (16) CI.

def 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. [IKW25] ex. (14a).

Equations

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

def 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. [IKW25] ex. (14b).

Equations

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

Architectural derivations

@[simp]

theorem 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 IppolitoKissWilliams2025.interrogative_blocks_support {W : Type u_1} {dox : Set W} {S : Question W} {μ : PMF W} {α : Set W} (h : ∀ q ∈ S.alt, ¬dox ⊆ q) : ¬IppolitoKissWilliams2022.Supports dox S α μ

[IKW25] §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 IppolitoKissWilliams2025.infoSeeking_S_undefined {W : Type u_1} (sent : Sentence W) (ctx : Context W) (h : ∀ q ∈ sent.sDen.alt, ¬ctx.dox ⊆ q) : ¬sent.isDefined ctx

[IKW25] §5.2, definedness half: when the speaker believes no alternative of S (an info-seeking interpretation), the third definedness clause — S supports some QUD answer — fails, so the discourse-only sentence is undefined. Discharges predictLeft .infoSeeking.

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

[IKW25] §5.2: an info-seeking interrogative S' trivially satisfies the CI's condition (ii) — Supports fails for every α, so ¬ Supports … holds.

theorem 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 ([IKW25] §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 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

[IKW25] 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.

The account: clause types, particles, predictions

The §7 typology as a derived prediction function rather than a table. predictLeft is the doxastic derivation, uniform across languages; Particle.predictPrejacent is the per-particle morphosyntactic overlay. Each clause carries a discharge theorem or a flagged stipulation:

• predictLeft .infoSeeking ← infoSeeking_S_undefined
• predictLeft .committed ← core_isDefined/core_ciContent
• prejacent default .acceptable ← interrogative_s'_ci_satisfied (info-seeking S'), rhetorical_s'_negative_route (rhetorical S'), core_ciContent (declarative; imperatives via [Kau12]'s modalized proposition and exclamatives via their propositional component, per §5.3)
• the wired-in-complementizer clause ← wiredIn_blocks_iff (1 bit → 10 cells: solo che (33b–e), csakhogy (31)-alternatives)
• the Mandarin exclamative clause ← stipulated; §7 records the generalization and leaves its mechanism to future research

inductive IppolitoKissWilliams2025.ClauseType : Type

Clause types of the paper's example paradigms — verbatim the parenthetical labels of (5) and (30)–(33).

• declarative : ClauseType
• canonicalPolarQ : ClauseType
• highNegPolarQ : ClauseType
• canonicalWhQ : ClauseType
• negRhetoricalWhQ : ClauseType
• posRhetoricalWhQ : ClauseType
• imperative : ClauseType
• exclamative : ClauseType

@[implicit_reducible]

instance IppolitoKissWilliams2025.instDecidableEqClauseType : DecidableEq ClauseType

Equations

• IppolitoKissWilliams2025.instDecidableEqClauseType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance IppolitoKissWilliams2025.instReprClauseType : Repr ClauseType

Equations

• IppolitoKissWilliams2025.instReprClauseType = { reprPrec := IppolitoKissWilliams2025.instReprClauseType.repr }

def IppolitoKissWilliams2025.instReprClauseType.repr : ClauseType → ℕ → Std.Format

Equations

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

inductive IppolitoKissWilliams2025.Interp : Type

§5.2's analytical cut: left-argument felicity tracks interpretation (speaker-committed vs info-seeking), not clause type — (21) and (22) are the same clause type with opposite judgments.

• committed : Interp
• infoSeeking : Interp

@[implicit_reducible]

instance IppolitoKissWilliams2025.instDecidableEqInterp : DecidableEq Interp

Equations

• IppolitoKissWilliams2025.instDecidableEqInterp x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance IppolitoKissWilliams2025.instReprInterp : Repr Interp

Equations

• IppolitoKissWilliams2025.instReprInterp = { reprPrec := IppolitoKissWilliams2025.instReprInterp.repr }

def IppolitoKissWilliams2025.instReprInterp.repr : Interp → ℕ → Std.Format

Equations

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

def IppolitoKissWilliams2025.ClauseType.defaultInterp : ClauseType → Interp

Default interpretation by clause type. High-negation polar questions are genuinely ambiguous (rhetorical (21) vs biased-info-seeking (22)), so rows of that type carry an explicit interpretation feature; rhetorical wh-questions commit the speaker to an answer, and imperatives/exclamatives carry speaker-committed propositional content (§5.3).

Equations

• IppolitoKissWilliams2025.ClauseType.canonicalPolarQ.defaultInterp = IppolitoKissWilliams2025.Interp.infoSeeking
• IppolitoKissWilliams2025.ClauseType.highNegPolarQ.defaultInterp = IppolitoKissWilliams2025.Interp.infoSeeking
• IppolitoKissWilliams2025.ClauseType.canonicalWhQ.defaultInterp = IppolitoKissWilliams2025.Interp.infoSeeking
• x✝.defaultInterp = IppolitoKissWilliams2025.Interp.committed

structure IppolitoKissWilliams2025.Particle : Type

A discourse-only particle with the two morphosyntactic parameters the §7 typology turns on.

• form : String

  Surface form.

• language : Data.Examples.Glottocode

  Glottocode of the particle's language.

• wiredInComplementizer : Bool

  §7: obligatorily cooccurs with a wired-in declarative complementizer, blocking all non-declarative prejacents.

• blocksExclamativePrejacent : Bool

  Residual stipulation: blocks exclamative prejacents (§7, mechanism left to future research).

@[implicit_reducible]

instance IppolitoKissWilliams2025.instDecidableEqParticle : DecidableEq Particle

Equations

• IppolitoKissWilliams2025.instDecidableEqParticle = IppolitoKissWilliams2025.instDecidableEqParticle.decEq

def IppolitoKissWilliams2025.instDecidableEqParticle.decEq (x✝ x✝¹ : Particle) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance IppolitoKissWilliams2025.instReprParticle : Repr Particle

Equations

• IppolitoKissWilliams2025.instReprParticle = { reprPrec := IppolitoKissWilliams2025.instReprParticle.repr }

def IppolitoKissWilliams2025.instReprParticle.repr : Particle → ℕ → Std.Format

Equations

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

def IppolitoKissWilliams2025.soloChe : Particle

Italian solo che: wired-in declarative complementizer che (§7).

Equations

• IppolitoKissWilliams2025.soloChe = { form := "solo che", language := "ital1282", wiredInComplementizer := true, blocksExclamativePrejacent := false }

def IppolitoKissWilliams2025.tolko : Particle

Russian tol'ko: all clause types as prejacent (30).

Equations

• IppolitoKissWilliams2025.tolko = { form := "tol'ko", language := "russ1263", wiredInComplementizer := false, blocksExclamativePrejacent := false }

def IppolitoKissWilliams2025.csak : Particle

Hungarian csak: all clause types as prejacent (31).

Equations

• IppolitoKissWilliams2025.csak = { form := "csak", language := "hung1274", wiredInComplementizer := false, blocksExclamativePrejacent := false }

def IppolitoKissWilliams2025.csakhogy : Particle

Hungarian csakhogy: wired-in complementizer hogy (§7; "unacceptable in any of the example sentences in (31)").

Equations

• IppolitoKissWilliams2025.csakhogy = { form := "csakhogy", language := "hung1274", wiredInComplementizer := true, blocksExclamativePrejacent := false }

def IppolitoKissWilliams2025.zhishi : Particle

Mandarin zhǐshì: blocks exclamative prejacents (32f).

Equations

• IppolitoKissWilliams2025.zhishi = { form := "zhǐshì", language := "mand1415", wiredInComplementizer := false, blocksExclamativePrejacent := true }

def IppolitoKissWilliams2025.englishOnly : Particle

English discourse only (§1–§2).

Equations

• IppolitoKissWilliams2025.englishOnly = { form := "only", language := "stan1293", wiredInComplementizer := false, blocksExclamativePrejacent := false }

def IppolitoKissWilliams2025.predictLeft : Interp → Features.Judgment

Predicted judgment for a clause in left (S) position: info-seeking interpretations fail the doxastic condition of Supports (infoSeeking_S_undefined) — a #-type pragmatic failure; committed interpretations satisfy it (core_isDefined). Uniform across languages and clause types.

Equations

• IppolitoKissWilliams2025.predictLeft IppolitoKissWilliams2025.Interp.committed = Features.Judgment.acceptable
• IppolitoKissWilliams2025.predictLeft IppolitoKissWilliams2025.Interp.infoSeeking = Features.Judgment.unacceptable

def IppolitoKissWilliams2025.Particle.predictPrejacent (p : Particle) (ct : ClauseType) : Features.Judgment

Predicted judgment for a clause type in prejacent (S′) position: semantically every clause type is fine (interrogative_s'_ci_satisfied, rhetorical_s'_negative_route, core_ciContent); the particle's morphosyntax overlays a *-type block when a wired-in declarative complementizer is present, and the stipulated #-type Mandarin exclamative block.

Equations

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

theorem IppolitoKissWilliams2025.wiredIn_blocks_iff {p : Particle} (hp : p.wiredInComplementizer = true) (ct : ClauseType) : p.predictPrejacent ct = Features.Judgment.ungrammatical ↔ ct ≠ ClauseType.declarative

The wired-in-complementizer parameter blocks exactly the non-declarative prejacents: one bit predicts the solo che (33b–e) and csakhogy ((31)-alternatives) star cells.

Empirical data

The paper's stimuli — English distribution (§1–§2, §5.2) and the §7 cross-linguistic clause-type paradigms (Italian solo che, Russian tol'ko, Hungarian csak, Mandarin zhǐshì) — live as typed LinguisticExamples in Data.Examples.IppolitoKissWilliams2025 (imported above; generated from the paper's JSON). paperFeatures carries the paper's own clause-type labels, the tested argument position, the particle, and (for the ambiguous high-negation rows) the interpretation. The csakhogy variants of (31) live in the alternatives slots.

Part I: End-to-End Derivation Chains

Concrete instantiations on a 8-world model of the house-buying scenario ([IKW25] §7). Connects the substrate predictions to the empirical data in the Examples block above.

§ 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 IppolitoKissWilliams2025.World : Type

Equations

• IppolitoKissWilliams2025.World = Fin 8

def IppolitoKissWilliams2025.beautiful : Set World

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

Equations

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

@[implicit_reducible]

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

Equations

• IppolitoKissWilliams2025.instDecidablePredWorldMemSetBeautiful w = (↑w).decLt 4

def IppolitoKissWilliams2025.expensive : Set World

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

Equations

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

@[implicit_reducible]

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

Equations

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

def IppolitoKissWilliams2025.renovated : Set World

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

Equations

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

@[implicit_reducible]

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

Equations

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

def IppolitoKissWilliams2025.buy : Set World

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

Equations

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

@[implicit_reducible]

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

Equations

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

noncomputable def IppolitoKissWilliams2025.prior : PMF World

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

Equations

• IppolitoKissWilliams2025.prior = PMF.ofFintype (fun (x : IppolitoKissWilliams2025.World) => 1 / 8) IppolitoKissWilliams2025.prior._proof_2

§ 2: QUD and Denotations

def IppolitoKissWilliams2025.qud : Question World

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

Equations

• IppolitoKissWilliams2025.qud = Question.polar IppolitoKissWilliams2025.buy

def IppolitoKissWilliams2025.sBeautiful : Question World

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

Equations

• IppolitoKissWilliams2025.sBeautiful = Question.polar IppolitoKissWilliams2025.beautiful

def IppolitoKissWilliams2025.s'Expensive : Question World

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

Equations

• IppolitoKissWilliams2025.s'Expensive = Question.polar IppolitoKissWilliams2025.expensive

def IppolitoKissWilliams2025.s'RenovatedQ : Question World

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

Equations

• IppolitoKissWilliams2025.s'RenovatedQ = Question.polar IppolitoKissWilliams2025.renovated

§ 3: Doxastic States

def IppolitoKissWilliams2025.doxBE : Set World

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

Equations

• IppolitoKissWilliams2025.doxBE = IppolitoKissWilliams2025.beautiful ∩ IppolitoKissWilliams2025.expensive

def 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

• IppolitoKissWilliams2025.doxB = IppolitoKissWilliams2025.beautiful

§ 4: Contexts

noncomputable def 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 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 IppolitoKissWilliams2025.declSentence : Sentence World

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

Equations

• IppolitoKissWilliams2025.declSentence = { sDen := IppolitoKissWilliams2025.sBeautiful, s'Den := IppolitoKissWilliams2025.s'Expensive }

def IppolitoKissWilliams2025.polarQSentence : Sentence World

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

Equations

• IppolitoKissWilliams2025.polarQSentence = { sDen := IppolitoKissWilliams2025.sBeautiful, s'Den := IppolitoKissWilliams2025.s'RenovatedQ }

§ 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 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 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 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 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 IppolitoKissWilliams2025.rhetorical_s'_negative_route : IppolitoKissWilliams2022.Supports doxBE s'Expensive buyᶜ prior ∧ ¬IppolitoKissWilliams2022.Supports doxBE s'Expensive buy prior ∧ declSentence.ciContent coreCtx

The rhetorical-S′ route to CI clause (ii) ((30d)/(31d)/(32d)): under the committed state doxBE the speaker believes an answer of S' (doxBE ⊆ expensive), so Supports.of_no_belief_fails is unavailable; instead S' supports the negative answer buyᶜ while failing to support buy — disagreement, not silence. Same 8-world model as the declarative core, since denotations are uniform.

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

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

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

§ 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 the info-seeking interrogative S' examples (30a–c, 31a–c, 32a–c): the specific question content doesn't matter for the CI — only that the speaker doesn't know the answer. It does not cover the rhetorical (d) examples: there the speaker believes an answer (dox ⊆ q), so hNoBelief fails; their CI route is via S' supporting the negative answer rather than nothing, which is not formalised here.

theorem 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

The clause-type matrix

The account/fit statement: Row.predicted (the derived account) compared to Row.observed (the paper's judgment) over every example row; the miss locus misses is the primitive, and misses_eq is the fit theorem.

inductive IppolitoKissWilliams2025.Position : Type

Tested argument position.

• left : Position
• right : Position

@[implicit_reducible]

instance IppolitoKissWilliams2025.instDecidableEqPosition : DecidableEq Position

Equations

• IppolitoKissWilliams2025.instDecidableEqPosition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def IppolitoKissWilliams2025.instReprPosition.repr : Position → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance IppolitoKissWilliams2025.instReprPosition : Repr Position

Equations

• IppolitoKissWilliams2025.instReprPosition = { reprPrec := IppolitoKissWilliams2025.instReprPosition.repr }

structure IppolitoKissWilliams2025.Row : Type

A typed matrix row lifted from a LinguisticExample.

• id : String

  The originating example's id (csakhogy alternatives get a suffix).

• particle : Particle
• clauseType : ClauseType
• interp : Interp
• position : Position
• observed : Features.Judgment

  The paper's judgment.

def IppolitoKissWilliams2025.instDecidableEqRow.decEq (x✝ x✝¹ : Row) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance IppolitoKissWilliams2025.instDecidableEqRow : DecidableEq Row

Equations

• IppolitoKissWilliams2025.instDecidableEqRow = IppolitoKissWilliams2025.instDecidableEqRow.decEq

def IppolitoKissWilliams2025.instReprRow.repr : Row → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance IppolitoKissWilliams2025.instReprRow : Repr Row

Equations

• IppolitoKissWilliams2025.instReprRow = { reprPrec := IppolitoKissWilliams2025.instReprRow.repr }

def IppolitoKissWilliams2025.ofExample (e : Data.Examples.LinguisticExample) : Option Row

Lift a LinguisticExample to a matrix Row, reading the clauseType/position/particle (and, where present, interpretation) paperFeatures keys.

Equations

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

def IppolitoKissWilliams2025.ofAlternatives (e : Data.Examples.LinguisticExample) : List Row

The csakhogy rows: the (31) alternatives are the csak → csakhogy substitutions (§7: "unacceptable in any of the example sentences in (31)"), inheriting the host row's clause type and position. The only alternatives in this paper's JSON are these, so the particle is fixed to csakhogy.

Equations

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

def IppolitoKissWilliams2025.matrixRows : List Row

All matrix rows: one per example, plus the csakhogy alternatives.

Equations

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

theorem IppolitoKissWilliams2025.ofExample_total (e : Data.Examples.LinguisticExample) : e ∈ Examples.all → (ofExample e).isSome = true

Adapter totality: every example yields a matrix row.

def IppolitoKissWilliams2025.Row.predicted (r : Row) : Features.Judgment

Predicted judgment for a row: the doxastic derivation in left position, the particle's morphosyntactic overlay over the prejacent.

Equations

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

def IppolitoKissWilliams2025.mandarinPolarQRow : Row

The %-marked Mandarin (32a) row — the account's one miss.

Equations

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

def IppolitoKissWilliams2025.misses : List Row

Rows where the account's prediction differs from the paper's judgment.

Equations

• IppolitoKissWilliams2025.misses = List.filter (fun (r : IppolitoKissWilliams2025.Row) => decide (r.predicted ≠ r.observed)) IppolitoKissWilliams2025.matrixRows

theorem IppolitoKissWilliams2025.misses_eq : misses = [mandarinPolarQRow]

THE matrix theorem: across all 40 rows (34 examples + 6 csakhogy alternatives) the account's only miss is the %-marked Mandarin (32a). A drift sentry: any judgment flip or new mis-predicted row falsifies it.

theorem IppolitoKissWilliams2025.mandarinPolarQ_overpredicted : mandarinPolarQRow.predicted = Features.Judgment.acceptable ∧ mandarinPolarQRow.observed = Features.Judgment.marginal

Direction of the one miss: the account over-predicts (32a) — full felicity where the paper reports speaker variation, for which the account has no mechanism.

theorem IppolitoKissWilliams2025.predicted_eq_observed_iff (r : Row) : r ∈ matrixRows → (r.predicted = r.observed ↔ r ≠ mandarinPolarQRow)

Pointwise corollary of misses_eq.

theorem IppolitoKissWilliams2025.predicted_eqOn : Set.EqOn Row.predicted Row.observed {r : Row | r ∈ matrixRows ∧ r ≠ mandarinPolarQRow}

Set.EqOn form, for mathlib-vocabulary interconnection.