[IM06]: The Composition of Complex Cardinals

[IM06] [Hur75]

[IM06] argue that complex cardinals are composed entirely in the syntax and interpreted by ordinary composition: simplex cardinals are modifiers of type ⟨⟨e,t⟩,⟨e,t⟩⟩ — their (5), ⟦n⟧ = λP λx. ∃S [Π(S)(x) ∧ |S| = n ∧ ∀s∈S P(s)] (here cardMod) — so two hundred books is iterative complementation [two [hundred [books]]], and multiplication needs no dedicated rule: cardMod_cardMod_atoms shows iterated modification computes the product, matching [Hur75]'s PHRASE projection rule (iterated_matches_phrase). Determiner and predicate types for cardinals are ruled out by complex cardinals (their §2.2): under predicate conjunction two hundred books is either contradictory (their (12), predicate_conjunction_contradictory) or satisfied by a plurality of just 100 — here scaled to two four satisfied by 4 (predicate_theory_undershoots, their (13)).

Addition is xNP coordination (their §4, (44)/(52)): twenty-two books = [twenty books] and [two books] with the split reading ⟦A and B⟧ = λx. ∃y z [x = y⊕z ∧ A(y) ∧ B(z)]; under the full split (no overlap — pragmatic, their §4.2.1 Gricean manner) coordination computes the sum (coord_card). The joint reading is semantically impossible for distinct cardinals (no_joint_reading, their (56a)).

Their (23) countability presupposition — a cardinal's complement must denote equicardinal pluralities — is Equicardinal; the keystone card_of_cardMod is exactly the definedness cascade it feeds: n cells of uniform size k make n·k.

Their §3.3 adopts [Hur75]'s thesis that most cardinals are singular nouns; the syntax here is his grammar (Syntax/Numeral/Composition.lean).

Main definitions

• IsPart: their (6) partition (Finset counterpart of Semantics.Plurality.Cover.IsPartition, chosen for cardinality counting)
• cardMod: their (5) cardinal-as-modifier
• Equicardinal: their (23) countability presupposition
• coordSem: their (52) coordination

Main results

• cardMod_atoms_iff: n books = an n-atom plurality of books
• cardMod_cardMod_atoms: iterated modification multiplies — and iterated_matches_phrase aligns it with the PHRASE projection rule
• predicate_conjunction_contradictory / predicate_theory_undershoots: their §2.2 refutation of non-modifier types
• coord_card / no_joint_reading: coordination adds; joint readings clash

Partitions and the cardinal modifier (their (5)–(7))

def IoninMatushansky2006.IsPart {α : Type u_1} [DecidableEq α] (S : Finset (Finset α)) (x : Finset α) : Prop

Their (6): S is a partition of x — nonempty, pairwise-disjoint cells whose union is x. Finset counterpart of Semantics.Plurality.Cover.IsPartition.

Equations

• IoninMatushansky2006.IsPart S x = ((∀ s ∈ S, s ≠ ∅) ∧ (↑S).PairwiseDisjoint id ∧ S.sup id = x)

def IoninMatushansky2006.cardMod {α : Type u_1} [DecidableEq α] (n : ℕ) (P : Finset α → Prop) (x : Finset α) : Prop

Their (5): ⟦n⟧ = λP λx. ∃S [Π(S)(x) ∧ |S| = n ∧ ∀s∈S P(s)] — the cardinal as an ⟨⟨e,t⟩,⟨e,t⟩⟩ modifier.

Equations

• IoninMatushansky2006.cardMod n P x = ∃ (S : Finset (Finset α)), IoninMatushansky2006.IsPart S x ∧ S.card = n ∧ ∀ s ∈ S, P s

def IoninMatushansky2006.IsAtomOf {α : Type u_1} (P : α → Prop) (s : Finset α) : Prop

The atomic complement: singleton pluralities of P-individuals — what their §3.1 atomicity requirement makes the lexical xNP denote.

Equations

• IoninMatushansky2006.IsAtomOf P s = ∃ (a : α), P a ∧ s = {a}

def IoninMatushansky2006.Equicardinal {α : Type u_1} (P : Finset α → Prop) (k : ℕ) : Prop

Their (23) countability presupposition: all pluralities in the complement's denotation have the same cardinality.

Equations

• IoninMatushansky2006.Equicardinal P k = ∀ (s : Finset α), P s → s.card = k

theorem IoninMatushansky2006.equicardinal_atoms {α : Type u_1} [DecidableEq α] (P : α → Prop) : Equicardinal (IsAtomOf P) 1

theorem IoninMatushansky2006.card_of_cardMod {α : Type u_1} [DecidableEq α] {P : Finset α → Prop} {k n : ℕ} {x : Finset α} (hP : Equicardinal P k) (h : cardMod n P x) : x.card = n * k

Keystone: n cells of uniform size k make a plurality of n·k — the definedness cascade their (23) presupposition feeds.

Simple and iterated modification (their (8)–(9))

theorem IoninMatushansky2006.cardMod_atoms_iff {α : Type u_1} [DecidableEq α] (n : ℕ) (P : α → Prop) (x : Finset α) : cardMod n (IsAtomOf P) x ↔ x.card = n ∧ ∀ a ∈ x, P a

Their (8): hundred books denotes the 100-atom pluralities of books — cardMod over an atomic complement counts atoms.

theorem IoninMatushansky2006.cardMod_cardMod_atoms {α : Type u_1} [DecidableEq α] {m : ℕ} (hm : 1 ≤ m) (n : ℕ) (P : α → Prop) (x : Finset α) : cardMod n (cardMod m (IsAtomOf P)) x ↔ x.card = n * m ∧ ∀ a ∈ x, P a

Their (9): iterated modification multiplies. two hundred books = ⟦two⟧(⟦hundred⟧(⟦books⟧)) denotes the 2 × 100-atom pluralities — complex cardinals need no semantic rule beyond ordinary composition.

theorem IoninMatushansky2006.iterated_matches_phrase {α : Type u_1} [DecidableEq α] (n : Syntax.Numeral.Number) (m : Syntax.Numeral.M) (P : α → Prop) (x : Finset α) : cardMod n.value (cardMod m.value (IsAtomOf P)) x ↔ x.card = (Syntax.Numeral.Phrase.mk n m).value ∧ ∀ a ∈ x, P a

Iterated modification computes [Hur75]'s PHRASE projection rule: ⟦[n m] books⟧ counts (Phrase.mk n m).value atoms.

Ruling out the predicate theory (their §2.2, (12)–(13))

theorem IoninMatushansky2006.predicate_conjunction_contradictory {α : Type u_1} [DecidableEq α] (x : Finset α) : ¬(x.card = 2 ∧ x.card = 100)

Their (12): under bare predicate conjunction two hundred books is self-contradictory — nothing has cardinality 2 and 100 at once.

theorem IoninMatushansky2006.predicate_theory_undershoots : ∃ (x : Finset (Fin 4)), cardMod 2 (fun (x : Finset (Fin 4)) => True) x ∧ cardMod 4 (fun (x : Finset (Fin 4)) => True) x ∧ x.card = 4

Their (13), scaled to two four: with partition-based predicate meanings conjoined instead of composed, a plurality of just 4 satisfies both conjuncts — where the modifier reading demands 2 × 4 = 8.

Addition as coordination (their §4, (52))

def IoninMatushansky2006.coordSem {α : Type u_1} [DecidableEq α] (A B : Finset α → Prop) (x : Finset α) : Prop

Their (52): coordinated xNPs split the plurality — ⟦A and B⟧ = λx. ∃y z [x = y⊕z ∧ A(y) ∧ B(z)].

Equations

• IoninMatushansky2006.coordSem A B x = ∃ (y : Finset α) (z : Finset α), x = y ∪ z ∧ A y ∧ B z

theorem IoninMatushansky2006.coord_card {α : Type u_1} [DecidableEq α] {P : α → Prop} {n m : ℕ} {x : Finset α} (h : ∃ (y : Finset α) (z : Finset α), Disjoint y z ∧ x = y ∪ z ∧ cardMod n (IsAtomOf P) y ∧ cardMod m (IsAtomOf P) z) : x.card = n + m ∧ ∀ a ∈ x, P a

Under the full split (their (56b); overlap excluded pragmatically by Gricean manner, their §4.2.1), coordination computes addition: twenty-two books counts 20 + 2 atoms.

theorem IoninMatushansky2006.no_joint_reading {α : Type u_1} [DecidableEq α] {P : α → Prop} {n m : ℕ} (hnm : n ≠ m) (x : Finset α) : ¬(cardMod n (IsAtomOf P) x ∧ cardMod m (IsAtomOf P) x)

Their (56a): the joint reading is semantically impossible for distinct cardinals — no plurality is 20 atoms and 2 atoms at once.