Borer (2005): In Name Only

This file formalizes the count structure of [Bor05]. Noun stems denote cumulative stuff and are mass by default; the mass/count distinction is not lexical but structural, with two open values in the nominal spine assigned range by the functional lexicon. The classifier head ⟨e⟩div divides the stuff, and plural inflection is the head feature that assigns it range, so a bare plural is divided but not counted (27). The quantity head ⟨e⟩# counts the divisions or measures undivided mass, much salt projecting no classifier phrase (28). Cardinals other than one and the plural-taking quantifiers are pure counters, which is why two meat and two boy fail (29), while a, one, every and each are portmanteau morphemes assigning range to both open values (30), as are the cardinals of Hungarian, Turkish and Armenian, which never co-occur with plural inflection (36) to (38); all takes a mass or a plural restriction and, dividing nothing, has no count reading on a bare stem (35). Each open value takes range once, so every boys and several a boy are out, and the distribution of the determiner classes of (20) over bare stems and plurals follows. Division creates no individuals: a reticule may have no complete cell, as in zero apples and 0.5 apples, and individuals emerge only when a counter selects a reticule with the requisite number of cells, so more than three circles presupposes circles where bare circles does not.

Main definitions

• Determiner: what a range assigner does at ⟨e⟩#, counting, measuring or either, and whether it also assigns range to ⟨e⟩div.
• Nominal: a nominal by its determiner, if any, and its plural inflection, with Divided and WellFormed, the two principles of range assignment.
• IsDivision, count: a reticule over stuff, a finset of cells, and the number of its complete cells.
• status: the mereological type a nominal spine composes bottom-up.

Main results

• wellFormed_counter_iff, not_wellFormed_of_divides, wellFormed_measure_iff, wellFormed_neutral: the distribution of the determiner classes derived from range assignment.
• sup'_mem: divided stuff is still stuff, which is SupClosed.finsetSup'_mem.
• exists_division_without_units, exists_unit_of_count_pos: individuals emerge at ⟨e⟩#, not at ⟨e⟩div.
• q_below_num: dividing feeds counting and nothing divides a quantity, the order the functional sequence records.

Implementation notes

The two open values ⟨e⟩div and ⟨e⟩# are the heads Q and Num of the substrate's nominal sequence. The existential closure and generic binding of ⟨e⟩d, the Hebrew and Chinese systems and the measure phrases of the later chapters are not formalized.

References

• [Bor05]
• [Kri98]
• [Chi98]

Range assignment to the two open values

inductive Borer2005.Quantity : Type

The range a determiner assigns to ⟨e⟩#, which is a count over the cells of a division, a measure over undivided mass, or either.

• count : Quantity
• measure : Quantity
• either : Quantity

@[instance_reducible]

instance Borer2005.instDecidableEqQuantity : DecidableEq Quantity

Equations

• Borer2005.instDecidableEqQuantity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Borer2005.instReprQuantity.repr : Quantity → ℕ → Std.Format

Equations

• Borer2005.instReprQuantity.repr Borer2005.Quantity.count prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2005.Quantity.count")).group prec✝
• Borer2005.instReprQuantity.repr Borer2005.Quantity.measure prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2005.Quantity.measure")).group prec✝
• Borer2005.instReprQuantity.repr Borer2005.Quantity.either prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2005.Quantity.either")).group prec✝

@[instance_reducible]

instance Borer2005.instReprQuantity : Repr Quantity

Equations

• Borer2005.instReprQuantity = { reprPrec := Borer2005.instReprQuantity.repr }

structure Borer2005.Determiner : Type

A range assigner from the functional lexicon, by the quantity it assigns to ⟨e⟩# and whether it also assigns range to ⟨e⟩div, as the portmanteau morphemes of (30) do.

• quantity : Quantity
• divides : Bool

def Borer2005.instDecidableEqDeterminer.decEq (x✝ x✝¹ : Determiner) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Borer2005.instDecidableEqDeterminer : DecidableEq Determiner

Equations

• Borer2005.instDecidableEqDeterminer = Borer2005.instDecidableEqDeterminer.decEq

def Borer2005.instReprDeterminer.repr : Determiner → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Borer2005.instReprDeterminer : Repr Determiner

Equations

• Borer2005.instReprDeterminer = { reprPrec := Borer2005.instReprDeterminer.repr }

def Borer2005.much : Determiner

much and little measure undivided mass (28).

Equations

• Borer2005.much = { quantity := Borer2005.Quantity.measure, divides := false }

def Borer2005.cardinal : Determiner

Cardinals other than one, zero included, and the plural-taking quantifiers several, many, few, a few and both are pure counters over a division established before them (30b).

Equations

• Borer2005.cardinal = { quantity := Borer2005.Quantity.count, divides := false }

def Borer2005.indefArticle : Determiner

a and one divide and count at once, the dividing and counting functions being one for singulars (30a).

Equations

• Borer2005.indefArticle = { quantity := Borer2005.Quantity.count, divides := true }

def Borer2005.every : Determiner

every and each are portmanteau dividers and counters over a bare stem (30c).

Equations

• Borer2005.every = { quantity := Borer2005.Quantity.count, divides := true }

def Borer2005.hungarianCardinal : Determiner

The cardinals of Hungarian, Turkish and Armenian divide as well as count (38a).

Equations

• Borer2005.hungarianCardinal = { quantity := Borer2005.Quantity.count, divides := true }

def Borer2005.all : Determiner

all, a lot of and most take a mass or a plural restriction and divide nothing (35).

Equations

• Borer2005.all = { quantity := Borer2005.Quantity.either, divides := false }

structure Borer2005.Nominal : Type

A nominal, by its determiner, if any, and whether it carries plural inflection, the head feature that assigns range to ⟨e⟩div.

• det : Option Determiner
• plural : Bool

def Borer2005.instDecidableEqNominal.decEq (x✝ x✝¹ : Nominal) : Decidable (x✝ = x✝¹)

Equations

• Borer2005.instDecidableEqNominal.decEq { det := a, plural := a_1 } { det := b, plural := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Borer2005.instDecidableEqNominal : DecidableEq Nominal

Equations

• Borer2005.instDecidableEqNominal = Borer2005.instDecidableEqNominal.decEq

@[instance_reducible]

instance Borer2005.instReprNominal : Repr Nominal

Equations

• Borer2005.instReprNominal = { reprPrec := Borer2005.instReprNominal.repr }

def Borer2005.instReprNominal.repr : Nominal → ℕ → Std.Format

Equations

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

def Borer2005.Nominal.Divided (n : Nominal) : Prop

⟨e⟩div has range, from plural inflection or from a dividing determiner, so the nominal is count; a bare stem is mass.

Equations

• n.Divided = (n.plural = true ∨ ∃ d ∈ n.det, d.divides = true)

def Borer2005.Nominal.WellFormed (n : Nominal) : Prop

The two principles of range assignment. No open value takes range twice, so plural inflection and a divider exclude each other, and a range assigner to ⟨e⟩# finds the restriction it needs, a counter a division and a measure undivided mass.

Equations

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

@[instance_reducible]

instance Borer2005.Nominal.instDecidableDivided (n : Nominal) : Decidable n.Divided

Equations

• n.instDecidableDivided = { decide := decide (n.plural = true) || decide (∃ d ∈ n.det, d.divides = true), reflects_decide := ⋯ }

@[instance_reducible]

instance Borer2005.Nominal.instDecidableWellFormed (n : Nominal) : Decidable n.WellFormed

Equations

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

theorem Borer2005.wellFormed_counter_iff {d : Determiner} (hq : d.quantity = Quantity.count) (hd : d.divides = false) (p : Bool) : { det := some d, plural := p }.WellFormed ↔ p = true

A pure counter needs the division that plural inflection supplies: three boys and several meats but not two meat or two boy (29).

theorem Borer2005.not_wellFormed_of_divides {d : Determiner} (hd : d.divides = true) : ¬{ det := some d, plural := true }.WellFormed

A divider never co-occurs with plural inflection, which would assign ⟨e⟩div range twice: a boy and every meat but not a boys or every boys, and no Hungarian cardinal with a plural (38).

theorem Borer2005.wellFormed_divider {d : Determiner} (hq : d.quantity = Quantity.count) (hd : d.divides = true) : { det := some d, plural := false }.WellFormed

A divider that counts takes a bare stem of either sort, a boy and one meat (30a).

theorem Borer2005.wellFormed_measure_iff {d : Determiner} (hq : d.quantity = Quantity.measure) (hd : d.divides = false) (p : Bool) : { det := some d, plural := p }.WellFormed ↔ p = false

A measure takes undivided mass alone: much salt but not much boys (28).

theorem Borer2005.wellFormed_neutral {d : Determiner} (hq : d.quantity = Quantity.either) (hd : d.divides = false) (p : Bool) : { det := some d, plural := p }.WellFormed ∧ ({ det := some d, plural := p }.Divided ↔ p = true)

A determiner indifferent to the quantity takes mass and plurals alike, all meat and all boys, and on a bare stem yields no count reading, since it divides nothing (35).

theorem Borer2005.determiner_classes : ({ det := some much, plural := false }.WellFormed ∧ ¬{ det := some much, plural := true }.WellFormed) ∧ (¬{ det := some cardinal, plural := false }.WellFormed ∧ { det := some cardinal, plural := true }.WellFormed) ∧ ({ det := some indefArticle, plural := false }.WellFormed ∧ ¬{ det := some indefArticle, plural := true }.WellFormed) ∧ ({ det := some every, plural := false }.WellFormed ∧ ¬{ det := some every, plural := true }.WellFormed) ∧ ({ det := some all, plural := false }.WellFormed ∧ { det := some all, plural := true }.WellFormed) ∧ { det := some hungarianCardinal, plural := false }.WellFormed ∧ ¬{ det := some hungarianCardinal, plural := true }.WellFormed

The two principles derive the distribution of the determiner classes of (20) over bare stems and plurals.

Dividing without individuating

Assigning range to ⟨e⟩div superimposes reticules on a mass denotation; a reticule carves cells, none of which need be a canonical unit, and the counter at ⟨e⟩# selects among the reticules one with the number of complete cells it requires.

def Borer2005.IsDivision {α : Type u_1} (P : α → Prop) (d : Finset α) : Prop

A finset of cells is a division of the P-stuff when every cell is carved from it.

Equations

• Borer2005.IsDivision P d = ∀ x ∈ d, P x

theorem Borer2005.sup'_mem {α : Type u_1} {P : α → Prop} [SemilatticeSup α] (hCum : Mereology.CUM P) {d : Finset α} (hne : d.Nonempty) (hd : IsDivision P d) : P (d.sup' hne id)

Divided stuff is still stuff: the sum of the cells of a cumulative root satisfies the root, apples plus apples being apples, the cumulativity bare plurals share with mass nouns.

theorem Borer2005.exists_division_without_units {α : Type u_1} {P : α → Prop} (unit : α → Prop) (h : ∃ (x : α), P x ∧ ¬unit x) : ∃ (d : Finset α), IsDivision P d ∧ d.Nonempty ∧ ∀ x ∈ d, ¬unit x

Plural marking presupposes no singulars: whenever the stuff has a noncanonical portion, some nonempty division contains no unit, the reticules behind zero apples and 0.5 apples.

def Borer2005.count {α : Type u_1} (unit : α → Prop) [DecidablePred unit] (d : Finset α) : ℕ

The number of complete cells of a division, those that are canonical units, by which a counter at ⟨e⟩# selects a reticule.

Equations

• Borer2005.count unit d = (Finset.filter unit d).card

theorem Borer2005.exists_unit_of_count_pos {α : Type u_1} {P : α → Prop} (unit : α → Prop) [DecidablePred unit] {d : Finset α} (hd : IsDivision P d) (h : 0 < count unit d) : ∃ (x : α), unit x ∧ P x

Individuals emerge at ⟨e⟩#: a division with a positive count contains a canonical unit of the stuff, so more than three circles cannot be true without individual circles, though bare circles can.

The nominal spine

inductive Borer2005.Status : Type

The mereological type of a nominal denotation along the spine, which is cumulative stuff, divided stuff, or a quantity.

• stuff : Status
• divided : Status
• quantity : Status

@[instance_reducible]

instance Borer2005.instDecidableEqStatus : DecidableEq Status

Equations

• Borer2005.instDecidableEqStatus x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Borer2005.instReprStatus.repr : Status → ℕ → Std.Format

Equations

• Borer2005.instReprStatus.repr Borer2005.Status.stuff prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2005.Status.stuff")).group prec✝
• Borer2005.instReprStatus.repr Borer2005.Status.divided prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2005.Status.divided")).group prec✝
• Borer2005.instReprStatus.repr Borer2005.Status.quantity prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Borer2005.Status.quantity")).group prec✝

@[instance_reducible]

instance Borer2005.instReprStatus : Repr Status

Equations

• Borer2005.instReprStatus = { reprPrec := Borer2005.instReprStatus.repr }

def Borer2005.steps : Minimalist.Cat → Status → Option Status

The semantically active heads are ⟨e⟩div, the head Q, which divides stuff, and ⟨e⟩#, the head Num, which counts a division or measures undivided stuff; the other heads are transparent, and nothing divides a quantity.

Equations

• Borer2005.steps Minimalist.Cat.Q Borer2005.Status.stuff = some Borer2005.Status.divided
• Borer2005.steps Minimalist.Cat.Q x✝ = none
• Borer2005.steps Minimalist.Cat.Num Borer2005.Status.quantity = none
• Borer2005.steps Minimalist.Cat.Num x✝ = some Borer2005.Status.quantity
• Borer2005.steps x✝¹ x✝ = some x✝

def Borer2005.status (spine : List Minimalist.Cat) : Option Status

The type of a spine's denotation, composed bottom-up from cumulative stuff, or none when a head has no well-typed input.

Equations

• Borer2005.status spine = List.foldl (fun (s : Option Borer2005.Status) (c : Minimalist.Cat) => s.bind (Borer2005.steps c)) (some Borer2005.Status.stuff) spine

theorem Borer2005.q_below_num : status [Minimalist.Cat.N, Minimalist.Cat.n, Minimalist.Cat.Q, Minimalist.Cat.Num] = some Status.quantity ∧ status [Minimalist.Cat.N, Minimalist.Cat.n, Minimalist.Cat.Num, Minimalist.Cat.Q] = none

Dividing feeds counting and nothing divides a quantity, so the only well-typed order puts the dividing head below the quantity head, the order (27) draws.

theorem Borer2005.quantified_mass : status [Minimalist.Cat.N, Minimalist.Cat.n, Minimalist.Cat.Num] = some Status.quantity

The quantity head alone over undivided stuff is quantified mass, much salt projecting no classifier phrase (28).

theorem Borer2005.status_truncations : status [Minimalist.Cat.N, Minimalist.Cat.n] = some Status.stuff ∧ status [Minimalist.Cat.N, Minimalist.Cat.n, Minimalist.Cat.Q] = some Status.divided

Of the truncations, the bare stem is mass and the divided stem a bare plural (27).

theorem Borer2005.fValue_Q_lt_Num : Minimalist.Cat.Q.fValue < Minimalist.Cat.Num.fValue

The functional sequence places the dividing head below the quantity head.