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

Type-shifting operations from @cite{partee-1987} / @cite{dayal-2004}.

These convert between semantic types:

• ∩ (down/cap): Property → Kind (nominalization)
• ι (iota): Property → Individual (definite description)
• ∃ (exists): Property → GQ (existential quantification)

• down : TypeShift
• iota : TypeShift
• exists : TypeShift

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

Equations

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

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

Equations

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

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

Equations

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

instance Semantics.Lexical.Noun.Kind.Dayal2004.instBEqTypeShift : BEq TypeShift

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqTypeShift = { beq := Semantics.Lexical.Noun.Kind.Dayal2004.instBEqTypeShift.beq }

def Semantics.Lexical.Noun.Kind.Dayal2004.instBEqTypeShift.beq : TypeShift → TypeShift → Bool

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqTypeShift.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Semantics.Lexical.Noun.Kind.Dayal2004.meaningPreservationRank : TypeShift → ℕ

Meaning Preservation Ranking (@cite{dayal-2004}: 408)

{∩, ι} > ∃

The key insight: ∩ and ι both preserve the full semantic content of the property, while ∃ introduces existential quantification that "loses" some information.

∩P preserves P's intension (the full function from worlds to extensions) ιP preserves P's intension (picks unique satisfier per world) ∃P only preserves existence of some satisfier (loses identity)

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.meaningPreservationRank Semantics.Lexical.Noun.Kind.Dayal2004.TypeShift.down = 1
• Semantics.Lexical.Noun.Kind.Dayal2004.meaningPreservationRank Semantics.Lexical.Noun.Kind.Dayal2004.TypeShift.iota = 1
• Semantics.Lexical.Noun.Kind.Dayal2004.meaningPreservationRank Semantics.Lexical.Noun.Kind.Dayal2004.TypeShift.exists = 2

def Semantics.Lexical.Noun.Kind.Dayal2004.equallyPreferred (t1 t2 : TypeShift) : Bool

Type shifts with equal rank are equally preferred

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.morePreferred (t1 t2 : TypeShift) : Bool

t1 is more preferred than t2 if it has lower rank

Equations

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

structure Semantics.Lexical.Noun.Kind.Dayal2004.InstantiationSet : Type

Instantiation set of a kind at a world.

The instantiation set is the collection of actual instances of the kind. For "dog-kind" at world w, this is the set of all dogs in w.

Key insight: Number morphology constrains the instantiation set:

• Singular: instantiation set is singleton OR inaccessible
• Plural: instantiation set has multiple accessible members

For computational purposes, we represent this abstractly.

• count : ℕ

  Count of instances (0 = empty, 1 = singleton, >1 = multiple)

• accessible : Bool

  Whether instances are "accessible" (epistemically available)

instance Semantics.Lexical.Noun.Kind.Dayal2004.instReprInstantiationSet : Repr InstantiationSet

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instReprInstantiationSet = { reprPrec := Semantics.Lexical.Noun.Kind.Dayal2004.instReprInstantiationSet.repr }

def Semantics.Lexical.Noun.Kind.Dayal2004.instReprInstantiationSet.repr : InstantiationSet → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Kind.Dayal2004.instDecidableEqInstantiationSet : DecidableEq InstantiationSet

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instDecidableEqInstantiationSet = Semantics.Lexical.Noun.Kind.Dayal2004.instDecidableEqInstantiationSet.decEq

def Semantics.Lexical.Noun.Kind.Dayal2004.instDecidableEqInstantiationSet.decEq (x✝ x✝¹ : InstantiationSet) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Lexical.Noun.Kind.Dayal2004.instBEqInstantiationSet : BEq InstantiationSet

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqInstantiationSet = { beq := Semantics.Lexical.Noun.Kind.Dayal2004.instBEqInstantiationSet.beq }

def Semantics.Lexical.Noun.Kind.Dayal2004.instBEqInstantiationSet.beq : InstantiationSet → InstantiationSet → Bool

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqInstantiationSet.beq { count := a, accessible := a_1 } { count := b, accessible := b_1 } = (a == b && a_1 == b_1)
• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqInstantiationSet.beq x✝¹ x✝ = false

def Semantics.Lexical.Noun.Kind.Dayal2004.InstantiationSet.isSingleton (is : InstantiationSet) : Bool

Accessibility of instantiation sets.

An instantiation set is "inaccessible" when:

1. The kind is extinct (no actual instances exist)
2. The instances are not salient/distinguishable in context
3. The kind is treated as atomic (collective reading)

Inaccessible instantiation sets allow singular morphology even for kinds with "conceptually plural" members.

Equations

• is.isSingleton = decide (is.count ≤ 1)

def Semantics.Lexical.Noun.Kind.Dayal2004.InstantiationSet.allowsSingular (is : InstantiationSet) : Bool

Equations

• is.allowsSingular = (!is.accessible || is.isSingleton)

def Semantics.Lexical.Noun.Kind.Dayal2004.InstantiationSet.allowsPlural (is : InstantiationSet) : Bool

Equations

• is.allowsPlural = is.accessible

inductive Semantics.Lexical.Noun.Kind.Dayal2004.NumberFeature : Type

Number feature on nominals.

Key insight from Dayal: Number is NOT about semantic plurality vs singularity. It's about whether the instantiation set is conceptualized as:

• Atomic/unitary (singular)
• Non-atomic/multiple (plural)

• sg : NumberFeature
• pl : NumberFeature
• mass : NumberFeature

instance Semantics.Lexical.Noun.Kind.Dayal2004.instDecidableEqNumberFeature : DecidableEq NumberFeature

Equations

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

instance Semantics.Lexical.Noun.Kind.Dayal2004.instReprNumberFeature : Repr NumberFeature

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instReprNumberFeature = { reprPrec := Semantics.Lexical.Noun.Kind.Dayal2004.instReprNumberFeature.repr }

def Semantics.Lexical.Noun.Kind.Dayal2004.instReprNumberFeature.repr : NumberFeature → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.instBEqNumberFeature.beq : NumberFeature → NumberFeature → Bool

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqNumberFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Noun.Kind.Dayal2004.instBEqNumberFeature : BEq NumberFeature

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqNumberFeature = { beq := Semantics.Lexical.Noun.Kind.Dayal2004.instBEqNumberFeature.beq }

inductive Semantics.Lexical.Noun.Kind.Dayal2004.SingularLicense : Type

License for singular morphology on kinds.

• singleton : SingularLicense

  Singleton instantiation set (unique in context)

• inaccessible : SingularLicense

  Inaccessible instantiation set (extinct, collective)

• taxonomic : SingularLicense

  Taxonomic reading (sub-kinds, not individuals)

instance Semantics.Lexical.Noun.Kind.Dayal2004.instDecidableEqSingularLicense : DecidableEq SingularLicense

Equations

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

instance Semantics.Lexical.Noun.Kind.Dayal2004.instReprSingularLicense : Repr SingularLicense

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instReprSingularLicense = { reprPrec := Semantics.Lexical.Noun.Kind.Dayal2004.instReprSingularLicense.repr }

def Semantics.Lexical.Noun.Kind.Dayal2004.instReprSingularLicense.repr : SingularLicense → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Kind.Dayal2004.instBEqSingularLicense : BEq SingularLicense

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqSingularLicense = { beq := Semantics.Lexical.Noun.Kind.Dayal2004.instBEqSingularLicense.beq }

def Semantics.Lexical.Noun.Kind.Dayal2004.instBEqSingularLicense.beq : SingularLicense → SingularLicense → Bool

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqSingularLicense.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Semantics.Lexical.Noun.Kind.Dayal2004.SingularKind : Type

Singular Kinds (@cite{dayal-2004}: 411-423)

Grammatically singular but denoting kinds:

• "The lion is a predator" (taxonomic)
• "The dodo is extinct" (no living instances)
• "The computer has revolutionized communication" (collective)

These are possible when the instantiation set is:

1. Singleton (unique species/type in context)
2. Inaccessible (extinct, conceptualized as atomic)

The ι operator applies to KIND-LEVEL properties, not individual-level.

• kind : String

  The underlying kind

• singularLicense : SingularLicense

  Why singular is allowed

instance Semantics.Lexical.Noun.Kind.Dayal2004.instReprSingularKind : Repr SingularKind

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instReprSingularKind = { reprPrec := Semantics.Lexical.Noun.Kind.Dayal2004.instReprSingularKind.repr }

def Semantics.Lexical.Noun.Kind.Dayal2004.instReprSingularKind.repr : SingularKind → ℕ → Std.Format

Equations

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

inductive Semantics.Lexical.Noun.Kind.Dayal2004.CNDenotation : Type

Taxonomic readings (@cite{dayal-2004}: 426-433)

Common nouns can denote:

1. Properties of INDIVIDUALS: dog(x) = "x is a dog individual"
2. Properties of SUB-KINDS: dog(k) = "k is a dog sub-kind"

Example: "The dog evolved from the wolf"

• Individual reading: Some specific dog evolved (anomalous)
• Taxonomic reading: Dog-kind evolved from wolf-kind (natural)

The taxonomic reading treats sub-kinds as the "atoms" of predication.

• individual : CNDenotation

  Property of individuals: λx. P(x)

• taxonomic : CNDenotation

  Property of sub-kinds: λk. P(k) where k ranges over sub-kinds

instance Semantics.Lexical.Noun.Kind.Dayal2004.instDecidableEqCNDenotation : DecidableEq CNDenotation

Equations

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

instance Semantics.Lexical.Noun.Kind.Dayal2004.instReprCNDenotation : Repr CNDenotation

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instReprCNDenotation = { reprPrec := Semantics.Lexical.Noun.Kind.Dayal2004.instReprCNDenotation.repr }

def Semantics.Lexical.Noun.Kind.Dayal2004.instReprCNDenotation.repr : CNDenotation → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.instBEqCNDenotation.beq : CNDenotation → CNDenotation → Bool

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqCNDenotation.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Noun.Kind.Dayal2004.instBEqCNDenotation : BEq CNDenotation

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqCNDenotation = { beq := Semantics.Lexical.Noun.Kind.Dayal2004.instBEqCNDenotation.beq }

def Semantics.Lexical.Noun.Kind.Dayal2004.taxonomicIota (kindName : String) : String

When a CN has a taxonomic reading, "the CN" can be singular even when the kind has multiple sub-kinds.

"The dog" (taxonomic) = ιk[dog-kind(k)] where k ranges over basic-level kinds

The uniqueness is at the TAXONOMIC level (one dog-kind), not the instance level.

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.taxonomicIota kindName = toString "ιk[" ++ toString kindName ++ toString "-kind(k)]"

structure Semantics.Lexical.Noun.Kind.Dayal2004.TaxonomicHierarchy : Type

Taxonomic hierarchy: kinds can have sub-kinds.

"Dogs" can mean:

• All dog individuals (individual reading)
• All dog breeds (taxonomic reading)

The taxonomic reading explains why some kind-level predicates work with "the NP" even when there are many instances.

• superKind : String

  The super-kind

• subKinds : List String

  Sub-kinds (breeds, species, etc.)

def Semantics.Lexical.Noun.Kind.Dayal2004.dogTaxonomy : TaxonomicHierarchy

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.dogTaxonomy = { superKind := "dog", subKinds := ["poodle", "labrador", "beagle", "collie"] }

structure Semantics.Lexical.Noun.Kind.Dayal2004.TypeShiftContext : Type

Type-shift availability given number and blocking.

Dayal's system: type-shifts are constrained by:

1. Meaning preservation ranking: prefer ∩/ι over ∃
2. Number morphology: sg requires singleton/inaccessible instantiation
3. Blocking: overt D blocks covert equivalent
4. ∩ definedness: requires kind-compatible property

• number : NumberFeature

  Number feature on the NP

• downDefined : Bool

  Is ∩ defined (is this a kind-compatible property)?

• iotaBlocked : Bool

  Is ι blocked by an overt definite article?

• existsBlocked : Bool

  Is ∃ blocked by an overt indefinite article?

• instantiationAccessible : Bool

  Is the instantiation set accessible?

instance Semantics.Lexical.Noun.Kind.Dayal2004.instReprTypeShiftContext : Repr TypeShiftContext

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instReprTypeShiftContext = { reprPrec := Semantics.Lexical.Noun.Kind.Dayal2004.instReprTypeShiftContext.repr }

def Semantics.Lexical.Noun.Kind.Dayal2004.instReprTypeShiftContext.repr : TypeShiftContext → ℕ → Std.Format

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.availableShifts (ctx : TypeShiftContext) : List TypeShift

Available type-shifts given context.

Returns shifts in preference order (most preferred first).

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.selectShift (ctx : TypeShiftContext) : Option TypeShift

Select the best available type-shift.

Follows Meaning Preservation: choose highest-ranked available shift.

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.selectShift ctx = (Semantics.Lexical.Noun.Kind.Dayal2004.availableShifts ctx).head?

structure Semantics.Lexical.Noun.Kind.Dayal2004.KindReferenceParams : Type

Language-specific parameters for kind reference (@cite{dayal-2004}: 433-445).

Languages differ in:

1. Whether they have definite/indefinite articles
2. Whether bare nominals can denote kinds
3. Whether singular kinds require "the"

• hasDefiniteArticle : Bool

  Does this language have a definite article?

• hasIndefiniteArticle : Bool

  Does this language have an indefinite article?

• bareKindsOK : Bool

  Can bare nominals denote kinds (∩ unblocked)?

• definiteSingularKinds : Bool

  Can singular kinds use "the"?

• definitePluralKinds : Bool

  Can plural kinds use "the"?

def Semantics.Lexical.Noun.Kind.Dayal2004.instReprKindReferenceParams.repr : KindReferenceParams → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Kind.Dayal2004.instReprKindReferenceParams : Repr KindReferenceParams

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instReprKindReferenceParams = { reprPrec := Semantics.Lexical.Noun.Kind.Dayal2004.instReprKindReferenceParams.repr }

def Semantics.Lexical.Noun.Kind.Dayal2004.englishKindRef : KindReferenceParams

English kind reference:

• Bare plurals for kinds: "Dogs are mammals"
• "The" for singular kinds: "The lion is a predator"
• "The" for plural kinds is marked: ?"The dogs are mammals"

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.romanceKindRef : KindReferenceParams

Romance (French, Italian, Spanish) kind reference:

• Definite article required for kinds: "Les chiens sont des mammifères"
• Both singular and plural kinds use definite article
• Bare nominals restricted to special contexts

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.determinerlessKindRef : KindReferenceParams

Determiner-less languages (Hindi, Russian, Chinese) kind reference:

• Bare nominals freely denote kinds
• No definite/indefinite distinction in morphology
• All interpretations available in context

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.germanKindRef : KindReferenceParams

German kind reference (intermediate):

• Bare plurals OK for kinds: "Hunde sind Säugetiere"
• Definite optional for plural/mass kinds
• Similar to English but with more flexibility

Equations

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

inductive Semantics.Lexical.Noun.Kind.Dayal2004.PredicateType : Type

DKP (Derived Kind Predication) - Dayal's version.

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

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

Key insight: DKP is only invoked when NECESSARY. If the predicate is kind-level, no coercion needed.

• kindLevel : PredicateType

  Kind-level predicates: extinct, widespread, evolve

• objectLevel : PredicateType

  Object-level predicates: bark, be in the garden

instance Semantics.Lexical.Noun.Kind.Dayal2004.instDecidableEqPredicateType : DecidableEq PredicateType

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.instReprPredicateType.repr : PredicateType → ℕ → Std.Format

Equations

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

instance Semantics.Lexical.Noun.Kind.Dayal2004.instReprPredicateType : Repr PredicateType

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instReprPredicateType = { reprPrec := Semantics.Lexical.Noun.Kind.Dayal2004.instReprPredicateType.repr }

def Semantics.Lexical.Noun.Kind.Dayal2004.instBEqPredicateType.beq : PredicateType → PredicateType → Bool

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqPredicateType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Semantics.Lexical.Noun.Kind.Dayal2004.instBEqPredicateType : BEq PredicateType

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.instBEqPredicateType = { beq := Semantics.Lexical.Noun.Kind.Dayal2004.instBEqPredicateType.beq }

def Semantics.Lexical.Noun.Kind.Dayal2004.requiresDKP : PredicateType → Bool

Does this predicate require DKP when applied to a kind?

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.requiresDKP Semantics.Lexical.Noun.Kind.Dayal2004.PredicateType.kindLevel = false
• Semantics.Lexical.Noun.Kind.Dayal2004.requiresDKP Semantics.Lexical.Noun.Kind.Dayal2004.PredicateType.objectLevel = true

def Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate : String → Bool

Kind-level predicates (@cite{dayal-2004}: 401-403):

• be extinct, be widespread, be rare
• evolve, originate, die out
• be invented, be discovered

These directly predicate of kinds without coercion.

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate "extinct" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate "widespread" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate "rare" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate "common" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate "evolve" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate "originate" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate "die_out" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate "invented" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate "discovered" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isKindLevelPredicate x✝ = false

def Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind : String → Bool

Well-established kinds (@cite{dayal-2004}: 417-420)

For ι to apply to a kind (giving "the NP"), the kind must be "well-established" - a recognized natural class.

• "The lion is a predator" - lion is well-established kind ✓
• *"The lion sitting here is a predator" - not a natural kind ✗

This explains why modified NPs resist the singular kind reading.

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "lion" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "tiger" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "dog" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "cat" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "dodo" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "mammoth" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "dinosaur" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "computer" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "telephone" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "automobile" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "wheel" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind "printing_press" = true
• Semantics.Lexical.Noun.Kind.Dayal2004.isWellEstablishedKind x✝ = false

structure Semantics.Lexical.Noun.Kind.Dayal2004.ModificationEffect : Type

Why modification blocks singular kind reading:

"The tall lion" cannot mean "the lion-kind" because:

1. "Tall lion" does not denote a well-established kind
2. Modification restricts the extension, breaking kind status
3. ι must apply at object-level → definite description of individual

• base : String

  Base noun (well-established kind)

• modifier : String

  Modifier

• stillKind : Bool

  Result is still a well-established kind?

def Semantics.Lexical.Noun.Kind.Dayal2004.modificationBlocksKind : ModificationEffect

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.modificationBlocksKind = { base := "lion", modifier := "tall" }

theorem Semantics.Lexical.Noun.Kind.Dayal2004.ranking_transitive (t1 t2 t3 : TypeShift) (h1 : morePreferred t1 t2 = true) (h2 : morePreferred t2 t3 = true) : morePreferred t1 t3 = true

Meaning preservation ranking is transitive

theorem Semantics.Lexical.Noun.Kind.Dayal2004.down_preferred_over_exists : morePreferred TypeShift.down TypeShift.exists = true

∩ and ι are always preferred over ∃

theorem Semantics.Lexical.Noun.Kind.Dayal2004.iota_preferred_over_exists : morePreferred TypeShift.iota TypeShift.exists = true

theorem Semantics.Lexical.Noun.Kind.Dayal2004.english_bare_plural_uses_down : have ctx := { number := NumberFeature.pl, downDefined := true, iotaBlocked := true, existsBlocked := true, instantiationAccessible := true }; selectShift ctx = some TypeShift.down

English bare plurals use ∩ (most preferred available shift)

theorem Semantics.Lexical.Noun.Kind.Dayal2004.english_singular_kind_uses_iota : have ctx := { number := NumberFeature.sg, downDefined := false, iotaBlocked := false, existsBlocked := true, instantiationAccessible := false }; selectShift ctx = some TypeShift.iota

English singular kinds use ι

def Semantics.Lexical.Noun.Kind.Dayal2004.chierchiaToContext (bp : Chierchia1998.BlockingPrinciple) (nt : MassCount) (isPlural : Bool) (instantiationAccessible : Bool := true) : TypeShiftContext

Convert Chierchia's BlockingPrinciple + noun info to Dayal's TypeShiftContext.

This shows how Dayal's framework generalizes Chierchia's:

• Chierchia: BlockingPrinciple + MassCount + isPlural → bare argument OK?
• Dayal: TypeShiftContext → which type-shift is selected?

Equations

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

def Semantics.Lexical.Noun.Kind.Dayal2004.englishBlocking : Chierchia1998.BlockingPrinciple

English-like blocking principle: has "the" and "a", so ι and ∃ blocked.

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.englishBlocking = { determiners := ["the", "a", "some"], iotaBlocked := true, existsBlocked := true, downBlocked := false }

theorem Semantics.Lexical.Noun.Kind.Dayal2004.dayal_consistent_english_bare_plural : have ctx := chierchiaToContext englishBlocking MassCount.count true; selectShift ctx = some TypeShift.down

Dayal's framework is consistent with Chierchia's for English.

When Chierchia predicts bare plurals are licensed (∩ defined and not blocked), Dayal's selectShift returns.down (the kind-forming shift).

theorem Semantics.Lexical.Noun.Kind.Dayal2004.dayal_consistent_english_bare_singular_out : have ctx := chierchiaToContext englishBlocking MassCount.count false; selectShift ctx = none

When ∩ is undefined (singular count) and ι/∃ are blocked (English), both frameworks predict bare singular is OUT.

theorem Semantics.Lexical.Noun.Kind.Dayal2004.dayal_consistent_english_mass_noun : have ctx := chierchiaToContext englishBlocking MassCount.mass false; selectShift ctx = some TypeShift.down

Mass nouns: both frameworks predict bare mass nouns are OK (use ∩).

theorem Semantics.Lexical.Noun.Kind.Dayal2004.dayal_subsumes_chierchia_plural_available : have ctx := chierchiaToContext englishBlocking MassCount.count true; (selectShift ctx).isSome = true

Dayal subsumes Chierchia: When a type-shift is available, selectShift finds it.

Verified for the key cases via the concrete theorems above. The general pattern: selectShift returns Some iff at least one of:

• ∩ is defined (bare plural/mass)
• ι is not blocked
• ∃ is not blocked

theorem Semantics.Lexical.Noun.Kind.Dayal2004.dayal_subsumes_chierchia_singular_blocked : have ctx := chierchiaToContext englishBlocking MassCount.count false; (selectShift ctx).isSome = false

def Semantics.Lexical.Noun.Kind.Dayal2004.romanceBlocking : Chierchia1998.BlockingPrinciple

Romance-like blocking: has definite article, so bare kinds need "the". But for kind reference, the definite is used (not blocked for that purpose).

Equations

• Semantics.Lexical.Noun.Kind.Dayal2004.romanceBlocking = { determiners := ["le", "la", "les", "un", "une", "des"], iotaBlocked := true, existsBlocked := true, downBlocked := false }

theorem Semantics.Lexical.Noun.Kind.Dayal2004.dayal_consistent_romance_bare_plural : have ctx := chierchiaToContext romanceBlocking MassCount.count true; selectShift ctx = some TypeShift.down

In Romance, bare plurals are also predicted to use ∩ when available.

theorem Semantics.Lexical.Noun.Kind.Dayal2004.meaning_preservation_derives_kind_preference : have ctx := { number := NumberFeature.pl, downDefined := true, iotaBlocked := true, existsBlocked := false, instantiationAccessible := true }; selectShift ctx = some TypeShift.down

Meaning Preservation explains Chierchia's blocking.

When both ∩ and ∃ are available, Dayal selects ∩ (more meaning-preserving). This derives Chierchia's observation that bare plurals prefer kind readings.

Related Theory

• Theories/Semantics/Lexical/Noun/Kind/Chierchia1998.lean - Chierchia's NMP, ∩/∪ operators, DKP
• Theories/Semantics/Lexical/Noun/Kind/Generics.lean - GEN operator for generic readings

Empirical Data

• Phenomena/Generics/KindReference.lean - cross-linguistic patterns, singular kinds, scopelessness