Solt & Waldon (2019): Numerals under Negation

This file formalizes the felicity constraint on numerical assertions of Solt and Waldon. A bare numeral in the scope of negation, she doesn't have 40 sheep, is infelicitous as an answer to how many sheep does Lisa have? yet acceptable once the value is under discussion, as the denial after does Lisa have 40 sheep?; negated more than 40 is acceptable in both contexts, negated between 40 and 50 in neither. The paper's account takes the question under discussion to be a partition (Groenendijk and Stokhof, Roberts). A how-many question partitions the worlds by a count, so the number line orders its cells, and the constraint requires the content of an assertion containing a numerical expression to be the union of a convex set of cells, convexity in the sense of Gärdenfors carried from lexical meanings to discourse. On the exact reading of the numeral (Kennedy), not 40 is the union of every cell but one, a disjoint region; 40, between 40 and 50, more than 40 and not more than 40 are convex. A polar question has two cells, whose every subset is convex, so the denial is felicitous. At the top of a bounded scale the negated endpoint is convex, which is why not 100% certain is acceptable where not 95% certain is not.

Felicitous f φ states the constraint for a question that sorts the worlds by an ordered value f, the how-many question by the count and the polar question by the indicator; a felicitous assertion is one the question decides (Felicitous.decides), and for a polar question the converse holds (felicitous_of_polar). Every numeral form is felicitous (felicitous_over), and so is the negation of every form but the two-sided one (felicitous_compl_over). not_felicitous_compl is the general form of the infelicity: negating a bounded range leaves a disjoint region whenever the count reaches below, into, and above it. The lower-bounded reading of the numeral would negate to a convex region, but the paper argues it is unavailable in comment position, where a numeral answers the exact value the question asks for.

Implementation notes

The corpus study and the two acceptability experiments are reported in prose. The corpus finds negated bare numerals in denials of assertions, in contexts where the value was mentioned or implied, and in negations of a minimum significant value with the lower-bounded reading. Experiment 1 finds negated bare numerals rated between licensed and unlicensed polarity items, far better when the value was mentioned or implied than when it was not inferable, and better than about n throughout. Experiment 2 finds bare numerals under negation quite unacceptable as answers to a how-many question and almost fully restored by prior mention, unlike any and some, whose unlicensed uses prior mention does not improve, and unlike the positive polarity items about n and at least n, which prior mention improves less; more than n is acceptable under negation in both contexts, between m and n in neither. Modified numerals other than between are polarity-sensitive for reasons beyond convexity, which the paper leaves open.

References

• [SW19]
• [GS84]
• [Rob96]
• [Gar04]
• [Ken15]

The felicity constraint

def SoltWaldon2019.Felicitous {W : Type u_1} {ι : Type u_2} [Preorder ι] (f : W → ι) (φ : Set W) : Prop

The felicity constraint on numerical assertions, relative to the question that sorts the worlds by the ordered value f, requires the content to be the union of a convex set of cells.

Equations

• SoltWaldon2019.Felicitous f φ = ∃ (I : Set ι), I.OrdConnected ∧ φ = f ⁻¹' I

theorem SoltWaldon2019.Felicitous.decides {W : Type u_1} {ι : Type u_2} [Preorder ι] {f : W → ι} {φ : Set W} (h : Felicitous f φ) : (Setoid.ker f).Decides φ

A felicitous assertion is a union of cells, so the question decides it.

theorem SoltWaldon2019.ordConnected_prop (I : Set Prop) : I.OrdConnected

Every subset of a two-cell question is convex.

theorem SoltWaldon2019.felicitous_of_polar {W : Type u_1} {p φ : Set W} (h : (Setoid.polar p).Decides φ) : Felicitous (fun (x : W) => x ∈ p) φ

Under a polar question every decided proposition is felicitous, the denial no, she doesn't have 40 sheep among them.

The how-many question

The assertion that the value satisfies a numerical meaning I is f ⁻¹' I, the union of the question's cells over the values in I, and a numeral form with comparison c and number m asserts f ⁻¹' c.interval m.

theorem SoltWaldon2019.felicitous_preimage {W : Type u_1} {ι : Type u_2} [Preorder ι] (f : W → ι) (I : Set ι) [hI : I.OrdConnected] : Felicitous f (f ⁻¹' I)

A numerical meaning that is a convex set of values makes a felicitous assertion.

theorem SoltWaldon2019.felicitous_over {W : Type u_1} {ι : Type u_3} [PartialOrder ι] (f : W → ι) (c : Degree.Comparison) (m : ι) : Felicitous f (f ⁻¹' c.interval m)

Every numeral form is felicitous. She has 40 sheep on the two-sided reading is a single cell, and she has more than 40 sheep a final segment of the cells.

theorem SoltWaldon2019.felicitous_between {W : Type u_1} (count : W → ℕ) (m k : ℕ) : Felicitous count (count ⁻¹' Set.Icc m k)

She has between 40 and 50 sheep.

theorem SoltWaldon2019.felicitous_compl_over {W : Type u_1} {ι : Type u_3} [LinearOrder ι] (f : W → ι) {c : Degree.Comparison} (hc : c ≠ Degree.Comparison.eq) (m : ι) : Felicitous f (f ⁻¹' c.interval m)ᶜ

The negation of every form but the two-sided one is convex. She doesn't have more than 40 sheep answers the how-many question, and the negation of the lower-bounded reading would too; the paper takes that reading to be unavailable where the numeral answers a how-many question.

theorem SoltWaldon2019.not_felicitous_compl {W : Type u_1} (count : W → ℕ) {I : Set ℕ} {a b c : W} (ha : count a ∉ I) (hb : count b ∈ I) (hc : count c ∉ I) (hab : count a ≤ count b) (hbc : count b ≤ count c) : ¬Felicitous count (count ⁻¹' I)ᶜ

Negating a bounded range leaves a disjoint region. With worlds whose counts lie below, inside, and above the range, the negated assertion is not the union of a convex set of cells.

theorem SoltWaldon2019.not_felicitous_not_bare {W : Type u_1} (count : W → ℕ) {m : ℕ} {a b c : W} (ha : count a < m) (hb : count b = m) (hc : m < count c) : ¬Felicitous count (count ⁻¹' {m})ᶜ

She doesn't have 40 sheep on the two-sided reading, as an answer to the how-many question, is infelicitous whenever the count can fall below, at, and above 40.

theorem SoltWaldon2019.not_felicitous_not_between {W : Type u_1} (count : W → ℕ) {m k : ℕ} {a b c : W} (ha : count a < m) (hb : count b ∈ Set.Icc m k) (hc : k < count c) : ¬Felicitous count (count ⁻¹' Set.Icc m k)ᶜ

She doesn't have between 40 and 50 sheep is infelicitous for the same reason.

theorem SoltWaldon2019.felicitous_not_bare_of_max {W : Type u_1} (count : W → ℕ) {m : ℕ} (hmax : ∀ (w : W), count w ≤ m) : Felicitous count (count ⁻¹' {m})ᶜ

At the top of a bounded scale the negated endpoint is convex, the region below it, so it's not 100% certain answers how likely is it? where it's not 95% certain does not.

theorem SoltWaldon2019.felicitous_denial {W : Type u_1} (count : W → ℕ) (m : ℕ) : Felicitous (fun (x : W) => x ∈ count ⁻¹' {m}) (count ⁻¹' {m})ᶜ

Context rescues the denial. Once the question is whether Lisa has exactly 40 sheep, the negative answer is a cell of the question and so felicitous.