McNally and de Swart (2011): Inflection and Derivation

This file formalizes the analysis of [McNdS11] of the three ways Dutch refers to abstract objects such as colours, illustrated with rood 'red': the uninflected nominal het rood and the derived de roodheid denote kinds, sets of subkinds, while the inflected het rode van de aardbeien denotes a trope, the entity correlate of a relational property instantiated in one bearer. The uninflected nominal of a root denotes the set of its subkinds, the shades of the colour (uninflectedNominal); the derived nominal, the noun in -heid of the root (Dutch.Adjectives.heid), denotes the same kind (derivedNominal); the inflectional suffix is not a category-changing nominalizer but a valence-increasing operator turning the adjective into a relation between an object and its aspect, which the determiner het, the nominalization operator of [Chi84] when it embeds an adjective phrase, reifies as a trope (inflectAdjective, inflectedWithHet). The three forms differ in what the determiner embeds and in what they denote, and the paper's distributional diagnostics follow from those two coordinates: adjectival modification and determiners other than het need a noun, and generic use needs a kind, so the inflected form alone fails all three (Form, inflected_diagnostics, fails_iff_inflected). The paper's three rival analyses of the inflected form are named for later comparison (InflectedAnalysis).

Implementation notes

The roots and their forms come from the Dutch adjective fragment, and the paper's primitive subkind relation is modelled as sharing a root; the model is extensional, so the kind denoted by the derived nominal coincides with the uninflected one. The trope is the pair of the aspect property and its bearer. The paper's observation that the inflected construction is rare with concrete adjectives, and its extension to Dutch nominalized infinitives and Spanish lo-nominals, are described in prose.

References

• L. McNally and H. de Swart, Inflection and Derivation: How Adjectives and Nouns Refer to Abstract Objects (2011)
• G. Chierchia, Topics in the Syntax and Semantics of Infinitives and Gerunds (1984)

Kinds: the uninflected and derived nominals

structure McNallyDeSwart2011.Shade : Type

A shade: an adjective entry of the fragment with an index, so that several shades belong to one colour.

• root : Dutch.Adjectives.Adjective
• idx : ℕ

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

Equations

• McNallyDeSwart2011.instDecidableEqShade.decEq { root := a, idx := a_1 } { root := b, idx := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance McNallyDeSwart2011.instDecidableEqShade : DecidableEq Shade

Equations

• McNallyDeSwart2011.instDecidableEqShade = McNallyDeSwart2011.instDecidableEqShade.decEq

@[instance_reducible]

instance McNallyDeSwart2011.instReprShade : Repr Shade

Equations

• McNallyDeSwart2011.instReprShade = { reprPrec := McNallyDeSwart2011.instReprShade.repr }

def McNallyDeSwart2011.instReprShade.repr : Shade → ℕ → Std.Format

Equations

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

def McNallyDeSwart2011.uninflectedNominal (a : Dutch.Adjectives.Adjective) : Set Shade

The uninflected noun rood (19): the set of subkinds, the shades, of the colour.

Equations

• McNallyDeSwart2011.uninflectedNominal a = {s : McNallyDeSwart2011.Shade | s.root = a}

@[simp]

theorem McNallyDeSwart2011.mem_uninflectedNominal {a : Dutch.Adjectives.Adjective} {s : Shade} : s ∈ uninflectedNominal a ↔ s.root = a

def McNallyDeSwart2011.ppModifier {Entity : Type u_1} (R : Shade → Entity → Prop) (s : Entity) : Modifier (Set Shade)

A prepositional modifier (20) meets the kind with the shades a contextual relation links to the complement's entity.

Equations

• McNallyDeSwart2011.ppModifier R s = Modifier.intersective {x : McNallyDeSwart2011.Shade | R x s}

theorem McNallyDeSwart2011.isSubsective_ppModifier {Entity : Type u_1} (R : Shade → Entity → Prop) (s : Entity) : (ppModifier R s).IsSubsective

A prepositional modifier restricts a kind to a subkind.

def McNallyDeSwart2011.derivedNominal (a : Dutch.Adjectives.Adjective) : Set Shade

The derived noun roodheid (24), the noun in -heid of the root, denotes the kind of the root.

Equations

• McNallyDeSwart2011.derivedNominal a = McNallyDeSwart2011.uninflectedNominal a

The trope: the inflected form

def McNallyDeSwart2011.AspectOf (Entity : Type u_1) : Type u_1

The aspect relation a language pairs with each adjectival property: the relation between a bearer and its aspect of that property.

Equations

• McNallyDeSwart2011.AspectOf Entity = ((McNallyDeSwart2011.Shade → Prop) → Entity → McNallyDeSwart2011.Shade → Prop)

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

The inflectional suffix (25): a valence-increasing operator taking the adjective's property to the aspect relation.

Equations

• McNallyDeSwart2011.inflectAdjective asp P = asp P

def McNallyDeSwart2011.inflectedWithHet {Entity : Type u_1} (asp : AspectOf Entity) (P : Shade → Prop) (s : Entity) : (Shade → Prop) × Entity

The trope het rode van de aardbeien (26): the aspect property saturated by the bearer, reified by het together with its bearer.

Equations

• McNallyDeSwart2011.inflectedWithHet asp P s = (McNallyDeSwart2011.inflectAdjective asp P s, s)

The three forms and the diagnostics

inductive McNallyDeSwart2011.Embedded : Type

What the determiner embeds.

• noun : Embedded
• adjectivePhrase : Embedded

@[instance_reducible]

instance McNallyDeSwart2011.instDecidableEqEmbedded : DecidableEq Embedded

Equations

• McNallyDeSwart2011.instDecidableEqEmbedded x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def McNallyDeSwart2011.instReprEmbedded.repr : Embedded → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance McNallyDeSwart2011.instReprEmbedded : Repr Embedded

Equations

• McNallyDeSwart2011.instReprEmbedded = { reprPrec := McNallyDeSwart2011.instReprEmbedded.repr }

inductive McNallyDeSwart2011.AbstractObject : Type

The kind of abstract object a form denotes.

• kind : AbstractObject
• trope : AbstractObject

@[instance_reducible]

instance McNallyDeSwart2011.instDecidableEqAbstractObject : DecidableEq AbstractObject

Equations

• McNallyDeSwart2011.instDecidableEqAbstractObject x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance McNallyDeSwart2011.instReprAbstractObject : Repr AbstractObject

Equations

• McNallyDeSwart2011.instReprAbstractObject = { reprPrec := McNallyDeSwart2011.instReprAbstractObject.repr }

def McNallyDeSwart2011.instReprAbstractObject.repr : AbstractObject → ℕ → Std.Format

Equations

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

structure McNallyDeSwart2011.Form : Type

A form of abstract reference: what the determiner embeds and what the whole denotes.

• embedded : Embedded
• denotation : AbstractObject

@[instance_reducible]

instance McNallyDeSwart2011.instDecidableEqForm : DecidableEq Form

Equations

• McNallyDeSwart2011.instDecidableEqForm = McNallyDeSwart2011.instDecidableEqForm.decEq

def McNallyDeSwart2011.instDecidableEqForm.decEq (x✝ x✝¹ : Form) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance McNallyDeSwart2011.instReprForm : Repr Form

Equations

• McNallyDeSwart2011.instReprForm = { reprPrec := McNallyDeSwart2011.instReprForm.repr }

def McNallyDeSwart2011.instReprForm.repr : Form → ℕ → Std.Format

Equations

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

def McNallyDeSwart2011.uninflected : Form

het rood: a neuter mass noun denoting a kind.

Equations

• McNallyDeSwart2011.uninflected = { embedded := McNallyDeSwart2011.Embedded.noun, denotation := McNallyDeSwart2011.AbstractObject.kind }

def McNallyDeSwart2011.derived : Form

de roodheid: a derived noun denoting a kind.

Equations

• McNallyDeSwart2011.derived = { embedded := McNallyDeSwart2011.Embedded.noun, denotation := McNallyDeSwart2011.AbstractObject.kind }

def McNallyDeSwart2011.inflected : Form

het rode van X: an adjective phrase under het, denoting a trope.

Equations

• McNallyDeSwart2011.inflected = { embedded := McNallyDeSwart2011.Embedded.adjectivePhrase, denotation := McNallyDeSwart2011.AbstractObject.trope }

def McNallyDeSwart2011.Form.AdmitsAdjectivalModification (f : Form) : Prop

Adjectival modification targets a noun (13).

Equations

• f.AdmitsAdjectivalModification = (f.embedded = McNallyDeSwart2011.Embedded.noun)

def McNallyDeSwart2011.Form.AdmitsOtherDeterminers (f : Form) : Prop

Determiners other than het select a noun; het alone carries the nominalization of an adjective phrase (14).

Equations

• f.AdmitsOtherDeterminers = (f.embedded = McNallyDeSwart2011.Embedded.noun)

def McNallyDeSwart2011.Form.AdmitsGeneric (f : Form) : Prop

Generic use needs a kind (15).

Equations

• f.AdmitsGeneric = (f.denotation = McNallyDeSwart2011.AbstractObject.kind)

@[instance_reducible]

instance McNallyDeSwart2011.instDecidablePredFormAdmitsAdjectivalModification : DecidablePred Form.AdmitsAdjectivalModification

Equations

• McNallyDeSwart2011.instDecidablePredFormAdmitsAdjectivalModification x✝ = McNallyDeSwart2011.instDecidablePredFormAdmitsAdjectivalModification._aux_1 x✝

@[instance_reducible]

instance McNallyDeSwart2011.instDecidablePredFormAdmitsOtherDeterminers : DecidablePred Form.AdmitsOtherDeterminers

Equations

• McNallyDeSwart2011.instDecidablePredFormAdmitsOtherDeterminers x✝ = McNallyDeSwart2011.instDecidablePredFormAdmitsOtherDeterminers._aux_1 x✝

@[instance_reducible]

instance McNallyDeSwart2011.instDecidablePredFormAdmitsGeneric : DecidablePred Form.AdmitsGeneric

Equations

• McNallyDeSwart2011.instDecidablePredFormAdmitsGeneric x✝ = McNallyDeSwart2011.instDecidablePredFormAdmitsGeneric._aux_1 x✝

theorem McNallyDeSwart2011.inflected_diagnostics : (¬inflected.AdmitsAdjectivalModification ∧ ¬inflected.AdmitsOtherDeterminers ∧ ¬inflected.AdmitsGeneric) ∧ ∀ f ∈ [uninflected, derived], f.AdmitsAdjectivalModification ∧ f.AdmitsOtherDeterminers ∧ f.AdmitsGeneric

The inflected form fails all three diagnostics, and the two nominal forms pass them.

theorem McNallyDeSwart2011.fails_iff_inflected (f : Form) (hf : f ∈ [uninflected, derived, inflected]) : ¬f.AdmitsAdjectivalModification ∨ ¬f.AdmitsOtherDeterminers ∨ ¬f.AdmitsGeneric ↔ f = inflected

Among the three forms, failing any diagnostic is being the inflected form: the distributional restrictions are the trope semantics.

inductive McNallyDeSwart2011.InflectedAnalysis : Type

The three analyses of the inflected form the paper weighs (§2.3): a category-changing nominalization, ellipsis of a noun, and het as the nominalization operator over an adjective phrase, the one adopted.

• nominalisation : InflectedAnalysis
• ellipsis : InflectedAnalysis
• hetAsCap : InflectedAnalysis

@[instance_reducible]

instance McNallyDeSwart2011.instDecidableEqInflectedAnalysis : DecidableEq InflectedAnalysis

Equations

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

@[instance_reducible]

instance McNallyDeSwart2011.instReprInflectedAnalysis : Repr InflectedAnalysis

Equations

• McNallyDeSwart2011.instReprInflectedAnalysis = { reprPrec := McNallyDeSwart2011.instReprInflectedAnalysis.repr }

def McNallyDeSwart2011.instReprInflectedAnalysis.repr : InflectedAnalysis → ℕ → Std.Format

Equations

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