Bar-Lev (2021): An Implicature Account of Homogeneity and Non-Maximality

Bar-Lev derives homogeneity as an implicature. A plural definite means existential pluralization, that some atom of the plurality in a domain has the property, and its alternatives replace the domain by its subsets; each alternative is one of the readings of the plural predication (supClosure_subset_readings). Exhaustifying over them gives the universal reading, while under negation exhaustification is vacuous. Pruning the alternatives to subdomains of a fixed size gives the threshold readings of non-maximality, which are readings of the plural predication as well (readings_subset_readings); the question the context raises selects among them, and a world is gappy when it verifies the reading one question selects and falsifies another's.

Main results

• exhIEII_eq_universal, exhIEII_compl_biUnion: the maximality implicature, and its absence under negation.
• exhIEII_pruned_eq_atLeast, isReading_polar_atLeast: pruning yields the threshold readings, and a polar question on a threshold selects it.
• gappy_iff_barePlural_eq_zero: the gappy worlds are those where Križ's trivalent plural is undefined; neg_barePlural_eq_zero_and_notMem_exhIEII_compl: the accounts part under negation.
• gappy_iff_krizChemla_gap, krizChemla_negation_residue: on Križ and Chemla's unembedded displays the account predicts their gaps for the positive sentence and misses those under negation.
• disjunction_not_both, plural_both, reading_66, reading_80, reading_81: the paper's examples.

Implementation notes

readings are the threshold readings, obtained by pruning to a fixed subdomain size; the paper's asymmetric conjunctions of alternatives are omitted, so IsReading agrees with the paper's selection on the partitions whose only decided readings are thresholds, which includes the polar questions of (66), (80) and (81). The maximality constraint on prunings is not formalized. Gappy ranges over all partitions and is context-free; that a context fixing the partition removes the gap is carried by reading_80 and reading_81.

TODO

• The negative sentence is modelled only at the LF with negation over ∃-PL; the LF with ∃-PL over negation and the cover-restricted ∃-PL of §5.3, the paper's source of the marginal negative non-maximal readings and of Križ and Chemla's negative gaps, are not formalized.
• The paper's full set of readings, and the non-distributive extension of §8.

References

• [BL21]
• [Mag09]
• [Mag14]
• [Fox07]
• [FS18]
• [CCF15]
• [BLF20]
• [Mal12]
• [Kri15b]
• [Kri16]
• [KC15]
• [KS21b]
• [TKC19]

Existential pluralization and its subdomain alternatives

The existential pluralization ∃-PL_D of P over x is the disjunction of the atoms of x in the domain D. A subdomain D' ⊆ D leaves the atoms of x ∩ D', so the subdomain alternatives are the closure of the atoms under disjunction, supClosure (atom P '' ↑(x ∩ D)).

def BarLev2021.atom {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) (a : Atom) : Set W

The proposition a satisfies P.

Equations

• BarLev2021.atom P a = {w : W | P a w}

@[instance_reducible]

instance BarLev2021.instDecidableMemSetAtom {Atom : Type u_1} {W : Type u_2} {P : Atom → W → Prop} [(a : Atom) → (w : W) → Decidable (P a w)] (w : W) (a : Atom) : Decidable (w ∈ atom P a)

Equations

• BarLev2021.instDecidableMemSetAtom w a = BarLev2021.instDecidableMemSetAtom._aux_1 w a

theorem BarLev2021.supClosure_subset_readings {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] : supClosure (atom P '' ↑(x ∩ D)) ⊆ Homogeneity.readings (fun (z : Finset Atom) => {w : W | ∀ a ∈ z, P a w}) x

The subdomain alternatives are readings of the distributive plural predication, since the sub-disjunctions of the atoms lie in the lattice they generate.

structure BarLev2021.Separating {Atom : Type u_1} {W : Type u_2} (D x : Finset Atom) (P : Atom → W → Prop) [DecidableEq Atom] : Prop

Every atom laughs alone at some world, and all laugh together at some world.

• single (a : Atom) : a ∈ x ∩ D → ∃ (w : W), ∀ b ∈ x ∩ D, P b w ↔ b = a

  Each atom of x ∩ D satisfies P alone at some world.

• all : ∃ (w : W), ∀ a ∈ x ∩ D, P a w

  All atoms of x ∩ D satisfy P together at some world.

Homogeneity

theorem BarLev2021.exhIEII_eq_universal {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] (h : Separating D x P) (hne : (x ∩ D).Nonempty) : Exhaustification.exhIEII (supClosure (atom P '' ↑(x ∩ D))) (⋃ b ∈ x ∩ D, atom P b) = {w : W | ∀ a ∈ x, a ∈ D → P a w}

Exhaustifying ∃-PL over its subdomain alternatives gives the universal reading, the maximality implicature.

theorem BarLev2021.exhIEII_compl_biUnion {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] {C : Set (Set W)} (hC : C ⊆ compl '' supClosure (atom P '' ↑(x ∩ D))) (hsat : (⋃ b ∈ x ∩ D, atom P b)ᶜ.Nonempty) : Exhaustification.exhIEII C (⋃ b ∈ x ∩ D, atom P b)ᶜ = (⋃ b ∈ x ∩ D, atom P b)ᶜ

With negation over ∃-PL every negated subdomain alternative is entailed by the negated prejacent, so exhaustification over any of them is vacuous and no pruning yields a non-maximal reading.

theorem BarLev2021.exists_mem_biUnion_and_not {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] (h : Separating D x P) {a : Atom} (ha : a ∈ x ∩ D) (h2 : 2 ≤ (x ∩ D).card) : ∃ w ∈ ⋃ b ∈ x ∩ D, atom P b, ¬P a w

The existential basic meaning does not entail that a given kid laughed, (6a).

theorem BarLev2021.not_of_notMem_biUnion {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] {w : W} (hw : w ∉ ⋃ b ∈ x ∩ D, atom P b) {a : Atom} (ha : a ∈ x ∩ D) : ¬P a w

Its negation entails that no given kid laughed, (6b).

theorem BarLev2021.not_forall_of_mem_exhIEII_insert_iInter {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] (h : Separating D x P) (h2 : 2 ≤ (x ∩ D).card) {w : W} (hw : w ∈ Exhaustification.exhIEII (insert (⋂ a ∈ x ∩ D, atom P a) (supClosure (atom P '' ↑(x ∩ D)))) (⋃ b ∈ x ∩ D, atom P b)) : ¬∀ a ∈ x ∩ D, P a w

Simple disjunction, whose alternatives include the conjunction, is strengthened the other way, the conjunction being denied.

Non-maximality by pruning

def BarLev2021.readings {Atom : Type u_1} {W : Type u_2} (D x : Finset Atom) (P : Atom → W → Prop) [DecidableEq Atom] : Set (Set W)

The readings of the kids laughed are the maximal one and the pruned ones.

Equations

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

def BarLev2021.IsReading {Atom : Type u_1} {W : Type u_2} (D x : Finset Atom) (P : Atom → W → Prop) [DecidableEq Atom] (Q : Setoid W) (q : Set W) : Prop

The reading a partition selects is the strongest reading it decides.

Equations

• BarLev2021.IsReading D x P Q q = (q ∈ BarLev2021.readings D x P ∧ Q.Decides q ∧ ∀ r ∈ BarLev2021.readings D x P, Q.Decides r → q ⊆ r)

theorem BarLev2021.IsReading.unique {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] {Q : Setoid W} {q r : Set W} (hq : IsReading D x P Q q) (hr : IsReading D x P Q r) : q = r

A partition selects at most one reading.

def BarLev2021.count {Atom : Type u_1} {W : Type u_2} (D x : Finset Atom) (P : Atom → W → Prop) [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (w : W) : ℕ

How many atoms of the plurality satisfy P at w.

Equations

• BarLev2021.count D x P w = {x ∈ x ∩ D | P x w}.card

def BarLev2021.atLeast {Atom : Type u_1} {W : Type u_2} (D x : Finset Atom) (P : Atom → W → Prop) [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (k : ℕ) : Set W

"At least k of the kids laughed".

Equations

• BarLev2021.atLeast D x P k = {w : W | k ≤ BarLev2021.count D x P w}

@[simp]

theorem BarLev2021.mem_atLeast {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] {k : ℕ} {w : W} : w ∈ atLeast D x P k ↔ k ≤ count D x P w

theorem BarLev2021.count_le_card {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (w : W) : count D x P w ≤ (x ∩ D).card

theorem BarLev2021.atLeast_antitone {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] : Antitone (atLeast D x P)

theorem BarLev2021.atLeast_card {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] : atLeast D x P (x ∩ D).card = {w : W | ∀ a ∈ x, a ∈ D → P a w}

The maximal reading is the threshold at the whole plurality.

theorem BarLev2021.exhIEII_pruned_eq_atLeast {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (h : Separating D x P) {m : ℕ} (hm : 0 < m) (hmn : m ≤ (x ∩ D).card) : Exhaustification.exhIEII (Exhaustification.subDisjsOfCard (x ∩ D) (atom P) m) (⋃ b ∈ x ∩ D, atom P b) = atLeast D x P ((x ∩ D).card + 1 - m)

Exhaustifying over the size-m alternatives yields "at least n + 1 - m of the kids laughed".

theorem BarLev2021.mem_readings_iff {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (h : Separating D x P) {q : Set W} : q ∈ readings D x P ↔ ∃ (k : ℕ), 0 < k ∧ k ≤ (x ∩ D).card ∧ q = atLeast D x P k

The readings are the thresholds from one to the whole plurality.

theorem BarLev2021.readings_subset_readings {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (h : Separating D x P) : readings D x P ⊆ Homogeneity.readings (fun (z : Finset Atom) => {w : W | ∀ a ∈ z, P a w}) x

The pruned readings are readings of the plural predication too, the threshold k reading the predicate over the parts of x with at least k atoms in the domain.

theorem BarLev2021.exhIEII_supClosure_subset_exhIEII_subDisjsOfCard {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (h : Separating D x P) (hne : (x ∩ D).Nonempty) {m : ℕ} (hm : 0 < m) (hmn : m ≤ (x ∩ D).card) : Exhaustification.exhIEII (supClosure (atom P '' ↑(x ∩ D))) (⋃ b ∈ x ∩ D, atom P b) ⊆ Exhaustification.exhIEII (Exhaustification.subDisjsOfCard (x ∩ D) (atom P) m) (⋃ b ∈ x ∩ D, atom P b)

Pruning only weakens, the maximal reading entailing every pruned one.

Relevance and gappiness

theorem BarLev2021.isReading_polar_atLeast {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (h : Separating D x P) (hcount : ∀ k ≤ (x ∩ D).card, ∃ (w : W), count D x P w = k) {k : ℕ} (hk : 0 < k) (hkn : k ≤ (x ∩ D).card) : IsReading D x P (Setoid.polar (atLeast D x P k)) (atLeast D x P k)

Given the polar question whether at least k of the kids laughed, the kids laughed means that at least k did, provided every number of laughers is realized at some world.

def BarLev2021.Gappy {Atom : Type u_1} {W : Type u_2} (D x : Finset Atom) (P : Atom → W → Prop) [DecidableEq Atom] (w : W) : Prop

A world is gappy when it is true on the reading some partition selects and false on another's.

Equations

• BarLev2021.Gappy D x P w = ((∃ (Q : Setoid W) (q : Set W), BarLev2021.IsReading D x P Q q ∧ w ∈ q) ∧ ∃ (Q : Setoid W) (q : Set W), BarLev2021.IsReading D x P Q q ∧ w ∉ q)

theorem BarLev2021.gappy_iff {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (h : Separating D x P) (hcount : ∀ k ≤ (x ∩ D).card, ∃ (w : W), count D x P w = k) (w : W) : Gappy D x P w ↔ 0 < count D x P w ∧ count D x P w < (x ∩ D).card

The worlds judged neither true nor false are those where some but not all of the kids laughed.

theorem BarLev2021.gappy_iff_barePlural_eq_zero {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (h : Separating D x P) (hcount : ∀ k ≤ (x ∩ D).card, ∃ (w : W), count D x P w = k) (w : W) : Gappy D x P w ↔ Homogeneity.barePlural P (x ∩ D) w = 0

A plain positive definite plural is gappy exactly where [Kri16]'s trivalent plural predication is undefined, where the accounts agree.

theorem BarLev2021.neg_barePlural_eq_zero_and_notMem_exhIEII_compl {Atom : Type u_1} {W : Type u_2} {D x : Finset Atom} {P : Atom → W → Prop} [DecidableEq Atom] [(a : Atom) → (w : W) → Decidable (P a w)] (h : Separating D x P) (hcount : ∀ k ≤ (x ∩ D).card, ∃ (w : W), count D x P w = k) {w : W} (hw : Gappy D x P w) (C : Set (Set W)) : -Homogeneity.barePlural P (x ∩ D) w = 0 ∧ w ∉ Exhaustification.exhIEII C (⋃ b ∈ x ∩ D, atom P b)ᶜ

At a gappy world the trivalent negation is still undefined, while the negative sentence with negation over ∃-PL, exhaustified over any of its alternatives, is plainly false, where the accounts part.

The model whose worlds record who laughed

@[reducible, inline]

abbrev BarLev2021.holds {Atom : Type u_1} (a : Atom) (w : Finset Atom) : Prop

In the model whose worlds are the sets of atoms satisfying the predicate, a satisfies it at the world w when a ∈ w.

Equations

• BarLev2021.holds a w = (a ∈ w)

theorem BarLev2021.separating_holds {Atom : Type u_1} (D x : Finset Atom) [DecidableEq Atom] : Separating D x holds

Every atom satisfies the predicate alone at some world and all do at some world.

theorem BarLev2021.count_holds {Atom : Type u_1} (D x : Finset Atom) [DecidableEq Atom] (w : Finset Atom) : count D x holds w = (x ∩ D ∩ w).card

theorem BarLev2021.exists_count_holds_eq {Atom : Type u_1} (D x : Finset Atom) [DecidableEq Atom] (k : ℕ) (hk : k ≤ (x ∩ D).card) : ∃ (w : Finset Atom), count D x holds w = k

Every number of laughers up to the size of the plurality is realized.

theorem BarLev2021.isReading_polar_atLeast_holds {Atom : Type u_1} (D x : Finset Atom) [DecidableEq Atom] {k : ℕ} (hk : 0 < k) (hkn : k ≤ (x ∩ D).card) : IsReading D x holds (Setoid.polar (atLeast D x holds k)) (atLeast D x holds k)

The paper's examples

inductive BarLev2021.Kid : Type

Kelly, Jane and Bill.

• kelly : Kid
• jane : Kid
• bill : Kid

@[instance_reducible]

instance BarLev2021.instDecidableEqKid : DecidableEq Kid

Equations

• BarLev2021.instDecidableEqKid x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance BarLev2021.instFintypeKid : Fintype Kid

Equations

• BarLev2021.instFintypeKid = { elems := { val := ↑BarLev2021.Kid.enumList, nodup := BarLev2021.Kid.enumList_nodup }, complete := BarLev2021.instFintypeKid._proof_1 }

def BarLev2021.kids : Finset Kid

The kids.

Equations

• BarLev2021.kids = Finset.univ

def BarLev2021.pair : Finset Kid

Kelly and Jane, the kids of (41).

Equations

• BarLev2021.pair = {BarLev2021.Kid.kelly, BarLev2021.Kid.jane}

@[reducible, inline]

abbrev BarLev2021.kellyLaughed : Set (Finset Kid)

Kelly laughed.

Equations

• BarLev2021.kellyLaughed = BarLev2021.atom BarLev2021.holds BarLev2021.Kid.kelly

@[reducible, inline]

abbrev BarLev2021.janeLaughed : Set (Finset Kid)

Jane laughed.

Equations

• BarLev2021.janeLaughed = BarLev2021.atom BarLev2021.holds BarLev2021.Kid.jane

theorem BarLev2021.disjunction_not_both : Exhaustification.exhIEII {kellyLaughed ∪ janeLaughed, kellyLaughed, janeLaughed, kellyLaughed ∩ janeLaughed} (kellyLaughed ∪ janeLaughed) = (kellyLaughed ∪ janeLaughed) \ (kellyLaughed ∩ janeLaughed)

Kelly or Jane laughed, (41a), whose alternatives include the conjunction, is strengthened to "not both".

theorem BarLev2021.plural_both : Exhaustification.exhIEII (supClosure (atom holds '' ↑pair)) (⋃ b ∈ pair, atom holds b) = {w : Finset Kid | pair ⊆ w}

The kids laughed, (41b), whose alternatives are the subdomain alternatives alone, is strengthened to "both".

theorem BarLev2021.reading_66 : IsReading kids kids holds (Setoid.polar (atLeast kids kids holds 2)) (atLeast kids kids holds 2)

Given the partition (66) — at most one kid laughed, or two or three did — the kids laughed means that at least two of the kids laughed.

@[reducible, inline]

abbrev BarLev2021.Book : Type

The ten books on the reading list.

Equations

• BarLev2021.Book = Fin 10

def BarLev2021.books : Finset Book

The books.

Equations

• BarLev2021.books = Finset.univ

theorem BarLev2021.reading_80 : IsReading books books holds (Setoid.polar (atLeast books books holds 5)) (atLeast books books holds 5)

In the context of (80), where reading any five of the ten books passes the test, Mary read the books means that she read at least five of them; the paper offers the prediction that a fixed partition removes the gap tentatively.

theorem BarLev2021.reading_81 : IsReading books books holds (Setoid.polar (atLeast books books holds 10)) (atLeast books books holds 10)

In the context of (81), where only reading all ten passes, Mary read the books has its maximal reading.

Križ and Chemla's unembedded displays

An unembedded display of [KC15] shows nine symbols, some number of which have the target color, so its worlds are the sets of target-colored symbols.

@[reducible, inline]

abbrev BarLev2021.Symbol : Type

The symbols of a display.

Equations

• BarLev2021.Symbol = Fin 9

theorem BarLev2021.gappy_iff_krizChemla_gap : (∀ i ∈ KrizChemla2015.items, i.embedding = KrizChemla2015.Embedding.unembedded → ∀ (w : Finset Symbol), i.cells = [w.card] → (Gappy Finset.univ Finset.univ holds w ↔ i.condition = KrizChemla2015.Condition.gap)) ∧ ∀ t ∈ KrizChemla2015.gapTests, t.embedding = KrizChemla2015.Embedding.unembedded → t.found = KrizChemla2015.Found.yes

On Križ and Chemla's unembedded displays the account makes the positive sentence gappy exactly at the GAP displays, and every experiment that tested them found a gap there (Table 2).

theorem BarLev2021.krizChemla_negation_residue : (∀ i ∈ KrizChemla2015.items, i.embedding = KrizChemla2015.Embedding.unembedded → i.condition = KrizChemla2015.Condition.gap → ∀ (w : Finset Symbol), i.cells = [w.card] → ∀ (C : Set (Set (Finset Symbol))), w ∉ Exhaustification.exhIEII C (⋃ b ∈ Finset.univ, atom holds b)ᶜ) ∧ ∀ t ∈ KrizChemla2015.gapTests, t.embedding = KrizChemla2015.Embedding.negation → t.found = KrizChemla2015.Found.yes

Under negation the account, with negation over ∃-PL, makes every GAP display plainly false whatever is pruned, while Table 2 found a gap there in Experiments A1 and B1, the residue the paper attributes to the LF with ∃-PL over negation.

theorem BarLev2021.rows_gappiness_positive (e : Datum) : e ∈ Examples.all → e.feature? "gappiness" = some "yes" → e.feature? "polarity" = some "positive"

The paper's examples report gappiness for positive sentences and reduced gappiness for the negative (82b), the asymmetry neg_barePlural_eq_zero_and_notMem_exhIEII_compl idealizes.