Reference to ad hoc kinds

@cite{mendia-2020}

@cite{mendia-2020} (L&P 43:589-631) argues that ad hoc kind reference — uses of that kind of dog to refer to a kind no lexicalized noun names — is best analysed by giving speakers the ability to choose, in context, an equivalence relation on the instances of a base kind. Members of each equivalence class then instantiate a subkind, and that kind of N picks out one such class via demonstration.

Subkinds-as-equivalence-classes is exactly mathlib's Setoid. This file provides Mendia's linguistic vocabulary (subkindOf, instantiates, disjointness_condition) on top of Setoid directly — no parallel struct is introduced. @cite{carlson-1977}'s Disjointness Condition is then a corollary of the standard fact that distinct equivalence classes are disjoint.

Consumers:

• Phenomena/Numerals/Studies/Snyder2026.lean — instantiates the framework for the kind TWO with subkinds 2_ℕ, 2_ℤ, 2_ℚ, 2_ℝ (Snyder §4.3, §5).
• Theories/Semantics/Kinds/MeaningPreservation.lean — singular kinds satisfy the framework with the discrete partition (one-class-per-kind).
• Future: Phenomena/Generics/KindReference.lean for ad hoc kind picking via that kind of N.

def Semantics.Kinds.Subkinds.subkindOf {Atom : Type u_1} (s : Setoid Atom) (a : Atom) : Set Atom

The subkind containing a under the salient kind-formation s: its equivalence class.

@cite{mendia-2020}: "For any entities instantiating a kind k, we can exhaustively partition those entities into disjoint subsets via a salient equivalence relation, where members of the resulting equivalence classes instantiate subkinds of k."

Equations

• Semantics.Kinds.Subkinds.subkindOf s a = {x : Atom | s a x}

def Semantics.Kinds.Subkinds.instantiates {Atom : Type u_1} (s : Setoid Atom) (a x : Atom) : Prop

An entity instantiates a subkind iff it belongs to that equivalence class.

Equations

• Semantics.Kinds.Subkinds.instantiates s a x = (x ∈ Semantics.Kinds.Subkinds.subkindOf s a)

theorem Semantics.Kinds.Subkinds.disjointness_condition {Atom : Type u_1} (s : Setoid Atom) {a b : Atom} (h : ¬s a b) : Disjoint (subkindOf s a) (subkindOf s b)

@cite{carlson-1977}'s Disjointness Condition, derived from the equivalence-class structure. Distinct classes of any equivalence relation are disjoint as subsets of the carrier.

theorem Semantics.Kinds.Subkinds.subkindOf_eq_iff {Atom : Type u_1} (s : Setoid Atom) (a b : Atom) : subkindOf s a = subkindOf s b ↔ s a b

Two atoms instantiate the same subkind iff they are equivalent under the salient relation.

theorem Semantics.Kinds.Subkinds.subkindOf_ne {Atom : Type u_1} (s : Setoid Atom) {a b : Atom} (h : ¬s a b) : subkindOf s a ≠ subkindOf s b

Distinct subkinds (under the salient relation) are unequal as sets.

theorem Semantics.Kinds.Subkinds.mem_subkindOf {Atom : Type u_1} (s : Setoid Atom) {a x : Atom} : x ∈ subkindOf s a ↔ s a x

Membership in a subkind via the salient relation.