Traditional Generic Semantics (GEN Operator)

[TG19] [Chi95] [KPC+95]

This module formalizes the traditional covert GEN operator posited for generic sentences like "Dogs bark", "Birds fly", etc.

GEN is grounded on the canonical generalized-quantifier substrate in Quantification/Counting.lean: traditionalGEN is Quantification.everyOn over the situation domain with restriction normal ∧ restrictor and nuclear scope scope (true by construction — see the definition). The prevalence-based alternative is the ℚ view Quantification.prevalenceOn (prevalence), with the threshold reading Quantification.thresholdGtOn (thresholdGeneric).

The Traditional Account

In the standard analysis, generics involve:

1. A covert quantifier GEN over situations/cases
2. A restrictor (the kind)
3. A nuclear scope (the property)
4. A hidden normalcy parameter

Structure: GEN_s [Restrictor(s)] [NuclearScope(s)]

Example: "Dogs bark" → GEN_s [dog(x,s)] [bark(x,s)] → "In normal situations s where there's a dog x, x barks in s"

The Problem with GEN

The normal parameter does all the explanatory work but is (1) not observable (covert), (2) context-dependent (varies by property), and (3) essentially circular (stipulated to give right results). The threshold-based alternative below (thresholdGeneric, grounded on Quantification.thresholdGtOn) eliminates it.

Descriptive vs Definitional ([Kri13])

[Kri13] distinguishes descriptive generics ("Dogs bark") from definitional generics ("A madrigal is polyphonic"). Only descriptive generics are eliminable via threshold semantics; definitional generics restrict the interpretation index, not the world index. See Studies/Krifka2013.lean for the two-index formalization.

Comparison with RSA Treatment

[TG19] and [Chi95] eliminate GEN via threshold semantics:

• Generic is true iff prevalence exceeds threshold
• Threshold is uncertain, inferred pragmatically
• Prior over prevalence varies by property

See Studies/TesslerGoodman2019.lean for the RSA account.

structure Semantics.Genericity.Situation : Type

A situation/case — the entities GEN quantifies over.

In situation semantics, situations are parts of worlds that can be evaluated for truth of basic propositions. For generics, situations represent "cases" or "occasions" where the kind appears.

For "Dogs bark", each situation s is a case where there is a dog that either barks or doesn't bark.

• id : ℕ

  Identifier for the situation

@[implicit_reducible]

instance Semantics.Genericity.instDecidableEqSituation : DecidableEq Situation

Equations

• Semantics.Genericity.instDecidableEqSituation = Semantics.Genericity.instDecidableEqSituation.decEq

def Semantics.Genericity.instDecidableEqSituation.decEq (x✝ x✝¹ : Situation) : Decidable (x✝ = x✝¹)

Equations

• Semantics.Genericity.instDecidableEqSituation.decEq { id := a } { id := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

def Semantics.Genericity.instReprSituation.repr : Situation → ℕ → Std.Format

Equations

• Semantics.Genericity.instReprSituation.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "id" ++ Std.Format.text " := " ++ (Std.Format.nest 6 (repr x✝.id)).group) " }"

@[implicit_reducible]

instance Semantics.Genericity.instReprSituation : Repr Situation

Equations

• Semantics.Genericity.instReprSituation = { reprPrec := Semantics.Genericity.instReprSituation.repr }

@[implicit_reducible]

instance Semantics.Genericity.instInhabitedSituation : Inhabited Situation

Equations

• Semantics.Genericity.instInhabitedSituation = { default := { id := 0 } }

@[reducible, inline]

abbrev Semantics.Genericity.Restrictor : Type

A restrictor is a property of situations (e.g., "there is a dog in s")

Equations

• Semantics.Genericity.Restrictor = (Semantics.Genericity.Situation → Bool)

@[reducible, inline]

abbrev Semantics.Genericity.Scope : Type

A scope is a property of situations (e.g., "the dog barks in s")

Equations

• Semantics.Genericity.Scope = (Semantics.Genericity.Situation → Bool)

@[reducible, inline]

abbrev Semantics.Genericity.NormalcyPredicate : Type

A normalcy predicate picks out "normal" or "characteristic" situations

Equations

• Semantics.Genericity.NormalcyPredicate = (Semantics.Genericity.Situation → Bool)

@[reducible]

def Semantics.Genericity.traditionalGEN (situations : List Situation) (normal : NormalcyPredicate) (restrictor : Restrictor) (scope : Scope) : Prop

Traditional GEN as a quantifier over situations.

GEN[restrictor][scope] is true iff in all NORMAL situations where restrictor holds, scope holds.

This is essentially a restricted universal quantifier: ∀s. (normal(s) ∧ restrictor(s)) → scope(s)

Equivalently, Quantification.everyOn situations.toFinset (λ s => normal s && restrictor s) scope, where the restriction is the conjunction of normalcy and restrictor — the canonical relativized restricted universal.

The key parameters:

• situations: the domain of quantification (possible cases)
• normal: which situations count as "normal" (the hidden parameter!)
• restrictor: the kind property (e.g., "is a dog in s")
• scope: the predicated property (e.g., "barks in s")

The normal parameter is where all the context-sensitivity and exception-tolerance is hidden.

Equations

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

def Semantics.Genericity.traditionalGEN_existential (situations : List Situation) (normal : NormalcyPredicate) (restrictor : Restrictor) (scope : Scope) : Prop

Alternative formulation: existential test for counterexamples.

GEN is true iff there's no normal restrictor-situation that fails the scope.

Equations

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

theorem Semantics.Genericity.gen_formulations_equiv (situations : List Situation) (normal : NormalcyPredicate) (restrictor : Restrictor) (scope : Scope) : traditionalGEN situations normal restrictor scope ↔ traditionalGEN_existential situations normal restrictor scope

The two formulations are equivalent: the relativized restricted universal is exactly the absence of a (normal restrictor) counterexample to scope.

def Semantics.Genericity.prevalence {D : Type} [DecidableEq D] (domain : List D) (restrictor scope : D → Bool) : ℚ

Prevalence: the proportion of restrictor-satisfying cases where scope holds.

Polymorphic over the domain type — works for situation-based models ([Coh99], [TG19]) and entity-based models ([Nic09]) alike. The genericity-named view of the canonical Quantification.prevalenceOn (the ℚ analogue of Rel.edgeDensity).

Equations

• Semantics.Genericity.prevalence domain restrictor scope = Quantification.prevalenceOn domain.toFinset (fun (d : D) => restrictor d = true) fun (d : D) => scope d = true

@[reducible]

def Semantics.Genericity.thresholdGeneric {D : Type} [DecidableEq D] (domain : List D) (restrictor scope : D → Bool) (num denom : ℕ) : Prop

Threshold-based generic (a la [TG19]).

The generic is true iff prevalence exceeds the threshold num/denom. This replaces the hidden "normalcy" with observable prevalence. The canonical cross-multiplied Quantification.thresholdGtOn (division-free Nat comparison) so the truth value is kernel-decide-able.

Equations

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

GEN is eliminable via threshold semantics — but only for descriptive generics ([Kri13]). Definitional generics ("A madrigal is polyphonic") restrict the interpretation index, not the world index, and cannot be reduced to a prevalence threshold. See Studies/TesslerGoodman2019.lean for the RSA account that makes the threshold uncertain and pragmatically inferred, and Studies/Krifka2013.lean for the descriptive/definitional split.

def Semantics.Genericity.dogSituations : List Situation

Example situations for "Dogs bark"

Equations

• Semantics.Genericity.dogSituations = [{ id := 0 }, { id := 1 }, { id := 2 }, { id := 3 }, { id := 4 }]

def Semantics.Genericity.isDogSituation : Restrictor

All situations involve dogs (restrictor = true)

Equations

• Semantics.Genericity.isDogSituation x✝ = true

def Semantics.Genericity.dogBarks : Scope

Most dogs bark in these situations

Equations

• Semantics.Genericity.dogBarks s = match s.id with | 2 => false | x => true

def Semantics.Genericity.normalDogSituation : NormalcyPredicate

"Normal" = typical/expected situations (NOT sleeping)

Equations

• Semantics.Genericity.normalDogSituation s = (s.id != 2)

theorem Semantics.Genericity.dogBarks_prevalence : prevalence dogSituations isDogSituation dogBarks = 4 / 5

Prevalence of barking among the (all-dog) situations is 4/5: four of the five dogs bark. Routed through the count form (ℚ division is not kernel-decide-able).

Related Theory

• Semantics/Lexical/Noun/Kind/NMP.lean - Kind reference, bare plurals, DKP
• Studies/TesslerGoodman2019.lean - RSA treatment of generics

def Semantics.Genericity.genHomogeneityPresup (situations : List Situation) (restrictor : Restrictor) (scope : Scope) : Prop

GEN's homogeneity presupposition ([Mag09]).

The covert generic operator GEN carries a presupposition that the nuclear scope either holds of ALL restrictor-satisfying elements or of NONE — the YES ∪ NO partition:

• YES = {w | ∀s. restrictor(s) → scope(s)} (all satisfy scope)
• NO = {w | ∀s. restrictor(s) → ¬scope(s)} (none satisfy scope)

This presupposition is detectable by negation: "It's false that John smokes" conveys "he never smokes," not "he doesn't always smoke." The stronger reading follows from the plain meaning + homogeneity presupposition ([vF97]).

Overt always does NOT carry this presupposition. This asymmetry is the key to [Mag09] §4.6: "#John is always tall" is odd because the blind strengthened presupposition (asserting that homogeneity fails) contradicts common knowledge.

Equations

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

theorem Semantics.Genericity.homogeneity_yes (situations : List Situation) (restrictor : Restrictor) (scope : Scope) (h : Quantification.everyOn situations.toFinset (fun (s : Situation) => restrictor s = true) fun (s : Situation) => scope s = true) : genHomogeneityPresup situations restrictor scope

Homogeneity holds when ALL restrictor-situations satisfy scope (the YES branch).

theorem Semantics.Genericity.homogeneity_no (situations : List Situation) (restrictor : Restrictor) (scope : Scope) (h : Quantification.noOn situations.toFinset (fun (s : Situation) => restrictor s = true) fun (s : Situation) => scope s = true) : genHomogeneityPresup situations restrictor scope

Homogeneity holds when NO restrictor-situation satisfies scope (the NO branch).