Ippolito, Kiss and Williams (2022): The Discourse Function of Adversative Conjunction

This file formalizes [IKW22], the account of Italian ma and English but introducing a single declarative or interrogative clause. A context (Context) fixes the question under discussion, the speaker's doxastic state, the propositions made salient by previous moves, and the evidence relation of [BG00] and [Gun08] that the paper leaves informal. A salient proposition supports an answer to the question under discussion when it provides evidence for it, (15) (Context.Supports); a question uttered by the speaker supports an answer when some answer to it that the speaker believes provides evidence for it, (21) (Context.QSupports). Two moves agree when they support a common answer and disagree when each supports an answer but no common one, (16), (17), (22) and (23). Discourse ma requires a salient relevant proposition that does not agree with its argument, (18) and (24) (Context.Ma), and but one that disagrees with it, (29) and (34) (Context.But). The table of question types follows: with nothing salient neither particle is licensed; a question none of whose answers the speaker believes, on the ignorance reading or with the negative bias, supports nothing, so ma is licensed by any salient relevant proposition and but by none; and a negative polar question whose believed answer supports the opposite answer from the salient proposition disagrees with it and licenses both.

Implementation notes

• Relevance to the question under discussion, which the paper does not define, is the substrate's Question.IsRelevantTo to the question under discussion together with the subquestions of its strategy, as the sequel [IKW25] assumes.
• A declarative argument of ma or but is asserted, so its support is that of the singleton question: belief plus evidence (Section 3.2.3).
• The amended notion of support (45), on which the interrogative speech act itself provides evidence, is not formalized.

References

• [IKW22]
• [BG00]
• [Gun08]
• [Rob12]

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

A discourse context: the question under discussion, the subquestions of its strategy, the speaker's doxastic state, the propositions made salient by previous verbal or non-verbal moves, and the evidence relation, Evidence p r when p provides evidence for r in the context.

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

def IppolitoKissWilliams2022.Context.issues {W : Type u_1} (c : Context W) : Set (Question W)

The questions a move must be relevant to: the question under discussion and the subquestions of its strategy.

Equations

• c.issues = insert c.qud c.subquestions

def IppolitoKissWilliams2022.Context.Supports {W : Type u_1} (c : Context W) (p r : Set W) : Prop

(15): a proposition supports an answer to the question under discussion when it provides evidence for it.

Equations

• c.Supports p r = c.Evidence p r

def IppolitoKissWilliams2022.Context.QSupports {W : Type u_1} (c : Context W) (S : Question W) (r : Set W) : Prop

(21): a question uttered by the speaker supports an answer when some answer to it that the speaker believes provides evidence for it.

Equations

• c.QSupports S r = ∃ q ∈ S.alt, c.dox ⊆ q ∧ c.Evidence q r

def IppolitoKissWilliams2022.Context.Agree {W : Type u_1} (c : Context W) (s t : Set W → Prop) : Prop

(16) and (22): two moves, given by what they support, agree when they support a common answer to the question under discussion.

Equations

• c.Agree s t = ∃ r ∈ c.qud.alt, s r ∧ t r

def IppolitoKissWilliams2022.Context.Disagree {W : Type u_1} (c : Context W) (s t : Set W → Prop) : Prop

(17) and (23): two moves disagree when each supports an answer but no common one.

Equations

• c.Disagree s t = ((∃ r ∈ c.qud.alt, s r) ∧ (∃ r ∈ c.qud.alt, t r) ∧ ¬c.Agree s t)

def IppolitoKissWilliams2022.Context.Ma {W : Type u_1} (c : Context W) (S : Question W) : Prop

(18) and (24): discourse ma with a declarative or interrogative argument is defined when the argument is relevant and some salient relevant proposition does not agree with it.

Equations

• c.Ma S = (S.IsRelevantTo c.issues ∧ ∃ p ∈ c.salient, (Question.ofSet p).IsRelevantTo c.issues ∧ ¬c.Agree (c.Supports p) (c.QSupports S))

def IppolitoKissWilliams2022.Context.But {W : Type u_1} (c : Context W) (S : Question W) : Prop

(29) and (34): discourse but is defined when some salient relevant proposition disagrees with its argument.

Equations

• c.But S = (S.IsRelevantTo c.issues ∧ ∃ p ∈ c.salient, (Question.ofSet p).IsRelevantTo c.issues ∧ c.Disagree (c.Supports p) (c.QSupports S))

theorem IppolitoKissWilliams2022.Context.Agree.symm {W : Type u_1} {c : Context W} {s t : Set W → Prop} (h : c.Agree s t) : c.Agree t s

theorem IppolitoKissWilliams2022.Context.Disagree.symm {W : Type u_1} {c : Context W} {s t : Set W → Prop} (h : c.Disagree s t) : c.Disagree t s

theorem IppolitoKissWilliams2022.Context.Disagree.not_agree {W : Type u_1} {c : Context W} {s t : Set W → Prop} (h : c.Disagree s t) : ¬c.Agree s t

Disagreement is the stronger relation.

theorem IppolitoKissWilliams2022.Context.Ma.of_but {W : Type u_1} {c : Context W} {S : Question W} (h : c.But S) : c.Ma S

but is licensed only where ma is.

@[simp]

theorem IppolitoKissWilliams2022.Context.qSupports_ofSet_iff {W : Type u_1} {c : Context W} {q r : Set W} : c.QSupports (Question.ofSet q) r ↔ c.dox ⊆ q ∧ c.Evidence q r

A declarative argument supports an answer when the speaker believes it and it provides evidence for the answer (Section 3.2.3).

theorem IppolitoKissWilliams2022.Context.not_qSupports_of_no_belief {W : Type u_1} {c : Context W} {S : Question W} (h : ∀ q ∈ S.alt, ¬c.dox ⊆ q) (r : Set W) : ¬c.QSupports S r

A question none of whose answers the speaker believes supports nothing: the ignorance reading and the negative bias alike.

theorem IppolitoKissWilliams2022.Context.not_ma_of_salient_empty {W : Type u_1} {c : Context W} {S : Question W} (h : c.salient = ∅) : ¬c.Ma S

Out of the blue, with nothing salient, ma is not licensed (BAKERY, (7) and (36)).

theorem IppolitoKissWilliams2022.Context.not_but_of_salient_empty {W : Type u_1} {c : Context W} {S : Question W} (h : c.salient = ∅) : ¬c.But S

Nor is but.

theorem IppolitoKissWilliams2022.Context.ma_of_no_belief {W : Type u_1} {c : Context W} {S : Question W} (hS : S.IsRelevantTo c.issues) (h : ∀ q ∈ S.alt, ¬c.dox ⊆ q) {p : Set W} (hp : p ∈ c.salient) (hr : (Question.ofSet p).IsRelevantTo c.issues) : c.Ma S

With a question the speaker has no belief about, ma is licensed by any salient relevant proposition: HELP, TWIN SISTERS, NIGHT and KEY, (26), (27), (28) and (35).

theorem IppolitoKissWilliams2022.Context.not_but_of_no_belief {W : Type u_1} {c : Context W} {S : Question W} (h : ∀ q ∈ S.alt, ¬c.dox ⊆ q) : ¬c.But S

With such a question but is never licensed: (31), (32), (33) and (37).

theorem IppolitoKissWilliams2022.Context.not_ma_of_agree {W : Type u_1} {c : Context W} {S : Question W} (h : ∀ p ∈ c.salient, c.Agree (c.Supports p) (c.QSupports S)) : ¬c.Ma S

The second argument of Section 3.3, (38): a question biased toward an answer that supports what every salient proposition supports agrees with them all, and ma is not licensed.

theorem IppolitoKissWilliams2022.Context.but_of_polar {W : Type u_1} {c : Context W} {S : Question W} {α : Set W} (hqud : c.qud = Question.polar α) (hne : α ≠ ∅) (hnu : α ≠ Set.univ) (hS : S.IsRelevantTo c.issues) {p : Set W} (hp : p ∈ c.salient) (hr : (Question.ofSet p).IsRelevantTo c.issues) (hpα : c.Evidence p α) (hpα' : ¬c.Evidence p αᶜ) (hq : ∃ q ∈ S.alt, c.dox ⊆ q) (hS' : ∀ q ∈ S.alt, c.dox ⊆ q → c.Evidence q αᶜ ∧ ¬c.Evidence q α) : c.But S

VEGETARIAN, (25) and (30): with a polar question under discussion, a salient proposition supporting one answer and a question whose believed answers support the other disagree, so both particles are licensed.

theorem IppolitoKissWilliams2022.Context.ma_of_polar {W : Type u_1} {c : Context W} {S : Question W} {α : Set W} (hqud : c.qud = Question.polar α) (hne : α ≠ ∅) (hnu : α ≠ Set.univ) (hS : S.IsRelevantTo c.issues) {p : Set W} (hp : p ∈ c.salient) (hr : (Question.ofSet p).IsRelevantTo c.issues) (hpα : c.Evidence p α) (hpα' : ¬c.Evidence p αᶜ) (hq : ∃ q ∈ S.alt, c.dox ⊆ q) (hS' : ∀ q ∈ S.alt, c.dox ⊆ q → c.Evidence q αᶜ ∧ ¬c.Evidence q α) : c.Ma S

VEGETARIAN, (25) and (30)

structure IppolitoKissWilliams2022.Vegetarian.World : Type

A world: whether Mia was vegetarian, has ordered a steak, and will eat meat.

• veg : Bool
• steak : Bool
• meat : Bool

def IppolitoKissWilliams2022.Vegetarian.instDecidableEqWorld.decEq (x✝ x✝¹ : World) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance IppolitoKissWilliams2022.Vegetarian.instDecidableEqWorld : DecidableEq World

Equations

• IppolitoKissWilliams2022.Vegetarian.instDecidableEqWorld = IppolitoKissWilliams2022.Vegetarian.instDecidableEqWorld.decEq

def IppolitoKissWilliams2022.Vegetarian.veg : Set World

Mia was vegetarian.

Equations

• IppolitoKissWilliams2022.Vegetarian.veg = {w : IppolitoKissWilliams2022.Vegetarian.World | w.veg = true}

def IppolitoKissWilliams2022.Vegetarian.steak : Set World

Mia has ordered a steak.

Equations

• IppolitoKissWilliams2022.Vegetarian.steak = {w : IppolitoKissWilliams2022.Vegetarian.World | w.steak = true}

def IppolitoKissWilliams2022.Vegetarian.meat : Set World

Mia will eat meat.

Equations

• IppolitoKissWilliams2022.Vegetarian.meat = {w : IppolitoKissWilliams2022.Vegetarian.World | w.meat = true}

def IppolitoKissWilliams2022.Vegetarian.ctx : Context World

Carla's context: whether Mia will eat meat is under discussion, with whether she was vegetarian and whether she ordered a steak as subquestions; Carla believes Mia was vegetarian; the steak order is salient; the order is evidence that Mia will eat meat and vegetarianism evidence that she will not.

Equations

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

theorem IppolitoKissWilliams2022.Vegetarian.but : ctx.But (Question.polar veg)

Carla's negative polar question weren't you vegetarian? disagrees with the salient steak order, so but is licensed.

theorem IppolitoKissWilliams2022.Vegetarian.ma : ctx.Ma (Question.polar veg)

And so is ma.