Enguehard (2024): What Number Marking on Indefinites Means

@cite{enguehard-2024}

Enguehard, Émile. 2024. What number marking on indefinites means: conceivability presuppositions and sensitivity to probabilities. Proceedings of Sinn und Bedeutung 28, 289–302.

Core Contributions

1. Conceivability presupposition (generalization 7): a sg (resp. pl) indefinite presupposes that it is conceivable the witness set has exactly one (resp. more than one) member. This presupposition projects under negation, questions, and conditionals — unlike scalar implicatures which are blocked in DE environments.

2. Gradient sensitivity (§3): an experiment shows that speakers' number choice on negated indefinites tracks the probability distribution over witness-set cardinalities, not a categorical presuppositional or MP-based boundary.

3. Forward-looking cooperation (§5.3, principle 23): speakers choose number to set up discourse referents whose number feature will be useful in potential continuations — a Manner-like maxim sensitive to prototypicality.

4. Dynamic potential (§5.1–5.2): negated indefinites introduce discourse referents accessible in bilateral dynamic semantics (@cite{elliott-2020}); the number feature on these referents constrains future pronoun binding, grounding the forward-looking principle.

Integration Points

• PhiFeatures.sgCardConceivable / plCardConceivable — the conceivability presuppositions defined in §7 of PhiFeatures.lean
• Sauerland2003 — challenges MP-derived complementary distribution
• Multiplicity — challenges the implicature theory's categorical predictions with gradient production data
• MaximizePresupposition.phiMP — MP is underdetermined when both conceivability presuppositions are satisfied
• PresuppositionContext.presupSatisfiable — conceivability = satisfiability in context

Relation to Sauerland (2003)

@cite{sauerland-2003} treats plSem as vacuous (no presupposition). Enguehard argues that indefinite plurals DO carry a non-trivial conceivability presupposition — not about the entity but about the predicate's extension. This refines rather than replaces Sauerland:

• For definites, sgSem/plSem with entity-level presuppositions remain appropriate (the referent is known).
• For indefinites (especially under negation), the conceivability presupposition governs number choice: the cardinality must be conceivable, not actual.

inductive Enguehard2024.IndefNumber : Type

Indefinite number marking: the two-way contrast.

• sg : IndefNumber
• pl : IndefNumber

@[implicit_reducible]

instance Enguehard2024.instDecidableEqIndefNumber : DecidableEq IndefNumber

Equations

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

@[implicit_reducible]

instance Enguehard2024.instReprIndefNumber : Repr IndefNumber

Equations

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

def Enguehard2024.instReprIndefNumber.repr : IndefNumber → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Enguehard2024.instInhabitedIndefNumber : Inhabited IndefNumber

Equations

• Enguehard2024.instInhabitedIndefNumber = { default := Enguehard2024.instInhabitedIndefNumber.default }

def Enguehard2024.instInhabitedIndefNumber.default : IndefNumber

Equations

• Enguehard2024.instInhabitedIndefNumber.default = Enguehard2024.IndefNumber.sg

inductive Enguehard2024.Condition : Type

Experimental conditions from §3.2: the probability that symbols of a given kind appear in multiples on a card (when present at all). Each condition determines a pMultiple value.

• sg : Condition

  0% chance of multiple symbols.

• sgPl : Condition

  10% chance of multiple symbols.

• mix : Condition

  50% chance of multiple symbols.

• plSg : Condition

  90% chance of multiple symbols.

• pl : Condition

  100% chance of multiple symbols.

@[implicit_reducible]

instance Enguehard2024.instDecidableEqCondition : DecidableEq Condition

Equations

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

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

Equations

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

@[implicit_reducible]

instance Enguehard2024.instReprCondition : Repr Condition

Equations

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

def Enguehard2024.instInhabitedCondition.default : Condition

Equations

• Enguehard2024.instInhabitedCondition.default = Enguehard2024.Condition.sg

@[implicit_reducible]

instance Enguehard2024.instInhabitedCondition : Inhabited Condition

Equations

• Enguehard2024.instInhabitedCondition = { default := Enguehard2024.instInhabitedCondition.default }

def Enguehard2024.Condition.pMultiple : Condition → ℚ

The probability of multiple symbols for each condition.

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

def Enguehard2024.Condition.pUnique (c : Condition) : ℚ

The probability of a unique symbol (complement).

Equations

• c.pUnique = 1 - c.pMultiple

§2: Book Examples — Conceivability in Action

@cite{enguehard-2024} examples (5)–(6) and @cite{farkas-de-swart-2010} generalization (8) illustrate conceivability presuppositions via world knowledge about books:

• Table of contents: prototypically unique → sg conceivable, pl not
• Chapter: prototypically multiple → sg not (prototypically), pl conceivable

We model this with Bool situations: false = prototypical, true = rare.

def Enguehard2024.tocCard : Bool → ℕ

A book's table-of-contents count in conceivable situations.

Equations

• Enguehard2024.tocCard false = 1
• Enguehard2024.tocCard true = 0

def Enguehard2024.allConceivable' : Bool → Prop

All situations are conceivable for table of contents.

Equations

• Enguehard2024.allConceivable' x✝ = True

theorem Enguehard2024.toc_sg_conceivable : Semantics.Presupposition.PhiFeatures.sgCardConceivable tocCard allConceivable'

Table of contents: sg conceivable (prototypical situation has |C|=1).

theorem Enguehard2024.toc_pl_not_conceivable : ¬Semantics.Presupposition.PhiFeatures.plCardConceivable tocCard allConceivable'

Table of contents: pl NOT conceivable (no situation has |C|≥2).

def Enguehard2024.chapterCard : Bool → ℕ

A book's chapter count in conceivable situations.

Equations

• Enguehard2024.chapterCard false = 5
• Enguehard2024.chapterCard true = 1

theorem Enguehard2024.chapter_pl_conceivable : Semantics.Presupposition.PhiFeatures.plCardConceivable chapterCard allConceivable'

Chapters: pl conceivable (prototypical situation has |C|=5 ≥ 2).

theorem Enguehard2024.chapter_sg_technically_conceivable : Semantics.Presupposition.PhiFeatures.sgCardConceivable chapterCard allConceivable'

Chapters: sg also conceivable (rare situation has |C|=1), BUT @cite{farkas-de-swart-2010} argues this is prototypically dispreferred because unique-chapter books are rare. The conceivability presupposition per se is satisfied, but prototypicality (= frequency) governs actual use.

theorem Enguehard2024.book_contrast : (Semantics.Presupposition.PhiFeatures.sgCardConceivable tocCard allConceivable' ∧ ¬Semantics.Presupposition.PhiFeatures.plCardConceivable tocCard allConceivable') ∧ Semantics.Presupposition.PhiFeatures.sgCardConceivable chapterCard allConceivable' ∧ Semantics.Presupposition.PhiFeatures.plCardConceivable chapterCard allConceivable'

Books: both conceivability presuppositions hold for chapters, but only sg holds for tables of contents. This contrast drives the felicity judgments in examples (5)–(6).

§3: Production Experiment (§3.2–3.3)

100 participants (Prolific). Each learned a probability distribution over symbol cardinalities through a card-validity task. After 20 trials, they described the rule by completing "the card is valid when..."

The result: SG productions decrease and PL productions increase monotonically with pMultiple, consistent with H₂ (gradient sensitivity to prototypicality/frequency).

structure Enguehard2024.ProductionResult : Type

Observed production proportions by condition (from Figure 2). Values are approximate readings from the published graph.

• condition : Condition
• sgRate : ℚ
• plRate : ℚ
• otherRate : ℚ

def Enguehard2024.instReprProductionResult.repr : ProductionResult → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Enguehard2024.instReprProductionResult : Repr ProductionResult

Equations

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

def Enguehard2024.sgResult : ProductionResult

Observed data: approximate proportions from Figure 2.

Equations

• Enguehard2024.sgResult = { condition := Enguehard2024.Condition.sg, sgRate := 73 / 100, plRate := 3 / 100, otherRate := 24 / 100 }

def Enguehard2024.sgPlResult : ProductionResult

Equations

• Enguehard2024.sgPlResult = { condition := Enguehard2024.Condition.sgPl, sgRate := 63 / 100, plRate := 10 / 100, otherRate := 27 / 100 }

def Enguehard2024.mixResult : ProductionResult

Equations

• Enguehard2024.mixResult = { condition := Enguehard2024.Condition.mix, sgRate := 50 / 100, plRate := 25 / 100, otherRate := 25 / 100 }

def Enguehard2024.plSgResult : ProductionResult

Equations

• Enguehard2024.plSgResult = { condition := Enguehard2024.Condition.plSg, sgRate := 30 / 100, plRate := 47 / 100, otherRate := 23 / 100 }

def Enguehard2024.plResult : ProductionResult

Equations

• Enguehard2024.plResult = { condition := Enguehard2024.Condition.pl, sgRate := 0, plRate := 80 / 100, otherRate := 20 / 100 }

def Enguehard2024.allResults : List ProductionResult

Equations

• Enguehard2024.allResults = [Enguehard2024.sgResult, Enguehard2024.sgPlResult, Enguehard2024.mixResult, Enguehard2024.plSgResult, Enguehard2024.plResult]

theorem Enguehard2024.sg_rate_monotone_decreasing : sgResult.sgRate ≥ sgPlResult.sgRate ∧ sgPlResult.sgRate ≥ mixResult.sgRate ∧ mixResult.sgRate ≥ plSgResult.sgRate ∧ plSgResult.sgRate ≥ plResult.sgRate

SG rate weakly decreases across conditions (monotonicity).

theorem Enguehard2024.pl_rate_monotone_increasing : sgResult.plRate ≤ sgPlResult.plRate ∧ sgPlResult.plRate ≤ mixResult.plRate ∧ mixResult.plRate ≤ plSgResult.plRate ∧ plSgResult.plRate ≤ plResult.plRate

PL rate weakly increases across conditions (monotonicity).

theorem Enguehard2024.sg_condition_sg_dominates : sgResult.sgRate > sgResult.plRate

In the extreme Sg condition, SG dominates PL.

theorem Enguehard2024.pl_condition_pl_dominates : plResult.plRate > plResult.sgRate

In the extreme Pl condition, PL dominates SG.

theorem Enguehard2024.mix_condition_both_used : mixResult.sgRate > 0 ∧ mixResult.plRate > 0

In the Mix condition, BOTH SG and PL are used — production is NOT complementary. This is the central empirical challenge to MP and scalar implicature approaches.

theorem Enguehard2024.sg_pl_production_asymmetry : sgResult.plRate > 0 ∧ plResult.sgRate = 0

Asymmetry between Sg and Pl conditions: some pl productions in Sg but NO sg productions in Pl. This reflects the semantic weakness of plural ("one or more") vs singular ("exactly one"): pl can intrude into sg-biased conditions because it's semantically compatible, but sg cannot intrude into pl-biased conditions.

§4: MP Underprediction

@cite{sauerland-2003}'s MP-based account (and all scalar-implicature accounts) predicts complementary distribution: where sg's presupposition is satisfied, use sg; elsewhere, use pl. The experiment shows overlapping use in all intermediate conditions.

The structural diagnosis: conceivability presuppositions of sg and pl are incomparable (conceivability_presups_incomparable in PhiFeatures.lean §7). MP requires a strength ordering; when presuppositions are not ordered, MP is silent.

This does NOT mean MP is wrong — it means MP underdetermines the choice in intermediate cases, and the residual variation is governed by probabilistic/prototypicality factors.

theorem Enguehard2024.mix_both_conceivable (witnessCard : Bool → ℕ) (h₁ : witnessCard false = 1) (h₂ : witnessCard true ≥ 2) : (Semantics.Presupposition.PhiFeatures.sgCardConceivable witnessCard fun (x : Bool) => True) ∧ Semantics.Presupposition.PhiFeatures.plCardConceivable witnessCard fun (x : Bool) => True

In the Mix condition, both conceivability presuppositions are satisfied: the card-validity task exposed participants to both unique and multiple symbols. The both_sg_pl_conceivable theorem from PhiFeatures.lean applies directly.

theorem Enguehard2024.conceivability_same_assertion {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (w : W) : { presup := fun (x : W) => Semantics.Presupposition.PhiFeatures.sgCardConceivable witnessCard conceivable, assertion := fun (x : W) => True }.assertion w ↔ { presup := fun (x : W) => Semantics.Presupposition.PhiFeatures.plCardConceivable witnessCard conceivable, assertion := fun (x : W) => True }.assertion w

The conceivability presuppositions have the same assertive content — both sg and pl indefinites contribute the same truth conditions (especially under negation: |C| = 0 for both). This mirrors Sauerland2003.sg_pl_same_assertion at the conceivability level: the competition is entirely presuppositional. But unlike Sauerland's entity-level presuppositions, the conceivability presuppositions are not ordered by strength.

§5: Gradient Data vs Categorical Predictions

Multiplicity.implicature_uniquely_predicts asserts the implicature theory uniquely predicts three patterns (children compute fewer, correlation with SI rates, polarity asymmetry). Enguehard's experiment reveals a fourth dimension where the implicature theory makes the wrong prediction: it predicts categorical (complementary) distribution, but production is gradient.

This does not refute the implicature theory for positive uses — the multiplicity inference in UE contexts remains well-modeled as an implicature/pex effect. But it shows the implicature theory is incomplete for negative uses, where the conceivability presupposition governs number choice.

theorem Enguehard2024.null_hypothesis_refuted : sgResult.sgRate ≠ plResult.sgRate

The experimental data is inconsistent with H₀ (no effect of distribution): SG rate differs across extreme conditions.

theorem Enguehard2024.gradient_hypothesis_supported : sgResult.sgRate > plResult.sgRate ∧ mixResult.sgRate > 0 ∧ mixResult.plRate > 0

The experimental data IS consistent with H₂ (gradient): SG rate monotonically decreases, PL rate monotonically increases, and intermediate conditions show overlap.

§6: Provide Useful Referents (Principle 23)

@cite{enguehard-2024} proposes a forward-looking pragmatic principle:

Provide useful referents: between utterances of equivalent acceptability as per other principles, prefer the one that sets up referents that can be used in well-formed continuations.

This is a Manner-like maxim: among truth-conditionally equivalent alternatives, prefer the one that facilitates future discourse.

Under negation, indefinites introduce discourse referents bearing the indefinite's number feature (cf. @cite{elliott-2020}'s bilateral semantics). The number feature constrains future pronoun binding:

• "There is no blue circle₁ on the card. It₁ is hard to see." (sg → "it")
• "There are no blue circles₂ on the card. They₂ are hard to see." (pl → "they")

When the pronoun's number does not match the actual witness cardinality, the continuation is infelicitous — the referent is "useless."

Formalization as Production Utility

"Provide useful referents" reduces to a production utility function: the speaker's expected payoff from choosing number n equals the probability that a continuation requiring a referent of number n would be well-formed. This probability tracks the distribution over prototypical witness cardinalities.

def Enguehard2024.productionUtility (pUnique : ℚ) : IndefNumber → ℚ

Production utility for a number choice given a prototypicality distribution. The utility of sg = P(unique witness in prototypical situations); the utility of pl = P(multiple witnesses).

Equations

• Enguehard2024.productionUtility pUnique Enguehard2024.IndefNumber.sg = pUnique
• Enguehard2024.productionUtility pUnique Enguehard2024.IndefNumber.pl = 1 - pUnique

theorem Enguehard2024.sg_utility_decreases (c₁ c₂ : Condition) (h : c₁.pMultiple ≤ c₂.pMultiple) : productionUtility c₂.pUnique IndefNumber.sg ≤ productionUtility c₁.pUnique IndefNumber.sg

Production utility for sg decreases with pMultiple.

theorem Enguehard2024.pl_utility_increases (c₁ c₂ : Condition) (h : c₁.pMultiple ≤ c₂.pMultiple) : productionUtility c₁.pUnique IndefNumber.pl ≤ productionUtility c₂.pUnique IndefNumber.pl

Production utility for pl increases with pMultiple.

theorem Enguehard2024.sg_utility_maximal_at_zero : productionUtility Condition.sg.pUnique IndefNumber.sg = 1

At pMultiple = 0 (Sg condition), sg utility is maximal (= 1).

theorem Enguehard2024.pl_utility_maximal_at_one : productionUtility Condition.pl.pUnique IndefNumber.pl = 1

At pMultiple = 1 (Pl condition), pl utility is maximal (= 1).

theorem Enguehard2024.mix_indifference : productionUtility Condition.mix.pUnique IndefNumber.sg = productionUtility Condition.mix.pUnique IndefNumber.pl

At pMultiple = 1/2 (Mix condition), both utilities are equal. This is the indifference point where both numbers are equally useful — explaining the overlap in production.

§7: Why Conceivability Projects Universally

The conceivability presupposition is a constant presupposition: it holds at all evaluation worlds or none, because it quantifies over conceivable situations rather than testing the evaluation world. This is the structural explanation for why it projects under negation, questions, and conditionals — constant presuppositions are immune to semantic operators that manipulate the evaluation world.

Contrast with standard sgSem: atomicity depends on the entity, so it can fail at some entities but not others. The conceivability version abstracts away from the actual entity.

def Enguehard2024.sgIndefPresup {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) : Core.Presupposition.PrProp W

The conceivability presupposition of a sg indefinite, packaged as a PrProp that is constant across evaluation worlds.

Equations

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

def Enguehard2024.plIndefPresup {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) : Core.Presupposition.PrProp W

The conceivability presupposition of a pl indefinite.

Equations

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

theorem Enguehard2024.sgIndefPresup_constant {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (w₁ w₂ : W) : Core.Presupposition.PrProp.defined w₁ (sgIndefPresup witnessCard conceivable) ↔ Core.Presupposition.PrProp.defined w₂ (sgIndefPresup witnessCard conceivable)

Conceivability presuppositions are constant: they hold at all evaluation worlds or none. This is why they project under every semantic operator — negation, questions, conditionals, modals.

theorem Enguehard2024.plIndefPresup_constant {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (w₁ w₂ : W) : Core.Presupposition.PrProp.defined w₁ (plIndefPresup witnessCard conceivable) ↔ Core.Presupposition.PrProp.defined w₂ (plIndefPresup witnessCard conceivable)

§8: Conceivability is Weaker than Pex

@cite{delpinal-bassi-sauerland-2024}'s presuppositional exhaustification (pex) derives the sharp multiplicity inference in positive contexts. For plural indefinites:

• pex(pl) presupposes ¬sg-alternative — i.e., the singular alternative (which entails |C|=1) is false at the actual world. In a positive context where a witness exists, this yields |C|≥2 AT THE ACTUAL WORLD.
• Conceivability(pl) presupposes ∃ conceivable situation with |C|≥2 — much weaker, merely requiring that multiple witnesses be possible.

The structural relationship: actual non-atomicity (from pex) ENTAILS conceivability of non-atomicity (by actual_implies_conceivable from PhiFeatures.lean), but not vice versa.

This explains the empirical asymmetry:

• Positive contexts: pex applies, deriving |C|≥2 at the actual world. Conceivability is trivially satisfied (the actual world witnesses it). The sharp multiplicity inference comes from pex, not from conceivability.
• Negative contexts: pex is blocked (no exhaustification in DE environments), but the conceivability presupposition projects (it's constant — sgIndefPresup_constant / plIndefPresup_constant). Only the weaker, gradient conceivability pattern survives.

Connection to pex infrastructure

pexIEII (from Presuppositional.lean) produces a PrProp with:

• assertion = φ (the prejacent)
• presupposition = ¬IE ∧ homog(II)

For plural with the singular alternative as the only IE member, the presupposition reduces to ¬sg. Under negation, pex_neg_presup proves the presupposition projects unchanged.

theorem Enguehard2024.conceivability_trivial_in_positive {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (w₀ : W) (hw₀ : conceivable w₀) (hpos : witnessCard w₀ ≥ 1) : witnessCard w₀ = 1 ∧ Semantics.Presupposition.PhiFeatures.sgCardConceivable witnessCard conceivable ∨ witnessCard w₀ ≥ 2 ∧ Semantics.Presupposition.PhiFeatures.plCardConceivable witnessCard conceivable

In a positive context where the actual witness set is non-empty, the actual situation witnesses sg conceivability (if |C|=1) or pl conceivability (if |C|≥2) — the presupposition is trivially satisfied and thus invisible.

theorem Enguehard2024.pex_entails_conceivability {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (w₀ : W) (hw₀ : conceivable w₀) (hpex : witnessCard w₀ ≥ 2) : Semantics.Presupposition.PhiFeatures.plCardConceivable witnessCard conceivable

Pex is stronger than conceivability: if the actual witness set has |C|≥2 (the pex-derived inference), then pl conceivability holds.

This follows directly from actual_implies_conceivable: the actual world is a conceivable world that witnesses |C|≥2.

The converse fails: conceivability only requires SOME conceivable situation to have |C|≥2, while pex requires the ACTUAL situation to.

theorem Enguehard2024.conceivability_does_not_entail_pex : ∃ (witnessCard : Bool → ℕ) (conceivable : Bool → Prop) (w₀ : Bool), conceivable w₀ ∧ witnessCard w₀ < 2 ∧ Semantics.Presupposition.PhiFeatures.plCardConceivable witnessCard conceivable

The converse of pex_entails_conceivability fails: there exist models where pl is conceivable (some conceivable situation has |C|≥2) but the actual situation has |C|=0 or |C|=1.

This is exactly the situation in negative contexts: "there are no blue circles" → |C|=0 at the actual world, but |C|≥2 may be conceivable. Pex would require |C|≥2 actually, which is false.

theorem Enguehard2024.pex_neg_preserves_presup {World : Type u_1} (ALT : Set (World → Prop)) (φ : World → Prop) (Rc : Set (World → Prop)) : (Exhaustification.Presuppositional.pexIEII ALT φ Rc).neg.presup = (Exhaustification.Presuppositional.pexIEII ALT φ Rc).presup

The pex infrastructure confirms: negating a pex'd proposition preserves its presupposition but negates its assertion. For plural: ¬pex(∃x.P(x)) asserts ¬∃x.P(x) and presupposes ¬sg-alternative. The presupposition-assertion split is what enables the conceivability pattern under negation: the presupposition (about conceivable cardinalities) is independent of the assertion (about actual cardinality).

§9: Refining the Implicature Theory

@cite{sauerland-2003}'s implicature theory (= Multiplicity.PluralTheory.implicature) correctly predicts the multiplicity inference in positive UE contexts. But it does not predict gradient production in negative contexts.

Enguehard's account is complementary: the conceivability presupposition is the underlying inference that persists across all environments; the sharp multiplicity inference in positive contexts is a strengthened version derived by pex or MP.

This parallels the scalar implicature landscape:

• Some/all: the "not all" implicature is sharp in UE, absent in DE; but "some is conceivable" is always presupposed.
• Sg/pl: the multiplicity inference is sharp in UE, absent in DE; but "unique is conceivable" / "multiple is conceivable" persists.

theorem Enguehard2024.productionUtility_normalized (pUnique : ℚ) : productionUtility pUnique IndefNumber.sg + productionUtility pUnique IndefNumber.pl = 1

The productionUtility model forms a probability distribution: sg and pl rates sum to 1 for any prototypicality parameter.

theorem Enguehard2024.productionUtility_nonneg (c : Condition) (n : IndefNumber) : 0 ≤ productionUtility c.pUnique n

Production utility is non-negative for all conditions. Combined with productionUtility_normalized, this makes productionUtility c.pUnique a probability distribution over IndefNumber.

theorem Enguehard2024.utility_predicts_extreme_dominance : productionUtility Condition.sg.pUnique IndefNumber.sg > productionUtility Condition.sg.pUnique IndefNumber.pl ∧ productionUtility Condition.pl.pUnique IndefNumber.pl > productionUtility Condition.pl.pUnique IndefNumber.sg

The production utility model correctly predicts the dominance pattern in extreme conditions, matching the observed data (sg_condition_sg_dominates, pl_condition_pl_dominates).

theorem Enguehard2024.productionUtility_characterized (f : ℚ → IndefNumber → ℚ) (hNorm : ∀ (p : ℚ), f p IndefNumber.sg + f p IndefNumber.pl = 1) (hLinear : ∀ (p : ℚ), f p IndefNumber.sg = p) (p : ℚ) (n : IndefNumber) : f p n = productionUtility p n

productionUtility is uniquely characterized by normalization (f p .sg + f p .pl = 1) and linearity (f p .sg = p). Any model satisfying both conditions IS productionUtility — it is not a free parameter but the unique solution.

§10: Conceivability = Satisfiability in Context

PresuppositionContext.presupSatisfiable c p checks whether p.presup is compatible with context set c. This is exactly Enguehard's conceivability condition at the context-set level:

• A sg indefinite's conceivability presupposition is satisfied iff the common ground is compatible with a world where |C| = 1.
• A pl indefinite's conceivability presupposition is satisfied iff the common ground is compatible with a world where |C| ≥ 2.

When the common ground rules out one cardinality entirely (e.g., it's common knowledge that books have exactly one table of contents), the corresponding conceivability presupposition fails — yielding the categorical judgments in examples (5)–(6).

theorem Enguehard2024.constant_presup_satisfied_iff_satisfiable {W : Type u_1} (witnessCard : W → ℕ) (conceivable : W → Prop) (c : Core.CommonGround.ContextSet W) (hne : c.nonEmpty) : Core.PresuppositionContext.presupSatisfied c (sgIndefPresup witnessCard conceivable) ↔ Core.PresuppositionContext.presupSatisfiable c (sgIndefPresup witnessCard conceivable)

Conceivability presuppositions are constant, so presupSatisfied and presupSatisfiable coincide for them (on non-empty contexts). Constant presuppositions are either entailed by every world or no world — there is no middle ground.

§11: Negated Indefinites in Bilateral Dynamic Semantics

@cite{enguehard-2024} §5.1–5.2 argues that negated indefinites introduce discourse referents accessible for subsequent anaphora, following @cite{elliott-2020}'s bilateral dynamic framework. The key mechanism:

1. exists_ x domain φ introduces a discourse referent x by random assignment into the positive update.
2. neg swaps positive and negative updates, so neg (exists_ x domain φ) has positive update: { p ∈ s | ∀ e ∈ domain, p.extend x e ∉ φ.positive (s.randomAssign x domain) } The possibilities that survive are those from the INPUT state s where no witness satisfies φ.
3. The discourse referent x is introduced in the INNER computation but the output possibilities come from s — so x is available for subsequent anaphora (via composition with further updates).

The number feature on the discourse referent (sg/pl) constrains what anaphoric continuations are felicitous. Enguehard argues that speakers choose the number feature to maximize the utility of the discourse referent for likely continuations — which reduces to the productionUtility model in §4.

The structural bridge

The bilateral neg ∘ exists_ construction yields possibilities from s that falsify the existential. These possibilities carry no witness in their assignments — the key structural fact is that the OUTPUT state preserves the input possibilities (those that survived universal falsification). This means the discourse referent is "set up" by the existential introduction but the output state is a subset of the input.

structure Enguehard2024.NumberedDRef : Type

A discourse referent paired with its indefinite number feature. This is the type-theoretic reflex of Enguehard's claim that number marking on indefinites is stored on the discourse referent.

• index : ℕ

  The variable index in the assignment function

• number : IndefNumber

  The number feature chosen by the speaker

def Enguehard2024.instDecidableEqNumberedDRef.decEq (x✝ x✝¹ : NumberedDRef) : Decidable (x✝ = x✝¹)

Equations

• Enguehard2024.instDecidableEqNumberedDRef.decEq { index := a, number := a_1 } { index := b, number := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[implicit_reducible]

instance Enguehard2024.instDecidableEqNumberedDRef : DecidableEq NumberedDRef

Equations

• Enguehard2024.instDecidableEqNumberedDRef = Enguehard2024.instDecidableEqNumberedDRef.decEq

def Enguehard2024.instReprNumberedDRef.repr : NumberedDRef → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Enguehard2024.instReprNumberedDRef : Repr NumberedDRef

Equations

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

theorem Enguehard2024.exists_negative_characterization {W : Type u_1} {E : Type u_2} (x : ℕ) (domain : Set E) (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) (p : Semantics.Dynamic.Core.Possibility W E) : p ∈ (Semantics.Dynamic.Core.BilateralDen.exists_ x domain φ).negative s ↔ p ∈ s ∧ ∀ e ∈ domain, p.extend x e ∉ φ.positive (s.randomAssign x domain)

The negative update of an existential keeps exactly those possibilities from s where no domain element witnesses φ.

theorem Enguehard2024.neg_exists_positive {W : Type u_1} {E : Type u_2} (x : ℕ) (domain : Set E) (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) (p : Semantics.Dynamic.Core.Possibility W E) : p ∈ (~(Semantics.Dynamic.Core.BilateralDen.exists_ x domain φ)).positive s ↔ p ∈ s ∧ ∀ e ∈ domain, p.extend x e ∉ φ.positive (s.randomAssign x domain)

Negating an existential: the positive update of ¬∃x.φ collects exactly those input possibilities where no witness satisfies φ. This is the bilateral analog of universal falsification.

theorem Enguehard2024.neg_exists_eliminative {W : Type u_1} {E : Type u_2} (x : ℕ) (domain : Set E) (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : (~(Semantics.Dynamic.Core.BilateralDen.exists_ x domain φ)).positive s ⊆ s

The output of ¬∃x.φ is a subset of the input state — negated existentials are eliminative. This is crucial for Enguehard's account: the surviving possibilities carry no witness, which is why the discourse referent's number feature matters for continuations (it encodes the speaker's expectation about the predicate's extension).

theorem Enguehard2024.neg_neg_exists {W : Type u_1} {E : Type u_2} (x : ℕ) (domain : Set E) (φ : Semantics.Dynamic.Core.BilateralDen W E) (s : Semantics.Dynamic.Core.InfoState W E) : (~~(Semantics.Dynamic.Core.BilateralDen.exists_ x domain φ)).positive s = (Semantics.Dynamic.Core.BilateralDen.exists_ x domain φ).positive s

Double negation elimination for the existential: ¬¬∃x.φ has the same positive update as ∃x.φ. This is definitional in bilateral semantics — neg swaps, so two swaps restore the original.

def Enguehard2024.agreementFelicitous {W : Type u_1} (dref : NumberedDRef) (witnessCard : W → ℕ) (conceivable : W → Prop) : Prop

Agreement constraint: a continuation sentence with pronoun y agreeing in number with discourse referent dref is felicitous only when the number feature matches the conceivability pattern.

When dref.number = .sg, continuations presuppose |C| = 1 is conceivable; when dref.number = .pl, they presuppose |C| ≥ 2. This connects back to sgCardConceivable/plCardConceivable.

Equations

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

theorem Enguehard2024.toc_agreement_matches_conceivability : agreementFelicitous { index := 0, number := IndefNumber.sg } tocCard allConceivable' ∧ ¬agreementFelicitous { index := 0, number := IndefNumber.pl } tocCard allConceivable'

The bilateral bridge: for the book examples, the agreement constraint on discourse referents matches the conceivability presupposition pattern. Table of contents: sg-marked dref is felicitous (sg conceivable), pl-marked is not.

theorem Enguehard2024.chapter_agreement_underdetermined : agreementFelicitous { index := 0, number := IndefNumber.sg } chapterCard allConceivable' ∧ agreementFelicitous { index := 0, number := IndefNumber.pl } chapterCard allConceivable'

Chapters: both sg and pl discourse referents are felicitous (both conceivability presuppositions hold), matching the underdetermination that Enguehard argues requires gradient utility to resolve.

theorem Enguehard2024.underdetermined_implies_gradient (witnessCard : Bool → ℕ) (hsg : witnessCard true = 1) (hpl : witnessCard false ≥ 2) (c₁ c₂ : Condition) (h : c₁.pMultiple ≤ c₂.pMultiple) : (agreementFelicitous { index := 0, number := IndefNumber.sg } witnessCard fun (x : Bool) => True) ∧ (agreementFelicitous { index := 0, number := IndefNumber.pl } witnessCard fun (x : Bool) => True) ∧ productionUtility c₂.pUnique IndefNumber.sg ≤ productionUtility c₁.pUnique IndefNumber.sg ∧ productionUtility c₁.pUnique IndefNumber.pl ≤ productionUtility c₂.pUnique IndefNumber.pl

The full pipeline from bilateral dynamics to production data:

1. Negated indefinites introduce discourse referents (neg_exists_eliminative)
2. The dref carries a number feature (NumberedDRef)
3. Agreement constrains continuations (agreementFelicitous)
4. When both sg and pl are felicitous (underdetermined), the speaker chooses number to maximize productionUtility
5. At pMultiple = 1/2, both utilities are equal (mix_indifference)

This theorem ties together steps 3-4: when agreement is underdetermined, production utility determines the choice, and the utility values track the observed production rates (sg dominates when pMultiple is low, pl dominates when pMultiple is high).