Enguehard (2024): What number marking on indefinites means: conceivability presuppositions and sensitivity to probabilities

Singular and plural indefinites infer exactly one witness and at least two, (1), but under negation both mean that there is none, (2)–(3). Following Spector and Zweig these inferences are scalar enrichments of a weak existential meaning, the exhaustifications of TieuEtAl2020, and the cardinalities a number fits are those English gives a referent of that many individuals. Enguehard shows that what survives negation is a conceivability presupposition (7): each number presupposes that a witness set it fits is conceivable, so a book has no table of contents and no chapters, (5)–(6).

In a production experiment the share of plural among negated indefinites rises gradiently with the probability that symbols come in multiples, and both numbers are produced at parity, (10)–(11). Productions form a kernel from conditions, and the categorical rule that Maximize Presupposition derives from Farkas and de Swart's prototypicality generalization (8) is a zero-one law, which the experiment refutes (§4.1). Enguehard's account has speakers prefer referents that later continuations can resume: a negated indefinite sets one up, as in the bilateral dynamic semantics of Krahmer and Muskens and of Elliott, and a pronoun resuming it bears its number, as Sudo assumes, and must fit the witness set, (14)–(23). The preference yields the conceivability presupposition, which fails exactly where the chance of ineffability is certain (§6).

Main statements

• useful_iff_negated_ne_zero: preferring useful referents yields the conceivability presupposition.
• negated_ne_zero_iff_ineffability_ne_one: the presupposition holds exactly when ineffability is not certain.
• unblocked_mpPresup_isCompl, not_H2_of_isZeroOneMeasure: Maximize Presupposition puts the two numbers in complementary distribution, and a speaker in complementary distribution is not gradient.
• not_H2_of_follows_bestGuess: a speaker producing only best guesses is not gradient either.

Implementation notes

• Worlds are witness cardinalities, as in TieuEtAl2020, and the conceivable cardinalities are a parameter, so the presupposition is constant across worlds. A negated indefinite is a trivalent proposition ℕ → SignType, undefined where its presupposition fails.
• A production is a negated indefinite of some number or another strategy (none), the three categories of Figure 2, and the hypotheses concern the productions conditioned on the indefinites, the second analysis of footnote 8. Figure 2 is a plot, so no share is typed.
• The limiting case takes the conceivable cardinalities to be those of positive probability, and a condition enters as the probability of multiples given a witness.
• The negated indefinites of (2) and the negative ones of (3) are both Polarity.negative.

TODO

• Exact minimization makes the best guess a majority rule (bestGuess_plural_iff), so a speaker producing only best guesses is categorical off parity, while Figure 2 shows both numbers in every intermediate condition. The gradience needs a probabilistic choice rule over ineffability, or variation in the distribution each participant saw (footnote 5), which the paper leaves open.
• Projection out of questions (§2) awaits a question semantics over trivalent propositions.

References

• [Eng24]
• [Spe07a]
• [Zwe09]
• [TBRC20]
• [FdS10]
• [Sau03]
• [KM95]
• [Ell20b]
• [Sud12b]

The number inference

def Enguehard2024.inference (n : Number) : Set ℕ

The number inference of a positive indefinite, (1), holds of the witness cardinalities that English gives the number.

Equations

• Enguehard2024.inference n = {k : ℕ | 1 ≤ k ∧ English.Nouns.numberSystem.ofCard k = n}

@[simp]

theorem Enguehard2024.inference_singular : inference Number.singular = TieuEtAl2020.singular

@[simp]

theorem Enguehard2024.inference_plural : inference Number.plural = TieuEtAl2020.strong

theorem Enguehard2024.inference_subset_weak (n : Number) : inference n ⊆ TieuEtAl2020.weak

theorem Enguehard2024.compl_weak : TieuEtAl2020.weakᶜ = {0}

theorem Enguehard2024.exhIE_weak_inference_plural : Exhaustification.exhIE {TieuEtAl2020.weak, inference Number.plural} TieuEtAl2020.weak = inference Number.singular

The singular's inference is its weak meaning exhaustified against (4), two, whose meaning is the plural's inference.

theorem Enguehard2024.exhIE_weak_inference_singular : Exhaustification.exhIE {TieuEtAl2020.weak, inference Number.singular} TieuEtAl2020.weak = inference Number.plural

The plural's inference is its weak meaning exhaustified against the enriched singular.

theorem Enguehard2024.exhIE_compl (m : Number) : Exhaustification.exhIE {TieuEtAl2020.weakᶜ, (inference m)ᶜ} TieuEtAl2020.weakᶜ = {0}

Under negation every competitor is entailed, so nothing is excluded and either number conveys that there is no witness, (2)–(3).

The rows of (1)–(3)

def Enguehard2024.numberTable : List (String × Number)

The rows name the numbers by these strings.

Equations

• Enguehard2024.numberTable = [("sg", Number.singular), ("pl", Number.plural)]

def Enguehard2024.polarityTable : List (String × Polarity)

The rows name the polarities by these strings, negated (2) and negative (3) indefinites both being negative.

Equations

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

def Enguehard2024.inferenceTable : List (String × Set ℕ)

The rows print the inferences as these sets of witness cardinalities.

Equations

• Enguehard2024.inferenceTable = [("one", {1}), ("atLeastTwo", {k : ℕ | 2 ≤ k}), ("zero", {0})]

structure Enguehard2024.IndefiniteRow : Type

An indefinite of (1)–(3) records its number, its polarity and the inference it carries.

• number : Number
• polarity : Polarity
• inference : Set ℕ

def Enguehard2024.IndefiniteRow.ofDatum (ex : Datum) : Option IndefiniteRow

An example yields a row when it records each feature.

Equations

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

def Enguehard2024.indefiniteRows : List IndefiniteRow

The examples (1)–(3) give the indefinite rows.

Equations

• Enguehard2024.indefiniteRows = List.filterMap Enguehard2024.IndefiniteRow.ofDatum Enguehard2024.Examples.all

theorem Enguehard2024.indefiniteRows_inference (r : IndefiniteRow) : r ∈ indefiniteRows → r.inference = if r.polarity = Polarity.positive then inference r.number else {0}

A positive indefinite carries the inference of its number and a negated one the empty witness set, whatever its number, (1)–(3).

The conceivability presupposition

noncomputable def Enguehard2024.negated (K : Set ℕ) (n : Number) : ℕ → SignType

The negated indefinite of number n, where the conceivable witness cardinalities are K, asserts that there is no witness and presupposes that a cardinality its number fits is conceivable, (7).

Equations

• Enguehard2024.negated K n = {_k : ℕ | (K ∩ Enguehard2024.inference n).Nonempty}.indicator fun (k : ℕ) => SignType.ofProp (k ∈ TieuEtAl2020.weakᶜ)

theorem Enguehard2024.negated_ne_zero_iff {K : Set ℕ} {n : Number} {k : ℕ} : negated K n k ≠ 0 ↔ (K ∩ inference n).Nonempty

theorem Enguehard2024.negated_eq_negated {K : Set ℕ} {n n' : Number} {k : ℕ} (h : negated K n k ≠ 0) (h' : negated K n' k ≠ 0) : negated K n k = negated K n' k

Both numbers assert the same thing under negation, so they agree wherever both are defined.

theorem Enguehard2024.support_negated_projects (K : Set ℕ) (n : Number) (q : ℕ → SignType) : Function.support (-negated K n) = Function.support (negated K n) ∧ (Function.support fun (k : ℕ) => (-negated K n k).joinMiddle (q k)) ⊆ Function.support (negated K n)

The presupposition projects through negation and out of a conditional antecedent (§2).

def Enguehard2024.tableOfContents : Set ℕ

A book has at most one table of contents.

Equations

• Enguehard2024.tableOfContents = Set.Iic 1

def Enguehard2024.chapters : Set ℕ

A book never has a single chapter.

Equations

• Enguehard2024.chapters = {1}ᶜ

theorem Enguehard2024.negated_tableOfContents : negated tableOfContents Number.singular 0 ≠ 0 ∧ negated tableOfContents Number.plural 0 = 0

The singular presupposition of table of contents is met and the plural one fails, (5).

theorem Enguehard2024.negated_chapters : negated chapters Number.plural 0 ≠ 0 ∧ negated chapters Number.singular 0 = 0

The plural presupposition of chapters is met and the singular one fails, (6).

def Enguehard2024.nounTable : List (String × Set ℕ)

The rows name the nouns, each standing for its conceivable cardinalities.

Equations

• Enguehard2024.nounTable = [("tableOfContents", Enguehard2024.tableOfContents), ("chapters", Enguehard2024.chapters)]

structure Enguehard2024.BookRow : Type

A negated indefinite of (5)–(6) records its noun's conceivable cardinalities, its number and its judgment.

• noun : Set ℕ
• number : Number
• judgment : Judgment

def Enguehard2024.BookRow.ofDatum (ex : Datum) : Option BookRow

An example yields a row when it records each feature.

Equations

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

def Enguehard2024.bookRows : List BookRow

The examples (5)–(6) give the book rows.

Equations

• Enguehard2024.bookRows = List.filterMap Enguehard2024.BookRow.ofDatum Enguehard2024.Examples.all

theorem Enguehard2024.bookRows_judgment (r : BookRow) : r ∈ bookRows → (r.judgment = Judgment.acceptable ↔ negated r.noun r.number 0 ≠ 0)

The judgments of (5)–(6) are the conceivability presupposition.

Referents and their continuations

def Enguehard2024.pronounTable : List (String × PersonalPronoun)

The rows name the pronouns by their forms.

Equations

• Enguehard2024.pronounTable = [("it", English.Pronouns.it), ("they", English.Pronouns.they)]

structure Enguehard2024.ContinuationRow : Type

A continuation of (18)–(19) records the number of the negated indefinite, the pronoun resuming it and the judgment.

• antecedent : Number
• pronoun : PersonalPronoun
• judgment : Judgment

@[instance_reducible]

instance Enguehard2024.instDecidableEqContinuationRow : DecidableEq ContinuationRow

Equations

• Enguehard2024.instDecidableEqContinuationRow = Enguehard2024.instDecidableEqContinuationRow.decEq

def Enguehard2024.instDecidableEqContinuationRow.decEq (x✝ x✝¹ : ContinuationRow) : Decidable (x✝ = x✝¹)

Equations

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

def Enguehard2024.ContinuationRow.ofDatum (ex : Datum) : Option ContinuationRow

An example yields a row when it records each feature.

Equations

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

def Enguehard2024.continuationRows : List ContinuationRow

The examples (18)–(19) give the continuation rows.

Equations

• Enguehard2024.continuationRows = List.filterMap Enguehard2024.ContinuationRow.ofDatum Enguehard2024.Examples.all

theorem Enguehard2024.continuationRows_match (r : ContinuationRow) : r ∈ continuationRows → (r.judgment = Judgment.acceptable ↔ r.pronoun.number = some r.antecedent)

A pronoun resuming a negated indefinite bears its number, (18)–(19).

def Enguehard2024.Usable (n : Number) (k : ℕ) : Prop

The referent of an indefinite of number n can be resumed when the witness set has k members, that is, when a third person pronoun bears n and, read maximally, its number fits k.

Equations

• Enguehard2024.Usable n k = ∃ p ∈ English.Pronouns.pronouns, p.person = some Person.third ∧ p.number = some n ∧ k ∈ Enguehard2024.inference n

theorem Enguehard2024.usable_iff {n : Number} (hn : n ∈ English.Nouns.numberSystem.values) {k : ℕ} : Usable n k ↔ k ∈ inference n

theorem Enguehard2024.not_usable_singular_of_two_le {k : ℕ} (hk : 2 ≤ k) : ¬Usable Number.singular k

The denier of (22) has a witness and no licit pronoun, since the referent of a negated singular indefinite cannot be resumed when there are several circles.

def Enguehard2024.Useful (K : Set ℕ) (n : Number) : Prop

A referent of number n is useful when some conceivable witness set lets a continuation resume it, (23).

Equations

• Enguehard2024.Useful K n = ∃ k ∈ K, Enguehard2024.Usable n k

theorem Enguehard2024.useful_iff_negated_ne_zero {n : Number} (hn : n ∈ English.Nouns.numberSystem.values) (K : Set ℕ) (k : ℕ) : Useful K n ↔ negated K n k ≠ 0

Preferring useful referents, (23), yields the conceivability presupposition (7).

theorem Enguehard2024.exists_not_usable {K : Set ℕ} (hsg : (K ∩ inference Number.singular).Nonempty) (hpl : (K ∩ inference Number.plural).Nonempty) {n : Number} (hn : n ∈ English.Nouns.numberSystem.values) : ∃ k ∈ K, 1 ≤ k ∧ ¬Usable n k

Where both numbers are conceivable, (23) cannot be obeyed, since each number's referent cannot be resumed in some conceivable situation with a witness.

The production experiment

inductive Enguehard2024.Condition : Type

The five conditions (11) differ in how often symbols come in multiples.

• sg : Condition
• sgPl : Condition
• mix : Condition
• plSg : Condition
• pl : Condition

@[instance_reducible]

instance Enguehard2024.instDecidableEqCondition : DecidableEq Condition

Equations

• Enguehard2024.instDecidableEqCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Enguehard2024.instReprCondition : Repr Condition

Equations

• Enguehard2024.instReprCondition = { reprPrec := Enguehard2024.instReprCondition.repr }

def Enguehard2024.instReprCondition.repr : Condition → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Enguehard2024.instFintypeCondition : Fintype Condition

Equations

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

def Enguehard2024.Condition.pMultiple : Condition → ℚ≥0

c.pMultiple is the probability in condition c that symbols of a kind come in multiples when there are any, (11).

Equations

• Enguehard2024.Condition.sg.pMultiple = 0
• Enguehard2024.Condition.sgPl.pMultiple = 1 / 10
• Enguehard2024.Condition.mix.pMultiple = 1 / 2
• Enguehard2024.Condition.plSg.pMultiple = 9 / 10
• Enguehard2024.Condition.pl.pMultiple = 1

theorem Enguehard2024.Condition.pMultiple_injective : Function.Injective pMultiple

@[instance_reducible]

instance Enguehard2024.instLinearOrderCondition : LinearOrder Condition

The conditions are ordered by the frequency of multiples, the order of Figure 2.

Equations

• Enguehard2024.instLinearOrderCondition = LinearOrder.lift' Enguehard2024.Condition.pMultiple Enguehard2024.Condition.pMultiple_injective

@[instance_reducible]

instance Enguehard2024.instMeasurableSpaceCondition : MeasurableSpace Condition

Equations

• Enguehard2024.instMeasurableSpaceCondition = ⊤

@[instance_reducible]

instance Enguehard2024.instMeasurableSpaceNumber_studies : MeasurableSpace Number

Equations

• Enguehard2024.instMeasurableSpaceNumber_studies = ⊤

instance Enguehard2024.instDiscreteMeasurableSpaceNumber_studies : DiscreteMeasurableSpace Number

@[reducible, inline]

abbrev Enguehard2024.Production : Type

A production is a negated indefinite of some number, or another strategy.

Equations

• Enguehard2024.Production = Option Number

def Enguehard2024.indefinite : Set Production

indefinite is the set of productions that are negated indefinites.

Equations

• Enguehard2024.indefinite = Set.range some

def Enguehard2024.H0 (κ : ProbabilityTheory.Kernel Condition Production) : Prop

Under H0, (10a), productions do not depend on the distribution.

Equations

• Enguehard2024.H0 κ = ∀ (c c' : Enguehard2024.Condition), κ c = κ c'

def Enguehard2024.H1 (κ : ProbabilityTheory.Kernel Condition Production) : Prop

Under H1, (10b), the singular is produced where uniqueness dominates and the plural otherwise, including at parity.

Equations

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

def Enguehard2024.H2 (κ : ProbabilityTheory.Kernel Condition Production) : Prop

Under H2, (10c), the more multiples there are the more plural is produced, and both numbers are produced at parity.

Equations

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

theorem Enguehard2024.H1.not_H0 {κ : ProbabilityTheory.Kernel Condition Production} (h : H1 κ) : ¬H0 κ

theorem Enguehard2024.not_H2_of_isZeroOneMeasure {κ : ProbabilityTheory.Kernel Condition Production} [MeasureTheory.IsZeroOneMeasure (κ Condition.mix)[|indefinite]] : ¬H2 κ

A speaker in complementary distribution at parity is not gradient (§4.1).

theorem Enguehard2024.H1.not_H2 {κ : ProbabilityTheory.Kernel Condition Production} (h : H1 κ) : ¬H2 κ

Maximize Presupposition over the conditions

def Enguehard2024.englishAlts : Number → Set Number

The English numbers are each other's alternatives.

Equations

• Enguehard2024.englishAlts x✝ = {n : Number | n ∈ English.Nouns.numberSystem.values}

def Enguehard2024.mpPresup (S : Set Condition) : Number → Set Condition

In the Maximize Presupposition account of §4.1 the singular presupposes S of the condition, the plural presupposes nothing, and the values outside English presuppose the impossible.

Equations

• Enguehard2024.mpPresup S Number.singular = S
• Enguehard2024.mpPresup S Number.plural = Set.univ
• Enguehard2024.mpPresup S x✝ = ∅

theorem Enguehard2024.unblocked_mpPresup_singular (S : Set Condition) : Competition.unblocked englishAlts (mpPresup S) Number.singular = S

theorem Enguehard2024.unblocked_mpPresup_plural {S : Set Condition} (hS : S ≠ Set.univ) : Competition.unblocked englishAlts (mpPresup S) Number.plural = Sᶜ

The plural is used exactly where the singular's presupposition fails.

theorem Enguehard2024.unblocked_mpPresup_isCompl {S : Set Condition} (hS : S ≠ Set.univ) : IsCompl (Competition.unblocked englishAlts (mpPresup S) Number.singular) (Competition.unblocked englishAlts (mpPresup S) Number.plural)

Maximize Presupposition puts the two numbers in complementary distribution over the conditions, as §4.1 says competition must.

def Enguehard2024.Follows (U : Number → Set Condition) (κ : ProbabilityTheory.Kernel Condition Production) : Prop

A production kernel follows the use conditions U when in every condition it almost surely produces a negated indefinite usable there.

Equations

• Enguehard2024.Follows U κ = ∀ (c : Enguehard2024.Condition), ∀ᵐ (p : Option Number) ∂(κ c)[|Enguehard2024.indefinite], ∀ (n : Number), p = some n → c ∈ U n

theorem Enguehard2024.Follows.eq_dirac {κ : ProbabilityTheory.Kernel Condition Production} {U : Number → Set Condition} (h : Follows U κ) {c : Condition} [MeasureTheory.IsProbabilityMeasure (κ c)[|indefinite]] {n : Number} (hn : ∀ (m : Number), c ∈ U m ↔ m = n) : (κ c)[|indefinite] = MeasureTheory.Measure.dirac (some n)

A speaker following use conditions that allow one number in a condition produces it there with certainty.

theorem Enguehard2024.Follows.H1_of_mpPresup {κ : ProbabilityTheory.Kernel Condition Production} [∀ (c : Condition), MeasureTheory.IsProbabilityMeasure (κ c)[|indefinite]] (h : Follows (Competition.unblocked englishAlts (mpPresup (Set.Iio Condition.mix))) κ) : H1 κ

Maximize Presupposition with the singular presupposing that uniqueness dominates, (8) read as uniqueness in most situations, yields H1 (§4.1).

The chance of ineffability

noncomputable def Enguehard2024.ineffability (μ : MeasureTheory.Measure ℕ) (n : Number) : ENNReal

The chance of ineffability of number n under the witness distribution μ is the probability, given a witness, that its cardinality does not fit n, so that the referent of a negated indefinite of number n cannot be resumed.

Equations

• Enguehard2024.ineffability μ n = μ[(Enguehard2024.inference n)ᶜ | TieuEtAl2020.weak]

theorem Enguehard2024.ineffability_singular (μ : MeasureTheory.Measure ℕ) : ineffability μ Number.singular = μ[TieuEtAl2020.strong | TieuEtAl2020.weak]

theorem Enguehard2024.ineffability_singular_add_plural (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsFiniteMeasure μ] (hμ : μ TieuEtAl2020.weak ≠ 0) : ineffability μ Number.singular + ineffability μ Number.plural = 1

Given a witness exactly one number fits it, so the two chances of ineffability sum to one.

theorem Enguehard2024.negated_ne_zero_iff_ineffability_ne_one (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsFiniteMeasure μ] (hμ : μ TieuEtAl2020.weak ≠ 0) (n : Number) (w : ℕ) : negated {k : ℕ | μ {k} ≠ 0} n w ≠ 0 ↔ ineffability μ n ≠ 1

The conceivability presupposition is the limiting case of the chance of ineffability (§6). With the conceivable cardinalities those of positive probability, a number's presupposition holds exactly when the chance that its referent cannot be resumed is not certain.

def Enguehard2024.BestGuess (μ : MeasureTheory.Measure ℕ) (n : Number) : Prop

A best guess under the witness distribution μ is an English number minimizing the chance of ineffability (§5.3).

Equations

• Enguehard2024.BestGuess μ n = IsMinOn (Enguehard2024.ineffability μ) {m : Number | m ∈ English.Nouns.numberSystem.values} n

theorem Enguehard2024.bestGuess_plural_iff (μ : MeasureTheory.Measure ℕ) [MeasureTheory.IsFiniteMeasure μ] (hμ : μ TieuEtAl2020.weak ≠ 0) : BestGuess μ Number.plural ↔ 1 / 2 ≤ μ[TieuEtAl2020.strong | TieuEtAl2020.weak]

The plural is a best guess exactly when multiples are at least as likely as not.

theorem Enguehard2024.not_H2_of_follows_bestGuess {κ : ProbabilityTheory.Kernel Condition Production} (μ : Condition → MeasureTheory.Measure ℕ) [∀ (c : Condition), MeasureTheory.IsFiniteMeasure (μ c)] (hμ : ∀ (c : Condition), (μ c) TieuEtAl2020.weak ≠ 0) (hp : ∀ (c : Condition), (μ c)[TieuEtAl2020.strong | TieuEtAl2020.weak] = ↑↑c.pMultiple) (h : Follows (fun (n : Number) => {c : Condition | BestGuess (μ c) n}) κ) : ¬H2 κ

A speaker who produces only best guesses is not gradient, since when the conditions teach their probabilities of multiples only the singular is a best guess in the Sg and SgPl conditions.