inductive Semantics.Kinds.MeaningPreservation.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
• iotaAnaphoric : TypeShift
• exists : TypeShift

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instDecidableEqTypeShift : DecidableEq TypeShift

Equations

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

def Semantics.Kinds.MeaningPreservation.instReprTypeShift.repr : TypeShift → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instReprTypeShift : Repr TypeShift

Equations

• Semantics.Kinds.MeaningPreservation.instReprTypeShift = { reprPrec := Semantics.Kinds.MeaningPreservation.instReprTypeShift.repr }

def Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.meaningPreservationRank Semantics.Kinds.MeaningPreservation.TypeShift.down = 1
• Semantics.Kinds.MeaningPreservation.meaningPreservationRank Semantics.Kinds.MeaningPreservation.TypeShift.iota = 1
• Semantics.Kinds.MeaningPreservation.meaningPreservationRank Semantics.Kinds.MeaningPreservation.TypeShift.iotaAnaphoric = 1
• Semantics.Kinds.MeaningPreservation.meaningPreservationRank Semantics.Kinds.MeaningPreservation.TypeShift.exists = 2

def Semantics.Kinds.MeaningPreservation.equallyPreferred (t1 t2 : TypeShift) : Bool

Type shifts with equal rank are equally preferred

Equations

• Semantics.Kinds.MeaningPreservation.equallyPreferred t1 t2 = (Semantics.Kinds.MeaningPreservation.meaningPreservationRank t1 == Semantics.Kinds.MeaningPreservation.meaningPreservationRank t2)

def Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.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)

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instReprInstantiationSet : Repr InstantiationSet

Equations

• Semantics.Kinds.MeaningPreservation.instReprInstantiationSet = { reprPrec := Semantics.Kinds.MeaningPreservation.instReprInstantiationSet.repr }

def Semantics.Kinds.MeaningPreservation.instReprInstantiationSet.repr : InstantiationSet → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instDecidableEqInstantiationSet : DecidableEq InstantiationSet

Equations

• Semantics.Kinds.MeaningPreservation.instDecidableEqInstantiationSet = Semantics.Kinds.MeaningPreservation.instDecidableEqInstantiationSet.decEq

def Semantics.Kinds.MeaningPreservation.instDecidableEqInstantiationSet.decEq (x✝ x✝¹ : InstantiationSet) : Decidable (x✝ = x✝¹)

Equations

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

def Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.InstantiationSet.allowsSingular (is : InstantiationSet) : Bool

Equations

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

def Semantics.Kinds.MeaningPreservation.InstantiationSet.allowsPlural (is : InstantiationSet) : Bool

Equations

• is.allowsPlural = is.accessible

inductive Semantics.Kinds.MeaningPreservation.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
• neutral : NumberFeature

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instDecidableEqNumberFeature : DecidableEq NumberFeature

Equations

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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instReprNumberFeature : Repr NumberFeature

Equations

• Semantics.Kinds.MeaningPreservation.instReprNumberFeature = { reprPrec := Semantics.Kinds.MeaningPreservation.instReprNumberFeature.repr }

def Semantics.Kinds.MeaningPreservation.instReprNumberFeature.repr : NumberFeature → ℕ → Std.Format

Equations

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

inductive Semantics.Kinds.MeaningPreservation.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)

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instDecidableEqSingularLicense : DecidableEq SingularLicense

Equations

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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instReprSingularLicense : Repr SingularLicense

Equations

• Semantics.Kinds.MeaningPreservation.instReprSingularLicense = { reprPrec := Semantics.Kinds.MeaningPreservation.instReprSingularLicense.repr }

def Semantics.Kinds.MeaningPreservation.instReprSingularLicense.repr : SingularLicense → ℕ → Std.Format

Equations

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

structure Semantics.Kinds.MeaningPreservation.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

def Semantics.Kinds.MeaningPreservation.instReprSingularKind.repr : SingularKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instReprSingularKind : Repr SingularKind

Equations

• Semantics.Kinds.MeaningPreservation.instReprSingularKind = { reprPrec := Semantics.Kinds.MeaningPreservation.instReprSingularKind.repr }

inductive Semantics.Kinds.MeaningPreservation.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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instDecidableEqCNDenotation : DecidableEq CNDenotation

Equations

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

def Semantics.Kinds.MeaningPreservation.instReprCNDenotation.repr : CNDenotation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instReprCNDenotation : Repr CNDenotation

Equations

• Semantics.Kinds.MeaningPreservation.instReprCNDenotation = { reprPrec := Semantics.Kinds.MeaningPreservation.instReprCNDenotation.repr }

def Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.taxonomicIota kindName = toString "ιk[" ++ toString kindName ++ toString "-kind(k)]"

structure Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.dogTaxonomy : TaxonomicHierarchy

Equations

• Semantics.Kinds.MeaningPreservation.dogTaxonomy = { superKind := "dog", subKinds := ["poodle", "labrador", "beagle", "collie"] }

structure Semantics.Kinds.MeaningPreservation.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?

• iotaAnaphoricBlocked : Bool

  Is ι^x blocked by an overt demonstrative or strong article? @cite{moroney-2021} §4.3: ι^x is blocked when an overt form (demonstrative, strong article) duplicates its anaphoric function.

• existsBlocked : Bool

  Is ∃ blocked by an overt indefinite article?

• instantiationAccessible : Bool

  Is the instantiation set accessible?

def Semantics.Kinds.MeaningPreservation.instReprTypeShiftContext.repr : TypeShiftContext → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instReprTypeShiftContext : Repr TypeShiftContext

Equations

• Semantics.Kinds.MeaningPreservation.instReprTypeShiftContext = { reprPrec := Semantics.Kinds.MeaningPreservation.instReprTypeShiftContext.repr }

def Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.selectShift (ctx : TypeShiftContext) : Option TypeShift

Select the best available type-shift.

Follows Meaning Preservation: choose highest-ranked available shift.

Equations

• Semantics.Kinds.MeaningPreservation.selectShift ctx = (Semantics.Kinds.MeaningPreservation.availableShifts ctx).head?

Intensional Semantics of Type-Shifts

The TypeShift enum above classifies type-shifts abstractly; the availableShifts/selectShift functions determine which are available. What's been missing is the intensional denotation of each shift.

Bare nouns have base type ⟨s,⟨e,t⟩⟩ — they denote properties across possible worlds (@cite{moroney-2021} §2.2; @cite{chierchia-1998}). Each type-shift converts this intensional property into a different semantic type:

• ∩ (.down): ⟨s,⟨e,t⟩⟩ → e — kind formation (Chierchia's ∩)
• ι (.iota): ⟨s,⟨e,t⟩⟩ × s → e — unique definite, world-relative
• ι^x (.iotaAnaphoric): ⟨s,⟨e,t⟩⟩ × ⟨e,t⟩ × s → e — anaphoric definite
• ∃ (.exists): ⟨s,⟨e,t⟩⟩ × s → Prop — existential closure at a world

These connect the abstract shift-selection machinery to Chierchia's down operator and the Core.Nominal.russellIotaList / Core.Presupposition.PrProp.presupOfReferent canonical pieces consumed by Theories/Semantics/Definiteness/Basic.lean.

@[reducible, inline]

abbrev Semantics.Kinds.MeaningPreservation.shiftDown {World Atom : Type} (P : NMP.Property World Atom) : NMP.Kind World Atom

∩-shift (kind formation): maps an intensional property to its kind individual. This IS NMP.down.

Equations

• Semantics.Kinds.MeaningPreservation.shiftDown P = Semantics.Kinds.NMP.down World Atom P

def Semantics.Kinds.MeaningPreservation.shiftIota {World Atom : Type} (P : NMP.Property World Atom) (w : World) (unique : ∃! x : NMP.Individual Atom, x ∈ P w) : NMP.Individual Atom

ι-shift (unique definite): at world w, returns the unique satisfier of P(w) if one exists. This is the world-relative definite description.

@cite{moroney-2021} §2.2: Shan bare nouns get this reading when the context supplies a unique referent.

Equations

• Semantics.Kinds.MeaningPreservation.shiftIota P w unique = Classical.choose ⋯

def Semantics.Kinds.MeaningPreservation.shiftIotaAnaphoric {World Atom : Type} (P : NMP.Property World Atom) (Q : NMP.Individual Atom → Prop) (w : World) (unique : ∃! x : NMP.Individual Atom, x ∈ P w ∧ Q x) : NMP.Individual Atom

ι^x-shift (anaphoric definite): at world w, returns the unique satisfier of P(w) ∧ Q(w) where Q is the anaphoric restrictor.

@cite{moroney-2021} §4.3: ι^x P Q = ιx[P(x) ∧ Q(x)]. Shan bare nouns get this reading in anaphoric contexts (narrative continuations, relational bridging); demonstrative-noun phrases optionally reinforce it.

Equations

• Semantics.Kinds.MeaningPreservation.shiftIotaAnaphoric P Q w unique = Classical.choose ⋯

def Semantics.Kinds.MeaningPreservation.shiftExists {World Atom : Type} (P : NMP.Property World Atom) (w : World) (predicate : NMP.Individual Atom → Prop) : Prop

∃-shift (existential closure): at world w, existentially closes over P(w). This is NMP.DPP restricted to a predicate.

@cite{moroney-2021} §2.3: the existential reading of Shan bare nouns arises via DPP at vP, yielding obligatory low scope w.r.t. negation.

Equations

• Semantics.Kinds.MeaningPreservation.shiftExists P w predicate = ∃ x ∈ P w, predicate x

theorem Semantics.Kinds.MeaningPreservation.rank_1_preferred_over_exists : meaningPreservationRank TypeShift.down < meaningPreservationRank TypeShift.exists ∧ meaningPreservationRank TypeShift.iota < meaningPreservationRank TypeShift.exists ∧ meaningPreservationRank TypeShift.iotaAnaphoric < meaningPreservationRank TypeShift.exists

∩ and ι are both rank-1 shifts (meaning-preserving). ∃ is rank-2 (meaning-losing). This is why Shan bare nouns default to definite/kind readings rather than existential — Meaning Preservation selects the highest-ranked available shift.

structure Semantics.Kinds.MeaningPreservation.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"?

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instReprKindReferenceParams : Repr KindReferenceParams

Equations

• Semantics.Kinds.MeaningPreservation.instReprKindReferenceParams = { reprPrec := Semantics.Kinds.MeaningPreservation.instReprKindReferenceParams.repr }

def Semantics.Kinds.MeaningPreservation.instReprKindReferenceParams.repr : KindReferenceParams → ℕ → Std.Format

Equations

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

def Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.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

• Semantics.Kinds.MeaningPreservation.germanKindRef = { hasDefiniteArticle := true, hasIndefiniteArticle := true, bareKindsOK := true, definiteSingularKinds := true, definitePluralKinds := true }

inductive Semantics.Kinds.MeaningPreservation.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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instDecidableEqPredicateType : DecidableEq PredicateType

Equations

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

@[implicit_reducible]

instance Semantics.Kinds.MeaningPreservation.instReprPredicateType : Repr PredicateType

Equations

• Semantics.Kinds.MeaningPreservation.instReprPredicateType = { reprPrec := Semantics.Kinds.MeaningPreservation.instReprPredicateType.repr }

def Semantics.Kinds.MeaningPreservation.instReprPredicateType.repr : PredicateType → ℕ → Std.Format

Equations

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

def Semantics.Kinds.MeaningPreservation.requiresDKP : PredicateType → Bool

Does this predicate require DKP when applied to a kind?

Equations

• Semantics.Kinds.MeaningPreservation.requiresDKP Semantics.Kinds.MeaningPreservation.PredicateType.kindLevel = false
• Semantics.Kinds.MeaningPreservation.requiresDKP Semantics.Kinds.MeaningPreservation.PredicateType.objectLevel = true

def Semantics.Kinds.MeaningPreservation.isKindLevelPredicate : String → Prop

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.Kinds.MeaningPreservation.isKindLevelPredicate "extinct" = True
• Semantics.Kinds.MeaningPreservation.isKindLevelPredicate "widespread" = True
• Semantics.Kinds.MeaningPreservation.isKindLevelPredicate "rare" = True
• Semantics.Kinds.MeaningPreservation.isKindLevelPredicate "common" = True
• Semantics.Kinds.MeaningPreservation.isKindLevelPredicate "evolve" = True
• Semantics.Kinds.MeaningPreservation.isKindLevelPredicate "originate" = True
• Semantics.Kinds.MeaningPreservation.isKindLevelPredicate "die_out" = True
• Semantics.Kinds.MeaningPreservation.isKindLevelPredicate "invented" = True
• Semantics.Kinds.MeaningPreservation.isKindLevelPredicate "discovered" = True
• Semantics.Kinds.MeaningPreservation.isKindLevelPredicate x✝ = False

def Semantics.Kinds.MeaningPreservation.isWellEstablishedKind : String → Prop

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.Kinds.MeaningPreservation.isWellEstablishedKind "lion" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "tiger" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "dog" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "cat" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "dodo" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "mammoth" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "dinosaur" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "computer" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "telephone" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "automobile" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "wheel" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind "printing_press" = True
• Semantics.Kinds.MeaningPreservation.isWellEstablishedKind x✝ = False

structure Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.modificationBlocksKind : ModificationEffect

Equations

• Semantics.Kinds.MeaningPreservation.modificationBlocksKind = { base := "lion", modifier := "tall" }

theorem Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.down_preferred_over_exists : morePreferred TypeShift.down TypeShift.exists = true

∩, ι, and ι^x are always preferred over ∃

theorem Semantics.Kinds.MeaningPreservation.iota_preferred_over_exists : morePreferred TypeShift.iota TypeShift.exists = true

theorem Semantics.Kinds.MeaningPreservation.iotaAnaphoric_preferred_over_exists : morePreferred TypeShift.iotaAnaphoric TypeShift.exists = true

theorem Semantics.Kinds.MeaningPreservation.iota_iotaAnaphoric_equal : equallyPreferred TypeShift.iota TypeShift.iotaAnaphoric = true

ι and ι^x are equally preferred (both rank 1).

theorem Semantics.Kinds.MeaningPreservation.english_bare_plural_uses_down : have ctx := { number := NumberFeature.pl, downDefined := true, iotaBlocked := true, iotaAnaphoricBlocked := true, existsBlocked := true, instantiationAccessible := true }; selectShift ctx = some TypeShift.down

English bare plurals use ∩ (most preferred available shift)

theorem Semantics.Kinds.MeaningPreservation.english_singular_kind_uses_iota : have ctx := { number := NumberFeature.sg, downDefined := false, iotaBlocked := false, iotaAnaphoricBlocked := true, existsBlocked := true, instantiationAccessible := false }; selectShift ctx = some TypeShift.iota

English singular kinds use ι

def Semantics.Kinds.MeaningPreservation.chierchiaToContext (bp : NMP.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.Kinds.MeaningPreservation.englishBlocking : NMP.BlockingPrinciple

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

Equations

• Semantics.Kinds.MeaningPreservation.englishBlocking = { determiners := ["the", "a", "some"], iotaBlocked := true, existsBlocked := true, downBlocked := false }

theorem Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.dayal_subsumes_chierchia_singular_blocked : have ctx := chierchiaToContext englishBlocking MassCount.count false; (selectShift ctx).isSome = false

def Semantics.Kinds.MeaningPreservation.romanceBlocking : NMP.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.Kinds.MeaningPreservation.romanceBlocking = { determiners := ["le", "la", "les", "un", "une", "des"], iotaBlocked := true, existsBlocked := true, downBlocked := false }

theorem Semantics.Kinds.MeaningPreservation.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.Kinds.MeaningPreservation.meaning_preservation_derives_kind_preference : have ctx := { number := NumberFeature.pl, downDefined := true, iotaBlocked := true, iotaAnaphoricBlocked := 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/NMP.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