Inflection and Derivation: How Adjectives and Nouns Refer to Abstract Objects

@cite{mcnally-deswart-2011}

@cite{mcnally-deswart-2011} (Proceedings of the 18th Amsterdam Colloquium, 425-434) analyses three morphologically distinct ways Dutch refers to abstract objects (colors, tastes, properties), illustrated with the colour rood 'red':

Form	Example	Semantic type
Uninflected nominal	het rood (van de aardbeien)	kind / set of subkinds
Derived -heid	de roodheid (van de huid)	kind / set of subkinds (of property correlate)
Inflected -e + het	het rode van de aardbeien	trope (entity correlate of relational property)

The paper's central morphosyntactic claim is that Dutch het is polysemous: with neuter nouns it denotes the iota operator, but when embedding an inflected adjective in a DP it denotes @cite{chierchia-1984}'s ∩ nominalization operator. The inflectional suffix -e is not a category-changing nominalizer; rather it is a valence-increasing operator that turns the adjective into a relation Pasp(y)(x) between an object y (saturated by the PP complement) and the P aspect x of that object.

The key empirical contrasts (paper §2.3):

• The inflected form admits adverbial but not adjectival modification (13) — evidence it remains adjectival, not nominal.
• The inflected form does not tolerate determiners other than het (14).
• The inflected form does not occur generically (15).
• The derived -heid form admits all determiners and pluralizes (9, 11).
• The uninflected form behaves as a regular neuter mass noun (6-8).

Substrate reuse

• Lexical data: Fragments/Dutch/Adjectives.lean provides the consensus Dutch adjective lexicon — the three morphological forms (uninflected, inflected with -e, derived nominalisation in -heid), gender-driven alternation, and the exception class (forms in /ə/, -a, -en). The formalisation here derives its colour and taste roots from that Fragment rather than enumerating them inline.
• Kind/subkind ontology: @cite{zamparelli-1995}'s layered DP plus @cite{carlson-1977} kinds. The subkind relation is exactly what Theories/Semantics/Kinds/Subkinds.lean provides: a salient equivalence relation on shade-atoms partitions them into colour subkinds, and McNally & de Swart's subkind(xk, red) is precisely Subkinds.subkindOf kfShade (canonicalShade rood). Carlson's Disjointness Condition follows.

This file is the second consumer of Subkinds.subkindOf, alongside Phenomena/Numerals/Studies/Snyder2026.lean. Together they witness that the Mendia substrate is genuinely cross-domain (numerals + colours), not paper-specific scaffolding for one analysis.

Cross-references

• Phenomena/Morphology/CategoryChanging.lean (RootFamily) formalises the @cite{marantz-1997} uncategorised-roots pattern that @cite{mcnally-deswart-2011} §3.1 explicitly invokes: [[rood]] = red is an entity-denoting root that both the noun rood_N and the adjective rood_A project from. The Dutch Fragment's AdjEntry plays the role of RootFamily for the colour and taste sub-paradigms; the connection is documented but not yet bridged formally (a AdjEntry → RootFamily adapter is plausible future work).
• Phenomena/Morphology/Studies/Panagiotidis2015.lean engages this file via a diagnostic-alignment bridge in its own §6 (namespace MdSBridge): Panagiotidis's §6.7.1 modifier-distribution diagnostic for SWITCH placement (geometric reasoning: SWITCH-dominated constituent projects nominally, takes adjectival mod; non-dominated constituent stays verbal/adjectival, takes adverbial mod) is shown to make the same predictions on each InflectedAnalysis rival as the M&deS-side PredictsAdverbialModOnly. Both diagnostics are inherited from Ackema & Neeleman 2004 (Beyond Morphology); the alignment is shared- source consequence rather than independent rediscovery. The bridge jointly motivates rejecting the nominalisation rival and supporting the adopted hetAsCap analysis.

Cross-framework note

@cite{snyder-2026} §6-7 conjectures that colour terms admit the same Polymorphic-Contextualism analysis as numerals: [[red]] = λxα. red(x), all forms via type-shifting. McNally & de Swart 2011 takes a different route — they distinguish category-projections of the root (rood_N vs rood_A) at the syntactic level, and use Chierchia ∩ for nominalisation rather than pure Partee shifters. The two analyses agree on the kind- formation substrate (both are Zamparelli/Carlson/Mendia subkind structure) and on iota for definites; they disagree on whether nominalisation is ∩ (this paper) or NOM-as-Partee-shifter (Snyder Polymorphic Contextualism). This is a genuine theoretical incompatibility surfaced by sharing substrate.

§3.1: Uncategorised roots and the Dutch lexicon

@cite{mcnally-deswart-2011} (18) posits entity-denoting roots: [[rood]] = red, [[zuur]] = acid. Both nominal and adjectival uses project from the same root. The roots themselves are the consensus Dutch lexical entries in Fragments/Dutch/Adjectives.lean; this file uses those entries as the carrier identifying each colour or taste subkind.

The @cite{marantz-1997} uncategorised-roots framework — formalised in Phenomena/Morphology/CategoryChanging.lean as RootFamily — is the substrate for the same idea. Each Dutch AdjEntry projects to a RootFamily whose forms list records the three category-stamped surface forms (uninflected adjective, inflected adjective per M&deS §3.4, derived noun in -heid). The adapter AdjEntry.toRootFamily below makes the connection code-level, not just docstring.

def Fragments.Dutch.Adjectives.AdjEntry.toRootFamily (a : AdjEntry) : Phenomena.Morphology.CategoryChanging.RootFamily

Lift a Dutch AdjEntry into a @cite{marantz-1997}-style RootFamily (Phenomena/Morphology/CategoryChanging.lean). The uninflected and inflected forms are both adjectival per @cite{mcnally-deswart-2011} §2.3, §3.4 (the inflected form remains adjectival under the het-as-∩ analysis); the -heid derivative is a noun. Forms absent from the entry (no inflected variant for the schwa-, -a-, -en- final exception class; no -heid for the same) are omitted from the forms list. This adapter exercises the previously unread .form and .formInfl Fragment fields. Defined in the Fragment's namespace so dot notation a.toRootFamily works.

Equations

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

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.toRootFamily_includes_uninflected (a : Fragments.Dutch.Adjectives.AdjEntry) : (a.form, CategoryChanging.LexCat.adjective) ∈ a.toRootFamily.forms

Adjectives spanning category projections always include the uninflected adjectival form.

§3.1, §3.2: Shades, colour partition, and Mendia substrate

@cite{mcnally-deswart-2011} follows @cite{zamparelli-1995}'s layered DP: the noun rood_N denotes the set of subkinds (shades) of the colour red. The subkind relation is @cite{mendia-2020}'s kind-formation framework — partition the domain of shade-atoms by the salient equivalence relation belongs to the same colour root.

structure Phenomena.Morphology.Studies.McNallyDeSwart2011.Shade : Type

A shade-atom: an adjective entry from the Dutch Fragment paired with a distinguishing index. The pair lets multiple shade-tokens belong to the same colour subkind (e.g., crimson and scarlet both belong to rood), so the @cite{mendia-2020} partition is exercised non-trivially.

• root : Fragments.Dutch.Adjectives.AdjEntry

  The adjective entry classifying this shade — drawn from the Dutch Fragment (e.g., Fragments.Dutch.Adjectives.rood).

• idx : ℕ

  Distinguishing index for multiple shade-tokens of the same root.

def Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqShade.decEq (x✝ x✝¹ : Shade) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqShade : DecidableEq Shade

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqShade = Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqShade.decEq

def Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprShade.repr : Shade → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprShade : Repr Shade

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprShade = { reprPrec := Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprShade.repr }

def Phenomena.Morphology.Studies.McNallyDeSwart2011.kfShade : Setoid Shade

The salient @cite{mendia-2020} kind-formation for shades: partitioned by their adjective-entry root. Each equivalence class is a subkind (set of shade-tokens for one Dutch adjective entry). The same setoid works for both colours and tastes — only the chosen entries differ.

Equations

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

def Phenomena.Morphology.Studies.McNallyDeSwart2011.canonicalShade (a : Fragments.Dutch.Adjectives.AdjEntry) : Shade

Canonical witness shade for an adjective entry.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.canonicalShade a = { root := a, idx := 0 }

def Phenomena.Morphology.Studies.McNallyDeSwart2011.uninflectedNominal (a : Fragments.Dutch.Adjectives.AdjEntry) : Set Shade

@cite{mcnally-deswart-2011} (19): the uninflected nominal rood_N denotes the set of subkinds (shades) of the colour red. Implemented as Subkinds.subkindOf kfShade (canonicalShade rood) — the equivalence class of any canonical witness. The Dutch Fragment entry Fragments.Dutch.Adjectives.rood is the actual lexical anchor.

Equations

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

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.uninflectedNominal_iff (a : Fragments.Dutch.Adjectives.AdjEntry) (s : Shade) : s ∈ uninflectedNominal a ↔ s.root = a

The uninflected nominal of a is exactly the set of shades whose root is a.

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.uninflectedNominal_disjoint {a₁ a₂ : Fragments.Dutch.Adjectives.AdjEntry} (h : a₁ ≠ a₂) : Disjoint (uninflectedNominal a₁) (uninflectedNominal a₂)

Distinct adjective entries project to disjoint uninflected nominals — a direct consequence of @cite{carlson-1977}'s Disjointness Condition derived from the Mendia partition.

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.rood_disjoint_from_wit : Disjoint (uninflectedNominal Fragments.Dutch.Adjectives.rood) (uninflectedNominal Fragments.Dutch.Adjectives.wit)

Concrete witness: rood and wit denote disjoint subkinds. The Dutch Fragment entries are non-equal as AdjEntry records, so the Mendia Disjointness Condition gives disjoint shade-sets directly.

§3.2: PP modification and het as iota (uninflected case)

@cite{mcnally-deswart-2011} (20): the PP van de aardbeien introduces a contextual relation R_i(x_k, s) where s is the PP-complement entity. Combined via predicate-modification with the noun's set of subkinds, then selected by het as iota, it picks out the unique strawberry-related shade of red.

def Phenomena.Morphology.Studies.McNallyDeSwart2011.ppModifier {Entity : Type u_1} (R : Shade → Entity → Prop) (s : Entity) (P : Set Shade) : Set Shade

@cite{mcnally-deswart-2011} (20): a PP modifier introduces a contextual relation between subkinds and the PP-complement entity. Modelled here as a predicate-restriction on shades.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.ppModifier R s P = {x : Phenomena.Morphology.Studies.McNallyDeSwart2011.Shade | x ∈ P ∧ R x s}

def Phenomena.Morphology.Studies.McNallyDeSwart2011.uninflectedNominalWithPP {Entity : Type u_1} (a : Fragments.Dutch.Adjectives.AdjEntry) (R : Shade → Entity → Prop) (s : Entity) : Set Shade

@cite{mcnally-deswart-2011} (21a): rood van de aardbeien denotes the set of red-shades that stand in R_i to the strawberries.

Equations

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

§3.3: Derived -heid form

@cite{mcnally-deswart-2011} (24a-c): the derivational suffix -heid operates on a property P (the adjective's denotation) and returns the set of subkinds of its entity correlate (Chierchia ∩P). Modelled here at the kind-of-subkinds layer.

def Phenomena.Morphology.Studies.McNallyDeSwart2011.adjectivalProperty (a : Fragments.Dutch.Adjectives.AdjEntry) : Shade → Prop

The adjectival denotation of a Dutch adjective entry, abbreviated as [[rood_A]] = λy. Red(y) per @cite{mcnally-deswart-2011} (23c). The paper distinguishes a gradable measure-function reading (23a, after @cite{kennedy-mcnally-2010}) from a non-gradable proxy reading (23b); we abbreviate as the paper does, and identify each adjective with its Dutch Fragment entry.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.adjectivalProperty a s = (s.root = a)

def Phenomena.Morphology.Studies.McNallyDeSwart2011.derivedNominal (a : Fragments.Dutch.Adjectives.AdjEntry) : Option (Set Shade)

@cite{mcnally-deswart-2011} (24b): roodheid_N denotes the set of subkinds of the entity correlate (Chierchia ∩) of the property λy. Red(y). The substantive Chierchia ∩ operator lives in Theories/Semantics/Kinds/NMP.lean (down/up for intensional kinds) and Theories/Semantics/Composition/TypeShifting.lean (NOM extensional counterpart, with NOM = iota in the finite setting); we do not call them here because the extensional collapse means the only Fragment-visible distinction is whether the adjective has a -heid form at all.

The construction is partial: when a lacks a -heid form (e.g., roze, mauve per @cite{mcnally-deswart-2011} §1), the derived nominal is outside the scope of the analysis — none, not some ∅. This matches the paper's framing (p. 426, set aside): "Not all adjectives allow modification by -heid to form a nominalization, or have uninflected nominal counterparts. We will focus on triplets…".

Equations

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

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.derivedNominal_eq_uninflected_of_heid {a : Fragments.Dutch.Adjectives.AdjEntry} (h : a.nominalHeid.isSome = true) : derivedNominal a = some (uninflectedNominal a)

When a admits a -heid form, the derived nominal coincides extensionally with the uninflected nominal — both denote the same Mendia subkind. This is the empirical convergence @cite{mcnally-deswart-2011} §3.2-3.3 establishes between the two kind-denoting routes; the formal divergence (∩ vs root projection) is suppressed in the extensional model.

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.derivedNominal_none_of_no_heid {a : Fragments.Dutch.Adjectives.AdjEntry} (h : a.nominalHeid = none) : derivedNominal a = none

When a has no -heid form (e.g., roze), the derived-nominal construction is outside the scope of the analysis.

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.roze_derivedNominal_none : derivedNominal Fragments.Dutch.Adjectives.roze = none

Concrete witness using the Fragment's exception class: roze 'pink' has no -heid form per @cite{mcnally-deswart-2011} §1, so its derived nominal is outside scope.

§1: Domain-driven felicity of inflected nominalisation

@cite{mcnally-deswart-2011} §1 observes that the inflected nominalisation construction (het rode van X, het vreemde van X) is frequent with abstract adjectives (vreemd, gezond, leuk, bijzonder) but rare with concrete adjectives — the cited contrast being ?*het dichte van deze doos 'the closed of this box'. We project this asymmetry off the Fragment's Domain field.

inductive Phenomena.Morphology.Studies.McNallyDeSwart2011.Frequency : Type

Frequency of the inflected nominalisation construction by domain. @cite{mcnally-deswart-2011} §1 + §3.4 reports a graded scale, not a binary contrast: abstract adjectives admit the construction most freely, colour and taste are the focal cases (admit all three forms productively), and concrete adjectives are marginal (only dicht is cited, with ?*het dichte van deze doos flagged).

• high : Frequency

  Most freely admitted (abstract: het vreemde van X, paper §3.4).

• medium : Frequency

  Productively admitted (colour, taste: het rode van X, paper §3.1).

• marginal : Frequency

  Marginally admitted (concrete: ?*het dichte van deze doos, §1).

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqFrequency : DecidableEq Frequency

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqFrequency x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprFrequency : Repr Frequency

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprFrequency = { reprPrec := Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprFrequency.repr }

def Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprFrequency.repr : Frequency → ℕ → Std.Format

Equations

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

def Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectedNominalisationFrequency : Fragments.Dutch.Adjectives.Domain → Frequency

The frequency-of-inflected-nominalisation predicted by a semantic Domain. Per @cite{mcnally-deswart-2011} §1 + §3.4.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectedNominalisationFrequency Fragments.Dutch.Adjectives.Domain.color = Phenomena.Morphology.Studies.McNallyDeSwart2011.Frequency.medium
• Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectedNominalisationFrequency Fragments.Dutch.Adjectives.Domain.taste = Phenomena.Morphology.Studies.McNallyDeSwart2011.Frequency.medium
• Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectedNominalisationFrequency Fragments.Dutch.Adjectives.Domain.abstract = Phenomena.Morphology.Studies.McNallyDeSwart2011.Frequency.high
• Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectedNominalisationFrequency Fragments.Dutch.Adjectives.Domain.concrete = Phenomena.Morphology.Studies.McNallyDeSwart2011.Frequency.marginal

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.domain_frequency_split : inflectedNominalisationFrequency Fragments.Dutch.Adjectives.rood.domain = Frequency.medium ∧ inflectedNominalisationFrequency Fragments.Dutch.Adjectives.vreemd.domain = Frequency.high ∧ inflectedNominalisationFrequency Fragments.Dutch.Adjectives.gezond.domain = Frequency.high ∧ inflectedNominalisationFrequency Fragments.Dutch.Adjectives.leuk.domain = Frequency.high ∧ inflectedNominalisationFrequency Fragments.Dutch.Adjectives.dicht.domain = Frequency.marginal

The §1 abstract/concrete asymmetry, formalised on Fragment entries along the graded Frequency scale. Abstract adjectives (vreemd, gezond, leuk) score .high; colours and tastes (rood) score .medium; the concrete adjective dicht scores .marginal. The proof reads .domain on each Fragment entry.

§3.4: Inflected -e form — relational trope semantics

@cite{mcnally-deswart-2011} (25): the inflectional suffix -e increases the adjective's valence by one, introducing a relation P_asp(y)(x) between an external entity y (saturated by PP) and the P aspect x of y. The het article then applies @cite{chierchia-1984}'s ∩ to reify the resulting property as a trope (an entity correlate of a property uniquely instantiated in one individual).

The crucial type-theoretic distinction: uninflected/derived denote kinds (sets of subkinds); inflected denotes a trope (a single property-aspect of a specific entity), which is not a kind.

def Phenomena.Morphology.Studies.McNallyDeSwart2011.AspectOf (Entity : Type u_1) : Type u_1

An AspectOf instance records, for each adjectival property P, the "P-aspect" relation the language pairs with P. This makes @cite{mcnally-deswart-2011}'s P_asp derivation explicit: the suffix -e does not introduce an arbitrary new relation; it produces the aspect-relation contextually associated with P (analogous to the cor function relating the proxy adjective to its associated property in (23b)).

Equations

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

def Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectAdjective {Entity : Type u_1} (asp : AspectOf Entity) (P : Shade → Prop) : Entity → Shade → Prop

@cite{mcnally-deswart-2011} (25a): [[-e]] = λPλyλx. P_asp(y)(x). The -e inflection takes a property P and produces P_asp via the contextual aspect-of mapping. Crucially P_asp is derived from P (not an independent input), so substituting a different property yields a different aspect relation.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectAdjective asp P = asp P

def Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectedWithPP {Entity : Type u_1} (Pasp : Entity → Shade → Prop) (s : Entity) : Shade → Prop

@cite{mcnally-deswart-2011} (26b): saturating the -e-inflected adjective with a PP-complement entity yields a property (the aspect-of-s property), not a set of kinds.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectedWithPP Pasp s = Pasp s

@cite{moltmann-2004} trope: the entity correlate of a property uniquely instantiated in one specific individual. We do not introduce a dedicated Trope struct — the inflected-form denotation is the bare pair (Shade → Prop) × Entity, with .fst recording the property aspect and .snd recording the bearer. A full @cite{moltmann-2004} / @cite{moltmann-2013} formalisation would additionally individuate by spatiotemporal location and carry a uniqueness-presupposition witness; promote to substrate (Theories/Semantics/Reference/Trope.lean or similar) when a second consumer arrives. No prior Trope type exists in linglib.

@[reducible, inline]

abbrev Phenomena.Morphology.Studies.McNallyDeSwart2011.TropePair (Entity : Type u_1) : Type u_1

The denotation of a het-reified inflected adjective: the bare pair (property-aspect, bearer).

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.TropePair Entity = ((Phenomena.Morphology.Studies.McNallyDeSwart2011.Shade → Prop) × Entity)

def Phenomena.Morphology.Studies.McNallyDeSwart2011.inflectedWithHet {Entity : Type u_1} (asp : AspectOf Entity) (P : Shade → Prop) (s : Entity) : TropePair Entity

@cite{mcnally-deswart-2011} (26c): het rode van de aardbeien denotes the trope obtained by reifying (Chierchia ∩) the property λx. Red_asp(strawberries)(x). The result is not a kind; it is a trope — an entity correlate uniquely tied to a specific bearer. The full pipeline (-e inflection + PP saturation + het-as-∩) composes inflectAdjective and inflectedWithPP.

Equations

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

§3.4-3.5: Type-theoretic contrast between the three forms

The architectural payoff of the paper: uninflected and derived forms denote sets of subkinds (kind-level); the inflected form denotes a trope (individual-level). The Lean types make this explicit.

inductive Phenomena.Morphology.Studies.McNallyDeSwart2011.Form : Type

The three Dutch forms are typologically distinct in their Lean return types: uninflected and derived return Set Shade (kinds); the inflected form returns TropePair Entity. This is the core contrast @cite{mcnally-deswart-2011} establishes.

• uninflected : Form

  het rood (van X) — uninflected nominal, neuter mass noun.

• derived : Form

  de roodheid (van X) — derived nominal via -heid, count or mass.

• inflected : Form

  het rode van X — inflected adjective + het-as-∩.

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqForm : DecidableEq Form

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprForm : Repr Form

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprForm = { reprPrec := Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprForm.repr }

def Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

inductive Phenomena.Morphology.Studies.McNallyDeSwart2011.AbstractObjectKind : Type

Whether a form's denotation is a kind (set of subkinds) or a trope (entity correlate of a uniquely instantiated property).

• kind : AbstractObjectKind
• trope : AbstractObjectKind

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqAbstractObjectKind : DecidableEq AbstractObjectKind

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqAbstractObjectKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprAbstractObjectKind.repr : AbstractObjectKind → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprAbstractObjectKind : Repr AbstractObjectKind

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprAbstractObjectKind = { reprPrec := Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprAbstractObjectKind.repr }

def Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.denotationType : Form → AbstractObjectKind

@cite{mcnally-deswart-2011}'s central typological claim: each Dutch form maps to a determinate kind of abstract object.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.uninflected.denotationType = Phenomena.Morphology.Studies.McNallyDeSwart2011.AbstractObjectKind.kind
• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.derived.denotationType = Phenomena.Morphology.Studies.McNallyDeSwart2011.AbstractObjectKind.kind
• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.inflected.denotationType = Phenomena.Morphology.Studies.McNallyDeSwart2011.AbstractObjectKind.trope

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.two_kinds_one_trope : Form.uninflected.denotationType = AbstractObjectKind.kind ∧ Form.derived.denotationType = AbstractObjectKind.kind ∧ Form.inflected.denotationType = AbstractObjectKind.trope

Uninflected and derived both denote kinds; inflected is the unique trope-denoting form. This is the empirically motivated three-way distinction the paper argues for (§3.4 + §5 conclusion).

§2.3: Rival analyses of the inflected form

@cite{mcnally-deswart-2011} §2.3 considers two rival analyses of het rode van X and rejects both, in favour of the third (het as Chierchia ∩):

1. Nominalisation analysis: the inflected rode IS a noun (changed category via -e). Rejected because nouns admit adjectival modification and other determiners (paper §2.3 (13)-(14)).
2. Ellipsis analysis: the inflected rode is an adjective hiding an empty/elided noun. Rejected because (a) determiner restrictions (14) and lack of generic readings (15) are unexplained, and (b) no plausible noun can be inserted (paper §2.3 (16): de is required for kleur, smaak).
3. Het-as-∩ analysis: het carries Chierchia ∩, embedding the AP directly under DP. The adjective remains adjectival (taking adverbial mod), and only het (the default ∩-marker for non-nominal categories) is licensed.

Following the @cite{snyder-2026} PolymorphicAnalysis pattern, we encode all three rivals and their predictions for the §2.3 diagnostics. The substantive theorem only_hetAsCap_matches_diagnostics shows only the adopted analysis matches the actual data — the other two would predict the wrong distribution.

inductive Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis : Type

The three rival analyses of Dutch het rode van X considered in @cite{mcnally-deswart-2011} §2.3.

• nominalisation : InflectedAnalysis

  The inflected adjective is a noun (category-changing). Rejected.

• ellipsis : InflectedAnalysis

  The inflected adjective hides an empty/elided noun. Rejected.

• hetAsCap : InflectedAnalysis

  het = Chierchia ∩, embedding the inflected AP under DP. Adopted.

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqInflectedAnalysis : DecidableEq InflectedAnalysis

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidableEqInflectedAnalysis x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprInflectedAnalysis.repr : InflectedAnalysis → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprInflectedAnalysis : Repr InflectedAnalysis

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprInflectedAnalysis = { reprPrec := Phenomena.Morphology.Studies.McNallyDeSwart2011.instReprInflectedAnalysis.repr }

def Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.PredictsAdverbialModOnly : InflectedAnalysis → Prop

Does the analysis predict that the form admits adverbial (rather than adjectival) modification? Per §2.3 (13). The three rivals diverge here: only nominalisation (which makes the form a noun) predicts adjectival mod is licensed and adverbial mod blocked. Under ellipsis, the visible element remains an adjective pre-ellipsis, so adverbial mod IS licensed.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.nominalisation.PredictsAdverbialModOnly = False
• Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.ellipsis.PredictsAdverbialModOnly = True
• Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.hetAsCap.PredictsAdverbialModOnly = True

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidablePredInflectedAnalysisPredictsAdverbialModOnly : DecidablePred InflectedAnalysis.PredictsAdverbialModOnly

Equations

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

def Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.PredictsHetOnlyDeterminer : InflectedAnalysis → Prop

Does the analysis predict that only het (no other determiners) licenses the form? Per §2.3 (14).

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.nominalisation.PredictsHetOnlyDeterminer = False
• Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.ellipsis.PredictsHetOnlyDeterminer = False
• Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.hetAsCap.PredictsHetOnlyDeterminer = True

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidablePredInflectedAnalysisPredictsHetOnlyDeterminer : DecidablePred InflectedAnalysis.PredictsHetOnlyDeterminer

Equations

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

def Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.PredictsNoGeneric : InflectedAnalysis → Prop

Does the analysis predict that the form rejects generic readings? Per §2.3 (15).

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.nominalisation.PredictsNoGeneric = False
• Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.ellipsis.PredictsNoGeneric = False
• Phenomena.Morphology.Studies.McNallyDeSwart2011.InflectedAnalysis.hetAsCap.PredictsNoGeneric = True

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidablePredInflectedAnalysisPredictsNoGeneric : DecidablePred InflectedAnalysis.PredictsNoGeneric

Equations

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

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.only_hetAsCap_matches_diagnostics (a : InflectedAnalysis) : a.PredictsAdverbialModOnly ∧ a.PredictsHetOnlyDeterminer ∧ a.PredictsNoGeneric ↔ a = InflectedAnalysis.hetAsCap

@cite{mcnally-deswart-2011}'s §2.3 argument made formal: only the hetAsCap analysis predicts the actual distribution (adverbial-mod only, het-only determiner, no generics). Each predicate is decided on the rival's own theoretical commitments; the conjunction discriminates rivals from data.

§2.3: Form-level distribution facts

The morphosyntactic facts (13)-(15) about each Dutch form: only the inflected form is restricted to het, to adverbial modification, and rejects generic uses.

def Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.AdmitsDetOtherThanHet : Form → Prop

Whether a form admits non-het determiners (a, this, his, no, many). @cite{mcnally-deswart-2011} (14): only inflected refuses.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.uninflected.AdmitsDetOtherThanHet = True
• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.derived.AdmitsDetOtherThanHet = True
• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.inflected.AdmitsDetOtherThanHet = False

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidablePredFormAdmitsDetOtherThanHet : DecidablePred Form.AdmitsDetOtherThanHet

Equations

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

def Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.AdmitsAdjectivalModification : Form → Prop

Whether a form admits adjectival modification (vs only adverbial). @cite{mcnally-deswart-2011} (13): only inflected refuses.

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.uninflected.AdmitsAdjectivalModification = True
• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.derived.AdmitsAdjectivalModification = True
• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.inflected.AdmitsAdjectivalModification = False

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidablePredFormAdmitsAdjectivalModification : DecidablePred Form.AdmitsAdjectivalModification

Equations

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

def Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.AdmitsGeneric : Form → Prop

Whether a form admits a generic interpretation. (8), (12) vs (15).

Equations

• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.uninflected.AdmitsGeneric = True
• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.derived.AdmitsGeneric = True
• Phenomena.Morphology.Studies.McNallyDeSwart2011.Form.inflected.AdmitsGeneric = False

@[implicit_reducible]

instance Phenomena.Morphology.Studies.McNallyDeSwart2011.instDecidablePredFormAdmitsGeneric : DecidablePred Form.AdmitsGeneric

Equations

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

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.morphosyntax_aligns_with_trope_semantics (f : Form) : ¬f.AdmitsDetOtherThanHet ∨ ¬f.AdmitsAdjectivalModification ∨ ¬f.AdmitsGeneric ↔ f.denotationType = AbstractObjectKind.trope

The morphosyntactic distribution (§2.3 — three diagnostics) and the semantic-type column (denotationType) are cross-aligned: a form fails any one of the three diagnostics iff it denotes a trope. This is the substantive content of the paper's claim that the morphosyntactic restrictions on het rode van X are because of its trope semantics — two independently-stated tables coincide.

theorem Phenomena.Morphology.Studies.McNallyDeSwart2011.trope_iff_inflected (f : Form) : f.denotationType = AbstractObjectKind.trope ↔ f = Form.inflected

Equivalent biconditional: a form denotes a trope iff it is the inflected form.

§3.5, §4: Cross-linguistic parallels

@cite{mcnally-deswart-2011} §3.5 places the inflected construction in parallel with Dutch het-nominalised infinitives (het zingen van Jan, §3.5 (28a)). For the semantics, the paper invokes @cite{chierchia-1984} on infinitives and gerunds, and @cite{hamm-vanlambalgen-2002} on formal foundations of nominalisation. @cite{pullum-1991}'s "NP with VP head" analysis treats the syntax of English -ing separately and is not itself a Chierchia-∩ analysis.

§4 considers Spanish lo-nominals (lo blanco de las dunas). Crucially, @cite{villalba-2009}'s own analysis uses Moltmann's properties/qualities ontology (introducing a quality sort distinct from properties), not Chierchia ∩. McNally & de Swart §4 propose extending their ∩-analysis to Spanish, against Villalba — the ∩-extension is M&deS's, not Villalba's.

The paper's central general claim (§5): natural languages exploit the inflection / derivation distinction to create subtle nuances in reference to abstract objects, all derivable from a parsimonious kind+token ontology — no separate "quality" sort is needed (contra Villalba).

The cross-linguistic cluster — Dutch het (inflected adjective AND het-nominalised infinitive), English -ing gerund (Chierchia 1984 + Hamm & van Lambalgen 2002 semantics, Pullum 1991 syntax), Spanish lo (M&deS extension, against Villalba) — is documented here in prose because none of the analogues besides Dutch inflected-adjective is currently formalised in linglib. Promote to a typed cluster when the second case lands.

§5: Cross-paper substrate alignment with Snyder 2026

Phenomena/Numerals/Studies/Snyder2026.lean (Polymorphic Contextualism) and this file (McNally & de Swart 2011) both consume the same substrate:

• Subkinds.subkindOf for kind formation by salient equivalence relation (numerals partition by mathematical system; colours partition by chromatic root).
• IOTA-as-definite for selecting a unique subkind from a modified noun predicate.

They disagree on:

• Whether nominalisation is Chierchia ∩ (this paper) or Partee NOM as a pure type-shifter (Snyder Polymorphic Contextualism, §2 (10a)). In the finite extensional setting these collapse (cf. Composition/TypeShifting.lean NOM = iota), but conceptually they diverge: ∩ is substantive (entity-correlate-of-property), NOM is formal (Partee-shifter combinator).
• Whether the lexical entry is unitary (Snyder: one λxα. two(x)) or category-projected (McNally & de Swart: distinct rood_N vs rood_A built from a shared root via different morphological projections).

The shared substrate (Mendia subkinds + IOTA) is genuine; the divergence on nominalisation and lexical-projection architecture is genuine theoretical incompatibility. This is exactly the kind of cross-framework engagement linglib is designed to surface.