Traditional Generic Semantics (GEN Operator)

@cite{tessler-goodman-2019} @cite{chierchia-1995} @cite{krifka-etal-1995}

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

GEN is an instance of the shared covert quantifier infrastructure in CovertQuantifier.lean: traditionalGEN = covertQ with D = Situation, restriction = normal ∧ restrictor, scope = scope.

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). See CovertQuantifier.lean for the shared structure and the threshold-based alternative that eliminates it.

Descriptive vs Definitional (@cite{krifka-2013})

@cite{krifka-2013} 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 Phenomena/Generics/Studies/Krifka2013.lean for the two-index formalization.

Comparison with RSA Treatment

@cite{tessler-goodman-2019} and @cite{chierchia-1995} eliminate GEN via threshold semantics:

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

See Phenomena/Generics/Studies/TesslerGoodman2019.lean for the RSA account and Comparisons/GenericSemantics.lean for the formal comparison.

structure Semantics.Lexical.Noun.Kind.Generics.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

def Semantics.Lexical.Noun.Kind.Generics.instDecidableEqSituation.decEq (x✝ x✝¹ : Situation) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Lexical.Noun.Kind.Generics.instDecidableEqSituation : DecidableEq Situation

Equations

• Semantics.Lexical.Noun.Kind.Generics.instDecidableEqSituation = Semantics.Lexical.Noun.Kind.Generics.instDecidableEqSituation.decEq

instance Semantics.Lexical.Noun.Kind.Generics.instReprSituation : Repr Situation

Equations

• Semantics.Lexical.Noun.Kind.Generics.instReprSituation = { reprPrec := Semantics.Lexical.Noun.Kind.Generics.instReprSituation.repr }

def Semantics.Lexical.Noun.Kind.Generics.instReprSituation.repr : Situation → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Kind.Generics.instInhabitedSituation : Inhabited Situation

Equations

• Semantics.Lexical.Noun.Kind.Generics.instInhabitedSituation = { default := { id := 0 } }

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Generics.Restrictor : Type

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

Equations

• Semantics.Lexical.Noun.Kind.Generics.Restrictor = (Semantics.Lexical.Noun.Kind.Generics.Situation → Bool)

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Generics.Scope : Type

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

Equations

• Semantics.Lexical.Noun.Kind.Generics.Scope = (Semantics.Lexical.Noun.Kind.Generics.Situation → Bool)

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Generics.NormalcyPredicate : Type

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

Equations

• Semantics.Lexical.Noun.Kind.Generics.NormalcyPredicate = (Semantics.Lexical.Noun.Kind.Generics.Situation → Bool)

def Semantics.Lexical.Noun.Kind.Generics.traditionalGEN (situations : List Situation) (normal : NormalcyPredicate) (restrictor : Restrictor) (scope : Scope) : Bool

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, covertQ situations (λ s => normal s && restrictor s) scope, where the restriction is the conjunction of normalcy and restrictor.

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.

theorem Semantics.Lexical.Noun.Kind.Generics.gen_is_covertQ (situations : List Situation) (normal : NormalcyPredicate) (restrictor : Restrictor) (scope : Scope) : traditionalGEN situations normal restrictor scope = CovertQuantifier.covertQ situations (fun (s : Situation) => normal s && restrictor s) scope

GEN is an instance of the shared covert quantifier, with restriction = normal ∧ restrictor.

def Semantics.Lexical.Noun.Kind.Generics.traditionalGEN_existential (situations : List Situation) (normal : NormalcyPredicate) (restrictor : Restrictor) (scope : Scope) : Bool

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.Lexical.Noun.Kind.Generics.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 (derived from shared De Morgan proof).

def Semantics.Lexical.Noun.Kind.Generics.prevalence {D : Type} (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 (@cite{cohen-1999a}, @cite{tessler-goodman-2019}) and entity-based models (@cite{nickel-2009}) alike. An alias for measure with a domain-specific name.

Equations

• Semantics.Lexical.Noun.Kind.Generics.prevalence domain restrictor scope = Semantics.Lexical.CovertQuantifier.measure domain restrictor scope

def Semantics.Lexical.Noun.Kind.Generics.thresholdGeneric {D : Type} (domain : List D) (restrictor scope : D → Bool) (threshold : ℚ) : Bool

Threshold-based generic (a la @cite{tessler-goodman-2019}).

The generic is true iff prevalence exceeds threshold. This replaces the hidden "normalcy" with observable prevalence.

Equations

• Semantics.Lexical.Noun.Kind.Generics.thresholdGeneric domain restrictor scope threshold = decide (Semantics.Lexical.Noun.Kind.Generics.prevalence domain restrictor scope > threshold)

GEN is eliminable via threshold semantics — but only for descriptive generics (@cite{krifka-2013}). Definitional generics ("A madrigal is polyphonic") restrict the interpretation index, not the world index, and cannot be reduced to a prevalence threshold.

The theorem gen_eliminable proving eliminability for the descriptive case is in Comparisons/GenericSemantics.lean, which connects traditional GEN to @cite{tessler-goodman-2019} RSA approach.

def Semantics.Lexical.Noun.Kind.Generics.dogSituations : List Situation

Example situations for "Dogs bark"

Equations

• Semantics.Lexical.Noun.Kind.Generics.dogSituations = [{ id := 0 }, { id := 1 }, { id := 2 }, { id := 3 }, { id := 4 }]

def Semantics.Lexical.Noun.Kind.Generics.isDogSituation : Restrictor

All situations involve dogs (restrictor = true)

Equations

• Semantics.Lexical.Noun.Kind.Generics.isDogSituation x✝ = true

def Semantics.Lexical.Noun.Kind.Generics.dogBarks : Scope

Most dogs bark in these situations

Equations

• Semantics.Lexical.Noun.Kind.Generics.dogBarks s = match s.id with | 2 => false | x => true

def Semantics.Lexical.Noun.Kind.Generics.normalDogSituation : NormalcyPredicate

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

Equations

• Semantics.Lexical.Noun.Kind.Generics.normalDogSituation s = (s.id != 2)

Related Theory

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

Empirical Data

• Phenomena/Generics/Data.lean - prevalence asymmetries, rare property generics
• Phenomena/Generics/KindReference.lean - kind-level predicates, cross-linguistic patterns

def Semantics.Lexical.Noun.Kind.Generics.genHomogeneityPresup (situations : List Situation) (restrictor : Restrictor) (scope : Scope) : Bool

GEN's homogeneity presupposition (@cite{magri-2009} eq. (137)).

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 (@cite{von-fintel-1997}).

Overt always does NOT carry this presupposition. This asymmetry is the key to @cite{magri-2009} §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.Lexical.Noun.Kind.Generics.homogeneity_yes (situations : List Situation) (restrictor : Restrictor) (scope : Scope) (h : (List.filter restrictor situations).all scope = true) : genHomogeneityPresup situations restrictor scope = true

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

theorem Semantics.Lexical.Noun.Kind.Generics.homogeneity_no (situations : List Situation) (restrictor : Restrictor) (scope : Scope) (h : ((List.filter restrictor situations).all fun (s : Situation) => !scope s) = true) : genHomogeneityPresup situations restrictor scope = true

Homogeneity holds trivially when NO situations satisfy scope (the NO branch).