Number resolution

A target agreeing with all of its conjoined noun phrases takes the number its language gives the group they form, in Slovene the dual for two singulars and the plural otherwise. Corbett observes that the values resolution produces match the semantics of number. A system with determinate values gives a referent of n individuals the determinate value of that cardinality if it has one and the plural otherwise, and the conjuncts denote distinct individuals, so the group's cardinality is the sum of theirs. When the determinate values form an initial segment of singular, dual and trial (Number.System.DeterminateInitial), the value of the sum depends only on the values of the parts, so resolution is a function of the conjuncts' numbers. The same classification gives the number of a target whose system lacks its controller's value, the plural of a Modern Hebrew verb agreeing with a dual noun.

Main definitions

• Number.System.ofCard: the value a system gives a referent of n individuals.
• Number.System.resolve: the resolved number of two conjuncts.
• Number.System.coarsen: the value a system gives the referent of another system's value.

Main results

• Number.System.resolve_ofCard: in a system whose determinate values are an initial segment, conjuncts of m and n individuals resolve to the value of m + n.
• Number.System.foldl_resolve_ofCard: any number of conjuncts resolve to the value of the sum of their cardinalities.
• Number.System.resolve_card_union: conjuncts denoting disjoint pluralities resolve to the value of their sum.
• Number.System.coarsen_ofCard: a target shows the value of its controller's referent when the controller's system has every determinate value of the target's.

Implementation notes

That resolution is a function of the conjuncts' numbers says that ofCard's kernel is a congruence for addition on positive cardinalities, the additive counterpart of the person systems' congruences for union; no consumer reads the quotient, so it is not built. The approximative values have no fixed cardinality boundary and the minimal and augmented are relative to person, so neither are classes of cardinalities. resolve and coarsen send them, as they send the plural, to the plural; no theorem here reaches them.

TODO

• Minimal–augmented systems, where the speaker and the addressee, each minimal, sum to the minimal inclusive, want person and number resolved together.

References

• [Cor91] §9.1.2, pp. 263–264
• [Cor00] §6.1, p. 180; §6.5.2, pp. 198–199
• [Cor06] §8.2, pp. 242–243; §8.5.4, p. 257
• [Lin83]

def Number.System.ofCard (ns : System) (n : ℕ) : Number

ns.ofCard n is the value a system gives a referent of n individuals, the determinate value of that cardinality if the system has it and the plural otherwise.

Equations

• ns.ofCard n = if Number.fromCard n ∈ ns.values then Number.fromCard n else Number.plural

def Number.System.resolve (ns : System) (a b : Number) : Number

ns.resolve a b is the resolved number of two conjuncts, the value of the sum of their cardinalities; a conjunct with no fixed cardinality makes it plural.

Equations

• ns.resolve a b = match a.exactCard, b.exactCard with | some m, some n => ns.ofCard (m + n) | x, x_1 => Number.plural

def Number.System.coarsen (ns : System) (v : Number) : Number

ns.coarsen v is the value a system gives the referent of a value v of another system, the value of its cardinality if v has one and the plural otherwise.

Equations

• ns.coarsen v = match v.exactCard with | some n => ns.ofCard n | none => Number.plural

theorem Number.System.resolve_comm (ns : System) (a b : Number) : ns.resolve a b = ns.resolve b a

theorem Number.System.ofCard_of_three_lt (ns : System) {n : ℕ} (h : 3 < n) : ns.ofCard n = plural

theorem Number.System.exactCard_ofCard (ns : System) {n : ℕ} (hn : 0 < n) : (ns.ofCard n).exactCard = if fromCard n ∈ ns.values ∧ n ≤ 3 then some n else none

A referent's value has its cardinality exactly when the system has a determinate value for it.

theorem Number.System.resolve_ofCard {ns : System} (h : ns.DeterminateInitial) {m n : ℕ} (hm : 0 < m) (hn : 0 < n) : ns.resolve (ns.ofCard m) (ns.ofCard n) = ns.ofCard (m + n)

In a system whose determinate values are an initial segment of singular, dual and trial, conjuncts of m and n individuals resolve to the value of m + n, so resolution matches the semantics of number.

theorem Number.System.foldl_resolve_ofCard {ns : System} (h : ns.DeterminateInitial) {m : ℕ} (hm : 0 < m) {ms : List ℕ} (hms : ∀ x ∈ ms, 0 < x) : List.foldl ns.resolve (ns.ofCard m) (List.map ns.ofCard ms) = ns.ofCard (m + ms.sum)

Any number of conjuncts, resolved in order, give the value of the sum of their cardinalities.

theorem Number.System.resolve_card_union {ns : System} {α : Type u_1} [DecidableEq α] (h : ns.DeterminateInitial) {s t : Finset α} (hs : s.Nonempty) (ht : t.Nonempty) (hst : Disjoint s t) : ns.resolve (ns.ofCard s.card) (ns.ofCard t.card) = ns.ofCard (s ∪ t).card

Conjuncts denoting disjoint pluralities resolve to the value of their sum.

theorem Number.System.coarsen_ofCard {src tgt : System} (h : ∀ v ∈ tgt.values, v.isDeterminate → v ∈ src.values) (n : ℕ) : tgt.coarsen (src.ofCard n) = tgt.ofCard n

A target shows the value of its controller's referent when the controller's system has every determinate value of the target's.