Core Types for Genericity #

Shared vocabulary for the study of generic sentences, used across Phenomena/Generics/ data files and Theories/ study files.

The two types here capture the organizing axes of the field as surveyed in the introduction to Genericity (Mari, Beyssade, Del Prete, OUP 2013):

GenericForm: what DP form expresses the generic meaning? The introduction spends 30 pages on this distinction (§1.1, §1.3.1).
GenericReading: what kind of generalization is being expressed? @cite{krifka-2013}'s descriptive/definitional split (ch. 15).

source

inductive Core.Genericity.GenericForm :

Type

The principal linguistic forms that express generic meaning.

This four-way distinction is the organizing axis of the field: cross-linguistic patterns, scope behavior, and theoretical status all depend on which form is used.

Form	Example	Carlson	Chierchia	Krifka 2004
IS	"A madrigal is polyphonic"	—	GEN quantifier	GEN over properties
BP	"Dogs bark"	Name of kind	∩(property)	Property + type shift
DS	"The lion is a predator"	—	ι over kind	ι over property
DP	"Les chiens aboient" (Fr.)	—	∩(property)	—

indefiniteSingular : GenericForm
Indefinite singular: "A madrigal is polyphonic." Tends toward definitional readings (@cite{krifka-2013}). Expresses rules (Cohen 2001a). Cannot be used for direct kind predication (*"A dinosaur is extinct").
barePlural : GenericForm
Bare plural: "Dogs bark" / "Madrigals are popular." Both descriptive and definitional readings available. Kind-denoting on Carlson/Chierchia; property-denoting on Krifka 2004. Scopeless (@cite{carlson-1977}).
definiteSingular : GenericForm
Definite singular: "The lion is a predator." Limited to well-established kinds (@cite{krifka-etal-1995}). Blocked by modification (*"The tall lion is a predator").
definitePlural : GenericForm
Definite plural: "Les chiens aboient" (Fr.), "I cani abbaiano" (It.) Romance-language kind reference via the plural definite article. Patterns partly with BPs, partly with DSs. @cite{dayal-2004} analyzes as ι applied to the plural kind.

Instances For

source

instance Core.Genericity.instDecidableEqGenericForm :

DecidableEq GenericForm

Equations

Core.Genericity.instDecidableEqGenericForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source

def Core.Genericity.instReprGenericForm.repr :

GenericForm → Nat → Std.Format

Equations

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

Instances For

source

instance Core.Genericity.instReprGenericForm :

Repr GenericForm

Equations

Core.Genericity.instReprGenericForm = { reprPrec := Core.Genericity.instReprGenericForm.repr }

source

def Core.Genericity.instBEqGenericForm.beq :

GenericForm → GenericForm → Bool

Equations

Core.Genericity.instBEqGenericForm.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

source

instance Core.Genericity.instBEqGenericForm :

BEq GenericForm

Equations

Core.Genericity.instBEqGenericForm = { beq := Core.Genericity.instBEqGenericForm.beq }

source

inductive Core.Genericity.GenericReading :

Type

Type of generic reading (@cite{krifka-2013}, ch. 15).

The descriptive/definitional distinction is orthogonal to GenericForm: BPs can express both, while ISs strongly prefer definitional.

Formally, descriptive generics restrict the set of possible worlds (DES update), while definitional generics restrict the set of admissible interpretations (DEF update). See Phenomena/Generics/Studies/Krifka2013.lean for the two-index formalization.

descriptive : GenericReading
Descriptive: empirical generalization about the world. "Dogs bark" — in normal worlds where there are dogs, they bark. Amenable to threshold/RSA treatment (@cite{tessler-goodman-2019}).
definitional : GenericReading
Definitional: restricts admissible interpretations. "A madrigal is polyphonic" — only interpretations where madrigals are polyphonic count as admissible. NOT reducible to prevalence thresholds.

Instances For

source

instance Core.Genericity.instDecidableEqGenericReading :

DecidableEq GenericReading

Equations