Number — lattice semantics for the values

[Har14a] [Lin83]

The denotation of a number value as a predicate restrictor over a join-semilattice of individuals ([Lin83]): Number.interp P n is the region of P's lattice the value n picks out, composed from the feature semantics of [Har14a] —

• (20) [±atomic] = λx. (¬)atom(x) — Mereology.Atom;
• (21) [±minimal] = minimality in a region — Number.minimalIn;
• (10) [±additive] = join-completeness in a region — Number.additiveIn.

The exact values (singular … unit augmented) are compositions of (20) and (21) over P alone; the approximative values (paucal, greater paucal, greater plural, global plural) additionally require a conventionalized cut — a contextually supplied subregion ([Har14a] (14), the sociosemantic convention) — so interp returns none for them: their semantics is additiveIn relative to a cut the lexicon does not fix.

This is the featural characterization of the values (the regions latticeToFeatures classifies, Features/Number/Decomposition.lean, which hosts the decidable mirrors and the equivalence lemmas). The inclusive/exclusive interpretation of the plural in assertion is a separate, pragmatic layer ([Cor00] Ch 7; Sauerland-style competition) and is deliberately not encoded here.

Because the domain is any SemilatticeSup, the same operator interprets verbal number: pluractionality is interp at the event lattice ([Cor00] ch. 8), and [+additive]'s identity with cumulativity (additive_subregion_is_cum, Mereology.CUM) is the number–aspect–telicity nexus of [Har14a] §4.4.

The [±minimal]/[±additive] predicates were first stated in Syntax/Minimalist/Phi/Recursion.lean and graduate here as the general substrate; Recursion consumes them for the feature-recursion theory.

The feature semantics ([Har14a] (20), (21), (10))

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

[+minimal] in region P: x is a minimal element of P under ≤ ([Har14a] (21): x has no proper P-part below it).

Equations

• Number.minimalIn P x = (P x ∧ ∀ (y : D), P y → y ≤ x → y = x)

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

[+additive] in region Q: x is join-complete in Q ([Har14a] (10): ∀ y ∈ Q, x ⊔ y ∈ Q).

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)

The [+additive] region is closed under join: joining two [+additive] elements gives another.

theorem Number.minimalIn_of_atom {D : Type u_1} [SemilatticeSup D] {P : D → Prop} (hAllAtoms : ∀ (x : D), P x → Mereology.Atom x) {x : D} (hPx : P x) : minimalIn P x

Atoms are minimal in any region containing them: the lattice-theoretic grounding of the containment [+atomic] → [+minimal], and the reason [±atomic] cannot undergo feature recursion ([Har14a] §4.2): [±minimal] over an all-atom region selects all of it or nothing.

theorem Number.not_nonminimal_of_atoms {D : Type u_1} [SemilatticeSup D] {P : D → Prop} (hAllAtoms : ∀ (x : D), P x → Mereology.Atom x) (x : D) : ¬(P x ∧ ¬minimalIn P x)

The [−minimal] complement of an all-atom region is empty ([Har14a] §4.2).

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

The [+additive] subregion is cumulative (Mereology.CUM): the number–aspect–telicity nexus of [Har14a] §4.4 — mass nouns are [+additive] (cumulative), telic predicates [−additive] (quantized), with one feature governing both.

The value denotations

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

The non-atoms of P: [−atomic] restricted to P.

Equations

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

def Number.interp {D : Type u_1} [SemilatticeSup D] (P : D → Prop) : Number → Option (D → Prop)

The denotation of a number value over the region P, composed from (20)/(21):

• general — non-committal: P itself;
• singular — the atoms of P;
• dual — the minimal non-atoms ([−atomic +minimal]);
• plural — the non-minimal non-atoms ([−atomic −minimal], the featural exclusive plural);
• trial — [±minimal] recursion: the minimal elements of the plural region;
• minimal / augmented / unitAugmented — the [±minimal]-only system and its recursion;
• approximative values — none: they are additiveIn relative to a conventionalized cut the lexicon does not supply.

Equations

• Number.interp P Number.general = some P
• Number.interp P Number.singular = some fun (x : D) => P x ∧ Mereology.Atom x
• Number.interp P Number.dual = some (Number.minimalIn (Number.nonAtomsOf P))
• Number.interp P Number.trial = some (Number.minimalIn fun (x : D) => Number.nonAtomsOf P x ∧ ¬Number.minimalIn (Number.nonAtomsOf P) x)
• Number.interp P Number.plural = some fun (x : D) => Number.nonAtomsOf P x ∧ ¬Number.minimalIn (Number.nonAtomsOf P) x
• Number.interp P Number.minimal = some (Number.minimalIn P)
• Number.interp P Number.augmented = some fun (x : D) => P x ∧ ¬Number.minimalIn P x
• Number.interp P Number.unitAugmented = some (Number.minimalIn fun (x : D) => P x ∧ ¬Number.minimalIn P x)
• Number.interp P x✝ = none

theorem Number.interp_isSome_iff {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (n : Number) : (interp P n).isSome = true ↔ n ∉ [paucal, greaterPaucal, greaterPlural, globalPlural]

The values interp defines are exactly the non-approximative, in-system values together with general: the approximatives are the cut-dependent ones.

theorem Number.singular_subset_minimal {D : Type u_1} [SemilatticeSup D] (P : D → Prop) {x : D} (h : P x ∧ Mereology.Atom x) : minimalIn P x

Singular entails minimal over any region: the value-level containment [+atomic] → [+minimal], derived from minimalIn_of_atom rather than stipulated — the semantic ground of Number.Features.WellFormed (Features/Number/Decomposition.lean).

theorem Number.dual_plural_partition {D : Type u_1} [SemilatticeSup D] (P : D → Prop) (x : D) (hx : nonAtomsOf P x) : (minimalIn (nonAtomsOf P) x ∨ nonAtomsOf P x ∧ ¬minimalIn (nonAtomsOf P) x) ∧ ¬(minimalIn (nonAtomsOf P) x ∧ nonAtomsOf P x ∧ ¬minimalIn (nonAtomsOf P) x)

Dual and plural partition the non-atoms: every non-atom of P is dual or plural, never both — the [±minimal] split of the [−atomic] region.

Decidability

On finite carriers the feature predicates are decidable, so concrete classifications (Features/Number/Decomposition.lean) are kernel-checked by decide.

@[implicit_reducible]

instance Number.instDecidableMinimalInOfFintypeOfDecidableEqOfDecidableLEOfDecidablePred {D : Type u_1} [SemilatticeSup D] {P : D → Prop} [Fintype D] [DecidableEq D] [DecidableLE D] [DecidablePred P] (x : D) : Decidable (minimalIn P x)

Equations

• Number.instDecidableMinimalInOfFintypeOfDecidableEqOfDecidableLEOfDecidablePred x = decidable_of_iff (P x ∧ ∀ (y : D), P y → y ≤ x → y = x) ⋯

@[implicit_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)) ⋯