Documentation

def Semantics.Lexical.Noun.Kind.Chierchia1998.Individual.atom {Atom : Type} (a : Atom) :

Individual Atom

Construct a singular individual from an atom.

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.Individual.atom a = {a}

Instances For

@[reducible, inline]

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

A property (intension): function from worlds to sets of individuals. This is Core.Intension World (Set (Individual Atom)).

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.Property World Atom = Core.Intension World (Set (Semantics.Lexical.Noun.Kind.Chierchia1998.Individual Atom))

Instances For

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Chierchia1998.IndividualConcept (World Atom : Type) :

An individual concept: function from worlds to individuals. This is Core.Intension World (Individual Atom).

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.IndividualConcept World Atom = Core.Intension World (Semantics.Lexical.Noun.Kind.Chierchia1998.Individual Atom)

Instances For

structure Semantics.Lexical.Noun.Kind.Chierchia1998.Kind (World Atom : Type) :

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

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.down (World Atom : Type) (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.Lexical.Noun.Kind.Chierchia1998.down World Atom P = { concept := fun (w : World) => {a : Atom | Semantics.Lexical.Noun.Kind.Chierchia1998.Individual.atom a ∈ P w} }

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.up (World Atom : Type) (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.Lexical.Noun.Kind.Chierchia1998.up World Atom k w = {x : Semantics.Lexical.Noun.Kind.Chierchia1998.Individual Atom | x ⊆ k.concept w}

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.IsMass (World Atom : Type) (P : Property World Atom) :

A property is mass iff its extension at every world is determined by atomic content: x ∈ P w ↔ ∀ a ∈ x, {a} ∈ P w (@cite{chierchia-1998} §2.2).

This implies both cumulative reference (CUM) and divisive reference (DIV): mass extensions are closed under union and subset.

Equations

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

Instances For

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.isMass_div {World Atom : Type} (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.Lexical.Noun.Kind.Chierchia1998.isMass_cum {World Atom : Type} (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.Lexical.Noun.Kind.Chierchia1998.pluralClosure (World Atom : Type) (P : Property World Atom) :

Property World Atom

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

This is @cite{link-1983}'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.Lexical.Noun.Kind.Chierchia1998.pluralClosure World Atom P w = Mereology.AlgClosure (P w)

Instances For

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.pluralClosure_mass {World Atom : Type} (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. This is Krifka's absorption rule ⊔⊔S = ⊔S from @cite{krifka-2026} (16).

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.subset_pluralClosure {World Atom : Type} (P : Property World Atom) (w : World) :

P w ⊆ pluralClosure World Atom P w

A property is contained in its plural closure.

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.pluralClosure_cum {World Atom : Type} (P : Property World Atom) (w : World) :

Mereology.CUM (pluralClosure World Atom P w)

Plural closure is always cumulative.

def Semantics.Lexical.Noun.Kind.Chierchia1998.kindAnaphorMass (World Atom : Type) (P : Property World Atom) :

Kind World Atom

Kind anaphor for [MASS] concepts: ⟦it⟧ = λP[MASS]. λi. ∩P(i).

Mass nouns are already cumulative, so ∩ applies directly without plural closure. The singular pronoun it picks up a mass concept dref and derives the corresponding kind individual.

Example: John noticed mold. He is allergic against it. ⟦it⟧(⟦mold⟧) = ∩⟦mold⟧ = the mold-kind

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.kindAnaphorMass World Atom P = Semantics.Lexical.Noun.Kind.Chierchia1998.down World Atom P

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.kindAnaphorCount (World Atom : Type) (P : Property World Atom) :

Kind World Atom

Kind anaphor for [COUNT] concepts: ⟦they⟧ = λP[COUNT]. λi. ∩(⊔P)(i).

Count nouns need plural closure (⊔) before nominalization (∩). The plural pronoun they picks up a count concept dref, applies plural closure to get a cumulative predicate, then derives the kind individual via ∩.

Example: John noticed a spider. He has a phobia against them. ⟦they⟧(⟦spider⟧) = ∩(⊔⟦spider⟧) = ∩⟦spiders⟧ = the spider-kind

Equations

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

Instances For

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.kindAnaphorCount_mass (World Atom : Type) (P : Property World Atom) (hMass : IsMass World Atom P) :

kindAnaphorCount World Atom P = kindAnaphorMass World Atom P

For mass nouns, the two anaphors yield the same kind (up to absorption). This is why it and they are interchangeable for mass concepts — except that the morphosyntactic [MASS] feature blocks they.

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.up_down_id (World Atom : Type) (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.Lexical.Noun.Kind.Chierchia1998.down_up_id (World Atom : Type) (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.Lexical.Noun.Kind.Chierchia1998.DKP (World Atom : Type) (P : Individual Atom → Bool) (k : Kind World Atom) (w : World) :

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.Lexical.Noun.Kind.Chierchia1998.DKP World Atom P k w = ∃ x ∈ Semantics.Lexical.Noun.Kind.Chierchia1998.up World Atom k w, P x = true

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.liftToKind (World Atom : Type) (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.Lexical.Noun.Kind.Chierchia1998.liftToKind World Atom P k w = Semantics.Lexical.Noun.Kind.Chierchia1998.DKP World Atom P k w

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.DPP (Atom : Type) (property predicate : Individual Atom → Bool) :

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. @cite{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.Lexical.Noun.Kind.Chierchia1998.DPP Atom property predicate = ∃ (x : Semantics.Lexical.Noun.Kind.Chierchia1998.Individual Atom), property x = true ∧ predicate x = true

Instances For

inductive Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping :

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

Instances For

DecidableEq NominalMapping

instance Semantics.Lexical.Noun.Kind.Chierchia1998.instDecidableEqNominalMapping :

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.instDecidableEqNominalMapping x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Lexical.Noun.Kind.Chierchia1998.instReprNominalMapping :

Repr NominalMapping

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.instReprNominalMapping = { reprPrec := Semantics.Lexical.Noun.Kind.Chierchia1998.instReprNominalMapping.repr }

def Semantics.Lexical.Noun.Kind.Chierchia1998.instReprNominalMapping.repr :

NominalMapping → ℕ → Std.Format

Equations

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

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.languageFamily :

NominalMapping → String

Language family classification

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.languageFamily Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.argOnly = "Chinese, Japanese (classifier languages)"
Semantics.Lexical.Noun.Kind.Chierchia1998.languageFamily Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.argAndPred = "English, German, Slavic (bare argument languages)"
Semantics.Lexical.Noun.Kind.Chierchia1998.languageFamily Semantics.Lexical.Noun.Kind.Chierchia1998.NominalMapping.predOnly = "French, Italian, Spanish (Romance languages)"

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.canDenoteKind (mapping : NominalMapping) (hasD : Bool) :

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

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.canDenoteProperty (mapping : NominalMapping) :

Whether a nominal can denote a property, given the mapping parameter.

Equations

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.pluralize {Atom : Type} (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.Lexical.Noun.Kind.Chierchia1998.pluralize F = {s : Semantics.Lexical.Noun.Kind.Chierchia1998.Individual Atom | Set.Nonempty s ∧ s ⊆ F}

Instances For

structure Semantics.Lexical.Noun.Kind.Chierchia1998.BlockingPrinciple :

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

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.bareArgumentLicensed (bp : BlockingPrinciple) (nounType : MassCount) :

Bare argument is licensed iff the required type shift is not blocked

Equations

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.downDefinedFor (nounType : MassCount) (isPlural : 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.Lexical.Noun.Kind.Chierchia1998.downDefinedFor MassCount.mass isPlural = true
Semantics.Lexical.Noun.Kind.Chierchia1998.downDefinedFor MassCount.count isPlural = isPlural

Instances For

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.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.

def Semantics.Lexical.Noun.Kind.Chierchia1998.dkpIsLocal :

Bare plurals are scopeless because DKP introduces a LOCAL existential.

The existential reading from DKP cannot scope out because the coercion applies inside the predicate abstract.

See Phenomena/Generics/KindReference.lean for empirical scope data.

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.dkpIsLocal = true

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.fallbackToExists (isKindDenoting : Bool) (bp : BlockingPrinciple) :

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.Lexical.Noun.Kind.Chierchia1998.fallbackToExists isKindDenoting bp = decide ((!isKindDenoting) = true ∧ (!bp.existsBlocked) = true)

Instances For

Computational DKP #

@cite{krifka-2004} @cite{chierchia-1998}

Simplified, decidable formalization of Chierchia's DKP for concrete scrambling comparisons with @cite{krifka-2004}. Uses List Entity and Bool (rather than Set Atom and Prop) so that examples reduce by rfl.

The parallel Krifka machinery is in Krifka2004.lean; both are instantiated side-by-side in Phenomena/Generics/Compare.lean.

See Theories/Comparisons/KindReference.lean for the formal comparison.

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Chierchia1998.KindExtension (Entity World : Type) :

A kind's extension at each world (the instances)

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.KindExtension Entity World = (World → List Entity)

Instances For

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Chierchia1998.ChierchiaVP (Entity World : Type) :

A VP meaning (intensional)

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.ChierchiaVP Entity World = (Entity → World → Bool)

Instances For

@[reducible, inline]

abbrev Semantics.Lexical.Noun.Kind.Chierchia1998.ChierchiaSent (World : Type) :

A sentence meaning (proposition)

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.ChierchiaSent World = (World → Bool)

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.dkpApply {Entity World : Type} (kind : KindExtension Entity World) (vp : ChierchiaVP Entity World) :

ChierchiaSent World

DKP (Derived Kind Predication): Coerce a kind to work with object-level predicates.

Given a kind (represented by its extension at each world) and an object-level VP, DKP introduces existential quantification:

DKP(VP)(k) = λw. ∃x ∈ k(w). VP(x)(w)

Property: The ∃ is introduced HERE, at the point of composition, not at a syntactic position. This makes DKP position-invariant.

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.dkpApply kind vp w = (kind w).any fun (x : Entity) => vp x w

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.chierchiaDerivUnscrambled {Entity World : Type} (kind : KindExtension Entity World) (vp : ChierchiaVP Entity World) :

ChierchiaSent World

Chierchia's derivation for "[niet [BP V]]" (unscrambled).

BP = kind k
VP = λx.V(x)
DKP: ∃x[k(x) ∧ V(x)]
Negation: ¬∃x[k(x) ∧ V(x)]

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.chierchiaDerivUnscrambled kind vp w = !Semantics.Lexical.Noun.Kind.Chierchia1998.dkpApply kind vp w

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.chierchiaDerivScrambled {Entity World : Type} (kind : KindExtension Entity World) (vp : ChierchiaVP Entity World) :

ChierchiaSent World

Chierchia's derivation for "[BP [niet V]]" (scrambled).

In Chierchia's system, scrambling doesn't change the derivation. DKP still applies when the kind meets the predicate, and the ∃ is introduced at that point (the trace position in LF).

Result: Same as unscrambled — ¬∃x[k(x) ∧ V(x)]

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.chierchiaDerivScrambled kind vp w = !Semantics.Lexical.Noun.Kind.Chierchia1998.dkpApply kind vp w

Instances For

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.chierchia_position_invariant {Entity World : Type} (kind : KindExtension Entity World) (vp : ChierchiaVP Entity World) :

chierchiaDerivScrambled kind vp = chierchiaDerivUnscrambled kind vp

Chierchia's DKP is position-invariant.

Scrambled and unscrambled derivations yield the same meaning. This is the source of Chierchia's incorrect prediction for Dutch scrambling.

Theories/Semantics/Lexical/Noun/Kind/Krifka2004.lean - Alternative: Bare NPs as properties
Theories/Semantics/Lexical/Noun/Kind/Dayal2004.lean - Meaning Preservation, singular kinds
Theories/Semantics/Lexical/Noun/Kind/Generics.lean - GEN operator for generic readings

Empirical Data #

For empirical patterns (cross-linguistic data, scope judgments, predicate class effects), see:

Phenomena/Generics/KindReference.lean - unified kind reference phenomena
Phenomena/Generics/BarePlurals.lean - generic vs existential readings
Phenomena/Generics/Data.lean - generic sentence patterns

structure Semantics.Lexical.Noun.Kind.Chierchia1998.KindFormation (Atom : Type) :

An equivalence relation on atoms partitions them into subkinds.

rel : Atom → Atom → Prop
The salient equivalence relation
isEquiv : Equivalence self.rel
Must be an equivalence

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.isSubkindOf {Atom : Type} (k₁ k₂ : Set Atom) :

Subkind relation: k₁ is a subkind of k₂ iff every entity instantiating k₁ also instantiates k₂.

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.isSubkindOf k₁ k₂ = (k₁ ⊆ k₂)

Instances For

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.disjointness_condition {Atom : Type} [DecidableEq Atom] (kf : KindFormation Atom) (a b : Atom) (h : ¬kf.rel a b) :

Disjoint {x : Atom | kf.rel a x} {x : Atom | kf.rel b x}

@cite{carlson-1977}'s Disjointness Condition: subkinds induced by an equivalence relation are pairwise disjoint in any context.

inductive Semantics.Lexical.Noun.Kind.Chierchia1998.MathSystem :

Mathematical number system taxonomy: NUMBER has subkinds ℕ, ℤ, ℚ, ℝ, etc. TWO has subkinds 2_ℕ, 2_ℤ, 2_ℚ, 2_ℝ (Snyder §4.3).

Named MathSystem to avoid confusion with grammatical number (UD.Number, Word.Number).

nat : MathSystem
int : MathSystem
rat : MathSystem
real : MathSystem

Instances For

instance Semantics.Lexical.Noun.Kind.Chierchia1998.instDecidableEqMathSystem :

DecidableEq MathSystem

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.instDecidableEqMathSystem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Lexical.Noun.Kind.Chierchia1998.instBEqMathSystem :

BEq MathSystem

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.instBEqMathSystem = { beq := Semantics.Lexical.Noun.Kind.Chierchia1998.instBEqMathSystem.beq }

def Semantics.Lexical.Noun.Kind.Chierchia1998.instBEqMathSystem.beq :

MathSystem → MathSystem → Bool

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.instBEqMathSystem.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.instReprMathSystem.repr :

MathSystem → ℕ → Std.Format

Equations

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

Instances For

instance Semantics.Lexical.Noun.Kind.Chierchia1998.instReprMathSystem :

Repr MathSystem

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.instReprMathSystem = { reprPrec := Semantics.Lexical.Noun.Kind.Chierchia1998.instReprMathSystem.repr }

instance Semantics.Lexical.Noun.Kind.Chierchia1998.instFintypeMathSystem :

Fintype MathSystem

Equations

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

def Semantics.Lexical.Noun.Kind.Chierchia1998.twoSubkinds :

MathSystem → MathSystem → Prop

Two twos from different systems are distinct subkinds of TWO.

Equations

Semantics.Lexical.Noun.Kind.Chierchia1998.twoSubkinds x1✝ x2✝ = (x1✝ ≠ x2✝)

Instances For

def Semantics.Lexical.Noun.Kind.Chierchia1998.MathSystem.all :

List MathSystem

The four mathematical number systems.

Equations

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

Instances For

theorem Semantics.Lexical.Noun.Kind.Chierchia1998.mathSystem_count :

MathSystem.all.length = 4

NUMBER has four subkinds (ℕ, ℤ, ℚ, ℝ). This is what makes taxonomic predication ("two comes in several varieties") felicitous: the kind TWO has genuinely distinct subkinds.