Harbour (2014): Paucity, Abundance, and the Theory of Number

Harbour characterizes the approximative numbers, paucal and greater plural, by a feature [±additive] of additive closure, beside the [±atomic] and [±minimal] that give the exact numbers. Each feature acts on a lattice of atoms and their sums, and the same two parameters govern all three: whether a feature is active on Number⁰ (22) and whether its two values may cooccur (23). A sociosemantic convention fixes the height of the cut [±additive] induces (14). A parameter setting generates a number system, the feature bundles with nonempty denotation, and the typology of Table 3 and the implications of Table 1 are claims about these systems.

Main definitions

• Setting, Bundle, Convention: parameter settings, feature bundles, and the placement of the cuts.
• Setting.cell: the region of a person lattice a bundle denotes in a setting.
• Setting.system: the number system a setting generates.
• PlusAdditive: the [+additive] elements of a region cut horizontally.
• table1, SatisfiesTable1: the implicational universals of Table 1.
• Generates, Requires: the legitimate settings as a formal context, and the order of its attribute concepts that (34) reads off them, one number requiring another.

Main results

• atomize_nonMinimalOf_iterate: the successor-like function (31).
• not_additiveIn_band, additiveIn_firstPerson_iff: below a cut no element of the third-person lattice is [+additive], and on the first-person lattice only the speaker is.
• not_ordConnected_plusAdditive_firstPerson: {±additive} alone cuts the first-person lattice nonconvexly, against the convexity condition (32).
• filter_cell_eq_system: on every person lattice with infinitely many atoms and for every placement of the cuts above four atoms, the bundles with nonempty cells form Setting.system.
• table3_generated: the systems of Table 3, with Corbett's records of its example languages.
• satisfiesTable1_toSystem_iff: Table 1 holds of every legitimate setting but {±additive(*), ±minimal*}, two lacunae whose unit augmented has no augmented.
• requires_of_mem_derivedImplications, not_requires_unitAugmented_augmented: the order the settings induce by (34) has the single implications of Table 1 but the unit augmented's.
• mem_of_requires_corbett: every system of Corbett's choices is a lower set of that order.
• meleFila_cell_plural, meleFila_classes: Mele-Fila's plural lies between the two cuts and shares a form with each neighbour (Table 4).

Implementation notes

• A bundle is a Finset of signed features, so the axiom of extension (27) is built in, and it is interpreted in the order (28); its cell is its denotation less the more specific bundles', as the plural of Figure 7 is Q+ \ Q′.
• card carries the features from a person lattice to its strata, where [±atomic] and [±minimal] leave one stratum or every stratum from one up (Strata) and [±additive] cuts horizontally. The strata above four only matter through the cuts, so collapse reduces every placement of the cuts to the cuts at five and six, where Setting.system is computed. The labels (p. 201) follow Table 3 and its note b.

TODO

• Banyun's greater and greatest plurals (Table 3, (18)) have no Number value, (24) omitting the greatest plural.

References

• [Har14a]
• [Cor00]
• [Gar04]

Person lattices and their strata (§2, (12))

theorem Harbour2014.atom_iff_eq_one {k : ℕ} : Mereology.Atom k ↔ k = 1

On the strata ℕ the atom is 1.

def Harbour2014.region {α : Type u_1} (B : Finset α) (S : ℕ → Prop) (s : Finset α) : Prop

A region of the person lattice over B holds of the sums containing B whose number of atoms satisfies S, a union of strata (12).

Equations

• Harbour2014.region B S s = (B ⊆ s ∧ S s.card)

theorem Harbour2014.atomize_region {α : Type u_1} {B : Finset α} {S : ℕ → Prop} (hS : ∀ (k : ℕ), S k → B.card ≤ k) : Mereology.atomize (region B S) = region B (Mereology.atomize S)

card carries the minimal elements of a region to its least strata, since between B and a sum lies a sum of every intermediate size.

theorem Harbour2014.atom_iff_card {α : Type u_1} {s : Finset α} : Mereology.Atom s ↔ Mereology.Atom s.card

The atoms of the powerset lattice are the sets of one atom.

theorem Harbour2014.atomsOf_region {α : Type u_1} {B : Finset α} {S : ℕ → Prop} [DecidableEq α] : Number.atomsOf (region B S) = region B (Number.atomsOf S)

theorem Harbour2014.nonAtomsOf_region {α : Type u_1} {B : Finset α} {S : ℕ → Prop} [DecidableEq α] : Number.nonAtomsOf (region B S) = region B (Number.nonAtomsOf S)

theorem Harbour2014.nonMinimalOf_region {α : Type u_1} {B : Finset α} {S : ℕ → Prop} [DecidableEq α] (hS : ∀ (k : ℕ), S k → B.card ≤ k) : Number.nonMinimalOf (region B S) = region B (Number.nonMinimalOf S)

The successor-like function (§4.4)

theorem Harbour2014.atomize_nonMinimalOf_iterate {α : Type u_1} [DecidableEq α] (n : ℕ) (s : Finset α) : Mereology.atomize (Number.nonMinimalOf^[n] (Number.nonAtomsOf Finset.Nonempty)) s ↔ s.card = n + 2

(+minimal(−minimalⁿ(−atomic(P)))) holds of exactly the sums of n + 2 atoms, the successor-like function (31); n = 0 gives the dual of (30) and n = 1 the trial.

theorem Harbour2014.atomize_atomsOf {α : Type u_1} [DecidableEq α] (s : Finset α) : Mereology.atomize (Number.atomsOf Finset.Nonempty) s ↔ s.card = 1

(+minimal(+atomic(P))) holds of exactly the atoms, the singular of (30).

Orders of composition (§§3.3, 4.1, 4.3)

theorem Harbour2014.not_atomsOf_nonAtomsOf {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (x : D) : ¬Number.atomsOf (Number.nonAtomsOf P) x

(αatomic(ᾱatomic(P))) is empty, so [±atomic]* adds nothing (§4.1, n. 15).

theorem Harbour2014.not_atomsOf_nonMinimalOf {D : Type u_1} [SemilatticeSup D] {P : D → Prop} (hP : ∀ (y : D), P y → ¬IsBot y) (x : D) : ¬Number.atomsOf (Number.nonMinimalOf P) x

(+atomic(−minimal(P))) is empty when P excludes the null individual, since an atom of P is minimal in it (§4.3).

[±additive] and horizontal cuts (§3.1)

def Harbour2014.Band {α : Type u_1} (lo hi : ℕ) (s : Finset α) : Prop

A band holds of the sums of at least lo and fewer than hi atoms.

Equations

• Harbour2014.Band lo hi s = (lo ≤ s.card ∧ s.card < hi)

theorem Harbour2014.not_additiveIn_band {α : Type u_1} [DecidableEq α] [Infinite α] {lo hi : ℕ} (hlo : 1 ≤ lo) (s : Finset α) : ¬Number.additiveIn (Band lo hi) s

No element of a band above the null individual is additive in it, given infinitely many atoms, since two of its elements can always sum past its upper bound. So the bounded region below a cut of the third-person lattice is [−additive] throughout (10), and (+additive(−additive(P))) is unsatisfiable (§3.3).

theorem Harbour2014.additiveIn_le_card {α : Type u_1} [DecidableEq α] {c : ℕ} {s : Finset α} (hs : c ≤ s.card) : Number.additiveIn (fun (x : Finset α) => c ≤ x.card) s

Every element above a cut is additive in the region above it (10), whose complement below the cut is thereby complement-complete (11).

theorem Harbour2014.additiveIn_le_card' {α : Type u_1} [DecidableEq α] {i : α} {c : ℕ} {s : Finset α} (hi : i ∈ s) (hs : c ≤ s.card) : Number.additiveIn (fun (t : Finset α) => i ∈ t ∧ c ≤ t.card) s

Likewise an element above a cut that contains a given atom is additive among such elements.

theorem Harbour2014.additiveIn_atomize_superset {α : Type u_1} [DecidableEq α] (B : Finset α) : Number.additiveIn (Mereology.atomize fun (x : Finset α) => B ⊆ x) B

The least element of the person lattice over B, the sums containing B, is B itself, which is additive among the least elements, so the first- and second-person singular and the inclusive minimal are [+additive] (n. 23).

theorem Harbour2014.not_additiveIn_atomize_nonempty {α : Type u_1} [DecidableEq α] [Nontrivial α] (s : Finset α) : ¬Number.additiveIn (Mereology.atomize Finset.Nonempty) s

On the third-person lattice the singular is [−additive], since two atoms join to a dyad (n. 23).

Convexity (§4.5)

def Harbour2014.PlusAdditive {α : Type u_1} [DecidableEq α] (c : ℕ) (P : Finset α → Prop) (s : Finset α) : Prop

An element of a region P cut at c is [+additive] (10) when it is additive in the bounded region below the cut or in the unbounded region above it.

Equations

• Harbour2014.PlusAdditive c P s = (Number.additiveIn (fun (t : Finset α) => P t ∧ t.card < c) s ∨ Number.additiveIn (fun (t : Finset α) => P t ∧ c ≤ t.card) s)

theorem Harbour2014.plusAdditive_nonempty_iff {α : Type u_1} [DecidableEq α] [Infinite α] {c : ℕ} (hc : 1 ≤ c) (s : Finset α) : PlusAdditive c Finset.Nonempty s ↔ c ≤ s.card

On the third-person lattice, with infinitely many atoms, the [+additive] elements are those above the cut.

theorem Harbour2014.ordConnected_plusAdditive_nonempty {α : Type u_1} [DecidableEq α] [Infinite α] {c : ℕ} (hc : 1 ≤ c) : {s : Finset α | PlusAdditive c Finset.Nonempty s}.OrdConnected

So {±additive} cuts the third-person lattice convexly (33), into paucal and plural.

theorem Harbour2014.additiveIn_firstPerson_iff {α : Type u_1} [DecidableEq α] [Infinite α] {i : α} {c : ℕ} (hc : 2 ≤ c) (s : Finset α) : Number.additiveIn (fun (t : Finset α) => i ∈ t ∧ t.card < c) s ↔ s = {i}

On the first-person exclusive lattice, the sums containing the speaker i, the speaker atom is the only element additive below a cut (Figure 8), being the lattice's bottom.

theorem Harbour2014.not_ordConnected_plusAdditive_firstPerson {α : Type u_1} [DecidableEq α] [Infinite α] (i : α) {c : ℕ} (hc : 3 ≤ c) : ¬{s : Finset α | PlusAdditive c (fun (x : Finset α) => i ∈ x) s}.OrdConnected

So {±additive} cuts the first-person lattice nonconvexly, a [−additive] paucal lying between the [+additive] speaker and a [+additive] plural (p. 212), and by the convexity condition (32), after [Gar04], [±additive] is never a language's sole number feature.

Parameters (§§4.1–4.3)

inductive Harbour2014.Feature : Type

Harbour's number features are [±atomic], [±minimal] and [±additive].

• atomic : Feature
• minimal : Feature
• additive : Feature

@[instance_reducible]

instance Harbour2014.instDecidableEqFeature : DecidableEq Feature

Equations

• Harbour2014.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Harbour2014.instFintypeFeature : Fintype Feature

Equations

• Harbour2014.instFintypeFeature = { elems := { val := ↑Harbour2014.Feature.enumList, nodup := Harbour2014.Feature.enumList_nodup }, complete := Harbour2014.instFintypeFeature._proof_1 }

@[instance_reducible]

instance Harbour2014.instReprFeature : Repr Feature

Equations

• Harbour2014.instReprFeature = { reprPrec := Harbour2014.instReprFeature.repr }

def Harbour2014.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Harbour2014.instReprFeature.repr Harbour2014.Feature.atomic prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Harbour2014.Feature.atomic")).group prec✝

inductive Harbour2014.Activation : Type

A feature on Number⁰ is inactive, active (22), or recursive, its two values allowed to cooccur (23), written [±F]*.

• inactive : Activation
• active : Activation
• recursive : Activation

@[instance_reducible]

instance Harbour2014.instDecidableEqActivation : DecidableEq Activation

Equations

• Harbour2014.instDecidableEqActivation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Harbour2014.instFintypeActivation : Fintype Activation

Equations

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

@[instance_reducible]

instance Harbour2014.instReprActivation : Repr Activation

Equations

• Harbour2014.instReprActivation = { reprPrec := Harbour2014.instReprActivation.repr }

def Harbour2014.instReprActivation.repr : Activation → ℕ → Std.Format

Equations

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

def Harbour2014.Activation.signs : Activation → List (Finset Bool)

Under an activation a bundle carries no value of [±F], one, or under recursion both, and no more by the axiom of extension (27).

Equations

• Harbour2014.Activation.inactive.signs = [∅]
• Harbour2014.Activation.active.signs = [{true}, {false}]
• Harbour2014.Activation.recursive.signs = [{true}, {false}, {true, false}]

structure Harbour2014.Setting : Type

A parameter setting fixes the activation of each feature.

• atomic : Activation

  The activation of [±atomic].

• minimal : Activation

  The activation of [±minimal].

• additive : Activation

  The activation of [±additive].

def Harbour2014.instDecidableEqSetting.decEq (x✝ x✝¹ : Setting) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Harbour2014.instDecidableEqSetting : DecidableEq Setting

Equations

• Harbour2014.instDecidableEqSetting = Harbour2014.instDecidableEqSetting.decEq

@[instance_reducible]

instance Harbour2014.instFintypeSetting : Fintype Setting

Equations

• Harbour2014.instFintypeSetting = Fintype.ofEquiv ((_ : Harbour2014.Activation) × (_ : Harbour2014.Activation) × Harbour2014.Activation) Harbour2014.Setting.proxyTypeEquiv

@[instance_reducible]

instance Harbour2014.instReprSetting : Repr Setting

Equations

• Harbour2014.instReprSetting = { reprPrec := Harbour2014.instReprSetting.repr }

def Harbour2014.instReprSetting.repr : Setting → ℕ → Std.Format

Equations

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

@[reducible, inline]

abbrev Harbour2014.Bundle : Type

A feature bundle is the set of its signed features, (F, true) standing for +F (§2.3).

Equations

• Harbour2014.Bundle = Finset (Harbour2014.Feature × Bool)

def Harbour2014.Setting.bundles (σ : Setting) : List Bundle

A bundle of a setting values every active feature once and a recursive one once or twice.

Equations

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

def Harbour2014.Setting.Legitimate (σ : Setting) : Prop

A setting is legitimate unless [±additive] is its sole feature, which the convexity condition (32) rules out (§4.5, not_ordConnected_plusAdditive_firstPerson).

Equations

• σ.Legitimate = (σ.additive ≠ Harbour2014.Activation.inactive → σ.atomic ≠ Harbour2014.Activation.inactive ∨ σ.minimal ≠ Harbour2014.Activation.inactive)

@[instance_reducible]

instance Harbour2014.Setting.instDecidableLegitimate (σ : Setting) : Decidable σ.Legitimate

Equations

• σ.instDecidableLegitimate = id inferInstance

inductive Harbour2014.Height : Type

A conventionalized cut (14) is low, bounding paucals, or high, bounding greater plurals.

• low : Height
• high : Height

@[instance_reducible]

instance Harbour2014.instDecidableEqHeight : DecidableEq Height

Equations

• Harbour2014.instDecidableEqHeight x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Harbour2014.instFintypeHeight : Fintype Height

Equations

• Harbour2014.instFintypeHeight = { elems := { val := ↑Harbour2014.Height.enumList, nodup := Harbour2014.Height.enumList_nodup }, complete := Harbour2014.instFintypeHeight._proof_1 }

def Harbour2014.instReprHeight.repr : Height → ℕ → Std.Format

Equations

• Harbour2014.instReprHeight.repr Harbour2014.Height.low prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Harbour2014.Height.low")).group prec✝
• Harbour2014.instReprHeight.repr Harbour2014.Height.high prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Harbour2014.Height.high")).group prec✝

@[instance_reducible]

instance Harbour2014.instReprHeight : Repr Height

Equations

• Harbour2014.instReprHeight = { reprPrec := Harbour2014.instReprHeight.repr }

inductive Harbour2014.Convention : Type

The sociosemantic convention (14) places no cut without [±additive], one cut with it, and under recursion a low cut and a second cut above it (§3.3). Two high cuts, Banyun's greater and greatest plurals, are left out.

• none : Convention
• one (h : Height) : Convention
• two (h : Height) : Convention

@[instance_reducible]

instance Harbour2014.instDecidableEqConvention : DecidableEq Convention

Equations

• Harbour2014.instDecidableEqConvention = Harbour2014.instDecidableEqConvention.decEq

def Harbour2014.instDecidableEqConvention.decEq (x✝ x✝¹ : Convention) : Decidable (x✝ = x✝¹)

Equations

• Harbour2014.instDecidableEqConvention.decEq Harbour2014.Convention.none Harbour2014.Convention.none = isTrue ⋯
• Harbour2014.instDecidableEqConvention.decEq Harbour2014.Convention.none (Harbour2014.Convention.one h) = isFalse ⋯
• Harbour2014.instDecidableEqConvention.decEq Harbour2014.Convention.none (Harbour2014.Convention.two h) = isFalse ⋯
• Harbour2014.instDecidableEqConvention.decEq (Harbour2014.Convention.one h) Harbour2014.Convention.none = isFalse ⋯
• Harbour2014.instDecidableEqConvention.decEq (Harbour2014.Convention.one a) (Harbour2014.Convention.one b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Harbour2014.instDecidableEqConvention.decEq (Harbour2014.Convention.one h) (Harbour2014.Convention.two h_1) = isFalse ⋯
• Harbour2014.instDecidableEqConvention.decEq (Harbour2014.Convention.two h) Harbour2014.Convention.none = isFalse ⋯
• Harbour2014.instDecidableEqConvention.decEq (Harbour2014.Convention.two h) (Harbour2014.Convention.one h_1) = isFalse ⋯
• Harbour2014.instDecidableEqConvention.decEq (Harbour2014.Convention.two a) (Harbour2014.Convention.two b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Harbour2014.instFintypeConvention : Fintype Convention

Equations

• Harbour2014.instFintypeConvention = Fintype.ofEquiv (Unit ⊕ Harbour2014.Height ⊕ Harbour2014.Height) Harbour2014.Convention.proxyTypeEquiv

def Harbour2014.instReprConvention.repr : Convention → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Harbour2014.instReprConvention : Repr Convention

Equations

• Harbour2014.instReprConvention = { reprPrec := Harbour2014.instReprConvention.repr }

def Harbour2014.Convention.Fits : Convention → Activation → Prop

A convention fits an activation of [±additive] when it has as many cuts.

Equations

• Harbour2014.Convention.none.Fits Harbour2014.Activation.inactive = True
• (Harbour2014.Convention.one h).Fits Harbour2014.Activation.active = True
• (Harbour2014.Convention.two h).Fits Harbour2014.Activation.recursive = True
• x✝¹.Fits x✝ = False

@[instance_reducible]

instance Harbour2014.instDecidableFits (c : Convention) (a : Activation) : Decidable (c.Fits a)

Equations

• Harbour2014.instDecidableFits Harbour2014.Convention.none Harbour2014.Activation.inactive = isTrue trivial
• Harbour2014.instDecidableFits (Harbour2014.Convention.one h) Harbour2014.Activation.active = isTrue trivial
• Harbour2014.instDecidableFits (Harbour2014.Convention.two h) Harbour2014.Activation.recursive = isTrue trivial
• Harbour2014.instDecidableFits Harbour2014.Convention.none Harbour2014.Activation.active = isFalse Harbour2014.instDecidableFits._proof_1
• Harbour2014.instDecidableFits Harbour2014.Convention.none Harbour2014.Activation.recursive = isFalse Harbour2014.instDecidableFits._proof_2
• Harbour2014.instDecidableFits (Harbour2014.Convention.one h) Harbour2014.Activation.inactive = isFalse ⋯
• Harbour2014.instDecidableFits (Harbour2014.Convention.one h) Harbour2014.Activation.recursive = isFalse ⋯
• Harbour2014.instDecidableFits (Harbour2014.Convention.two h) Harbour2014.Activation.inactive = isFalse ⋯
• Harbour2014.instDecidableFits (Harbour2014.Convention.two h) Harbour2014.Activation.active = isFalse ⋯

def Harbour2014.Bundle.label (c : Convention) (b : Bundle) : Number

A bundle is labelled with the descriptive name of its number (p. 201), after Table 3.

Equations

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

The strata of a bundle (§§2.2, 4.3)

inductive Harbour2014.Strata : Type

A region of strata is empty, the stratum n, or every positive stratum from n up.

• empty : Strata
• point (n : ℕ) : Strata
• ray (n : ℕ) : Strata

@[instance_reducible]

instance Harbour2014.instDecidableEqStrata : DecidableEq Strata

Equations

• Harbour2014.instDecidableEqStrata = Harbour2014.instDecidableEqStrata.decEq

def Harbour2014.instDecidableEqStrata.decEq (x✝ x✝¹ : Strata) : Decidable (x✝ = x✝¹)

Equations

• Harbour2014.instDecidableEqStrata.decEq Harbour2014.Strata.empty Harbour2014.Strata.empty = isTrue ⋯
• Harbour2014.instDecidableEqStrata.decEq Harbour2014.Strata.empty (Harbour2014.Strata.point n) = isFalse ⋯
• Harbour2014.instDecidableEqStrata.decEq Harbour2014.Strata.empty (Harbour2014.Strata.ray n) = isFalse ⋯
• Harbour2014.instDecidableEqStrata.decEq (Harbour2014.Strata.point n) Harbour2014.Strata.empty = isFalse ⋯
• Harbour2014.instDecidableEqStrata.decEq (Harbour2014.Strata.point a) (Harbour2014.Strata.point b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• Harbour2014.instDecidableEqStrata.decEq (Harbour2014.Strata.point n) (Harbour2014.Strata.ray n_1) = isFalse ⋯
• Harbour2014.instDecidableEqStrata.decEq (Harbour2014.Strata.ray n) Harbour2014.Strata.empty = isFalse ⋯
• Harbour2014.instDecidableEqStrata.decEq (Harbour2014.Strata.ray n) (Harbour2014.Strata.point n_1) = isFalse ⋯
• Harbour2014.instDecidableEqStrata.decEq (Harbour2014.Strata.ray a) (Harbour2014.Strata.ray b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Harbour2014.instReprStrata : Repr Strata

Equations

• Harbour2014.instReprStrata = { reprPrec := Harbour2014.instReprStrata.repr }

def Harbour2014.instReprStrata.repr : Strata → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Harbour2014.instReprStrata.repr Harbour2014.Strata.empty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Harbour2014.Strata.empty")).group prec✝

def Harbour2014.Strata.Mem : Strata → ℕ → Prop

s.Mem k holds when k is a stratum of s.

Equations

• Harbour2014.Strata.empty.Mem x✝ = False
• (Harbour2014.Strata.point n).Mem x✝ = (x✝ = n)
• (Harbour2014.Strata.ray n).Mem x✝ = (max n 1 ≤ x✝)

@[instance_reducible]

instance Harbour2014.Strata.instDecidablePredNatMem (s : Strata) : DecidablePred s.Mem

Equations

• Harbour2014.Strata.empty.instDecidablePredNatMem = fun (x : ℕ) => instDecidableFalse
• (Harbour2014.Strata.point n).instDecidablePredNatMem = fun (k : ℕ) => { decide := k.beq n, reflects_decide := ⋯ }
• (Harbour2014.Strata.ray n).instDecidablePredNatMem = fun (k : ℕ) => { decide := (max n 1).ble k, reflects_decide := ⋯ }

def Harbour2014.Strata.atomic : Strata → Strata

[+atomic] keeps the stratum one.

Equations

• (Harbour2014.Strata.point n).atomic = if n = 1 then Harbour2014.Strata.point 1 else Harbour2014.Strata.empty
• (Harbour2014.Strata.ray n).atomic = if n ≤ 1 then Harbour2014.Strata.point 1 else Harbour2014.Strata.empty
• Harbour2014.Strata.empty.atomic = Harbour2014.Strata.empty

def Harbour2014.Strata.nonAtomic : Strata → Strata

[−atomic] drops the stratum one.

Equations

• (Harbour2014.Strata.point n).nonAtomic = if n = 1 then Harbour2014.Strata.empty else Harbour2014.Strata.point n
• (Harbour2014.Strata.ray n).nonAtomic = Harbour2014.Strata.ray (max n 2)
• Harbour2014.Strata.empty.nonAtomic = Harbour2014.Strata.empty

def Harbour2014.Strata.minimal : Strata → Strata

[+minimal] keeps the least stratum.

Equations

• (Harbour2014.Strata.ray n).minimal = Harbour2014.Strata.point (max n 1)
• x✝.minimal = x✝

def Harbour2014.Strata.nonMinimal : Strata → Strata

[−minimal] drops the least stratum.

Equations

• (Harbour2014.Strata.ray n).nonMinimal = Harbour2014.Strata.ray (max n 1 + 1)
• x✝.nonMinimal = Harbour2014.Strata.empty

def Harbour2014.Strata.bound : Strata → ℕ

Membership in a region of strata is constant from its bound on.

Equations

• Harbour2014.Strata.empty.bound = 0
• (Harbour2014.Strata.point n).bound = n + 1
• (Harbour2014.Strata.ray n).bound = max n 1

theorem Harbour2014.Strata.atomsOf_mem (s : Strata) : Number.atomsOf s.Mem = s.atomic.Mem

theorem Harbour2014.Strata.nonAtomsOf_mem (s : Strata) : Number.nonAtomsOf s.Mem = s.nonAtomic.Mem

theorem Harbour2014.Strata.atomize_mem (s : Strata) : Mereology.atomize s.Mem = s.minimal.Mem

theorem Harbour2014.Strata.nonMinimalOf_mem (s : Strata) : Number.nonMinimalOf s.Mem = s.nonMinimal.Mem

theorem Harbour2014.Strata.mem_iff_of_bound_le {s : Strata} (hs : s.bound ≤ 4) {k : ℕ} (hk : 4 ≤ k) : s.Mem k ↔ s.Mem 4

def Harbour2014.Bundle.step {X : Type u_1} (b : Bundle) (v : Feature × Bool) (f : X → X) (x : X) : X

b.step v f applies f when the bundle b carries the signed feature v.

Equations

• b.step v f x = if v ∈ b then f x else x

def Harbour2014.Bundle.exact {D : Type u_1} [SemilatticeSup D] (b : Bundle) (P : D → Prop) : D → Prop

The region a bundle's [±atomic] and [±minimal] values select from P, in the order (28).

Equations

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

def Harbour2014.Bundle.strata (b : Bundle) (s : Strata) : Strata

The strata a bundle's [±atomic] and [±minimal] values select from s, in the order (28).

Equations

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

theorem Harbour2014.Bundle.exact_mem (b : Bundle) (s : Strata) : b.exact s.Mem = (b.strata s).Mem

theorem Harbour2014.Bundle.exact_le {D : Type u_1} [SemilatticeSup D] (b : Bundle) (P : D → Prop) {x : D} (h : b.exact P x) : P x

theorem Harbour2014.bound_strata_le (b : Bundle) (p : ℕ) : p ≤ 2 → (b.strata (Strata.ray p)).bound ≤ 4

The exact strata of every bundle on a person lattice over a base of at most two atoms change membership by the stratum four.

theorem Harbour2014.le_three_of_strata_eq_point (b : Bundle) {p : ℕ} (hp : p ≤ 2) {n : ℕ} (h : b.strata (Strata.ray p) = Strata.point n) : n ≤ 3

The axiom of extension caps the exact numbers at the trial and the unit augmented, three atoms on the third-person lattice and the inclusive one alike, so there is no dyad augmented (§4.2).

theorem Harbour2014.Bundle.exact_region {α : Type u_1} [DecidableEq α] {B : Finset α} (b : Bundle) {s : Strata} (hs : ∀ (k : ℕ), s.Mem k → B.card ≤ k) : b.exact (region B s.Mem) = region B (b.strata s).Mem

card carries a bundle's region on the person lattice over B to its strata.

Cells and number systems (§5.1)

def Harbour2014.Bundle.Cut (lo hi : ℕ) (b : Bundle) (k : ℕ) : Prop

b.Cut lo hi k holds when the stratum k survives the cuts the [±additive] values of b make at lo and hi, lying below the first for [−additive], at or above it for [+additive], and between the two for both (§3.3).

Equations

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

@[instance_reducible]

instance Harbour2014.instDecidablePredNatCut (lo hi : ℕ) (b : Bundle) : DecidablePred (Bundle.Cut lo hi b)

Equations

• Harbour2014.instDecidablePredNatCut lo hi b x✝ = id inferInstance

def Harbour2014.Bundle.denote {D : Type u_1} [SemilatticeSup D] (g : D → ℕ) (lo hi : ℕ) (b : Bundle) (P : D → Prop) (x : D) : Prop

A bundle denotes the elements of its exact region that survive its cuts, graded by g.

Equations

• Harbour2014.Bundle.denote g lo hi b P x = (b.exact P x ∧ Harbour2014.Bundle.Cut lo hi b (g x))

def Harbour2014.Setting.cell {D : Type u_1} [SemilatticeSup D] (σ : Setting) (g : D → ℕ) (lo hi : ℕ) (P : D → Prop) (b : Bundle) (x : D) : Prop

The cell of a bundle in a setting is its denotation less those of the more specific bundles, as the plural of Figure 7 is Q+ \ Q′.

Equations

• σ.cell g lo hi P b x = (Harbour2014.Bundle.denote g lo hi b P x ∧ ∀ b' ∈ σ.bundles, b ⊂ b' → ¬Harbour2014.Bundle.denote g lo hi b' P x)

theorem Harbour2014.Setting.cell_strata_iff (σ : Setting) (lo hi : ℕ) (s : Strata) (b : Bundle) (k : ℕ) : σ.cell id lo hi s.Mem b k ↔ ((b.strata s).Mem k ∧ Bundle.Cut lo hi b k) ∧ ∀ b' ∈ σ.bundles, b ⊂ b' → ¬((b'.strata s).Mem k ∧ Bundle.Cut lo hi b' k)

@[instance_reducible]

instance Harbour2014.instDecidablePredNatCellIdMem (σ : Setting) (lo hi : ℕ) (s : Strata) (b : Bundle) : DecidablePred (σ.cell id lo hi s.Mem b)

Equations

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

def Harbour2014.collapse (lo hi k : ℕ) : ℕ

collapse lo hi keeps the strata up to four and sends those below lo, those from lo below hi, and those from hi up to four, five and six.

Equations

• Harbour2014.collapse lo hi k = if k ≤ 4 then k else if k < lo then 4 else if k < hi then 5 else 6

theorem Harbour2014.cut_collapse {lo hi : ℕ} (h : 4 < lo) (b : Bundle) (k : ℕ) : Bundle.Cut lo hi b k ↔ Bundle.Cut 5 6 b (collapse lo hi k)

theorem Harbour2014.mem_strata_collapse {lo hi p : ℕ} (hp : p ≤ 2) (b : Bundle) (k : ℕ) : (b.strata (Strata.ray p)).Mem k ↔ (b.strata (Strata.ray p)).Mem (collapse lo hi k)

theorem Harbour2014.cell_collapse {lo hi p : ℕ} (h : 4 < lo) (hp : p ≤ 2) (σ : Setting) (b : Bundle) (k : ℕ) : σ.cell id lo hi (Strata.ray p).Mem b k ↔ σ.cell id 5 6 (Strata.ray p).Mem b (collapse lo hi k)

The cells for the cuts at lo and hi are those for the cuts at five and six, collapsed.

theorem Harbour2014.exists_cell_iff {lo hi p : ℕ} (h₁ : 4 < lo) (h₂ : lo < hi) (hp : p ≤ 2) (σ : Setting) (b : Bundle) : (∃ (k : ℕ), σ.cell id lo hi (Strata.ray p).Mem b k) ↔ ∃ k ≤ 6, σ.cell id 5 6 (Strata.ray p).Mem b k

def Harbour2014.Setting.system (σ : Setting) (p : ℕ) : List Bundle

The number system of a setting on the person lattice over a base of p atoms consists of its bundles with nonempty cells, computed with the cuts at five and six (filter_cell_eq_system).

Equations

• σ.system p = List.filter (fun (b : Harbour2014.Bundle) => decide (∃ k ≤ 6, σ.cell id 5 6 (Harbour2014.Strata.ray p).Mem b k)) σ.bundles

theorem Harbour2014.Setting.mem_system {σ : Setting} {p : ℕ} {b : Bundle} : b ∈ σ.system p ↔ b ∈ σ.bundles ∧ ∃ k ≤ 6, σ.cell id 5 6 (Strata.ray p).Mem b k

def Harbour2014.Setting.values (σ : Setting) (c : Convention) (p : ℕ) : List Number

The values of a setting's system are its bundles' labels.

Equations

• σ.values c p = List.map (Harbour2014.Bundle.label c) (σ.system p)

def Harbour2014.Setting.toSystem (σ : Setting) (c : Convention) : Number.System

A setting's third-person system as a Number.System sets general number apart.

Equations

• σ.toSystem c = { values := (List.filter (fun (x : Number) => decide (x ≠ Number.general)) (σ.values c 0)).toFinset, hasGeneral := decide (Number.general ∈ σ.values c 0) }

theorem Harbour2014.cell_region {α : Type u_1} [DecidableEq α] {B : Finset α} {lo hi : ℕ} (σ : Setting) (b : Bundle) (x : Finset α) : σ.cell Finset.card lo hi (region B (Strata.ray B.card).Mem) b x ↔ B ⊆ x ∧ σ.cell id lo hi (Strata.ray B.card).Mem b x.card

theorem Harbour2014.filter_cell_eq_system {α : Type u_1} [DecidableEq α] [Infinite α] {B : Finset α} (hB : B.card ≤ 2) {lo hi : ℕ} (h₁ : 4 < lo) (h₂ : lo < hi) (σ : Setting) : List.filter (fun (b : Bundle) => decide (∃ (x : Finset α), σ.cell Finset.card lo hi (region B (Strata.ray B.card).Mem) b x)) σ.bundles = σ.system B.card

On the person lattice over any base of at most two atoms, given infinitely many atoms, and for every placement of the cuts above four atoms, the bundles of a setting with nonempty cells form its system.

The typology (§5.1)

By filter_cell_eq_system, the following hold of every person lattice and every placement of the cuts above four atoms.

theorem Harbour2014.exists_mem_cell {lo hi p : ℕ} (h : 4 < lo) (hp : p ≤ 2) (σ : Setting) {k : ℕ} (hk : max p 1 ≤ k) : ∃ b ∈ σ.bundles, σ.cell id lo hi (Strata.ray p).Mem b k

The cells of a setting cover the strata of its lattice.

theorem Harbour2014.disjoint_cell {lo hi p : ℕ} (h : 4 < lo) (hp : p ≤ 2) (σ : Setting) {b b' : Bundle} (hb : b ∈ σ.bundles) (hb' : b' ∈ σ.bundles) (hne : b ≠ b') : Disjoint (σ.cell id lo hi (Strata.ray p).Mem b) (σ.cell id lo hi (Strata.ray p).Mem b')

Distinct bundles of a setting have disjoint cells, so the system partitions the lattice.

theorem Harbour2014.nodup_values (σ : Setting) (c : Convention) : c.Fits σ.additive → (σ.values c 0).Nodup

Distinct numbers of a system have distinct labels.

theorem Harbour2014.values_atomic_recursive (m d : Activation) (c : Convention) : { atomic := Activation.recursive, minimal := m, additive := d }.values c 0 = { atomic := Activation.active, minimal := m, additive := d }.values c 0

[±atomic]* adds no number to [±atomic] (§4.1).

theorem Harbour2014.system_atomic_minimal : { atomic := Activation.active, minimal := Activation.inactive, additive := Activation.inactive }.system 0 = [{(Feature.atomic, true)}, {(Feature.atomic, false)}] ∧ { atomic := Activation.inactive, minimal := Activation.active, additive := Activation.inactive }.system 0 = [{(Feature.minimal, true)}, {(Feature.minimal, false)}] ∧ { atomic := Activation.active, minimal := Activation.inactive, additive := Activation.inactive }.system 2 = [{(Feature.atomic, false)}] ∧ { atomic := Activation.inactive, minimal := Activation.active, additive := Activation.inactive }.system 2 = [{(Feature.minimal, true)}, {(Feature.minimal, false)}]

{±atomic} and {±minimal} cut the third-person lattice alike, but on the inclusive lattice, whose least element is the speaker and hearer, [±atomic] draws no line and [±minimal] does, so Svan's singular and plural and Winnebago's minimal and augmented need different features (p. 203).

theorem Harbour2014.length_approximative_le_two (σ : Setting) (c : Convention) : c.Fits σ.additive → (List.filter (fun (x : Number) => decide (x ∈ [Number.paucal, Number.greaterPaucal, Number.greaterPlural])) (σ.values c 0)).length ≤ 2

A system has at most two approximative numbers (p. 205).

theorem Harbour2014.length_values_le_six (σ : Setting) (c : Convention) : c.Fits σ.additive → (σ.values c 0).length ≤ 6

No system has more than six numbers.

structure Harbour2014.Implication : Type

An implication of Table 1 says that a system with its antecedent has one of its consequents.

• antecedent : Number

  The number that requires another.

• consequents : Finset Number

  The numbers one of which it requires.

def Harbour2014.instDecidableEqImplication.decEq (x✝ x✝¹ : Implication) : Decidable (x✝ = x✝¹)

Equations

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

@[instance_reducible]

instance Harbour2014.instDecidableEqImplication : DecidableEq Implication

Equations

• Harbour2014.instDecidableEqImplication = Harbour2014.instDecidableEqImplication.decEq

def Harbour2014.Implication.Holds (u : Implication) (s : Finset Number) : Prop

A system satisfies an implication when, with its antecedent, it has one of its consequents.

Equations

• u.Holds s = (u.antecedent ∈ s → ∃ v ∈ u.consequents, v ∈ s)

@[instance_reducible]

instance Harbour2014.instDecidableHolds (u : Implication) (s : Finset Number) : Decidable (u.Holds s)

Equations

• Harbour2014.instDecidableHolds u s = id inferInstance

def Harbour2014.table1 : List Implication

Table 1, the implications the features are to derive, in the printed order; its last row, for the greater and the global plural alike, is two implications.

Equations

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

def Harbour2014.SatisfiesTable1 (s : Finset Number) : Prop

A system satisfies Table 1 when it satisfies each of its implications.

Equations

• Harbour2014.SatisfiesTable1 s = ∀ u ∈ Harbour2014.table1, u.Holds s

@[instance_reducible]

instance Harbour2014.instDecidableSatisfiesTable1 (s : Finset Number) : Decidable (SatisfiesTable1 s)

Equations

• Harbour2014.instDecidableSatisfiesTable1 s = id inferInstance

theorem Harbour2014.satisfiesTable1_toSystem_iff (σ : Setting) (c : Convention) : c.Fits σ.additive → σ.Legitimate → (SatisfiesTable1 (σ.toSystem c).values ↔ ¬(σ.atomic = Activation.inactive ∧ σ.minimal = Activation.recursive ∧ σ.additive ≠ Activation.inactive))

Every legitimate setting satisfies Table 1 except {±additive(*), ±minimal*}, two lacunae of Table 3 whose unit augmented has no augmented.

theorem Harbour2014.satisfiesTable1_corbett (c : Corbett2000.Choices) : SatisfiesTable1 c.toSystem.values

Every system of [Cor00]'s sequences of choices satisfies Table 1.

def Harbour2014.table3 : List (Setting × Convention × Finset Number)

Table 3 pairs each setting and convention with the system of its example language, as [Cor00] records it where it does, or of a lacuna; Banyun's row is left out.

Equations

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

theorem Harbour2014.table3_generated (r : Setting × Convention × Finset Number) : r ∈ table3 → (r.1.toSystem r.2.1).values = r.2.2

Every row of Table 3 is generated.

theorem Harbour2014.table3_legitimate (r : Setting × Convention × Finset Number) : r ∈ table3 → r.2.1.Fits r.1.additive ∧ r.1.Legitimate

Every row of Table 3 is a legitimate setting under a convention that fits it.

The order the settings induce

By (34) a number requires another when the settings that generate the first generate the second. With the legitimate settings as a formal context, requirement is the order of the numbers' attribute concepts, the markedness order of number derived from the features.

def Harbour2014.Generates (p : { p : Setting × Convention // p.2.Fits p.1.additive ∧ p.1.Legitimate }) (v : Number) : Prop

The legitimate settings, under the conventions that fit them, form a formal context in which a setting generates the numbers of its system.

Equations

• Harbour2014.Generates p v = (v ∈ ((↑p).1.toSystem (↑p).2).values)

@[reducible, inline]

abbrev Harbour2014.Requires (b a : Number) : Prop

A number requires another when its attribute concept lies below the other's, the implication schema (34).

Equations

• Harbour2014.Requires b a = (Concept.ofAttribute Harbour2014.Generates b ≤ Concept.ofAttribute Harbour2014.Generates a)

theorem Harbour2014.requires_iff {b a : Number} : Requires b a ↔ ∀ (σ : Setting) (c : Convention), c.Fits σ.additive → σ.Legitimate → b ∈ (σ.toSystem c).values → a ∈ (σ.toSystem c).values

A number requires another when every system a legitimate setting generates with the first has the second.

def Harbour2014.derivedImplications : List (Number × Number)

Implications with one consequent that the settings derive, Table 1's but the unit augmented's, which requires the minimal instead, with the greater plural's strengthened to the plural, since no setting generates the greater plural with the augmented.

Equations

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

theorem Harbour2014.requires_of_mem_derivedImplications (e : Number × Number) : e ∈ derivedImplications → Requires e.1 e.2

The settings derive each implication of derivedImplications.

theorem Harbour2014.not_requires_unitAugmented_augmented : ¬Requires Number.unitAugmented Number.augmented

The unit augmented does not require the augmented, since {±additive, ±minimal*} generates it without.

theorem Harbour2014.mem_table3_of_requires {b a : Number} (h : Requires b a) {r : Setting × Convention × Finset Number} (hr : r ∈ table3) (hb : b ∈ r.2.2) : a ∈ r.2.2

With a number, a system of Table 3 has every number it requires.

theorem Harbour2014.mem_of_requires_corbett (c : Corbett2000.Choices) {b a : Number} (h : Requires b a) (hb : b ∈ c.toSystem.values) : a ∈ c.toSystem.values

Every system of [Cor00]'s sequences of choices is a lower set of the order the settings induce, having with a number every number that number requires.

theorem Harbour2014.mem_of_requires_minimalAugmented {b a : Number} (h : Requires b a) (ns : Number.System) : ns ∈ [Corbett2000.piraha, Corbett2000.rembarrnga, Corbett2000.ilocano] → b ∈ ns.values → a ∈ ns.values

So are the systems of [Cor00] without singular and plural, Pirahã's, Rembarrnga's and Ilocano's.

Composed number (§5.2)

theorem Harbour2014.yimas_system : (List.map (fun (b : Bundle) => (Bundle.label (Convention.one Height.low) b, b)) ({ atomic := Activation.active, minimal := Activation.active, additive := Activation.active }.system 0)).Perm [(Number.singular, {(Feature.atomic, true), (Feature.minimal, true), (Feature.additive, false)}), (Number.dual, {(Feature.atomic, false), (Feature.minimal, true), (Feature.additive, false)}), (Number.paucal, {(Feature.atomic, false), (Feature.minimal, false), (Feature.additive, false)}), (Number.plural, {(Feature.atomic, false), (Feature.minimal, false), (Feature.additive, true)})]

In the singular–dual–paucal–plural system of Yimas and Motuna the paucal shares [−additive] with the dual and [−minimal] with the plural, so Motuna composes it from a dual–paucal and a paucal–plural morpheme ((38)–(40)) and Yimas marks it by [−additive] on a [−minimal] form ((44)–(45)).

@[reducible, inline]

abbrev Harbour2014.meleFila : Setting

Mele-Fila's setting is {±additive*, ±minimal, ±atomic}, with a low and a high cut.

Equations

• Harbour2014.meleFila = { atomic := Harbour2014.Activation.active, minimal := Harbour2014.Activation.active, additive := Harbour2014.Activation.recursive }

theorem Harbour2014.meleFila_system : (List.map (fun (b : Bundle) => (Bundle.label (Convention.two Height.high) b, b)) (meleFila.system 0)).Perm [(Number.singular, {(Feature.atomic, true), (Feature.minimal, true), (Feature.additive, false)}), (Number.dual, {(Feature.atomic, false), (Feature.minimal, true), (Feature.additive, false)}), (Number.paucal, {(Feature.atomic, false), (Feature.minimal, false), (Feature.additive, false)}), (Number.plural, {(Feature.atomic, false), (Feature.minimal, false), (Feature.additive, false), (Feature.additive, true)}), (Number.greaterPlural, {(Feature.atomic, false), (Feature.minimal, false), (Feature.additive, true)})]

Mele-Fila's five numbers have the bundles of Table 4, the plural carrying both values of [±additive].

theorem Harbour2014.meleFila_cell_plural {α : Type u_1} [DecidableEq α] {lo hi : ℕ} (h₁ : 4 < lo) (x : Finset α) : meleFila.cell Finset.card lo hi Finset.Nonempty {(Feature.atomic, false), (Feature.minimal, false), (Feature.additive, false), (Feature.additive, true)} x ↔ lo ≤ x.card ∧ x.card < hi

On every third-person lattice the plural holds of the sums from the lower cut up to the upper, [+additive] relative to the one and [−additive] relative to the other.

theorem Harbour2014.meleFila_classes : (List.map (Bundle.label (Convention.two Height.high)) (List.filter (fun (x : Bundle) => decide ((Feature.additive, true) ∈ x)) (meleFila.system 0))).Perm [Number.plural, Number.greaterPlural] ∧ (List.map (Bundle.label (Convention.two Height.high)) (List.filter (fun (b : Bundle) => decide ((Feature.minimal, false) ∈ b ∧ (Feature.additive, false) ∈ b)) (meleFila.system 0))).Perm [Number.paucal, Number.plural]

So the plural belongs to two natural classes (Table 4), [+additive] with the greater plural, realized by the article a, and [−minimal −additive] with the paucal, realized by the pronoun raateu.