Generic Quantification as Modal Necessity

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

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. Cohen identifies two devices: Predicate Transfer (pragmatic, for generics — yields scope ambiguities except in opaque contexts) and type-shifting (semantic, for habituals — yields narrow scope only). See Theories/Semantics/Composition/PredicateTransfer.lean for the formal definitions (T_g, γ, QuantifierSource) and Phenomena/Generics/Studies/Cohen2013.lean for the scope predictions verified on finite models. The present module draws a further connection not made by Cohen: the resulting generic quantifier has the structure of modal quantification (restricted universal over a contextually filtered domain).

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

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 Phenomena.Generics.CompareModality.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 Phenomena.Generics.CompareModality.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 Phenomena.Generics.CompareModality.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 Phenomena.Generics.CompareModality.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 Phenomena.Generics.CompareModality.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

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

theorem Phenomena.Generics.CompareModality.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 Phenomena.Generics.CompareModality.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 Phenomena.Generics.CompareModality.instDecidableEqDomainFilterStrategy : DecidableEq DomainFilterStrategy

Equations

• Phenomena.Generics.CompareModality.instDecidableEqDomainFilterStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Generics.CompareModality.instReprDomainFilterStrategy.repr : DomainFilterStrategy → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.CompareModality.instReprDomainFilterStrategy : Repr DomainFilterStrategy

Equations

• Phenomena.Generics.CompareModality.instReprDomainFilterStrategy = { reprPrec := Phenomena.Generics.CompareModality.instReprDomainFilterStrategy.repr }

structure Phenomena.Generics.CompareModality.Correspondence : Type

Summary of the structural correspondence between generic and modal theories.

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

def Phenomena.Generics.CompareModality.instReprCorrespondence.repr : Correspondence → ℕ → Std.Format

Equations

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

instance Phenomena.Generics.CompareModality.instReprCorrespondence : Repr Correspondence

Equations

• Phenomena.Generics.CompareModality.instReprCorrespondence = { reprPrec := Phenomena.Generics.CompareModality.instReprCorrespondence.repr }

def Phenomena.Generics.CompareModality.correspondenceTable : List Correspondence

Equations

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