Documentation

Linglib.Semantics.Quantification.BinominalDefs

Quantification.Binominal — Defs #

Cross-linguistic types for binominal (N₁-of-N₂) constructions: the 3-way BinominalType (Saab 2026, Romance-cross-linguistic) and the 6-way OfBinominalType (ten-Wolde 2023, English-specific grammaticalization cline). Plus the structural-property predicates, the cline ordering, and diachronic-monotonicity theorems.

Provenance #

Moved from Core/Lexical/Binominal.lean in the cleanup that dissolved Core/Lexical/. Lives at Semantics/Quantification/ (sibling of the existing Binominal.lean semantic-composition file, which consumes OfBinominalType for quantizingToOfBinominal and other construction-specific compositions). Naming follows the mathlib Defs.lean idiom: this file holds the data + structural predicates; the sibling Binominal.lean holds the semantic composition rules.

Framework commitment #

The 6-way OfBinominalType taxonomy and the grammaticalization cline (clinePosition, bleaching_monotone, plural_loss_monotone, agreement_loosens_monotone, etc.) follow [tW23]'s specific framework. This is one carve-up among several active frameworks for binominal noun phrase structure:

[tW23]: 6-way grammaticalization cline (formalized here).
Aarts 1998 Binominal noun phrases in English: different headedness diagnostics, no commitment to a single linear cline. Not currently in references.bib.
den Dikken 2006 Relators and Linkers: RP (Relator Phrase) analysis where N-of-N is a predication structure with predicate inversion, not a cline. Den Dikken's evaluative BNPs work via predicate inversion, not via [N₁ of a]-as-modifier reanalysis. Not currently in references.bib.
Selkirk 1977 / Akmajian-Lehrer measure-phrase analysis for pseudo-partitives.
Constructional accounts (Bergen-Binsted, Goldberg): store [a hell of a N] as a stored construction with no head-switching.

The 3-way BinominalType (Saab 2026) is closer to consensus across Romance binominals (pseudoPartitive / quantificational / qualitative) but is not without contestation: e.g., Espinal & Mateu on Romance evaluatives differ from Saab 2026's grouping.

UNVERIFIED: All ten-Wolde Table/§ references (Table 4.2, §4.3.4, §4.3.5, §4.4.5, Ch. 7) cited from memory; verify before treating as authoritative.

: Three-Way Classification (Spanish, cross-linguistic) #

inductive Quantification.Binominal.BinominalType :

The three-way binominal classification ([Saa26]).

This coarser-grained taxonomy covers the structural types attested across Romance binominals. The finer-grained English subtypes are captured by OfBinominalType.

pseudoPartitive : BinominalType
quantificational : BinominalType
qualitative : BinominalType

Instances For

@[implicit_reducible]

instance Quantification.Binominal.instDecidableEqBinominalType :

DecidableEq BinominalType

Equations

Quantification.Binominal.instDecidableEqBinominalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Quantification.Binominal.instReprBinominalType :

Repr BinominalType

Equations

Quantification.Binominal.instReprBinominalType = { reprPrec := Quantification.Binominal.instReprBinominalType.repr }

def Quantification.Binominal.instReprBinominalType.repr :

BinominalType → Nat → Std.Format

Equations

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

Instances For

def Quantification.Binominal.BinominalType.licensesNPE :

BinominalType → Bool

Does this binominal type license NP-ellipsis? [Saa26]: pseudo-partitive and quantificational yes; qualitative no.

Equations

Instances For

def Quantification.Binominal.BinominalType.hasNumE :

BinominalType → Bool

Does the Num head in this structure carry [E]? [Saa26]: Num[E] is present iff the complement of Num is a standard nP (not an EquP with an indexical empty noun).

Equations

Instances For

theorem Quantification.Binominal.npe_iff_numE (b : BinominalType) :

b.licensesNPE = b.hasNumE

Core result: NP-ellipsis is licensed iff Num has [E].

: Six-Way Classification (English, ten-Wolde 2023) #

inductive Quantification.Binominal.BNPHead :

Which noun is the semantic head of the binominal construction.

n₁ : BNPHead
n₂ : BNPHead

Instances For

def Quantification.Binominal.instReprBNPHead.repr :

BNPHead → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Quantification.Binominal.instReprBNPHead :

Equations

Quantification.Binominal.instReprBNPHead = { reprPrec := Quantification.Binominal.instReprBNPHead.repr }

@[implicit_reducible]

instance Quantification.Binominal.instDecidableEqBNPHead :

DecidableEq BNPHead

Equations

Quantification.Binominal.instDecidableEqBNPHead x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

inductive Quantification.Binominal.OfBinominalType :

The six types of of-binominal construction ([tW23]).

The ordering reflects the grammaticalization cline: N+PP → Head-Classifier → Pseudo-partitive / Evaluative → EM → BI.

UNVERIFIED: Cline ordering and per-type characterization rests on ten-Wolde's diachronic reconstruction; competing frameworks (Aarts, den Dikken, Selkirk) carve the space differently.

nPP : OfBinominalType
N+PP: N₁ denotes a referent, PP ascribes a property. the beast of the field, the hell of the damned
headClassifier : OfBinominalType
Head-classifier: PP classifies the type or material of N₁. a cake of rye, a beast of prey
pseudoPartitive : OfBinominalType
Pseudo-partitive: N₁ quantizes, N₂ is semantic head. a glass of water, a piece of cake, a bunch of flowers
evaluative : OfBinominalType
Evaluative BNP (EBNP): N₁ ascribes evaluative property to N₂. that idiot of a doctor, a whale of a man
evaluativeModifier : OfBinominalType
Evaluative Modifier (EM): [N₁ of a] is a complex modifier. a hell of a time, a whale of a job
binominalIntensifier : OfBinominalType
Binominal Intensifier (BI): [N₁ of a] intensifies Adj/Quant. a hell of a good time, a whale of a lot of fun

Instances For

@[implicit_reducible]

instance Quantification.Binominal.instReprOfBinominalType :

Repr OfBinominalType

Equations

Quantification.Binominal.instReprOfBinominalType = { reprPrec := Quantification.Binominal.instReprOfBinominalType.repr }

def Quantification.Binominal.instReprOfBinominalType.repr :

OfBinominalType → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Quantification.Binominal.instDecidableEqOfBinominalType :

DecidableEq OfBinominalType

Equations

Quantification.Binominal.instDecidableEqOfBinominalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Quantification.Binominal.OfBinominalType.head :

OfBinominalType → BNPHead

Which noun is the semantic head of each construction type.

For evaluative BNPs, N₂ is the semantic and discourse head, though syntactic evidence for headedness is inconclusive ([tW23]). For EM and BI, N₂ is semantic, syntactic, and discourse head.

Equations

Instances For

def Quantification.Binominal.OfBinominalType.n₁IsEvaluative :

OfBinominalType → Bool

Is N₁ evaluative (expresses speaker attitude)?

Equations

Instances For

def Quantification.Binominal.OfBinominalType.n₁IsReferential :

OfBinominalType → Bool

Is N₁ referential (denotes an entity in the world)?

Equations

Quantification.Binominal.OfBinominalType.nPP.n₁IsReferential = true
Quantification.Binominal.OfBinominalType.headClassifier.n₁IsReferential = true
x✝.n₁IsReferential = false

Instances For

def Quantification.Binominal.OfBinominalType.n₁Bleached :

OfBinominalType → Bool

Does N₁ undergo semantic bleaching (loss of lexical content)? Bleaching increases along the grammaticalization cline.

The nature of bleaching differs: pseudo-partitive N₁ (glass, piece) bleaches from referential noun → quantizing measure term; evaluative N₁ bleaches from gradable predicate (EBNP) → evaluative modifier (EM) → degree intensifier (BI).

Equations

Instances For

def Quantification.Binominal.OfBinominalType.ofIsLinker :

OfBinominalType → Bool

Does of function as a linking device (no independent semantics)? In earlier constructions, of retains prepositional meaning (location, possession); in later ones it is a pure linker.

Equations

Instances For

def Quantification.Binominal.OfBinominalType.n₁AllowsPlural :

OfBinominalType → Bool

Can N₁ appear in plural form? Along the cline, N₁ loses the ability to inflect.

Equations

Instances For

def Quantification.Binominal.OfBinominalType.det₂MarksNumber :

OfBinominalType → Bool

Does Det₂ still mark number? In the EBNP, the second determiner marks number; in EM and BI it no longer does.

Equations

Instances For

def Quantification.Binominal.OfBinominalType.ofReplaceableByCopula :

OfBinominalType → Bool

Can of be replaced by a copular verb? In EBNP, of can sometimes be paraphrased with be (e.g., "the doctor is an idiot"); in EM and BI it cannot.

Equations

Instances For

def Quantification.Binominal.OfBinominalType.n₁OfAIsConstituent :

OfBinominalType → Bool

Does [N₁ of a] function as a single constituent (modifier phrase)? The reanalysis of [N₁ of a] into a modifier unit is the defining structural change at the EM stage.

Equations

Instances For

def Quantification.Binominal.OfBinominalType.n₁AllowsDescriptivePremod :

OfBinominalType → Bool

Does N₁ allow descriptive premodification? EBNP strongly favors premodification of N₁ (a total idiot of a doctor); EM and BI block it because [N₁ of a] has been reanalyzed as a unit. Earlier constructions (N+PP, HC, PP) allow free premodification of N₁.

Equations

Instances For

def Quantification.Binominal.OfBinominalType.n₂AllowsMass :

OfBinominalType → Bool

Can N₂ be a mass noun? EBNP and EM restrict N₂ to count and collective nouns; BI extends to mass nouns (sporadically — not freely productive), reflecting the structural change where [N₁ of a] modifies a following adjective rather than N₂ directly. Earlier types (N+PP, HC, PP) have no such restriction.

Equations

Quantification.Binominal.OfBinominalType.evaluative.n₂AllowsMass = false
Quantification.Binominal.OfBinominalType.evaluativeModifier.n₂AllowsMass = false
x✝.n₂AllowsMass = true

Instances For

inductive Quantification.Binominal.AgreementLevel :

Level of number agreement between N₁ and N₂.

agree : AgreementLevel
N₁ and N₂ agree in number.
usuallyAgree : AgreementLevel
N₁ and N₂ usually agree, with some exceptions.
noAgreement : AgreementLevel
N₁ and N₂ do not have to agree in number.

Instances For

@[implicit_reducible]

instance Quantification.Binominal.instReprAgreementLevel :

Repr AgreementLevel

Equations

Quantification.Binominal.instReprAgreementLevel = { reprPrec := Quantification.Binominal.instReprAgreementLevel.repr }

def Quantification.Binominal.instReprAgreementLevel.repr :

AgreementLevel → Nat → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Quantification.Binominal.instDecidableEqAgreementLevel :

DecidableEq AgreementLevel

Equations

Quantification.Binominal.instDecidableEqAgreementLevel x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Quantification.Binominal.AgreementLevel.toNat :

AgreementLevel → Nat

Numeric encoding: agreement loosens over time.

Equations

Instances For

@[implicit_reducible]

instance Quantification.Binominal.instLEAgreementLevel :

LE AgreementLevel

Equations

Quantification.Binominal.instLEAgreementLevel = { le := fun (a b : Quantification.Binominal.AgreementLevel) => a.toNat ≤ b.toNat }

@[implicit_reducible]

instance Quantification.Binominal.instDecidableLeAgreementLevel (a b : AgreementLevel) :

Decidable (a ≤ b)

Equations

Quantification.Binominal.instDecidableLeAgreementLevel a b = a.toNat.decLe b.toNat

def Quantification.Binominal.OfBinominalType.n₁N₂Agreement :

OfBinominalType → AgreementLevel

N₁ & N₂ number agreement along the cline. Agreement loosens as grammaticalization proceeds: full agreement → usually agree → no agreement required.

Equations

Instances For

def Quantification.Binominal.OfBinominalType.ofObligatory :

OfBinominalType → Bool

Is of obligatory in the construction? Mandatory for all types except BI, where it can be absent in reduced forms like helluva, hella.

Equations

Quantification.Binominal.OfBinominalType.binominalIntensifier.ofObligatory = false
x✝.ofObligatory = true

Instances For

: Grammaticalization Cline #

def Quantification.Binominal.OfBinominalType.clinePosition :

OfBinominalType → Nat

Position on the grammaticalization cline (0 = most lexical, 5 = most grammatical).

Supported by diachronic corpus evidence ([tW23]): constructions appear in English in this order historically, and N₁ nouns progress through these stages with increasing semantic bleaching.

Equations

Instances For

theorem Quantification.Binominal.cline_injective (t₁ t₂ : OfBinominalType) :

t₁.clinePosition = t₂.clinePosition → t₁ = t₂

The cline is a total order: each type has a unique position.

theorem Quantification.Binominal.bleaching_after_position_2 (t : OfBinominalType) :

2 ≤ t.clinePosition → t.n₁Bleached = true

Bleaching increases along the cline: all types at position ≥ 2 are bleached.

theorem Quantification.Binominal.head_switches_at_2 (t : OfBinominalType) :

(t.head = BNPHead.n₁) = (t.clinePosition < 2)

Head switches from N₁ to N₂ at position 2.

theorem Quantification.Binominal.plural_lost_at_4 (t : OfBinominalType) :

4 ≤ t.clinePosition → t.n₁AllowsPlural = false

N₁ plural ability is lost at position 4 (EM).

theorem Quantification.Binominal.det₂_number_lost_at_4 (t : OfBinominalType) :

4 ≤ t.clinePosition → t.det₂MarksNumber = false

Det₂ number marking is lost at the same point as N₁ plural (position 4).

theorem Quantification.Binominal.n₁_of_a_constituent_at_4 (t : OfBinominalType) :

4 ≤ t.clinePosition → t.n₁OfAIsConstituent = true

[N₁ of a] constituency emerges at position 4 (EM).

theorem Quantification.Binominal.premod_lost_at_4 (t : OfBinominalType) :

4 ≤ t.clinePosition → t.n₁AllowsDescriptivePremod = false

N₁ descriptive premodification is lost at position 4 (EM), together with N₁ plural and [N₁ of a] constituency.

theorem Quantification.Binominal.premod_loss_monotone (t₁ t₂ : OfBinominalType) :

t₁.clinePosition ≤ t₂.clinePosition → t₁.n₁AllowsDescriptivePremod = false → t₂.n₁AllowsDescriptivePremod = false

Monotonicity: once N₁ premodification is lost, it stays lost.

theorem Quantification.Binominal.copula_only_evaluative (t : OfBinominalType) :

t.ofReplaceableByCopula = true → t = OfBinominalType.evaluative

Copula replacement is unique to evaluative BNPs.

theorem Quantification.Binominal.evaluative_is_n₂_headed (t : OfBinominalType) :

t.n₁IsEvaluative = true → t.head = BNPHead.n₂

Evaluative types are always N₂-headed.

theorem Quantification.Binominal.referential_is_n₁_headed (t : OfBinominalType) :

t.n₁IsReferential = true → t.head = BNPHead.n₁

Referential types are always N₁-headed.

theorem Quantification.Binominal.bleaching_monotone (t₁ t₂ : OfBinominalType) :

t₁.clinePosition ≤ t₂.clinePosition → t₁.n₁Bleached = true → t₂.n₁Bleached = true

Monotonicity: once bleaching starts, it never reverses.

theorem Quantification.Binominal.plural_loss_monotone (t₁ t₂ : OfBinominalType) :

t₁.clinePosition ≤ t₂.clinePosition → t₁.n₁AllowsPlural = false → t₂.n₁AllowsPlural = false

Monotonicity: once N₁ plural is lost, it stays lost.

theorem Quantification.Binominal.agreement_loosens_monotone (t₁ t₂ : OfBinominalType) :

t₁.clinePosition ≤ t₂.clinePosition → t₁.n₁N₂Agreement.toNat ≤ t₂.n₁N₂Agreement.toNat

Agreement loosens monotonically along the cline.

theorem Quantification.Binominal.n₂_mass_nonmonotone :

OfBinominalType.nPP.n₂AllowsMass = true ∧ OfBinominalType.evaluative.n₂AllowsMass = false ∧ OfBinominalType.binominalIntensifier.n₂AllowsMass = true

N₂ mass restriction is non-monotone: it narrows at the evaluative stage (positions 3–4) and widens again at BI (position 5), reflecting the structural change where [N₁ of a] shifts into AdjP.

theorem Quantification.Binominal.of_optional_only_at_bi (t : OfBinominalType) :

t.ofObligatory = false → t.clinePosition = 5

of becomes optional only at the most grammaticalized stage (BI).

: Cross-Linguistic Mapping #

def Quantification.Binominal.BinominalType.toOfBinominalType :

BinominalType → OfBinominalType

Map the three-way Spanish type to the six-way English type.

UNVERIFIED CROSS-LINGUISTIC CLAIM: this mapping presupposes that Spanish qualitative maps to English evaluative (Saab's qualitative ≡ ten-Wolde's evaluative). Espinal & Mateu on Romance evaluatives differ from Saab in details; verify whether the grouping survives their critique.

Equations

Instances For

theorem Quantification.Binominal.qualitative_is_evaluative :

BinominalType.qualitative.toOfBinominalType.head = BNPHead.n₂

Spanish qualitative maps to an evaluative (N₂-headed) English type.

theorem Quantification.Binominal.quantifying_is_n₂_headed (b : BinominalType) :

b = BinominalType.pseudoPartitive ∨ b = BinominalType.quantificational → b.toOfBinominalType.head = BNPHead.n₂

Spanish pseudo-partitive/quantificational map to N₂-headed types.