Ippolito, Kiss and Williams (2025): Discourse only

This file formalizes [IKW25], the account of discourse only, the particle of the house is beautiful, only it's too expensive whose prejacent may be a declarative, an interrogative, an imperative or an exclamative. Support, agreement and disagreement are those of [IKW22], with sentences of every clause type denoting sets of propositions, (13) to (15). A context (Context) adds the true partial answers to the question under discussion established in the discourse, and the meaning (16) has a definedness condition, that both arguments are relevant and the left argument supports an answer (Context.Defined), and a conventional implicature (Context.CI): some answer that every established partial answer other than the prejacent supports and the prejacent does not. A canonical question, none of whose answers the speaker believes, supports nothing, so it cannot be the left argument, (19) and (6), while as prejacent it satisfies the second clause of the implicature, (18); a rhetorical or otherwise committed question can be the left argument, (20) and (21). The house-buying context of Section 5 is built explicitly and the declarative and interrogative cases derived in it.

Implementation notes

• The paper's first clause of the implicature quantifies over every true partial answer outside the question under discussion; its prose excludes the prejacent, which the formal statement would contradict, so the exclusion is built in as p ∉ alt S'.
• The implicature "ensures lack of agreement" between the arguments only when the left argument supports no answer but the implicature's, which not_agree_of_ci assumes.
• The cross-linguistic distribution of Section 7 (Italian solo che, Russian tol'ko, Hungarian csak and csakhogy, Mandarin zhǐshì) and the weight asymmetry of Section 6 are recorded as example rows; the paper derives from the semantics only that a left-argument question must be non-canonical.

References

• [IKW25]
• [IKW22]
• [Rob12]
• [AD77]

structure IppolitoKissWilliams2025.Context (W : Type u_2) extends IppolitoKissWilliams2022.Context W : Type u_2

A context for discourse only: the context of [IKW22] with the true partial answers to the question under discussion established in the discourse.

• qud : Question W
• subquestions : Set (Question W)
• dox : Set W
• salient : Set (Set W)
• Evidence : Set W → Set W → Prop
• partialAnswers : Set (Set W)

def IppolitoKissWilliams2025.Context.Defined {W : Type u_1} (c : Context W) (S S' : Question W) : Prop

(16), definedness: both arguments are relevant to the question under discussion and the left argument supports one of its answers.

Equations

• c.Defined S S' = (S.IsRelevantTo c.issues ∧ S'.IsRelevantTo c.issues ∧ ∃ α ∈ c.qud.alt, c.QSupports S α)

def IppolitoKissWilliams2025.Context.CI {W : Type u_1} (c : Context W) (S' : Question W) : Prop

(16), the conventional implicature: some answer to the question under discussion that every established true partial answer outside the question and other than the prejacent supports, and the prejacent does not.

Equations

• c.CI S' = ∃ α ∈ c.qud.alt, (∀ p ∈ c.partialAnswers, p ∉ c.qud.alt → p ∉ S'.alt → c.Supports p α) ∧ ¬c.QSupports S' α

theorem IppolitoKissWilliams2025.Context.not_defined_of_no_belief {W : Type u_1} {c : Context W} {S S' : Question W} (h : ∀ q ∈ S.alt, ¬c.dox ⊆ q) : ¬c.Defined S S'

Section 5.2, (19b) and (6a): a left argument none of whose answers the speaker believes, a canonical question, leaves the sentence undefined.

theorem IppolitoKissWilliams2025.Context.ci_iff_of_no_belief {W : Type u_1} {c : Context W} {S' : Question W} (h : ∀ q ∈ S'.alt, ¬c.dox ⊆ q) : c.CI S' ↔ ∃ α ∈ c.qud.alt, ∀ p ∈ c.partialAnswers, p ∉ c.qud.alt → p ∉ S'.alt → c.Supports p α

(18): a canonical question as prejacent satisfies the second clause of the implicature for every answer, so the implicature reduces to its first clause.

theorem IppolitoKissWilliams2025.Context.not_agree_of_ci {W : Type u_1} {c : Context W} {S S' : Question W} {α : Set W} (hS' : ¬c.QSupports S' α) (hS : ∀ r ∈ c.qud.alt, c.QSupports S r → r = α) : ¬c.Agree (c.QSupports S) (c.QSupports S')

The implicature ensures lack of agreement between the arguments when the left argument supports no answer but the implicature's.

theorem IppolitoKissWilliams2025.Context.disagree_of_ci {W : Type u_1} {c : Context W} {S S' : Question W} {α : Set W} (hα : α ∈ c.qud.alt) (hSα : c.QSupports S α) (hS' : ¬c.QSupports S' α) (hS : ∀ r ∈ c.qud.alt, c.QSupports S r → r = α) (hS'' : ∃ r ∈ c.qud.alt, c.QSupports S' r) : c.Disagree (c.QSupports S) (c.QSupports S')

Section 5.1: when the prejacent supports an answer of its own, the arguments disagree, the special case of lack of agreement.

theorem IppolitoKissWilliams2025.Context.weak_non_agreement {W : Type u_1} {c : Context W} {S S' : Question W} (h : ∀ q ∈ S'.alt, ¬c.dox ⊆ q) : ¬c.Agree (c.QSupports S) (c.QSupports S') ∧ ¬c.Disagree (c.QSupports S) (c.QSupports S')

(18) and the prose of Section 5.2: with a canonical question as prejacent the arguments neither agree nor disagree.

The house-buying context of Section 5

structure IppolitoKissWilliams2025.House.World : Type

A world: whether the house is beautiful, expensive, affordable, and to be bought.

• beautiful : Bool
• expensive : Bool
• afford : Bool
• buy : Bool

@[instance_reducible]

instance IppolitoKissWilliams2025.House.instDecidableEqWorld : DecidableEq World

Equations

• IppolitoKissWilliams2025.House.instDecidableEqWorld = IppolitoKissWilliams2025.House.instDecidableEqWorld.decEq

def IppolitoKissWilliams2025.House.instDecidableEqWorld.decEq (x✝ x✝¹ : World) : Decidable (x✝ = x✝¹)

Equations

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

def IppolitoKissWilliams2025.House.beautiful : Set World

The house is beautiful.

Equations

• IppolitoKissWilliams2025.House.beautiful = {w : IppolitoKissWilliams2025.House.World | w.beautiful = true}

def IppolitoKissWilliams2025.House.expensive : Set World

The house is expensive.

Equations

• IppolitoKissWilliams2025.House.expensive = {w : IppolitoKissWilliams2025.House.World | w.expensive = true}

def IppolitoKissWilliams2025.House.afford : Set World

We can afford the house.

Equations

• IppolitoKissWilliams2025.House.afford = {w : IppolitoKissWilliams2025.House.World | w.afford = true}

def IppolitoKissWilliams2025.House.buy : Set World

We should buy the house.

Equations

• IppolitoKissWilliams2025.House.buy = {w : IppolitoKissWilliams2025.House.World | w.buy = true}

def IppolitoKissWilliams2025.House.Evidence (p r : Set World) : Prop

The evidence of Section 5.1: beauty for buying, expense against.

Equations

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

def IppolitoKissWilliams2025.House.ctx₁₇ : Context World

The context of (17): whether to buy the house is under discussion, with its beauty, its price and its affordability as subquestions; the speaker believes the house beautiful and expensive, and both are established partial answers.

Equations

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

def IppolitoKissWilliams2025.House.ctx₁₈ : Context World

The context of (18): only the beauty of the house has been established.

Equations

• IppolitoKissWilliams2025.House.ctx₁₈ = { toContext := IppolitoKissWilliams2025.House.ctx₁₇.toContext, partialAnswers := {IppolitoKissWilliams2025.House.beautiful} }

def IppolitoKissWilliams2025.House.ctxNeutral : Context World

The context of (6a) and (19b): a speaker neutral about the house's beauty.

Equations

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

theorem IppolitoKissWilliams2025.House.defined₁₇ : ctx₁₇.Defined (Question.ofSet beautiful) (Question.ofSet expensive)

(17): the house is beautiful, only it's too expensive is defined.

theorem IppolitoKissWilliams2025.House.ci₁₇ : ctx₁₇.CI (Question.ofSet expensive)

(17): its implicature holds with buying as the answer beauty supports and expense does not.

theorem IppolitoKissWilliams2025.House.disagree₁₇ : ctx₁₇.Disagree (ctx₁₇.QSupports (Question.ofSet beautiful)) (ctx₁₇.QSupports (Question.ofSet expensive))

(17): the two arguments disagree, expense supporting not buying.

theorem IppolitoKissWilliams2025.House.defined_ci₁₈ : ctx₁₈.Defined (Question.ofSet beautiful) (Question.polar afford) ∧ ctx₁₈.CI (Question.polar afford)

(18): the house is beautiful, only can we afford it? is defined and carries its implicature, the canonical question supporting nothing.

theorem IppolitoKissWilliams2025.House.weak₁₈ : ¬ctx₁₈.Agree (ctx₁₈.QSupports (Question.ofSet beautiful)) (ctx₁₈.QSupports (Question.polar afford)) ∧ ¬ctx₁₈.Disagree (ctx₁₈.QSupports (Question.ofSet beautiful)) (ctx₁₈.QSupports (Question.polar afford))

(18): the arguments neither agree nor disagree.

theorem IppolitoKissWilliams2025.House.not_defined_neutral : ¬ctxNeutral.Defined (Question.polar beautiful) (Question.ofSet expensive)

(6a) and (19b): a speaker neutral about the house's beauty cannot ask whether it is beautiful as the left argument.

theorem IppolitoKissWilliams2025.House.defined_rhetorical : ctx₁₇.Defined (Question.polar beautiful) (Question.ofSet expensive)

(6b) and (21): read rhetorically, by a speaker committed to the house's beauty, the same question is a fine left argument.