Roelofsen and Farkas (2015): Polarity particle responses as a window onto the interpretation of questions and assertions

This file formalizes [RF15]'s account of polarity particle responses. A response carries a relative feature, [agree] or [reverse], and an absolute feature, [+] or [−], each presupposing something of the possibilities its prejacent and its antecedent highlight; together they fix what the response expresses (absolutePresup_and_relativePresup_iff). So yes, it is conveys the even answer after Is it even? and the odd one after Is it odd? (presup_query_ofPolarity), and on a response sharing its antecedent's radical the relative feature is Farkas and Bruce's relative polarity (relativePresup_smul_iff).

Languages differ in which particles realize which features, and a particle dedicated to a combination blocks the others. English yes and no each realize a natural class of features, so both occur in responses to a negative antecedent (english_usable), while French si and German doch realize [reverse, +] alone. The account agrees with what Farkas and Bruce say the English particles mark (usable_english_iff_mem).

Implementation notes

• The most salient antecedent possibility is the one the antecedent formula highlights; the discourse context of the paper is not modelled.
• Features are polarities, [agree] and [+] being positive, so the prejacent of a relative feature r highlights r • β for the antecedent possibility β.
• In the planets examples odd is the complement of even, so each proposition is recorded as the polarity whose action yields it from even.
• French (9) prints its French sentences in the opposite order to their glosses; the French rows are (119)–(122).

TODO

• The Romanian and Hungarian systems of §5.1, and the preferences among realizable particles, which rest on markedness, are not formalized.

References

• [RF15]
• [FB10]
• [RvG10]

Polarity features (§4.1)

def RoelofsenFarkas2015.AbsolutePresup {W : Type u_1} (s : Polarity) (q : Question W) (H : Set (Polarity × Set W)) : Prop

The absolute feature s presupposes that the prejacent expresses a proposition q with a single possibility, which it highlights with polarity s (68), (69).

Equations

• RoelofsenFarkas2015.AbsolutePresup s q H = ∃ (α : Set W), q = Question.ofSet α ∧ H = {(s, α)}

def RoelofsenFarkas2015.RelativePresup {W : Type u_1} (r : Polarity) (H ant : Set (Polarity × Set W)) : Prop

The relative feature r, [agree] when positive and [reverse] when negative, presupposes that the antecedent highlights a unique possibility and that the prejacent highlights its image under r, the same possibility with the same polarity or its complement with the opposite polarity (70), (71).

Equations

• RoelofsenFarkas2015.RelativePresup r H ant = ∃ (β : Polarity × Set W), ant = {β} ∧ H = {r • β}

theorem RoelofsenFarkas2015.absolutePresup_and_relativePresup_iff {W : Type u_1} {r s : Polarity} {q : Question W} {H ant : Set (Polarity × Set W)} : AbsolutePresup s q H ∧ RelativePresup r H ant ↔ ∃ (α : Set W), ant = {(r * s, α)} ∧ q = Question.ofSet (r • α) ∧ H = {(s, r • α)}

An absolute feature s and a relative feature r together presuppose that the antecedent highlights a single possibility, of polarity r * s, and that the prejacent expresses its image under r, highlighted with polarity s (72)–(75).

theorem RoelofsenFarkas2015.relativePresup_smul_iff {W : Type u_1} {r s t : Polarity} (x : Polarity × Set W) : RelativePresup r {s • x} {t • x} ↔ r = s / t

On a prejacent of polarity s sharing the radical of an antecedent of polarity t, the two highlighting the images of one possibility x under s and t, the relative feature is the relative polarity of [FB10] (Discourse.Response.relative): [agree] iff s = t.

The questions of §3.3

theorem RoelofsenFarkas2015.proposition_query_even_eq_odd {W : Type u_1} {A : Type u_2} (v : A → Set W) {e o : A} (hodd : v o = (v e)ᶜ) : Highlighting.Formula.proposition v (Highlighting.Formula.atom e).query = Highlighting.Formula.proposition v (Highlighting.Formula.atom o).query

Is the number of planets even? and Is it odd? express the same issue.

theorem RoelofsenFarkas2015.presup_query_ofPolarity {W : Type u_1} {A : Type u_2} (v : A → Set W) {r s t : Polarity} (a : A) {q : Question W} {H : Set (Polarity × Set W)} (h : AbsolutePresup s q H ∧ RelativePresup r H (Highlighting.Formula.highlights v (Highlighting.Formula.ofPolarity t a).query)) : q = Question.ofSet (s • v a) ∧ r = s / t

A response of polarity s to a polar question of polarity t on a expresses s • v a, with the relative feature s / t: yes, it is conveys the even answer after Is it even? and the odd one after Is it odd?, and no, it isn't conveys that the number is not odd after Is it odd? and that it is not even after Is it not even? (49), (50), (52), (53).

theorem RoelofsenFarkas2015.not_relativePresup_disj {W : Type u_1} {A : Type u_2} (v : A → Set W) {e o : A} [Nonempty W] (hodd : v o = (v e)ᶜ) (r : Polarity) (H : Set (Polarity × Set W)) : ¬RelativePresup r H (Highlighting.Formula.highlights v ((Highlighting.Formula.atom e).inqDisj (Highlighting.Formula.atom o)))

The alternative question Is it even↑, or odd↓? highlights two possibilities, so no relative feature, and no particle response, is licensed after it (51).

Realization (§4.2, §5.2)

inductive RoelofsenFarkas2015.Feature : Type

A polarity feature is relative, [agree] when positive and [reverse] when negative, or absolute, [+] or [−].

• relative (r : Polarity) : Feature
• absolute (s : Polarity) : Feature

@[instance_reducible]

instance RoelofsenFarkas2015.instDecidableEqFeature : DecidableEq Feature

Equations

• RoelofsenFarkas2015.instDecidableEqFeature = RoelofsenFarkas2015.instDecidableEqFeature.decEq

def RoelofsenFarkas2015.instDecidableEqFeature.decEq (x✝ x✝¹ : Feature) : Decidable (x✝ = x✝¹)

Equations

• RoelofsenFarkas2015.instDecidableEqFeature.decEq (RoelofsenFarkas2015.Feature.relative a) (RoelofsenFarkas2015.Feature.relative b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqFeature.decEq (RoelofsenFarkas2015.Feature.relative r) (RoelofsenFarkas2015.Feature.absolute s) = isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqFeature.decEq (RoelofsenFarkas2015.Feature.absolute s) (RoelofsenFarkas2015.Feature.relative r) = isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqFeature.decEq (RoelofsenFarkas2015.Feature.absolute a) (RoelofsenFarkas2015.Feature.absolute b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def RoelofsenFarkas2015.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance RoelofsenFarkas2015.instReprFeature : Repr Feature

Equations

• RoelofsenFarkas2015.instReprFeature = { reprPrec := RoelofsenFarkas2015.instReprFeature.repr }

def RoelofsenFarkas2015.Feature.value : Feature → Polarity

The polarity of a feature, positive for the unmarked [agree] and [+] and negative for the marked [reverse] and [−] (78), (80).

Equations

• (RoelofsenFarkas2015.Feature.relative r).value = r
• (RoelofsenFarkas2015.Feature.absolute s).value = s

inductive RoelofsenFarkas2015.Target : Type

A particle realizes features, or a feature combination [r, s] as a whole.

• feature (f : Feature) : Target
• combination (r s : Polarity) : Target

@[instance_reducible]

instance RoelofsenFarkas2015.instDecidableEqTarget : DecidableEq Target

Equations

• RoelofsenFarkas2015.instDecidableEqTarget = RoelofsenFarkas2015.instDecidableEqTarget.decEq

def RoelofsenFarkas2015.instDecidableEqTarget.decEq (x✝ x✝¹ : Target) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.
• RoelofsenFarkas2015.instDecidableEqTarget.decEq (RoelofsenFarkas2015.Target.feature a) (RoelofsenFarkas2015.Target.feature b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqTarget.decEq (RoelofsenFarkas2015.Target.feature f) (RoelofsenFarkas2015.Target.combination r s) = isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqTarget.decEq (RoelofsenFarkas2015.Target.combination r s) (RoelofsenFarkas2015.Target.feature f) = isFalse ⋯

def RoelofsenFarkas2015.instReprTarget.repr : Target → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance RoelofsenFarkas2015.instReprTarget : Repr Target

Equations

• RoelofsenFarkas2015.instReprTarget = { reprPrec := RoelofsenFarkas2015.instReprTarget.repr }

def RoelofsenFarkas2015.english : English.PolarityParticle → List Target

English yes realizes [agree] and [+], and no [reverse] and [−] (76).

Equations

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

def RoelofsenFarkas2015.french : French.PolarityParticle → List Target

French oui realizes [+], non [−], and si the combination [reverse, +] (118).

Equations

• RoelofsenFarkas2015.french French.PolarityParticle.oui = [RoelofsenFarkas2015.Target.feature (RoelofsenFarkas2015.Feature.absolute Polarity.positive)]
• RoelofsenFarkas2015.french French.PolarityParticle.non = [RoelofsenFarkas2015.Target.feature (RoelofsenFarkas2015.Feature.absolute Polarity.negative)]
• RoelofsenFarkas2015.french French.PolarityParticle.si = [RoelofsenFarkas2015.Target.combination Polarity.negative Polarity.positive]

def RoelofsenFarkas2015.german : German.PolarityParticle → List Target

German ja realizes [agree] and [+], nein [reverse] and [−], and doch the combination [reverse, +] (123).

Equations

• One or more equations did not get rendered due to their size.
• RoelofsenFarkas2015.german German.PolarityParticle.doch = [RoelofsenFarkas2015.Target.combination Polarity.negative Polarity.positive]

def RoelofsenFarkas2015.Realizes {P : Type u_2} (R : P → List Target) (p : P) (r s : Polarity) : Prop

A particle can realize the combination [r, s] when it realizes one of its features or the combination itself.

Equations

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

def RoelofsenFarkas2015.Usable {P : Type u_2} (R : P → List Target) (p : P) (r s : Polarity) : Prop

A particle is usable in an [r, s] response when it can realize it and no particle dedicated to the combination blocks it.

Equations

• RoelofsenFarkas2015.Usable R p r s = (RoelofsenFarkas2015.Realizes R p r s ∧ ∀ (q : P), RoelofsenFarkas2015.Target.combination r s ∈ R q → RoelofsenFarkas2015.Target.combination r s ∈ R p)

@[instance_reducible]

instance RoelofsenFarkas2015.instDecidableRealizes {P : Type u_2} (R : P → List Target) (p : P) (r s : Polarity) : Decidable (Realizes R p r s)

Equations

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

@[instance_reducible]

instance RoelofsenFarkas2015.instDecidableUsableOfDecidableEq {P : Type u_2} [Fintype P] (R : P → List Target) [DecidableEq P] (p : P) (r s : Polarity) : Decidable (Usable R p r s)

Equations

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

theorem RoelofsenFarkas2015.english_usable (p : English.PolarityParticle) : (Usable english p Polarity.positive Polarity.positive ↔ p = English.PolarityParticle.yes) ∧ (Usable english p Polarity.negative Polarity.negative ↔ p = English.PolarityParticle.no) ∧ Usable english p Polarity.positive Polarity.negative ∧ Usable english p Polarity.negative Polarity.positive

In English, [agree, +] responses take yes, [reverse, −] responses no, and [agree, −] and [reverse, +] responses either particle (77).

theorem RoelofsenFarkas2015.french_usable (p : French.PolarityParticle) : (Usable french p Polarity.positive Polarity.positive ↔ p = French.PolarityParticle.oui) ∧ (Usable french p Polarity.negative Polarity.positive ↔ p = French.PolarityParticle.si) ∧ (Usable french p Polarity.positive Polarity.negative ↔ p = French.PolarityParticle.non) ∧ (Usable french p Polarity.negative Polarity.negative ↔ p = French.PolarityParticle.non)

French [agree, +] responses take oui, [reverse, +] responses si, and [agree, −] and [reverse, −] responses non (119)–(122).

theorem RoelofsenFarkas2015.german_usable (p : German.PolarityParticle) : (Usable german p Polarity.positive Polarity.positive ↔ p = German.PolarityParticle.ja) ∧ (Usable german p Polarity.negative Polarity.positive ↔ p = German.PolarityParticle.doch) ∧ (Usable german p Polarity.negative Polarity.negative ↔ p = German.PolarityParticle.nein) ∧ (Usable german p Polarity.positive Polarity.negative ↔ p ≠ German.PolarityParticle.doch)

German [agree, +] responses take ja, [reverse, +] responses doch, [reverse, −] responses nein, and [agree, −] responses ja or nein (124)–(127).

theorem RoelofsenFarkas2015.mem_english_iff (f : Feature) : (Target.feature f ∈ english English.PolarityParticle.yes ↔ f.value = Polarity.positive) ∧ (Target.feature f ∈ english English.PolarityParticle.no ↔ f.value = Polarity.negative)

The English particles each realize a natural class of features, yes the unmarked and no the marked ones (80).

theorem RoelofsenFarkas2015.usable_english_iff_mem (p : English.PolarityParticle) (x : Discourse.Response) : Usable english p x.relative x.polarity ↔ x ∈ FarkasBruce2010.english p

The English particles are usable in exactly the responses [FB10] say they mark: yes [same] or [+], no [reverse] or [−].

theorem RoelofsenFarkas2015.usable_si_iff_mem_reversePositive (x : Discourse.Response) : Usable french French.PolarityParticle.si x.relative x.polarity ↔ x ∈ FarkasBruce2010.reversePositive

French si is usable in exactly the [reverse, +] responses of [FB10].

The examples

inductive RoelofsenFarkas2015.Particle : Type

The particles of the examples.

• en (p : English.PolarityParticle) : Particle
• fr (p : French.PolarityParticle) : Particle
• de (p : German.PolarityParticle) : Particle

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

Equations

• RoelofsenFarkas2015.instDecidableEqParticle.decEq (RoelofsenFarkas2015.Particle.en a) (RoelofsenFarkas2015.Particle.en b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqParticle.decEq (RoelofsenFarkas2015.Particle.en p) (RoelofsenFarkas2015.Particle.fr p_1) = isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqParticle.decEq (RoelofsenFarkas2015.Particle.en p) (RoelofsenFarkas2015.Particle.de p_1) = isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqParticle.decEq (RoelofsenFarkas2015.Particle.fr p) (RoelofsenFarkas2015.Particle.en p_1) = isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqParticle.decEq (RoelofsenFarkas2015.Particle.fr a) (RoelofsenFarkas2015.Particle.fr b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqParticle.decEq (RoelofsenFarkas2015.Particle.fr p) (RoelofsenFarkas2015.Particle.de p_1) = isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqParticle.decEq (RoelofsenFarkas2015.Particle.de p) (RoelofsenFarkas2015.Particle.en p_1) = isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqParticle.decEq (RoelofsenFarkas2015.Particle.de p) (RoelofsenFarkas2015.Particle.fr p_1) = isFalse ⋯
• RoelofsenFarkas2015.instDecidableEqParticle.decEq (RoelofsenFarkas2015.Particle.de a) (RoelofsenFarkas2015.Particle.de b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance RoelofsenFarkas2015.instDecidableEqParticle : DecidableEq Particle

Equations

• RoelofsenFarkas2015.instDecidableEqParticle = RoelofsenFarkas2015.instDecidableEqParticle.decEq

@[instance_reducible]

instance RoelofsenFarkas2015.instReprParticle : Repr Particle

Equations

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

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

Equations

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

def RoelofsenFarkas2015.Particle.Usable : Particle → Polarity → Polarity → Prop

A particle is usable in an [r, s] response in its language.

Equations

• (RoelofsenFarkas2015.Particle.en p).Usable x✝¹ x✝ = RoelofsenFarkas2015.Usable RoelofsenFarkas2015.english p x✝¹ x✝
• (RoelofsenFarkas2015.Particle.fr p).Usable x✝¹ x✝ = RoelofsenFarkas2015.Usable RoelofsenFarkas2015.french p x✝¹ x✝
• (RoelofsenFarkas2015.Particle.de p).Usable x✝¹ x✝ = RoelofsenFarkas2015.Usable RoelofsenFarkas2015.german p x✝¹ x✝

@[instance_reducible]

instance RoelofsenFarkas2015.instDecidableUsable (p : Particle) (r s : Polarity) : Decidable (p.Usable r s)

Equations

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

def RoelofsenFarkas2015.particleTable : List (String × List (String × Particle))

The particles of each language, by Glottocode and spelling.

Equations

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

def RoelofsenFarkas2015.polarityTable : List (String × Polarity)

Equations

• RoelofsenFarkas2015.polarityTable = [("positive", Polarity.positive), ("negative", Polarity.negative)]

structure RoelofsenFarkas2015.Row : Type

A row records a particle response to an assertion, with the polarities of the antecedent and of the response, the relative feature the paper assigns it, the particle, and the judgment.

• response : Discourse.Response
• relative : Polarity
• particle : Particle
• judgment : Judgment

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

Equations

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

@[instance_reducible]

instance RoelofsenFarkas2015.instDecidableEqRow : DecidableEq Row

Equations

• RoelofsenFarkas2015.instDecidableEqRow = RoelofsenFarkas2015.instDecidableEqRow.decEq

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

Equations

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

@[instance_reducible]

instance RoelofsenFarkas2015.instReprRow : Repr Row

Equations

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

def RoelofsenFarkas2015.relativeTable : List (String × Polarity)

Equations

• RoelofsenFarkas2015.relativeTable = [("agree", Polarity.positive), ("reverse", Polarity.negative)]

def RoelofsenFarkas2015.Row.ofDatum (ex : Datum) : Option Row

Equations

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

def RoelofsenFarkas2015.rows : List Row

Equations

• RoelofsenFarkas2015.rows = List.filterMap RoelofsenFarkas2015.Row.ofDatum RoelofsenFarkas2015.Examples.all

theorem RoelofsenFarkas2015.relative_eq (r : Row) : r ∈ rows → r.response.relative = r.relative

The relative feature of every response, the quotient of its polarity by its antecedent's (relativePresup_smul_iff), is the one the paper assigns it.

theorem RoelofsenFarkas2015.judgment_iff_usable (r : Row) : r ∈ rows → (r.judgment = Judgment.acceptable ↔ r.particle.Usable r.response.relative r.response.polarity)

Every example is judged acceptable exactly when its particle is usable in its response.

def RoelofsenFarkas2015.planetTable : List (String × Polarity)

The propositions of the planets examples are even and its complement odd, each recorded as the polarity whose action yields it from even.

Equations

• RoelofsenFarkas2015.planetTable = [("even", Polarity.positive), ("odd", Polarity.negative), ("not even", Polarity.negative), ("not odd", Polarity.positive)]

structure RoelofsenFarkas2015.QuestionRow : Type

A question row records a response by an English particle to a question about the number of planets: the polarity and radical of a polar question, or none for the alternative question, the polarity of the response, its particle, what it conveys, and the judgment.

• question : Option (Polarity × Polarity)
• response : Polarity
• particle : English.PolarityParticle
• conveys : Option Polarity
• judgment : Judgment

@[instance_reducible]

instance RoelofsenFarkas2015.instDecidableEqQuestionRow : DecidableEq QuestionRow

Equations

• RoelofsenFarkas2015.instDecidableEqQuestionRow = RoelofsenFarkas2015.instDecidableEqQuestionRow.decEq

def RoelofsenFarkas2015.instDecidableEqQuestionRow.decEq (x✝ x✝¹ : QuestionRow) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance RoelofsenFarkas2015.instReprQuestionRow : Repr QuestionRow

Equations

• RoelofsenFarkas2015.instReprQuestionRow = { reprPrec := RoelofsenFarkas2015.instReprQuestionRow.repr }

def RoelofsenFarkas2015.instReprQuestionRow.repr : QuestionRow → ℕ → Std.Format

Equations

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

def RoelofsenFarkas2015.QuestionRow.ofDatum (ex : Datum) : Option QuestionRow

Equations

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

def RoelofsenFarkas2015.questionRows : List QuestionRow

Equations

• RoelofsenFarkas2015.questionRows = List.filterMap RoelofsenFarkas2015.QuestionRow.ofDatum RoelofsenFarkas2015.Examples.all

theorem RoelofsenFarkas2015.ofDatum_isSome (ex : Datum) : ex ∈ Examples.all → (Row.ofDatum ex).isSome = true ∨ (QuestionRow.ofDatum ex).isSome = true

def RoelofsenFarkas2015.QuestionRow.Predicted : QuestionRow → Prop

The prediction for a question row: a response of polarity s to a polar question of polarity t is acceptable when its particle is usable with the relative feature s / t and conveys s applied to the radical (presup_query_ofPolarity); no particle response to the alternative question is acceptable (not_relativePresup_disj).

Equations

• One or more equations did not get rendered due to their size.
• { question := none, response := response, particle := particle, conveys := conveys, judgment := j }.Predicted = (j ≠ Judgment.acceptable)

@[instance_reducible]

instance RoelofsenFarkas2015.instDecidablePredQuestionRowPredicted : DecidablePred QuestionRow.Predicted

Equations

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

theorem RoelofsenFarkas2015.questionRows_predicted (r : QuestionRow) : r ∈ questionRows → r.Predicted

The account predicts the judgment and the conveyed proposition of every response to the questions of (49)–(53).