Bare NPs as properties

[Kri04] [Kri03]

Krifka's analysis of bare NPs ("Bare NPs: Kind-referring, Indefinites, Both, or Neither?", SALT 13 / EISS 5). Bare NPs are basically properties; context-sensitive type shifts coerce them to kind or indefinite readings — so, in the title's terms, neither kind-referring nor indefinite, but shiftable to both.

Count nouns carry a natural-number argument: den w n x reads "in w, the individual x consists of n instances", and a count noun is an additive extensive measure function in that argument (IsExtensiveMeasure). Number morphology saturates the argument: the singular fills it with 1, the semantic plural binds it existentially with no > 1 restriction (so the bare plural is true of a single instance — "Do you have dogs? — Yes, one"). A bare singular count noun is therefore the wrong type to be an argument — number-indexed ⟨n,⟨e,t⟩⟩, not a predicate ⟨e,t⟩ — which is why *Dog barks is out. Kind reference reuses [Chi98]'s ∩ operator (Semantics.Kinds.NMP.down), which Krifka adopts (§4.3), and requires topic position; the existential shift applies at the surface position, deriving the narrow scope of bare plurals and their wide scope under scrambling.

Main declarations

• CountNounDen, MassNounDen — count (number-indexed) vs mass denotations
• IsExtensiveMeasure — the count noun's uniqueness + additivity laws
• singularize, pluralize — number morphology (fill 1 / bind ∃ n)
• availableInterpretations, kind_requires_topic — topic-gating of kind reference
• krifkaDerivScrambled, krifkaDerivUnscrambled — the surface-position ∃-shift (built on the shared closure NMP.existsClose) used for the Dutch/German scrambling contrast
• scope_follows_position — scrambled and unscrambled derivations diverge

Count and mass denotations

Atom is Type (not Type*) to align with NMP.Individual, the Link/Chierchia individual lattice (Set Atom) that this file reuses for kind reference.

@[reducible, inline]

abbrev Krifka2004.CountNounDen (World Atom : Type) : Type

Count noun denotation ⟨s,⟨n,⟨e,t⟩⟩⟩: den w n x holds iff in world w the individual x consists of n instances.

Equations

• Krifka2004.CountNounDen World Atom = (World → ℕ → Semantics.Kinds.NMP.Individual Atom → Prop)

@[reducible, inline]

abbrev Krifka2004.MassNounDen (World Atom : Type) : Type

Mass noun denotation ⟨s,⟨e,t⟩⟩: no number argument.

Equations

• Krifka2004.MassNounDen World Atom = (World → Semantics.Kinds.NMP.Individual Atom → Prop)

@[reducible, inline]

abbrev Krifka2004.Property (World Atom : Type) : Type

The basic type of a bare NP: a property ⟨s,⟨e,t⟩⟩.

Equations

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

def Krifka2004.IsExtensiveMeasure {World Atom : Type} (den : CountNounDen World Atom) : Prop

Count nouns are additive extensive measure functions in their number argument: the count of an individual is unique, and the counts of disjoint individuals add.

Equations

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

Number morphology

def Krifka2004.singularize {World Atom : Type} (den : CountNounDen World Atom) : Property World Atom

Singular morphology fills the number argument with 1.

Equations

• Krifka2004.singularize den w x = den w 1 x

def Krifka2004.pluralize {World Atom : Type} (den : CountNounDen World Atom) : Property World Atom

Semantic plural morphology binds the number argument existentially, with no > 1 restriction — the analysis Krifka adopts over the rejected ∃ n > 1 variant.

Equations

• Krifka2004.pluralize den w x = ∃ (n : ℕ), den w n x

theorem Krifka2004.pluralize_of_singular {World Atom : Type} (den : CountNounDen World Atom) {w : World} {x : Semantics.Kinds.NMP.Individual Atom} (h : den w 1 x) : pluralize den w x

The bare plural is true of a single instance ("Do you have dogs? — Yes, one"): this is why the plural cannot mean ∃ n > 1.

theorem Krifka2004.morphology_saturates {World Atom : Type} (den : CountNounDen World Atom) (w : World) (x : Semantics.Kinds.NMP.Individual Atom) : singularize den w x = den w 1 x ∧ pluralize den w x = ∃ (n : ℕ), den w n x

The bare-singular block is a type fact, not a stipulation. The only routes from a number-indexed CountNounDen to an argument-type Property are the morphological saturations singularize (fill 1) and pluralize (bind ∃ n); a bare singular saturates nothing, so *Dog barks has no argument-type parse.

Type shifts and information structure

inductive Krifka2004.TypeShift : Type

The type shifts available to a property-denoting bare NP.

• existsShift : TypeShift

  ∃ shift: P ↦ λQ. ∃x[P(x) ∧ Q(x)].

• iota : TypeShift

  ι shift: P ↦ ιx.P(x).

• down : TypeShift

  ∩ (down) shift: P ↦ kind. This is [Chi98]'s operator (Semantics.Kinds.NMP.down), which Krifka adopts (§4.3).

@[implicit_reducible]

instance Krifka2004.instDecidableEqTypeShift : DecidableEq TypeShift

Equations

• Krifka2004.instDecidableEqTypeShift x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka2004.instReprTypeShift.repr : TypeShift → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krifka2004.instReprTypeShift.repr Krifka2004.TypeShift.iota prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2004.TypeShift.iota")).group prec✝
• Krifka2004.instReprTypeShift.repr Krifka2004.TypeShift.down prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2004.TypeShift.down")).group prec✝

@[implicit_reducible]

instance Krifka2004.instReprTypeShift : Repr TypeShift

Equations

• Krifka2004.instReprTypeShift = { reprPrec := Krifka2004.instReprTypeShift.repr }

inductive Krifka2004.InfoStructure : Type

Information-structure position of the bare NP.

• topic : InfoStructure
• focus : InfoStructure
• neutral : InfoStructure

@[implicit_reducible]

instance Krifka2004.instDecidableEqInfoStructure : DecidableEq InfoStructure

Equations

• Krifka2004.instDecidableEqInfoStructure x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Krifka2004.instReprInfoStructure : Repr InfoStructure

Equations

• Krifka2004.instReprInfoStructure = { reprPrec := Krifka2004.instReprInfoStructure.repr }

def Krifka2004.instReprInfoStructure.repr : InfoStructure → ℕ → Std.Format

Equations

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

def Krifka2004.availableInterpretations : InfoStructure → List TypeShift

Shifts available at each position. Kind reference (∩) requires topic position; elsewhere only the existential shift applies.

Equations

• Krifka2004.availableInterpretations Krifka2004.InfoStructure.topic = [Krifka2004.TypeShift.down, Krifka2004.TypeShift.existsShift]
• Krifka2004.availableInterpretations Krifka2004.InfoStructure.focus = [Krifka2004.TypeShift.existsShift]
• Krifka2004.availableInterpretations Krifka2004.InfoStructure.neutral = [Krifka2004.TypeShift.existsShift]

theorem Krifka2004.kind_requires_topic {p : InfoStructure} (h : TypeShift.down ∈ availableInterpretations p) : p = InfoStructure.topic

Kind reference requires topic position: the ∩ (down) shift is available only when the bare NP is a topic.

Surface-position ∃-shift (scrambling)

Krifka's existential type shift is a local type repair applied "as late, or as locally, as possible" (§4.2) at the bare NP's surface position, so scope follows position: a bare plural under negation scopes narrow, one raised above negation scopes wide. Built on the shared closure NMP.existsClose, so Krifka's narrow reading is definitionally Chierchia's DKP derivation (NMP.chierchiaDerivUnscrambled); the accounts diverge only on the scrambled reading (compared in Studies/LeBruynDeSwart2022.lean).

def Krifka2004.krifkaDerivUnscrambled {Entity : Type u_1} (dom : List Entity) (P Q : Entity → Prop) : Prop

Unscrambled [niet [BP V]]: ∃-shift below negation — ¬ ∃ x ∈ dom, P x ∧ Q x (narrow scope). Definitionally NMP.chierchiaDerivUnscrambled.

Equations

• Krifka2004.krifkaDerivUnscrambled dom P Q = ¬Semantics.Kinds.NMP.existsClose dom P Q

def Krifka2004.krifkaDerivScrambled {Entity : Type u_1} (dom : List Entity) (P Q : Entity → Prop) : Prop

Scrambled [BP [niet V]]: ∃-shift above negation — ∃ x ∈ dom, P x ∧ ¬ Q x (wide scope over negation).

Equations

• Krifka2004.krifkaDerivScrambled dom P Q = Semantics.Kinds.NMP.existsClose dom P fun (x : Entity) => ¬Q x

theorem Krifka2004.scope_follows_position : ∃ (Entity : Type) (dom : List Entity) (P : Entity → Prop) (Q : Entity → Prop), krifkaDerivScrambled dom P Q ≠ krifkaDerivUnscrambled dom P Q

Scope follows position: the scrambled (wide) and unscrambled (narrow) derivations diverge on some model — witnessed by a two-element domain where one element satisfies the predicate and the other does not.