@[reducible, inline]

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

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 u_1} (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 : Type u_1) (Atom : Type u_2) : Type (max u_1 u_2)

A property (intension): function from worlds to sets of individuals.

Equations

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

@[reducible, inline]

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

An individual concept: function from worlds to individuals.

Equations

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

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

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 : Type u_1) (Atom : Type u_2) (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 : Type u_1) (Atom : Type u_2) (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 : Type u_1) (Atom : Type u_2) (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 ([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 : Type u_3} {Atom : Type u_4} (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 : Type u_3} {Atom : Type u_4} (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 : Type u_1) (Atom : Type u_2) (P : Property World Atom) : Property World Atom

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

This is [Lin83]'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 : Type u_3} {Atom : Type u_4} (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, whence the absorption rule ⊔⊔S = ⊔S ([krifka-2026]).

theorem Semantics.Kinds.NMP.subset_pluralClosure {World : Type u_3} {Atom : Type u_4} (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 : Type u_3} {Atom : Type u_4} (P : Property World Atom) (w : World) : Mereology.CUM (pluralClosure World Atom P w)

Plural closure is always cumulative.

theorem Semantics.Kinds.NMP.up_down_id (World : Type u_1) (Atom : Type u_2) (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 : Type u_1) (Atom : Type u_2) (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 : Type u_1) (Atom : Type u_2) (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 : Type u_1) (Atom : Type u_2) (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 u_2) (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. [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. [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

@[instance_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 ⋯

@[instance_reducible]

instance Semantics.Kinds.NMP.instReprNominalMapping : Repr NominalMapping

Equations

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

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

Equations

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

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

@[instance_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

@[instance_reducible]

instance Semantics.Kinds.NMP.instDecidablePredNominalMappingCanDenoteProperty : DecidablePred CanDenoteProperty

Equations

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

inductive Semantics.Kinds.NMP.NominalDenotation : Type

Denotation type for bare nominal expressions: kind (type e individual concept) vs property (type ⟨e,t⟩). The two values name the targets of CanDenoteKind and CanDenoteProperty.

• kind : NominalDenotation
• property : NominalDenotation

def Semantics.Kinds.NMP.instReprNominalDenotation.repr : NominalDenotation → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Semantics.Kinds.NMP.instReprNominalDenotation : Repr NominalDenotation

Equations

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

@[instance_reducible]

instance Semantics.Kinds.NMP.instDecidableEqNominalDenotation : DecidableEq NominalDenotation

Equations

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

def Semantics.Kinds.NMP.pluralize {Atom : Type u_3} (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.

Bare plurals are scopeless because DKP introduces a local existential: the existential closure sits inside negation and cannot scope out. This locality is the theorem chierchia_position_invariant below — Chierchia's derivation is the same whether or not the bare plural has scrambled. See Data/Examples/LeBruynDeSwart2022.json for empirical scope data.

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)

DKP scope derivation (Chierchia side of the scrambling comparison)

[krifka-2003] [chierchia-1998]

Chierchia's Derived Kind Predication introduces the existential locally — where the kind meets the predicate — so negation always scopes outside it. Modelled with plain Prop existential closure (existsClose) over the kind's instances. The position-sensitive ∃-shift that Studies/LeBruynDeSwart2022.lean reads into [krifka-2003] reuses the same existsClose, so the two accounts share one closure and differ only in where negation sits; they are compared there on the Dutch scrambling data.

existsClose is Partee's A (existential closure) in plain extensional form. The same operator dressed in the DWP/Gallin deep embedding is Quantification.A, needed there for type-shift metatheory but not for this scope contrast.

@[reducible]

def Semantics.Kinds.NMP.existsClose {Entity : Type u_3} (dom : List Entity) (P Q : Entity → Prop) : Prop

Existential closure of a property P against a predicate Q over a finite domain: ∃ x ∈ dom, P x ∧ Q x. Partee's A type shift in plain extensional form; reducible so concrete instances are Decidable.

Equations

• Semantics.Kinds.NMP.existsClose dom P Q = ∃ x ∈ dom, P x ∧ Q x

def Semantics.Kinds.NMP.chierchiaDerivUnscrambled {Entity : Type u_3} (kind : List Entity) (P Q : Entity → Prop) : Prop

Chierchia's DKP, unscrambled [niet [BP V]]: ¬ ∃ x ∈ kind, P x ∧ Q x. The existential is introduced locally, so negation scopes outside it (narrow scope).

Equations

• Semantics.Kinds.NMP.chierchiaDerivUnscrambled kind P Q = ¬Semantics.Kinds.NMP.existsClose kind P Q

def Semantics.Kinds.NMP.chierchiaDerivScrambled {Entity : Type u_3} (kind : List Entity) (P Q : Entity → Prop) : Prop

Chierchia's DKP, scrambled [BP [niet V]]: identical to the unscrambled derivation. DKP locality means surface position cannot move the existential.

Equations

• Semantics.Kinds.NMP.chierchiaDerivScrambled kind P Q = ¬Semantics.Kinds.NMP.existsClose kind P Q

theorem Semantics.Kinds.NMP.chierchia_position_invariant {Entity : Type u_3} (kind : List Entity) (P Q : Entity → Prop) : chierchiaDerivScrambled kind P Q = chierchiaDerivUnscrambled kind P Q

DKP is local: the scrambled and unscrambled derivations coincide, so Chierchia predicts obligatory narrow scope regardless of surface position. This is the content the former dkpIsLocal : Bool := true stipulated — now a theorem about the derivations.

Related Theory

• Studies/Krifka2003.lean - Alternative: Bare NPs as properties
• Semantics/Lexical/Noun/Kind/MeaningPreservation.lean - Meaning Preservation, singular kinds
• Semantics/Genericity/Basic.lean - GEN operator for generic readings

Empirical Data

For empirical patterns (scope judgments, predicate class effects), see Data/Examples/LeBruynDeSwart2022.json and Data/Examples/CohenErteschikShir2002.json.

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