Numbers as kinds: Polymorphic Contextualism #

@cite{snyder-2026}

@cite{snyder-2026} (L&P 49:57-100) argues that the lexical meaning of two is an atomic predicate λxα. two(x) that applies to different countable entities (numeral tokens, kinds, subkinds of TWO) in different contexts; all other meanings derive via Partee type-shifting. This generalises and strictly subsumes two earlier analyses Snyder labels:

Polymorphic Substantivalism: lexical [[two]] = 2 is a numeral (entity of type e); cardinal predicates derive via CARD; all else via type-shifting. (@cite{landman-2004}; @cite{scontras-2014}; @cite{snyder-2017}.)
Polymorphic Adjectivalism: lexical [[two]] = λx. μ#(x) = 2 is a cardinality predicate; numerals derive via NOM + Rothstein's Schematic Equation. (@cite{partee-1987}; @cite{geurts-2006}; @cite{rothstein-2013}; @cite{rothstein-2017}; @cite{kennedy-2015}; @cite{bylinina-nouwen-2020}.)
Polymorphic Contextualism (@cite{snyder-2026}): lexical [[two]] = λxα. two(x) is an atomic predicate over relativized atoms; all meanings derive via type-shifting (CARD/PM/A/NOM/IOTA), including taxonomic, kind-, and token-referential uses the first two analyses miss.

The diagram from §5 (76a-j):

                     CARD            PM
   (76g),(76i),(76e) ───→ (76a) ───→ (76b)
         ↑ IOTA            │           │
         │                NOM          A
         │                 ↓           ↓
    λxα. two(x)         (76d)      (76c)
         ↓ PM + IOTA
   (76h),(76j),(76f) — close appositives

Architecture #

Theories/Semantics/Kinds/Subkinds.lean — substrate: kind formation by salient equivalence relation (= mathlib's Setoid); Carlson's Disjointness Condition. Snyder's account of why TWO has disjoint subkinds 2_ℕ, 2_ℤ, 2_ℚ, 2_ℝ (§4.3, §5) instantiates the Mendia framework via the local kfTWO : Setoid TwoToken partition (defined below).
This file additionally implements Snyder's §6-§7 colour-word extension via a second local Mendia partition kfRed : Setoid ColorToken, consuming the Dutch adjective Fragment for colour roots.
Phenomena/Morphology/Studies/McNallyDeSwart2011.lean is a sibling Mendia consumer, with kfShade : Setoid Shade partitioning Dutch colour and taste shades by adjective root. Together with the two partitions in this file, the Mendia substrate now has three consumers (numerals + Snyder colours + M&deS colours/tastes), genuinely cross-domain. All four partitions follow the project-wide kf{Carrier} naming convention.

The two colour analyses (Snyder §6 here vs M&deS over there) are competing — they consume the same Mendia substrate (subkindOf) and agree on iota for definites, but disagree on lexical-projection architecture (Snyder: unitary λxα. red(x) over relativized atoms; M&deS: distinct rood_N vs rood_A projected from a shared root) and on nominalisation operator (Snyder: Partee NOM as typed shifter; M&deS: Chierchia ∩ carried by het). Having both formalised makes the divergence load-bearing instead of docstring-only.

This file:

Models the three analyses' lexical types and the nine semantic functions' target types as a small inductive SemTy (e, et, ett).
Gives each Partee/Snyder operator a typed signature; a derivation path is well-typed iff its operator chain composes from lexical type to target type. Coverage theorems then witness type-checking results, not just table lookup.
Instantiates the Mendia framework over a TwoToken carrier with multiple tokens per number system, so disjointness_condition does real work in the Identification-Problem theorem.
Uses a real Sharvy iota for close appositives — the (16b) [[the N₁ N₂]] = ιx[N₁(x) ∧ N₂(x)] clause carries a uniqueness presupposition, modelled as a partial Option-valued operation.

The Identification Problem (@cite{benacerraf-1965}; @cite{snyder-2026} §3.1, §5.2; @cite{snyder-2025}) is dissolved by derivation from the substrate: distinct equivalence classes of TWO under the salient partition are disjoint, so close-appositive iota over modifier-restricted subkinds yields distinct referents whenever the uniqueness presupposition is satisfied. Cf. @cite{moltmann-2013}, @cite{hofweber-2005}, @cite{rieppel-2021} for rival treatments of close-appositive coreference, and @cite{anderson-morzycki-2015} for the Degrees-as-Kinds view Snyder adopts in §5.3.

Semantic types #

A small fragment of the Heim & Kratzer / Partee type system, sufficient to carry the Snyder paths. PM is treated monadically (et → et) — the implicit second predicate is supplied at the syntax level.

Numbers as kinds: Polymorphic Contextualism #

Architecture #

Semantic types #

§2-3, §5: the three polymorphic analyses #

§1, §5: nine semantic functions #

§5: Partee/Snyder operators with type signatures #

§2, §5: derivation maps for the three analyses #

Type-soundness of the derivation paths #

Coverage theorems #

§4.3, §5: numbers as kinds — the TWO taxonomy #

Sharvy iota at the Set level #

§5.2: the Identification Problem dissolved #

§1, §3.1, §3.4: empirical examples #

Cross-framework hooks #

§6-§7: Polymorphic Contextualism for colour terms #

§6 colour-Polymorphic-Contextualism theorems #

§6 empirical examples (94)-(98) #