Documentation

Studies.Spector2013

Spector (2013): Bare Numerals and Scalar Implicatures #

This file formalizes the comparison of accounts of bare numerals in [Spe13a]. On the neo-Gricean account ([Hor72]) a numeral means at least n and the exactly reading is a scalar implicature; on the underspecification account ([Car88]) context selects among at least, exactly and at most; on the exactly-only account ([Bre08]) the numeral means exactly n and the other readings are contextual by-products; on the ambiguity account, lexical in [Geu06] and through a covert exhaustivity operator in [CFS12], the numeral has both an at least and an exactly reading. The paper's three generalizations are that at least readings are available in every embedded environment, exactly readings in every environment, and at most readings only in downward-entailing ones. The readings are the intervals Comparison.ge.interval, Comparison.eq.interval and Comparison.le.interval of the degree substrate; exhaustifying a family of readings indexed by the numeral against the stronger numerals asserts the prejacent and denies every stronger numeral alternative, and on the numeral itself it is the exact reading (exh_iff_bare, the substrate's exhNumeral).

The theorems are symbolic in the numeral. Under a necessity modal the neo-Gricean wide-scope implicature is weaker than the exact reading (necessity_implicature_of_exact, necessity_implicature_ne_exact); under negation the account predicts an indirect implicature, exactly n − 1, that is not perceived (indirect_implicature), and cannot reach the at most reading of the tax-exemption conditional, since a strengthening must entail the literal meaning (atMost_reading_not_entails_literal). The lexical at most entry under a possibility modal is satisfied by any small accessible value (poss_atMost_of_le), while the neo-Gricean derivation gives the intended bound (poss_implicature_iff). The exactly-only account reaches the at most and at least readings of the conditionals through law-like background knowledge (exact_extends_downward, exact_extends_upward) but cannot weaken the exact reading in upward-entailing contexts, where the in fact, five continuation is consistent only with at least, nor in degree uses like the voting age, where the exact reading under necessity is false and the exhaustified at least reading says the minimum (not_nec_exact_Ici, nec_Ici_exh_iff). The ambiguity account derives the third generalization: unembedded, at most does not entail exactly, so no background can strengthen the exact reading to it (atMost_not_entails_exact), while under negation it does (not_atMost_imp_not_exact). The exhaustivity operator scoping below or above a possibility modal yields three readings of which a lexical ambiguity provides two (wide_scope_ne_narrow, narrow_ne_base), and the intermediate embedded implicature of the professor example is the parse between the contradictory at least parse and the vacuous exactly parse (intermediate_parse_iff).

Implementation notes #

Modal environments are quantification over a set of accessible values, the counts or degrees compatible with the requirement or permission. Exhaustification denies every stronger alternative; for the antitone families of numeral readings this is the denial of the next numeral alone (Exhaustification.exhAgainst_lt_iff_succOrder), which is how the paper computes it. Prosodic marking, the metalinguistic use of negation, and the acquisition and processing evidence the paper reviews are not formalized.

References #

Environments and exhaustification #

def Spector2013.nec (A I : Set ℕ) :

Necessity over the accessible values A holds when every one of them is among I.

Equations
Instances For
    def Spector2013.poss (A I : Set ℕ) :

    Possibility over the accessible values A holds when one of them is among I.

    Equations
    Instances For
      theorem Spector2013.antitone_atLeast (k : ℕ) :
      Antitone fun (m : ℕ) => k ∈ Degree.Comparison.ge.interval m
      theorem Spector2013.antitone_nec (A : Set ℕ) :
      Antitone fun (m : ℕ) => nec A (Degree.Comparison.ge.interval m)
      theorem Spector2013.antitone_poss (A : Set ℕ) :
      Antitone fun (m : ℕ) => poss A (Degree.Comparison.ge.interval m)
      theorem Spector2013.exhNumeral_iff_exh (m k : ℕ) :
      k ∈ Numerals.exhNumeral m ↔ Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => k ∈ Degree.Comparison.ge.interval m) m

      On the numeral itself the operator is the substrate's exhNumeral.

      theorem Spector2013.exh_iff_bare (m k : ℕ) :
      Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => k ∈ Degree.Comparison.ge.interval m) m ↔ k ∈ Degree.Comparison.eq.interval m

      Exhaustifying the at least reading is the exactly reading, the second generalization's source.

      The neo-Gricean account #

      theorem Spector2013.necessity_implicature_of_exact {A : Set ℕ} (hA : A.Nonempty) {m : ℕ} (h : nec A (Degree.Comparison.eq.interval m)) :
      Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => nec A (Degree.Comparison.ge.interval m)) m

      Under a necessity modal the exact reading entails the wide-scope implicature: required to solve exactly three entails required to solve at least three and not required to solve at least four.

      theorem Spector2013.necessity_implicature_ne_exact (m : ℕ) :
      ∃ (A : Set ℕ), Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => nec A (Degree.Comparison.ge.interval m)) m ∧ ¬nec A (Degree.Comparison.eq.interval m)

      The converse fails: the requirement may be met by three or four, so the numeral loses its exact reading under the modal while the implicature is still triggered.

      Under negation the scale reverses: the alternative with the next numeral is weaker.

      The indirect implicature the account predicts for Peter didn't solve n + 1 problems: denying the stronger alternative didn't solve n yields exactly n, which is not perceived.

      theorem Spector2013.atMost_reading_not_entails_literal (m : ℕ) :
      ∃ (B : ℕ → Prop), (∀ k ∈ Degree.Comparison.le.interval m, ¬B k) ∧ ¬∀ k ∈ Degree.Comparison.gt.interval m, ¬B k

      A pragmatic strengthening entails the literal meaning, so the at most reading of if you have three children, you do not qualify is out of the account's reach: it does not entail the at least reading's consequence that more than three disqualify.

      The underspecification account #

      theorem Spector2013.poss_atMost_of_le {A : Set ℕ} {k m : ℕ} (hk : k ∈ A) (h : k ≤ m) :

      The lexical at most entry under a possibility modal is satisfied by any accessible value at or below the numeral: Sue can have 2000 calories would be true as soon as she can have one.

      theorem Spector2013.poss_implicature_iff (A : Set ℕ) (m : ℕ) :
      Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => poss A (Degree.Comparison.ge.interval m)) m ↔ poss A (Degree.Comparison.ge.interval m) ∧ nec A (Degree.Comparison.le.interval m)

      The intended reading is the neo-Gricean one: the at least reading under the possibility modal, exhaustified, says that no accessible value exceeds the numeral.

      The exactly-only account #

      theorem Spector2013.exact_extends_downward {B : ℕ → Prop} (hB : ∀ (k k' : ℕ), k ≤ k' → B k → B k') {m : ℕ} (h : ¬B m) (k : ℕ) :
      k ∈ Degree.Comparison.le.interval m → ¬B k

      With a law-like background that is monotone in the count, the exact reading of the antecedent extends downward: if exactly three children disqualify, so do fewer.

      theorem Spector2013.exact_extends_upward {B : ℕ → Prop} (hB : ∀ (k k' : ℕ), k ≤ k' → B k → B k') {m : ℕ} (h : B m) (k : ℕ) :

      The same holds upward: if exactly three children qualify, so do more.

      theorem Spector2013.atLeast_of_exact_background {B : ℕ → Prop} {m k : ℕ} (h : k ∈ Degree.Comparison.eq.interval m) :

      In an upward-entailing context no background can weaken the exact reading, which entails the at least reading: I have four chairs; in fact, I have five is consistent only with the latter.

      theorem Spector2013.not_nec_exact_Ici (m : ℕ) :

      In a degree use the exact reading under necessity is false whenever more than the numeral is admitted: one has to be exactly 18 is not what the voting rule says.

      theorem Spector2013.nec_Ici_exh_iff (n m : ℕ) :
      Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => nec (Set.Ici n) (Degree.Comparison.ge.interval m)) m ↔ n = m

      The exhaustified at least reading under necessity says that the numeral is the minimum required.

      The ambiguity account and the third generalization #

      Unembedded, the at most reading does not entail the exact reading, so no background knowledge can produce it by strengthening.

      Under negation it does: nobody read four or fewer entails nobody read exactly four, which is why the at most reading surfaces only in downward-entailing environments.

      Exhaustivity operators and embedded implicatures #

      theorem Spector2013.wide_scope_ne_narrow (m : ℕ) :
      ∃ (A : Set ℕ), poss A (Degree.Comparison.eq.interval m) ∧ ¬Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => poss A (Degree.Comparison.ge.interval m)) m

      The operator above the modal, possible at least n and not possible at least n + 1, differs from the operator below it, possible exactly n: the former fails, the latter holds, when both n and n + 1 are possible.

      theorem Spector2013.narrow_ne_base (m : ℕ) :

      And the operator below the modal differs from its absence: when only n + 1 is possible, possible at least n holds and possible exactly n does not.

      theorem Spector2013.atLeast_parse_contradiction {S : Type u_1} (n : S → ℕ) (managed : S → Prop) (m : ℕ) (h : ∀ (s : S), nec (Set.Ici (n s)) (Degree.Comparison.ge.interval m) → managed s) :
      ¬∃ (s : S), m < n s ∧ ¬managed s

      The professor sentence on the at least parse contradicts its continuation but not when she asked us to solve more: the situations demanding more are situations demanding at least the numeral.

      theorem Spector2013.exact_parse_vacuous {S : Type u_1} (n : S → ℕ) (m : ℕ) (s : S) :
      ¬nec (Set.Ici (n s)) (Degree.Comparison.eq.interval m)

      The exactly parse is vacuous when more than the demanded number may always be solved.

      theorem Spector2013.intermediate_parse_iff {S : Type u_1} (n : S → ℕ) (managed : S → Prop) (m : ℕ) :
      (∀ (s : S), Exhaustification.exhAgainst (fun (x1 x2 : ℕ) => x1 < x2) (fun (m : ℕ) => nec (Set.Ici (n s)) (Degree.Comparison.ge.interval m)) m → managed s) ↔ ∀ (s : S), n s = m → managed s

      The intermediate embedded implicature, the operator between whenever and demanded, restricts the quantification to the situations whose minimum is the numeral.