Generic Quantification as Modal Necessity

@cite{krifka-etal-1995} @cite{cohen-2013} @cite{asher-pelletier-2013}

This module makes explicit the structural parallel between the GEN operator and Kratzer's modal necessity.

The Parallel

GEN	Modal necessity (Kratzer)
Domain: situations	Domain: possible worlds
Restriction: normal ∧ kind	Restriction: modal base f(w)
Scope: predicated property	Scope: prejacent proposition p
Hidden: normalcy predicate	Hidden: ordering source g(w)
Force: quasi-universal (∀)	Force: necessity (∀ over best)

Both are restricted universal quantifiers over a contextually determined domain. The normalcy predicate in GEN plays the same structural role as the ordering source in Kratzer's semantics: it selects the "best" or "most normal" elements from the accessible domain.

Cohen's Argument (@cite{cohen-2013})

Ariel Cohen (ch. 13 of the Genericity book) argues that GEN is not a phonologically null version of an overt quantifier — it is introduced by the hearer through reinterpretation. This connects to the modal analysis: the "generic quantifier" is not a syntactic object but an interpretive strategy that has the structure of modal quantification.

Asher & Pelletier (@cite{asher-pelletier-2013})

Asher & Pelletier (ch. 12) analyze generics as modal quantification over circumstances, with the restrictor providing the modal base and normalcy providing the ordering source.

structure Comparisons.GenericModality.RestrictedUniversal (D : Type) : Type

GEN and modal necessity share the same logical form: ∀x ∈ BEST(domain, ordering). scope(x)

This structure captures the parallel at the type level.

• domain : List D

  The domain of quantification

• restriction : D → Bool

  The restriction (selects relevant elements)

• scope : D → Bool

  The scope (what must hold of restricted elements)

def Comparisons.GenericModality.RestrictedUniversal.eval {D : Type} (ru : RestrictedUniversal D) : Bool

Evaluate a restricted universal: ∀d ∈ domain. restriction(d) → scope(d)

Equations

• ru.eval = ru.domain.all fun (d : D) => !ru.restriction d || ru.scope d

def Comparisons.GenericModality.genAsRU (situations : List Semantics.Lexical.Noun.Kind.Generics.Situation) (normal : Semantics.Lexical.Noun.Kind.Generics.NormalcyPredicate) (restrictor : Semantics.Lexical.Noun.Kind.Generics.Restrictor) (scope : Semantics.Lexical.Noun.Kind.Generics.Scope) : RestrictedUniversal Semantics.Lexical.Noun.Kind.Generics.Situation

GEN as a restricted universal over situations.

Equations

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

theorem Comparisons.GenericModality.gen_matches_ru (situations : List Semantics.Lexical.Noun.Kind.Generics.Situation) (normal : Semantics.Lexical.Noun.Kind.Generics.NormalcyPredicate) (restrictor : Semantics.Lexical.Noun.Kind.Generics.Restrictor) (scope : Semantics.Lexical.Noun.Kind.Generics.Scope) : Semantics.Lexical.Noun.Kind.Generics.traditionalGEN situations normal restrictor scope = (genAsRU situations normal restrictor scope).eval

GEN evaluation matches the restricted universal evaluation.

def Comparisons.GenericModality.modalAsRU (accessible : List Semantics.Attitudes.Intensional.World) (p : Semantics.Attitudes.Intensional.World → Bool) : RestrictedUniversal Semantics.Attitudes.Intensional.World

Modal necessity as a restricted universal over worlds. With empty ordering source, this is simple necessity over accessible worlds.

Equations

• Comparisons.GenericModality.modalAsRU accessible p = { domain := accessible, restriction := fun (x : Semantics.Attitudes.Intensional.World) => true, scope := p }

theorem Comparisons.GenericModality.modal_matches_ru (accessible : List Semantics.Attitudes.Intensional.World) (p : Semantics.Attitudes.Intensional.World → Bool) : accessible.all p = (modalAsRU accessible p).eval

Modal necessity matches the restricted universal. (With the trivial restriction, the RU reduces to ∀w ∈ accessible. p(w).)

inductive Comparisons.GenericModality.DomainFilterStrategy : Type

The normalcy predicate in GEN plays the same role as the ordering source in Kratzer semantics. Both filter the domain down to "best" elements.

This is a structural observation, not a definitional identity: GEN uses a binary normal/abnormal distinction while Kratzer uses a preorder. The binary case is the degenerate case where the ordering has exactly two equivalence classes.

• binaryNormalcy : DomainFilterStrategy
• preorderBest : DomainFilterStrategy

instance Comparisons.GenericModality.instDecidableEqDomainFilterStrategy : DecidableEq DomainFilterStrategy

Equations

• Comparisons.GenericModality.instDecidableEqDomainFilterStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Comparisons.GenericModality.instReprDomainFilterStrategy.repr : DomainFilterStrategy → ℕ → Std.Format

Equations

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

instance Comparisons.GenericModality.instReprDomainFilterStrategy : Repr DomainFilterStrategy

Equations

• Comparisons.GenericModality.instReprDomainFilterStrategy = { reprPrec := Comparisons.GenericModality.instReprDomainFilterStrategy.repr }

structure Comparisons.GenericModality.Correspondence : Type

Summary of the structural correspondence between generic and modal theories.

• genericComponent : String
• modalComponent : String
• notes : String

instance Comparisons.GenericModality.instReprCorrespondence : Repr Correspondence

Equations

• Comparisons.GenericModality.instReprCorrespondence = { reprPrec := Comparisons.GenericModality.instReprCorrespondence.repr }

def Comparisons.GenericModality.instReprCorrespondence.repr : Correspondence → ℕ → Std.Format

Equations

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

def Comparisons.GenericModality.correspondenceTable : List Correspondence

Equations

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