Number features as region operators

Harbour decomposes grammatical number into three features acting on a region of a join-semilattice of individuals. [±atomic] keeps the region's atoms or the rest, [±minimal] its minimal elements or the rest, and [±additive] the elements whose join with any element of a subregion stays in it. Features compose by application, so the dual is [+minimal] applied to [−atomic], and the trial [+minimal] applied to [−minimal] applied to [−atomic]. Which bundle a value names depends on the number system: the plural of English is [−atomic], that of a language with a dual [−atomic, −minimal]. The systems a parameter setting generates, and the cells of their bundles, are computed in Studies/Harbour2014.lean.

Main definitions

• Number.atomsOf, Number.nonAtomsOf: the [+atomic] and [−atomic] regions.
• Number.nonMinimalOf: the [−minimal] region, the [+minimal] one being Mereology.atomize.
• Number.dualOf: the [−atomic, +minimal] region, the dual.
• Number.additiveIn: the [+additive] elements of a subregion.

Main results

• Number.additive_subregion_is_cum: the [+additive] elements form a cumulative predicate.
• Number.singular_subset_minimal: in a region without the null individual an atom is minimal, so [+atomic] entails [+minimal].
• Number.atomize_eq_of_atoms: [+minimal] applied to a region of atoms changes nothing.
• Number.not_nonMinimalOf_atomize: [−minimal] applied after [+minimal] is empty.

Implementation notes

Harbour presupposes that the element lies in the region ([±minimal]) and in the subregion ([±additive]); here these are conjuncts. Minimality is mathlib's Minimal, exposed as Mereology.atomize. With a null individual in the region an atom has a proper part, so [+atomic] no longer entails [+minimal]; Martí's revision of [±minimal] for that case, which counts only parts of nonzero numerosity, is not modelled. [−atomic] gives the exclusive plural. Whether the inclusive reading in downward-entailing contexts is a second meaning or an implicature is open: Martí argues for the former within Harbour's typology, and the experiments of Tieu, Bill, Romoli and Crain favour the latter (Studies/TieuEtAl2020.lean). The carrier is any join-semilattice, so the operators apply to events as well as individuals.

References

• [Har14a] (9) and (10), p. 195; (20) and (21), p. 202; (30), p. 210
• [Mar20a] pp. 3:30–3:31
• [Mar22] (8) and (9), pp. 217–218; (40), p. 224
• [TBRC20]
• [Lin83]

def Number.additiveIn {D : Type u_1} [SemilatticeSup D] (Q : D → Prop) (x : D) : Prop

x is additive in the region Q if Q x and Q (x ⊔ y) for every y with Q y, Harbour's [+additive].

Equations

• Number.additiveIn Q x = (Q x ∧ ∀ (y : D), Q y → Q (x ⊔ y))

theorem Number.additiveIn_sup {D : Type u_1} [SemilatticeSup D] {Q : D → Prop} {x y : D} (hx : additiveIn Q x) (hy : additiveIn Q y) : additiveIn Q (x ⊔ y)

theorem Number.additive_subregion_is_cum {D : Type u_1} [SemilatticeSup D] (Q : D → Prop) : Mereology.CUM (additiveIn Q)

The additive elements of a region form a cumulative predicate.

@[instance_reducible]

instance Number.instDecidableAdditiveInOfFintypeOfDecidablePred {D : Type u_1} [SemilatticeSup D] {Q : D → Prop} [Fintype D] [DecidablePred Q] (x : D) : Decidable (additiveIn Q x)

Equations

• Number.instDecidableAdditiveInOfFintypeOfDecidablePred x = decidable_of_iff (Q x ∧ ∀ (y : D), Q y → Q (x ⊔ y)) ⋯

@[reducible, inline]

abbrev Number.atomsOf {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (x : D) : Prop

The atoms of P form Harbour's [+atomic] region, the singular.

Equations

• Number.atomsOf P x = (P x ∧ Mereology.Atom x)

@[reducible, inline]

abbrev Number.nonAtomsOf {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (x : D) : Prop

The non-atoms of P form Harbour's [−atomic] region.

Equations

• Number.nonAtomsOf P x = (P x ∧ ¬Mereology.Atom x)

@[reducible, inline]

abbrev Number.nonMinimalOf {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (x : D) : Prop

The non-minimal elements of P form Harbour's [−minimal] region, the complement in P of atomize P.

Equations

• Number.nonMinimalOf P x = (P x ∧ ¬Mereology.atomize P x)

theorem Number.not_nonMinimalOf_atomize {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (x : D) : ¬nonMinimalOf (Mereology.atomize P) x

The minimal elements of a region of minimal elements are all of them, so (−minimal(+minimal(P))) is empty.

@[reducible, inline]

abbrev Number.dualOf {D : Type u_1} [SemilatticeSup D] (P : D → Prop) : D → Prop

The minimal non-atoms of P form the [−atomic, +minimal] region, the dual.

Equations

• Number.dualOf P = Mereology.atomize (Number.nonAtomsOf P)

theorem Number.singular_subset_minimal {D : Type u_1} [SemilatticeSup D] {P : D → Prop} (hP : ∀ (y : D), P y → ¬IsBot y) {x : D} (hx : atomsOf P x) : Mereology.atomize P x

An atom of a region excluding the null individual is minimal in it, so [+atomic] entails [+minimal].

theorem Number.atomize_eq_of_atoms {D : Type u_1} [SemilatticeSup D] {P : D → Prop} (hAll : ∀ (x : D), P x → Mereology.Atom x) : Mereology.atomize P = P

Over a region of atoms [+minimal] selects everything, so (+minimal(+atomic(P))) is (+atomic(P)), the singular.