Cohen and Krifka 2014: superlative quantifiers and meta-speech acts

Cohen and Krifka analyse superlative quantifiers as quantifying over meta-speech acts. Over commitment spaces, the meta-speech act GRANT is the denegation of asserting the negation: it keeps the root and prunes the continuations in which the speaker asserts the negation. At most n says that the greatest value whose GRANT the speaker leaves open is n, and is performed by denying the GRANT of every value above n, which amounts to asserting the denial of each; at least n does the same for the values below n. We state this exclusion over an arbitrary set of values on a linear scale, after the paper's generalization beyond numerals. The context set of the updated root is the intersection of the asserted denials, while no denial of a value in range is entailed, the trace in the model of the paper's claim that the sentence's falsity is semantic and its truth an implicature.

Main statements

• assert_le_grant, sdiff_coe_grant: a GRANT includes but does not enforce the assertion, and denegating a GRANT is asserting the negation.
• coe_exclude, sdiff_coe_exclude: the exclusion is the conjunction of the assertions of the denials, and its denegation is the disjunction of the GRANTs it denied, which keeps the root and so commits the speaker to nothing.
• contextSet_atMost_exactly, contextSet_atLeast_exactly: on count scales the derived truth conditions are the classical Keenan and Stavi meanings of the numeral quantifiers.
• atMost_mono, contextSet_atLeast_exactly_mono: at most strengthens as the bound drops and as the count grows, while a larger count weakens at least, the asymmetry behind NPI licensing.

Implementation notes

• The strength comparisons across different count scales ((87): denying n ever against denying n last year) are stated on the context sets of the updated roots rather than as (86)'s inclusion of spaces: the latter needs states closed under entailment, which the paper invokes as a consistency requirement and this representation does not impose. The per-value entailment claimed there also fails for the exact propositions of (44)/(46) — with three visitors ever and two last year, ¬(exactly two ever) holds while ¬(exactly two last year) does not — though the whole conjunctions are ordered as (87) concludes.
• The general theorems carry freshness (no denial already in the root) and membership hypotheses locating the updated roots among the space's states, and the greatest- and least-grantable characterizations injectivity of the scale; the free space satisfies all of them, as the count model checks.

TODO

• The evaluative reading (§5.2.3–§5.2.4) and its good/bad-consequent presupposition are left informal by the paper.
• The compositional route through the superlative morphology ((67), (70)) needs degree composition with an illocutionary operator in the lexical entry.
• Wide-scope at most over deontic may (p. 71) denies permissions, which the preferential commitment force could express.

References

• A. Cohen and M. Krifka, Superlative quantifiers and meta-speech acts (2014)
• B. Geurts and R. Nouwen, `At least' et al.: The semantics of scalar modifiers (2007)
• E. Keenan and J. Stavi, A Semantic Characterization of Natural Language Determiners (1986)

Assertions and GRANTs (§2.3)

def CohenKrifka2014.grant {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) : Commitment.Space (Commitment.State A W)

GRANT φ = ∼ASSERT ¬φ ((38)).

Equations

• CohenKrifka2014.grant C a φ = C.denegate ↑(C.assert a φᶜ)

@[simp]

theorem CohenKrifka2014.root_grant {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) : (grant C a φ).root = C.root

theorem CohenKrifka2014.mem_grant {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) {d : Commitment.State A W} : d ∈ grant C a φ ↔ d = C.root ∨ d ∈ C ∧ Commitment.commit a φᶜ ∉ d

A grant keeps the root and the states in which a has not asserted ¬φ.

theorem CohenKrifka2014.assert_le_grant {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) (hmem : (C.assert a φ).root ∈ C) (hcons : ∀ d ∈ C, Commitment.commit a φ ∈ d → Commitment.commit a φᶜ ∉ d) : C.assert a φ ≤ grant C a φ

On a space whose states never carry both a commitment and its denial, every state reached by asserting φ survives granting φ, so the grant includes the assertion ((39)).

theorem CohenKrifka2014.sdiff_coe_grant {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : Set W) (hmem : (C.assert a φᶜ).root ∈ C) (h : Commitment.commit a φᶜ ∉ C.root) : ↑C \ ↑(grant C a φ) = ↑(C.assert a φᶜ)

Denegating the GRANT of φ is asserting ¬φ ((40)), for an assertion the space admits that is not redundant.

Quantifying over GRANTs (§3.1, §3.6)

def CohenKrifka2014.denials {A : Type u_1} {W : Type u_2} {ι : Type u_3} (a : A) (φ : ι → Set W) (s : Set ι) : Commitment.State A W

The denials by a of the values of φ in s are the commitments to ¬φ(m) for m ∈ s.

Equations

• CohenKrifka2014.denials a φ s = (fun (m : ι) => Commitment.commit a (φ m)ᶜ) '' s

def CohenKrifka2014.exclude {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (s : Set ι) : Commitment.Space (Commitment.State A W)

In the meta-speech act excluding the values of φ in s, a asserts ¬φ(m) for every m ∈ s at once ((46), (51)).

Equations

• CohenKrifka2014.exclude C a φ s = C.update (CohenKrifka2014.denials a φ s)

theorem CohenKrifka2014.root_exclude {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (s : Set ι) (hK : denials a φ s ∪ C.root ∈ C) : (exclude C a φ s).root = denials a φ s ∪ C.root

When the space projects the root with the denials, that state is the root of the exclusion.

theorem CohenKrifka2014.root_exclude_mem {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (s : Set ι) (hK : denials a φ s ∪ C.root ∈ C) : (exclude C a φ s).root ∈ C

theorem CohenKrifka2014.denials_eq_sSup {A : Type u_1} {W : Type u_2} {ι : Type u_3} (a : A) (φ : ι → Set W) (s : Set ι) : denials a φ s = sSup ((fun (m : ι) => {Commitment.commit a (φ m)ᶜ}) '' s)

theorem CohenKrifka2014.commit_mem_root_exclude_iff {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (s : Set ι) (hK : denials a φ s ∪ C.root ∈ C) (hroot : ∀ (m : ι), Commitment.commit a (φ m)ᶜ ∉ C.root) (hinj : Function.Injective φ) {m : ι} : Commitment.commit a (φ m)ᶜ ∈ (exclude C a φ s).root ↔ m ∈ s

The exclusion denies φ(m) exactly for the excluded values.

theorem CohenKrifka2014.root_notMem_exclude {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (s : Set ι) (hne : s.Nonempty) (hroot : ∀ m ∈ s, Commitment.commit a (φ m)ᶜ ∉ C.root) : C.root ∉ exclude C a φ s

The exclusion moves the root, so its denegation keeps the root and commits the speaker to nothing (§5.2.2).

theorem CohenKrifka2014.coe_exclude {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (s : Set ι) (hne : s.Nonempty) (hK : denials a φ s ∪ C.root ∈ C) : ↑(exclude C a φ s) = ⋂ m ∈ s, ↑(C.assert a (φ m)ᶜ)

The exclusion is the generalized conjunction ((31)) of the single assertions of the denials ((46), (51)).

theorem CohenKrifka2014.coe_exclude_eq_iInter_sdiff_grant {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (s : Set ι) (hne : s.Nonempty) (hroot : ∀ m ∈ s, Commitment.commit a (φ m)ᶜ ∉ C.root) (hK : denials a φ s ∪ C.root ∈ C) (hmem : ∀ m ∈ s, insert (Commitment.commit a (φ m)ᶜ) C.root ∈ C) : ↑(exclude C a φ s) = ⋂ m ∈ s, ↑C \ ↑(grant C a (φ m))

In (44) and (49) each conjunct is the denegation of the GRANT of φ(m), which is the assertion of its denial by (40).

theorem CohenKrifka2014.sdiff_coe_exclude {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (s : Set ι) (hne : s.Nonempty) (hroot : ∀ m ∈ s, Commitment.commit a (φ m)ᶜ ∉ C.root) (hK : denials a φ s ∪ C.root ∈ C) : ↑C \ ↑(exclude C a φ s) = ⋃ m ∈ s, ↑(grant C a (φ m))

The denegation of the superlative is the disjunction of the GRANTs it denied ((97)–(98), by (34)).

theorem CohenKrifka2014.exclude_anti {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) {s t : Set ι} (hst : s ⊆ t) (hK : denials a φ t ∪ C.root ∈ C) : exclude C a φ t ≤ exclude C a φ s

Excluding more values is the stronger speech act ((86)), since its update is included in the weaker one's.

theorem CohenKrifka2014.contextSet_root_exclude {A : Type u_1} {W : Type u_2} {ι : Type u_3} (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (s : Set ι) (hK : denials a φ s ∪ C.root ∈ C) : Commitment.contextSet (exclude C a φ s).root = (⋂ m ∈ s, (φ m)ᶜ) ∩ Commitment.contextSet C.root

On the derived truth conditions (§3.2), what the exclusion asserts is the intersection of the asserted denials ((52)).

At most and at least over a linear scale

def CohenKrifka2014.atMost {A : Type u_1} {W : Type u_2} {ι : Type u_3} [LinearOrder ι] (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (n : ι) : Commitment.Space (Commitment.State A W)

At most n ((42)–(46)) excludes the values above n.

Equations

• CohenKrifka2014.atMost C a φ n = CohenKrifka2014.exclude C a φ (Set.Ioi n)

def CohenKrifka2014.atLeast {A : Type u_1} {W : Type u_2} {ι : Type u_3} [LinearOrder ι] (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (n : ι) : Commitment.Space (Commitment.State A W)

At least n ((47)–(51)) excludes the values below n.

Equations

• CohenKrifka2014.atLeast C a φ n = CohenKrifka2014.exclude C a φ (Set.Iio n)

theorem CohenKrifka2014.atMost_mono {A : Type u_1} {W : Type u_2} {ι : Type u_3} [LinearOrder ι] (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) {n n' : ι} (hnn : n ≤ n') (hK : denials a φ (Set.Ioi n) ∪ C.root ∈ C) : atMost C a φ n ≤ atMost C a φ n'

A lower bound makes at most stronger ((55), (118), by (86)).

theorem CohenKrifka2014.atLeast_anti {A : Type u_1} {W : Type u_2} {ι : Type u_3} [LinearOrder ι] (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) {n n' : ι} (hnn : n ≤ n') (hK : denials a φ (Set.Iio n') ∪ C.root ∈ C) : atLeast C a φ n' ≤ atLeast C a φ n

A higher bound makes at least stronger ((86)).

theorem CohenKrifka2014.atMost_isGreatest {A : Type u_1} {W : Type u_2} {ι : Type u_3} [LinearOrder ι] (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (n : ι) (hK : denials a φ (Set.Ioi n) ∪ C.root ∈ C) (hroot : ∀ (m : ι), Commitment.commit a (φ m)ᶜ ∉ C.root) (hinj : Function.Injective φ) : IsGreatest {m : ι | Commitment.commit a (φ m)ᶜ ∉ (atMost C a φ n).root} n

The value n is the greatest whose GRANT at most n leaves performable ((43), (60b)).

theorem CohenKrifka2014.atLeast_isLeast {A : Type u_1} {W : Type u_2} {ι : Type u_3} [LinearOrder ι] (C : Commitment.Space (Commitment.State A W)) (a : A) (φ : ι → Set W) (n : ι) (hK : denials a φ (Set.Iio n) ∪ C.root ∈ C) (hroot : ∀ (m : ι), Commitment.commit a (φ m)ᶜ ∉ C.root) (hinj : Function.Injective φ) : IsLeast {m : ι | Commitment.commit a (φ m)ᶜ ∉ (atLeast C a φ n).root} n

The value n is the least whose GRANT at least n leaves performable ((48), (60a)).

Count scales and the classical truth conditions (§3.2, §4)

def CohenKrifka2014.exactly {W : Type u_2} (f : W → ℕ) : ℕ → Set W

The scale of exact numeral claims over the count f ((74)) gives the two-sided numeral meaning at each value.

Equations

• CohenKrifka2014.exactly f n = f ⁻¹' {n}

theorem CohenKrifka2014.contextSet_atMost_exactly {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (n : ℕ) (f : W → ℕ) (hK : denials a (exactly f) (Set.Ioi n) ∪ C.root ∈ C) : Commitment.contextSet (atMost C a (exactly f) n).root = f ⁻¹' Set.Iic n ∩ Commitment.contextSet C.root

The derived truth conditions of at most n are the classical Keenan and Stavi meaning of the quantifier ((82)).

theorem CohenKrifka2014.contextSet_atLeast_exactly {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (n : ℕ) (f : W → ℕ) (hK : denials a (exactly f) (Set.Iio n) ∪ C.root ∈ C) : Commitment.contextSet (atLeast C a (exactly f) n).root = f ⁻¹' Set.Ici n ∩ Commitment.contextSet C.root

The derived truth conditions of at least n are the classical Keenan and Stavi meaning of the quantifier ((82)).

theorem CohenKrifka2014.contextSet_atMost_exactly_anti {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (n : ℕ) {f g : W → ℕ} (hfg : ∀ (w : W), g w ≤ f w) (hf : denials a (exactly f) (Set.Ioi n) ∪ C.root ∈ C) (hg : denials a (exactly g) (Set.Ioi n) ∪ C.root ∈ C) : Commitment.contextSet (atMost C a (exactly f) n).root ⊆ Commitment.contextSet (atMost C a (exactly g) n).root

A pointwise larger count strengthens at most on derived truth conditions, so denying counts of visitors ever entails denying counts last year ((84b), (87)).

theorem CohenKrifka2014.contextSet_atLeast_exactly_mono {A : Type u_1} {W : Type u_2} (C : Commitment.Space (Commitment.State A W)) (a : A) (n : ℕ) {f g : W → ℕ} (hfg : ∀ (w : W), g w ≤ f w) (hf : denials a (exactly f) (Set.Iio n) ∪ C.root ∈ C) (hg : denials a (exactly g) (Set.Iio n) ∪ C.root ∈ C) : Commitment.contextSet (atLeast C a (exactly g) n).root ⊆ Commitment.contextSet (atLeast C a (exactly f) n).root

A pointwise larger count weakens at least, the asymmetry behind NPI licensing ((84a), (88)).

John petted at least three rabbits ((1a), (47))

Worlds are the possible counts of petted rabbits, the acts the speaker's, and the space the free one, so every hypothesis of the general theorems holds and the pipeline runs end to end: the derived truth conditions are the classical at least three, a four-rabbit world verifies them and a two-rabbit world falsifies them ((52)), the denial of four is not among the commitments ((53)), and three is the least grantable value ((48)).

def CohenKrifka2014.rabbits : Commitment.Space (Commitment.State Discourse.Role ℕ)

The free space over counting worlds, with no prior commitments.

Equations

• CohenKrifka2014.rabbits = Commitment.Space.Ici ∅

theorem CohenKrifka2014.exactly_id_injective : Function.Injective (exactly id)

theorem CohenKrifka2014.rabbits_root_fresh (m : ℕ) : Commitment.commit Discourse.Role.speaker (exactly id m)ᶜ ∉ rabbits.root

theorem CohenKrifka2014.rabbits_atLeast_contextSet : Commitment.contextSet (atLeast rabbits Discourse.Role.speaker (exactly id) 3).root = Degree.Comparison.ge.interval 3

The derived truth conditions of (1a) are the classical at least three ((82)).

theorem CohenKrifka2014.four_mem_rabbits_atLeast : 4 ∈ Commitment.contextSet (atLeast rabbits Discourse.Role.speaker (exactly id) 3).root

Petting four rabbits verifies (1a), since every asserted denial holds ((52)).

theorem CohenKrifka2014.two_notMem_rabbits_atLeast : 2 ∉ Commitment.contextSet (atLeast rabbits Discourse.Role.speaker (exactly id) 3).root

Petting two rabbits falsifies (1a) semantically ((52a)).

theorem CohenKrifka2014.rabbits_atLeast_grant_four : Commitment.commit Discourse.Role.speaker (exactly id 4)ᶜ ∉ (atLeast rabbits Discourse.Role.speaker (exactly id) 3).root

The denial of four is not among the speaker's commitments ((53)), so that (1a) is true at four is implicature, not entailment.

theorem CohenKrifka2014.rabbits_atLeast_isLeast : IsLeast {m : ℕ | Commitment.commit Discourse.Role.speaker (exactly id m)ᶜ ∉ (atLeast rabbits Discourse.Role.speaker (exactly id) 3).root} 3

Three is the least value the speaker leaves grantable ((48), (60a)).

theorem CohenKrifka2014.rabbits_sdiff_atLeast : ↑rabbits \ ↑(atLeast rabbits Discourse.Role.speaker (exactly id) 3) = ⋃ m ∈ Set.Iio 3, ↑(grant rabbits Discourse.Role.speaker (exactly id m))

Denegating (1a) leaves the disjunction of the three GRANTs ((89b), (97)–(98)).

theorem CohenKrifka2014.rabbits_root_notMem_atLeast : rabbits.root ∉ atLeast rabbits Discourse.Role.speaker (exactly id) 3

The denegation keeps the root ((98)), so the negated superlative asserts nothing, which is why superlative quantifiers resist downward-entailing contexts (§5.2.2).

Granting includes but does not enforce asserting ((39), p. 54)

A two-state consistent space: nothing conceded, or φ asserted. Granting φ prunes neither state, while asserting φ leaves only the second.

def CohenKrifka2014.raining : Set Bool

It is raining, over two weather worlds.

Equations

• CohenKrifka2014.raining = {true}

def CohenKrifka2014.granting : Commitment.Space (Commitment.State Discourse.Role Bool)

The two-state space holds no commitments or the speaker's assertion of raining.

Equations

• CohenKrifka2014.granting = { carrier := {∅, insert (Commitment.commit Discourse.Role.speaker CohenKrifka2014.raining) ∅}, root := ∅, isLeast' := CohenKrifka2014.granting._proof_2 }

theorem CohenKrifka2014.raining_ne_compl : raining ≠ rainingᶜ

theorem CohenKrifka2014.granting_consistent (d : Commitment.State Discourse.Role Bool) : d ∈ granting → Commitment.commit Discourse.Role.speaker raining ∈ d → Commitment.commit Discourse.Role.speaker rainingᶜ ∉ d

theorem CohenKrifka2014.granting_assert_lt_grant : granting.assert Discourse.Role.speaker raining < grant granting Discourse.Role.speaker raining

Granting raining includes every state its assertion reaches, and also the root, which the assertion leaves behind, so the grant does not enforce the assertion ((39), p. 54).