Bare NPs as Properties

@cite{krifka-2004} @cite{krifka-2003}

Formalizes Krifka's analysis from "Bare NPs: Kind-referring, Indefinites, Both, or Neither?" (SALT 2003 / EISS5 2004).

Bare NPs are fundamentally properties, type-shifted to kind or indefinite readings depending on context. Count nouns carry a number argument (⟨s,⟨n,⟨e,t⟩⟩⟩); pluralization existentially binds it locally. Kind readings require topic position.

Aspect	@cite{chierchia-1998}	@cite{krifka-2004}
Basic denotation	Kind (via ∩)	Property
Existential reading	DKP coercion	Direct ∃ type shift
Narrow scope	DKP locality	Local ∃ shift locality
Singular exclusion	∩ undefined for non-cumulative	Unfilled number argument
Kind reading	Always available	Requires topic position

inductive Semantics.Lexical.Noun.Kind.Krifka2004.Individual (Atom : Type) : Type

An individual is either an atom or a plurality (as in Chierchia)

• atom {Atom : Type} : Atom → Individual Atom
• plural {Atom : Type} : Set Atom → Individual Atom

inductive Semantics.Lexical.Noun.Kind.Krifka2004.Number : Type

Number values for count nouns

• one : Number
• two : Number
• many : Number

instance Semantics.Lexical.Noun.Kind.Krifka2004.instDecidableEqNumber : DecidableEq Number

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.instDecidableEqNumber x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Lexical.Noun.Kind.Krifka2004.instReprNumber : Repr Number

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.instReprNumber = { reprPrec := Semantics.Lexical.Noun.Kind.Krifka2004.instReprNumber.repr }

def Semantics.Lexical.Noun.Kind.Krifka2004.instReprNumber.repr : Number → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Noun.Kind.Krifka2004.instBEqNumber.beq : Number → Number → Bool

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.instBEqNumber.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Noun.Kind.Krifka2004.instBEqNumber : BEq Number

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.instBEqNumber = { beq := Semantics.Lexical.Noun.Kind.Krifka2004.instBEqNumber.beq }

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Krifka2004.CountNounDen (World Atom : Type) : Type

Count noun denotation with number argument: ⟨s,⟨n,⟨e,t⟩⟩⟩. ⟦dog⟧(w)(1)(fido) = true iff fido is a single dog in w.

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.CountNounDen World Atom = (World → Semantics.Lexical.Noun.Kind.Krifka2004.Number → Semantics.Lexical.Noun.Kind.Krifka2004.Individual Atom → Bool)

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Krifka2004.MassNounDen (World Atom : Type) : Type

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

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.MassNounDen World Atom = (World → Semantics.Lexical.Noun.Kind.Krifka2004.Individual Atom → Bool)

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Krifka2004.Property (World Atom : Type) : Type

A general property (intensional): the basic type for bare NPs in Krifka.

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.Property World Atom = (World → Semantics.Lexical.Noun.Kind.Krifka2004.Individual Atom → Bool)

def Semantics.Lexical.Noun.Kind.Krifka2004.singularize (World Atom : Type) (P : CountNounDen World Atom) : Property World Atom

Singular morpheme: binds number argument to 1. ⟦-sg⟧(P) = λw.λx[P(w)(1)(x)]

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.singularize World Atom P w x = P w Semantics.Lexical.Noun.Kind.Krifka2004.Number.one x

def Semantics.Lexical.Noun.Kind.Krifka2004.pluralize (World Atom : Type) (P : CountNounDen World Atom) : Property World Atom

Plural morpheme: existentially quantifies over number > 1. ⟦-pl⟧(P) = λw.λx[∃n > 1. P(w)(n)(x)]. The ∃ is local (not a scope-taking operation).

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.pluralize World Atom P w x = (P w Semantics.Lexical.Noun.Kind.Krifka2004.Number.two x || P w Semantics.Lexical.Noun.Kind.Krifka2004.Number.many x)

theorem Semantics.Lexical.Noun.Kind.Krifka2004.plural_is_local (World Atom : Type) (P : CountNounDen World Atom) : pluralize World Atom P = fun (w : World) (x : Individual Atom) => P w Number.two x || P w Number.many x

Scopelessness follows from local number binding.

structure Semantics.Lexical.Noun.Kind.Krifka2004.BareSingularRestriction : Type

Bare singulars (*"Dog barks") are blocked because the number parameter is unfilled — morphology must bind it (cf. Chierchia: ∩ undefined).

• hasNumberParam : Bool
• singularFills : Bool
• pluralFills : Bool
• bareUnfilled : Bool

def Semantics.Lexical.Noun.Kind.Krifka2004.existentialShiftPositionSensitive : Bool

∃-shift is position-sensitive: it applies at the surface position of the bare NP. Scrambled BPs scope wide; unscrambled BPs scope narrow. Evidence: Dutch/German scrambling.

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.existentialShiftPositionSensitive = true

inductive Semantics.Lexical.Noun.Kind.Krifka2004.TypeShift : Type

Type shifts available for properties.

• exists_ : TypeShift
• iota : TypeShift
• down : TypeShift

instance Semantics.Lexical.Noun.Kind.Krifka2004.instDecidableEqTypeShift : DecidableEq TypeShift

Equations

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

def Semantics.Lexical.Noun.Kind.Krifka2004.instReprTypeShift.repr : TypeShift → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Kind.Krifka2004.instReprTypeShift : Repr TypeShift

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.instReprTypeShift = { reprPrec := Semantics.Lexical.Noun.Kind.Krifka2004.instReprTypeShift.repr }

def Semantics.Lexical.Noun.Kind.Krifka2004.downShift (World Atom : Type) (P : Property World Atom) : World → Individual Atom

∩ (down) shift: property → kind. ∩P = λw[ιP(w)]. Unlike Chierchia, not restricted to cumulative properties.

Equations

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

inductive Semantics.Lexical.Noun.Kind.Krifka2004.InfoStructure : Type

Information structure position of an NP.

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

instance Semantics.Lexical.Noun.Kind.Krifka2004.instDecidableEqInfoStructure : DecidableEq InfoStructure

Equations

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

instance Semantics.Lexical.Noun.Kind.Krifka2004.instReprInfoStructure : Repr InfoStructure

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.instReprInfoStructure = { reprPrec := Semantics.Lexical.Noun.Kind.Krifka2004.instReprInfoStructure.repr }

def Semantics.Lexical.Noun.Kind.Krifka2004.instReprInfoStructure.repr : InfoStructure → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Noun.Kind.Krifka2004.availableInterpretations (position : InfoStructure) : List TypeShift

Available interpretations depend on information structure. Topic favors ∩ (kind); focus favors ∃ (indefinite).

Equations

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

theorem Semantics.Lexical.Noun.Kind.Krifka2004.kind_requires_topic : TypeShift.down ∈ availableInterpretations InfoStructure.topic ∧ availableInterpretations InfoStructure.focus = [TypeShift.exists_, TypeShift.down]

Kind readings require topic position.

Position-Sensitive ∃-Shift

@cite{carlson-1977} @cite{le-bruyn-de-swart-2022} @cite{partee-1987}

∃-shift applies at the surface position of the bare plural, predicting that scrambled BPs take wide scope over negation.

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Krifka2004.KrifkaProp (Entity World : Type) : Type

A property (the basic meaning of bare NPs in Krifka)

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.KrifkaProp Entity World = (World → Entity → Bool)

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Krifka2004.KrifkaVP (Entity World : Type) : Type

A VP meaning

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.KrifkaVP Entity World = (Entity → World → Bool)

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Krifka2004.KrifkaSent (World : Type) : Type

A sentence meaning

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.KrifkaSent World = (World → Bool)

def Semantics.Lexical.Noun.Kind.Krifka2004.KrifkaVP.neg {Entity World : Type} (vp : KrifkaVP Entity World) : KrifkaVP Entity World

Negate a VP

Equations

• vp.neg x w = !vp x w

def Semantics.Lexical.Noun.Kind.Krifka2004.existsShiftApply {Entity World : Type} (domain : List Entity) (prop : KrifkaProp Entity World) (vp : KrifkaVP Entity World) : KrifkaSent World

∃-shift: ∃x ∈ domain. P(w)(x) ∧ VP(x)(w). Applies at surface position.

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.existsShiftApply domain prop vp w = domain.any fun (x : Entity) => prop w x && vp x w

def Semantics.Lexical.Noun.Kind.Krifka2004.krifkaDerivUnscrambled {Entity World : Type} (domain : List Entity) (prop : KrifkaProp Entity World) (vp : KrifkaVP Entity World) : KrifkaSent World

Unscrambled: [niet [BP V]] → ¬∃x[P(x) ∧ V(x)].

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.krifkaDerivUnscrambled domain prop vp w = !Semantics.Lexical.Noun.Kind.Krifka2004.existsShiftApply domain prop vp w

def Semantics.Lexical.Noun.Kind.Krifka2004.krifkaDerivScrambled {Entity World : Type} (domain : List Entity) (prop : KrifkaProp Entity World) (vp : KrifkaVP Entity World) : KrifkaSent World

Scrambled: [BP [niet V]] → ∃x[P(x) ∧ ¬V(x)] (wide scope).

Equations

• Semantics.Lexical.Noun.Kind.Krifka2004.krifkaDerivScrambled domain prop vp = Semantics.Lexical.Noun.Kind.Krifka2004.existsShiftApply domain prop vp.neg

theorem Semantics.Lexical.Noun.Kind.Krifka2004.krifka_position_sensitive {Entity World : Type} (domain : List Entity) (prop : KrifkaProp Entity World) (vp : KrifkaVP Entity World) : krifkaDerivScrambled domain prop vp = existsShiftApply domain prop vp.neg

Scrambled derivation composes ∃-shift with negated VP.