@[reducible, inline]

abbrev Semantics.Kinds.NMP.Individual (Atom : Type) : Type

An individual is a non-empty set of atoms. Atoms are singletons {a}, pluralities are larger sets. The part-of relation (⊆) and join (∪) are inherited from Mathlib's Set instances, giving us Link's complete atomic join semilattice.

Equations

• Semantics.Kinds.NMP.Individual Atom = Set Atom

def Semantics.Kinds.NMP.Individual.atom {Atom : Type} (a : Atom) : Individual Atom

Construct a singular individual from an atom.

Equations

• Semantics.Kinds.NMP.Individual.atom a = {a}

@[reducible, inline]

abbrev Semantics.Kinds.NMP.Property (World Atom : Type) : Type

A property (intension): function from worlds to sets of individuals. This is Core.Intension World (Set (Individual Atom)).

Equations

• Semantics.Kinds.NMP.Property World Atom = Core.Intension World (Set (Semantics.Kinds.NMP.Individual Atom))

@[reducible, inline]

abbrev Semantics.Kinds.NMP.IndividualConcept (World Atom : Type) : Type

An individual concept: function from worlds to individuals. This is Core.Intension World (Individual Atom).

Equations

• Semantics.Kinds.NMP.IndividualConcept World Atom = Core.Intension World (Semantics.Kinds.NMP.Individual Atom)

structure Semantics.Kinds.NMP.Kind (World Atom : Type) : Type

Kinds are a special subset of individual concepts.

A kind is an individual concept that maps each world to the totality of instances (a set of atoms) and represents a "natural" class with regular behavior.

Not every individual concept is a kind. Only those corresponding to natural properties qualify.

• concept : IndividualConcept World Atom

  The underlying individual concept

def Semantics.Kinds.NMP.down (World Atom : Type) (P : Property World Atom) : Kind World Atom

The "down" operator ∩ (cap): nominalize a property to a kind.

∩P = λs. ιPₛ

That is, at each world s, take the largest individual in the extension of P. For plural/mass properties, this is the fusion of all instances.

Note: ∩ is only semantically defined for plural/mass nouns (see downDefinedFor). This function computes the nominalization for any property; the partiality constraint is enforced externally.

Equations

• Semantics.Kinds.NMP.down World Atom P = { concept := fun (w : World) => {a : Atom | Semantics.Kinds.NMP.Individual.atom a ∈ P w} }

def Semantics.Kinds.NMP.up (World Atom : Type) (k : Kind World Atom) : Property World Atom

The "up" operator ∪ (cup): predicativize a kind to a property.

∪k = λx[x ⊆ kₛ]

The extension is the ideal generated by the kind's instances: all individuals that are "part of" the totality of instances.

Property: ∪ applied to a kind yields a MASS denotation. This is because the extension includes both atoms and pluralities.

Equations

• Semantics.Kinds.NMP.up World Atom k w = {x : Semantics.Kinds.NMP.Individual Atom | x ⊆ k.concept w}

def Semantics.Kinds.NMP.IsMass (World Atom : Type) (P : Property World Atom) : Prop

A property is mass iff its extension at every world is determined by atomic content: x ∈ P w ↔ ∀ a ∈ x, {a} ∈ P w (@cite{chierchia-1998} §2.2).

This implies both cumulative reference (CUM) and divisive reference (DIV): mass extensions are closed under union and subset.

Equations

• Semantics.Kinds.NMP.IsMass World Atom P = ∀ (w : World) (x : Semantics.Kinds.NMP.Individual Atom), x ∈ P w ↔ ∀ a ∈ x, Semantics.Kinds.NMP.Individual.atom a ∈ P w

theorem Semantics.Kinds.NMP.isMass_div {World Atom : Type} (P : Property World Atom) (hMass : IsMass World Atom P) (w : World) : Mereology.DIV (P w)

Mass properties have divisive reference: if x ∈ P w and y ⊆ x, then y ∈ P w. Every part of a mass-noun instance is also an instance.

theorem Semantics.Kinds.NMP.isMass_cum {World Atom : Type} (P : Property World Atom) (hMass : IsMass World Atom P) (w : World) : Mereology.CUM (P w)

Mass properties have cumulative reference: if x ∈ P w and y ∈ P w, then x ∪ y ∈ P w. Combining mass-noun instances yields an instance.

def Semantics.Kinds.NMP.pluralClosure (World Atom : Type) (P : Property World Atom) : Property World Atom

Plural closure of a property: close extensions under join (⊔) at each world.

This is @cite{link-1983}'s *P operator, Krifka's ⊔ superscript: the smallest superset of P(w) closed under set union. Singular count nouns like spider are not cumulative, so pluralClosure(⟦spider⟧) adds pluralities — the denotation of the bare plural spiders.

Mass nouns like mold are already cumulative, so plural closure is a no-op: pluralClosure(⟦mold⟧) = ⟦mold⟧ (see pluralClosure_mass).

Equations

• Semantics.Kinds.NMP.pluralClosure World Atom P w = Mereology.AlgClosure (P w)

theorem Semantics.Kinds.NMP.pluralClosure_mass {World Atom : Type} (P : Property World Atom) (hMass : IsMass World Atom P) : pluralClosure World Atom P = P

Plural closure is idempotent for mass nouns: ⊔P = P when P is cumulative. This is Krifka's absorption rule ⊔⊔S = ⊔S from @cite{krifka-2026} (16).

theorem Semantics.Kinds.NMP.subset_pluralClosure {World Atom : Type} (P : Property World Atom) (w : World) : P w ⊆ pluralClosure World Atom P w

A property is contained in its plural closure.

theorem Semantics.Kinds.NMP.pluralClosure_cum {World Atom : Type} (P : Property World Atom) (w : World) : Mereology.CUM (pluralClosure World Atom P w)

Plural closure is always cumulative.

def Semantics.Kinds.NMP.kindAnaphorMass (World Atom : Type) (P : Property World Atom) : Kind World Atom

Kind anaphor for [MASS] concepts: ⟦it⟧ = λP[MASS]. λi. ∩P(i).

Mass nouns are already cumulative, so ∩ applies directly without plural closure. The singular pronoun it picks up a mass concept dref and derives the corresponding kind individual.

Example: John noticed mold. He is allergic against it. ⟦it⟧(⟦mold⟧) = ∩⟦mold⟧ = the mold-kind

Equations

• Semantics.Kinds.NMP.kindAnaphorMass World Atom P = Semantics.Kinds.NMP.down World Atom P

def Semantics.Kinds.NMP.kindAnaphorCount (World Atom : Type) (P : Property World Atom) : Kind World Atom

Kind anaphor for [COUNT] concepts: ⟦they⟧ = λP[COUNT]. λi. ∩(⊔P)(i).

Count nouns need plural closure (⊔) before nominalization (∩). The plural pronoun they picks up a count concept dref, applies plural closure to get a cumulative predicate, then derives the kind individual via ∩.

Example: John noticed a spider. He has a phobia against them. ⟦they⟧(⟦spider⟧) = ∩(⊔⟦spider⟧) = ∩⟦spiders⟧ = the spider-kind

Equations

• Semantics.Kinds.NMP.kindAnaphorCount World Atom P = Semantics.Kinds.NMP.down World Atom (Semantics.Kinds.NMP.pluralClosure World Atom P)

theorem Semantics.Kinds.NMP.kindAnaphorCount_mass (World Atom : Type) (P : Property World Atom) (hMass : IsMass World Atom P) : kindAnaphorCount World Atom P = kindAnaphorMass World Atom P

For mass nouns, the two anaphors yield the same kind (up to absorption). This is why it and they are interchangeable for mass concepts — except that the morphosyntactic [MASS] feature blocks they.

theorem Semantics.Kinds.NMP.up_down_id (World Atom : Type) (P : Property World Atom) (hMass : IsMass World Atom P) : up World Atom (down World Atom P) = P

Key theorem: ∪(∩P) = P for mass properties.

Going down and then up returns the original property (for suitable P). The mass-noun condition IsMass ensures that the extension at each world is determined by its atomic content, which is exactly what down extracts and up reconstructs.

theorem Semantics.Kinds.NMP.down_up_id (World Atom : Type) (k : Kind World Atom) : down World Atom (up World Atom k) = k

Key theorem: ∩(∪k) = k for any kind k.

Going up and then down returns the original kind.

def Semantics.Kinds.NMP.DKP (World Atom : Type) (P : Individual Atom → Bool) (k : Kind World Atom) (w : World) : Prop

Derived Kind Predication: coerce object-level predicates to accept kinds.

When an object-level predicate P applies to a kind k, introduce existential quantification over instances:

P(k) = ∃x[∪k(x) ∧ P(x)]

This is a type-coercion triggered by sort mismatch.

Example: "Lions are roaring in the zoo"

• "lions" denotes a kind
• "roaring in the zoo" is an object-level predicate
• DKP yields: ∃x[lion(x) ∧ roaring-in-the-zoo(x)]

Equations

• Semantics.Kinds.NMP.DKP World Atom P k w = ∃ x ∈ Semantics.Kinds.NMP.up World Atom k w, P x = true

def Semantics.Kinds.NMP.liftToKind (World Atom : Type) (P : Individual Atom → Bool) : Kind World Atom → World → Prop

DKP as a type-shifting operation on predicates.

Takes an object-level predicate and returns a kind-level predicate.

Equations

• Semantics.Kinds.NMP.liftToKind World Atom P k w = Semantics.Kinds.NMP.DKP World Atom P k w

def Semantics.Kinds.NMP.DPP (Atom : Type) (property predicate : Individual Atom → Bool) : Prop

Derived Property Predication: coerce a property to yield an existential.

When a property P (rather than a kind) composes with a predicate Q, introduce low-scoped existential quantification:

DPP(Q)(P) = ∃x[P(x) ∧ Q(x)]

This is the mirror image of DKP. Where DKP applies to kinds (via ∪), DPP applies to properties directly. @cite{moroney-2021} (85): DPP applies when bare nouns (base type ⟨s,⟨e,t⟩⟩) compose with a verb at vP, yielding obligatory low scope w.r.t. negation. @cite{guerrini-2026} §5.3: the existential reading of bare plurals in episodic sentences arises from property-level LFs via DPP, not from kind-level DKP.

Example: "Bears are destroying my garden" (existential reading)

• "bears" denotes a property (λx.bear(x))
• "destroying my garden" is a predicate
• DPP yields: ∃x[bear(x) ∧ destroying-my-garden(x)]

DPP applies locally (like DKP), so it yields obligatory low scope.

Equations

• Semantics.Kinds.NMP.DPP Atom property predicate = ∃ (x : Semantics.Kinds.NMP.Individual Atom), property x = true ∧ predicate x = true

inductive Semantics.Kinds.NMP.NominalMapping : Type

The Nominal Mapping Parameter.

Languages vary in what they let their NPs denote:

• [+arg]: NPs can be argumental (type e, denoting kinds)
• [+pred]: NPs can be predicative (type ⟨e,t⟩)

The combination determines the language's nominal system.

• argOnly : NominalMapping

  [+arg, -pred]: All nouns are kinds (Chinese-like)

  • All nouns are mass-like
  • No plural morphology
  • Generalized classifier system
  • Bare arguments everywhere
• argAndPred : NominalMapping

  [+arg, +pred]: Nouns can be kinds or predicates (Germanic-like)

  • Mass/count distinction
  • Bare plurals and mass nouns as arguments
  • Singular count nouns require D
• predOnly : NominalMapping

  [-arg, +pred]: All nouns are predicates (Romance-like)

  • Mass/count distinction
  • Bare arguments restricted (need licensing)
  • D must be projected for argumenthood

@[implicit_reducible]

instance Semantics.Kinds.NMP.instDecidableEqNominalMapping : DecidableEq NominalMapping

Equations

• Semantics.Kinds.NMP.instDecidableEqNominalMapping x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Kinds.NMP.instReprNominalMapping.repr : NominalMapping → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Kinds.NMP.instReprNominalMapping : Repr NominalMapping

Equations

• Semantics.Kinds.NMP.instReprNominalMapping = { reprPrec := Semantics.Kinds.NMP.instReprNominalMapping.repr }

def Semantics.Kinds.NMP.languageFamily : NominalMapping → String

Language family classification

Equations

• Semantics.Kinds.NMP.languageFamily Semantics.Kinds.NMP.NominalMapping.argOnly = "Chinese, Japanese (classifier languages)"
• Semantics.Kinds.NMP.languageFamily Semantics.Kinds.NMP.NominalMapping.argAndPred = "English, German, Slavic (bare argument languages)"
• Semantics.Kinds.NMP.languageFamily Semantics.Kinds.NMP.NominalMapping.predOnly = "French, Italian, Spanish (Romance languages)"

def Semantics.Kinds.NMP.CanDenoteKind (mapping : NominalMapping) (hasD : Prop) [Decidable hasD] : Prop

Whether a nominal can denote a kind, given the language's mapping parameter and whether an overt determiner (D) is present.

• [+arg] languages: nouns can denote kinds without D (covert ∩ available)
• [-arg, +pred] languages: D is required to map predicates to arguments; without D, nouns remain predicates (properties)

Equations

• Semantics.Kinds.NMP.CanDenoteKind Semantics.Kinds.NMP.NominalMapping.argOnly hasD = True
• Semantics.Kinds.NMP.CanDenoteKind Semantics.Kinds.NMP.NominalMapping.argAndPred hasD = True
• Semantics.Kinds.NMP.CanDenoteKind Semantics.Kinds.NMP.NominalMapping.predOnly hasD = hasD

@[implicit_reducible]

instance Semantics.Kinds.NMP.instDecidableCanDenoteKind (m : NominalMapping) (h : Prop) [Decidable h] : Decidable (CanDenoteKind m h)

Equations

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

def Semantics.Kinds.NMP.CanDenoteProperty (mapping : NominalMapping) : Prop

Whether a nominal can denote a property, given the mapping parameter.

Equations

• Semantics.Kinds.NMP.CanDenoteProperty Semantics.Kinds.NMP.NominalMapping.argOnly = False
• Semantics.Kinds.NMP.CanDenoteProperty Semantics.Kinds.NMP.NominalMapping.argAndPred = True
• Semantics.Kinds.NMP.CanDenoteProperty Semantics.Kinds.NMP.NominalMapping.predOnly = True

@[implicit_reducible]

instance Semantics.Kinds.NMP.instDecidablePredNominalMappingCanDenoteProperty : DecidablePred CanDenoteProperty

Equations

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

def Semantics.Kinds.NMP.pluralize {Atom : Type} (F : Set Atom) : Set (Individual Atom)

Pluralization / mass extension: the set of non-empty sub-individuals.

For count nouns, PL(F) = { s | s.Nonempty ∧ s ⊆ F } — the set of pluralities whose atomic parts are all in the original extension.

Mass nouns come out of the lexicon "already pluralized": a mass noun like "furniture" is true of individual pieces AND pluralities of pieces, without distinction. Its extension has the same form: { s | s.Nonempty ∧ s ⊆ atoms }.

Equations

• Semantics.Kinds.NMP.pluralize F = {s : Semantics.Kinds.NMP.Individual Atom | Set.Nonempty s ∧ s ⊆ F}

structure Semantics.Kinds.NMP.BlockingPrinciple : Type

The Blocking Principle: covert type shifting is blocked when an overt determiner has the same meaning.

For any type shifting operation τ and any X: *τ(X) if there is a determiner D such that D(X) = τ(X)

In English:

• ι (iota) is blocked by "the" → can't use ι covertly
• ∃ is blocked by "a/some" for singulars → can't use ∃ covertly for singulars
• ∩ is NOT blocked → can use ∩ freely for bare plurals/mass

This explains why English allows bare plurals but not bare singulars.

• determiners : List String

  Available overt determiners

• iotaBlocked : Bool

  Whether ι (definite) is blocked

• existsBlocked : Bool

  Whether ∃ (indefinite singular) is blocked

• downBlocked : Bool

  Whether ∩ (kind formation) is blocked

def Semantics.Kinds.NMP.bareArgumentLicensed (bp : BlockingPrinciple) (nounType : MassCount) : Bool

Bare argument is licensed iff the required type shift is not blocked

Equations

• Semantics.Kinds.NMP.bareArgumentLicensed bp MassCount.mass = !bp.downBlocked
• Semantics.Kinds.NMP.bareArgumentLicensed bp MassCount.count = !bp.downBlocked

def Semantics.Kinds.NMP.downDefinedFor (nounType : MassCount) (isPlural : Bool) : Bool

The key insight: ∩ is undefined for singular count nouns.

∩ applied to a singular property would need to yield a kind. But kinds necessarily have plurality of instances (across worlds). A property that is necessarily instantiated by just one individual does not qualify as a kind.

Therefore:

• ∩(dogs) = the dog-kind ✓
• ∩(dog) = undefined ✗

This, combined with blocking of ι and ∃ by articles, explains why bare singular count nouns cannot occur as arguments in English.

Equations

• Semantics.Kinds.NMP.downDefinedFor MassCount.mass isPlural = true
• Semantics.Kinds.NMP.downDefinedFor MassCount.count isPlural = isPlural

theorem Semantics.Kinds.NMP.bare_plural_ok_bare_singular_not (bp : BlockingPrinciple) (hIota : bp.iotaBlocked = true) (hExists : bp.existsBlocked = true) : downDefinedFor MassCount.count true = true ∧ downDefinedFor MassCount.count false = false ∧ bp.iotaBlocked = true ∧ bp.existsBlocked = true

Why bare plurals are OK but bare singulars are not (in languages with articles).

Given a language where:

• ι is blocked (has "the")
• ∃ is blocked for singulars (has "a")
• ∩ is not blocked

Then:

• Bare plurals OK: ∩ is defined and not blocked
• Bare singulars OUT: ∩ is undefined, and ι/∃ are blocked

Language-specific configurations live in Fragments/{Language}/Nouns.lean.

def Semantics.Kinds.NMP.dkpIsLocal : Bool

Bare plurals are scopeless because DKP introduces a LOCAL existential.

The existential reading from DKP cannot scope out because the coercion applies inside the predicate abstract.

See Phenomena/Generics/KindReference.lean for empirical scope data.

Equations

• Semantics.Kinds.NMP.dkpIsLocal = true

def Semantics.Kinds.NMP.fallbackToExists (isKindDenoting : Bool) (bp : BlockingPrinciple) : Bool

When ∩ is undefined (NP doesn't denote a kind), we fall back to ∃.

For non-kind-denoting NPs like "parts of that machine":

• ∩ is undefined (no corresponding natural kind)
• ∃ is available (not blocked for plurals)
• Result: these NPs behave like regular existential GQs

Equations

• Semantics.Kinds.NMP.fallbackToExists isKindDenoting bp = decide ((!isKindDenoting) = true ∧ (!bp.existsBlocked) = true)

Computational DKP

@cite{krifka-2004} @cite{chierchia-1998}

Simplified, decidable formalization of Chierchia's DKP for concrete scrambling comparisons with @cite{krifka-2004}. Uses List Entity and Bool (rather than Set Atom and Prop) so that examples reduce by rfl.

The parallel Krifka machinery is in Krifka2004.lean; both are instantiated side-by-side in Phenomena/Generics/Compare.lean.

See Theories/Comparisons/KindReference.lean for the formal comparison.

@[reducible, inline]

abbrev Semantics.Kinds.NMP.KindExtension (Entity World : Type) : Type

A kind's extension at each world (the instances)

Equations

• Semantics.Kinds.NMP.KindExtension Entity World = (World → List Entity)

@[reducible, inline]

abbrev Semantics.Kinds.NMP.ChierchiaVP (Entity World : Type) : Type

A VP meaning (intensional)

Equations

• Semantics.Kinds.NMP.ChierchiaVP Entity World = (Entity → World → Bool)

@[reducible, inline]

abbrev Semantics.Kinds.NMP.ChierchiaSent (World : Type) : Type

A sentence meaning (proposition)

Equations

• Semantics.Kinds.NMP.ChierchiaSent World = (World → Bool)

def Semantics.Kinds.NMP.dkpApply {Entity World : Type} (kind : KindExtension Entity World) (vp : ChierchiaVP Entity World) : ChierchiaSent World

DKP (Derived Kind Predication): Coerce a kind to work with object-level predicates.

Given a kind (represented by its extension at each world) and an object-level VP, DKP introduces existential quantification:

DKP(VP)(k) = λw. ∃x ∈ k(w). VP(x)(w)

Property: The ∃ is introduced HERE, at the point of composition, not at a syntactic position. This makes DKP position-invariant.

Equations

• Semantics.Kinds.NMP.dkpApply kind vp w = (kind w).any fun (x : Entity) => vp x w

def Semantics.Kinds.NMP.chierchiaDerivUnscrambled {Entity World : Type} (kind : KindExtension Entity World) (vp : ChierchiaVP Entity World) : ChierchiaSent World

Chierchia's derivation for "[niet [BP V]]" (unscrambled).

1. BP = kind k
2. VP = λx.V(x)
3. DKP: ∃x[k(x) ∧ V(x)]
4. Negation: ¬∃x[k(x) ∧ V(x)]

Equations

• Semantics.Kinds.NMP.chierchiaDerivUnscrambled kind vp w = !Semantics.Kinds.NMP.dkpApply kind vp w

def Semantics.Kinds.NMP.chierchiaDerivScrambled {Entity World : Type} (kind : KindExtension Entity World) (vp : ChierchiaVP Entity World) : ChierchiaSent World

Chierchia's derivation for "[BP [niet V]]" (scrambled).

In Chierchia's system, scrambling doesn't change the derivation. DKP still applies when the kind meets the predicate, and the ∃ is introduced at that point (the trace position in LF).

Result: Same as unscrambled — ¬∃x[k(x) ∧ V(x)]

Equations

• Semantics.Kinds.NMP.chierchiaDerivScrambled kind vp w = !Semantics.Kinds.NMP.dkpApply kind vp w

theorem Semantics.Kinds.NMP.chierchia_position_invariant {Entity World : Type} (kind : KindExtension Entity World) (vp : ChierchiaVP Entity World) : chierchiaDerivScrambled kind vp = chierchiaDerivUnscrambled kind vp

Chierchia's DKP is position-invariant.

Scrambled and unscrambled derivations yield the same meaning. This is the source of Chierchia's incorrect prediction for Dutch scrambling.

Related Theory

• Theories/Semantics/Lexical/Noun/Kind/Krifka2004.lean - Alternative: Bare NPs as properties
• Theories/Semantics/Lexical/Noun/Kind/MeaningPreservation.lean - Meaning Preservation, singular kinds
• Theories/Semantics/Lexical/Noun/Kind/Generics.lean - GEN operator for generic readings

Empirical Data

For empirical patterns (cross-linguistic data, scope judgments, predicate class effects), see:

• Phenomena/Generics/KindReference.lean - unified kind reference phenomena
• Phenomena/Generics/BarePlurals.lean - generic vs existential readings
• Phenomena/Generics/Data.lean - generic sentence patterns

For kind formation by salient equivalence relations (the Mendia 2020 framework that subsumes Carlson's Disjointness Condition), see Theories/Semantics/Kinds/Subkinds.lean.