Landman (2020) — Iceberg Semantics for Mass Nouns and Count Nouns

[Lan20]

Formalizes the formal core of:

Landman, F. (2020). Iceberg Semantics for Mass Nouns and Count Nouns: A New Framework for Boolean Semantics. Studies in Linguistics and Philosophy 105. Springer.

The framework

Mountain semantics (Link-style Boolean semantics, [Lin83]) grounds counting in atomicity: singular count nouns denote sets of Boolean atoms. Iceberg semantics replaces this vertical picture with a horizontal one: every interpretation is an i-set ⟨body, base⟩ where the base generates the body under sum, and the mass/count distinction lives in the base — count iff the base is disjoint (§6.1.2); mass and count are perspectives on the same stuff, and Boolean atoms play no role.

Main results (all generic over a complete Boolean algebra)

• ISet, the two null i-sets, and ISet.body_eq_of_base_empty (the nulls are exactly the empty-based i-sets — his §6.1.2 Lemma).
• Counting is correct given disjointness, not atomicity (the mathematical heart of ch. 5): for a disjoint, ⊥-free Z, membership in a sum of Z-elements is membership in the summands (mem_iff_le_sSup_of_disjoint, by frame distributivity), so every element of *Z is recovered from its distribution set (sSup_partsIn), the distribution map is injective (partsIn_injOn), and card counts correctly.
• atomsIn_eq_of_disjoint (a ⊥-free disjoint set is all-minimal) and the §6.1.2 Lemma ISet.IsCount.isNeat: count i-sets are neat — with the book's atomisticity definition of neat, which §6.1.2 explicitly substitutes for the base-atomicity of [Lan11]/[Lan16].
• The Head Principle (§5.3): base(α) = (body α] ∩ base(H), and its Lemma — disjointness inherits from head to complex (ISet.headBase_disjoint) — making mass/count compositional.
• ISet.plur leaves the base fixed (ISet.plur_base_eq_headBase), so pluralization preserves countness (ISet.plur_isCount) — the generic content of the §5.4 white cats computation, where (*body(P)] ∩ base(P) = base(P).
• The noun classes: number-neutral neat mass nouns (poultry, ⟨*X₀, *X₀⟩, §7.1) are neat (numberNeutral_isNeat) but their base overlaps (star_overlapPred, hence mass); atomless bases are mess (water, §8.1.5: not_neat_of_atomless).

Connections

• The disjointness machinery is Semantics/Mereology's OverlapPred/DisjointPred/nullSchema (shared with [SF21], whose counting bases are this book's bases and whose individuation schemas select among its perspectives — Mereology.IsMaxDisjointIn).
• Mountain semantics' pluralization * is the Link closure of Semantics/Plurality/Algebra.lean; Iceberg's star is its complete-join generalization (sums of arbitrary subsets, so *∅ = {⊥}).
• The base-perspective on mass/count is the semantic ground for keeping countability out of the Number value space (Features/Number/Basic.lean): count/mass classifies bases; number values classify referents.

Boolean background (his ch. 2)

star X is closure under arbitrary sums — *X = {b : ∃ Y ⊆ X, b = ⊔Y}, so *∅ = {⊥}. Mereological overlap is non-null meet. plus Z is Z⁺ (Z minus the null element); atomsIn Z is the set of minimal elements of Z⁺ — Z-atoms, relativized to Z, not Boolean atoms.

def Landman2020.star {B : Type u_1} [CompleteBooleanAlgebra B] (X : Set B) : Set B

Closure of X under arbitrary sums.

Equations

• Landman2020.star X = {b : B | ∃ Y ⊆ X, b = sSup Y}

theorem Landman2020.subset_star {B : Type u_1} [CompleteBooleanAlgebra B] {X : Set B} : X ⊆ star X

theorem Landman2020.sSup_mem_star {B : Type u_1} [CompleteBooleanAlgebra B] {X Y : Set B} (h : Y ⊆ X) : sSup Y ∈ star X

theorem Landman2020.star_mono {B : Type u_1} [CompleteBooleanAlgebra B] {X Y : Set B} (h : X ⊆ Y) : star X ⊆ star Y

theorem Landman2020.sSup_star_eq {B : Type u_1} [CompleteBooleanAlgebra B] {X : Set B} : sSup (star X) = sSup X

theorem Landman2020.star_empty {B : Type u_1} [CompleteBooleanAlgebra B] : star ∅ = {⊥}

theorem Landman2020.star_star {B : Type u_1} [CompleteBooleanAlgebra B] {X : Set B} : star (star X) = star X

star is idempotent: a sum of sums of X-elements is a sum of X-elements.

def Landman2020.mOverlap {B : Type u_1} [CompleteBooleanAlgebra B] (x y : B) : Prop

Mereological overlap: a non-null common part.

Equations

• Landman2020.mOverlap x y = (x ⊓ y ≠ ⊥)

def Landman2020.plus {B : Type u_1} [CompleteBooleanAlgebra B] (Z : Set B) : Set B

Z⁺: Z minus the null element.

Equations

• Landman2020.plus Z = Z \ {⊥}

def Landman2020.atomsIn {B : Type u_1} [CompleteBooleanAlgebra B] (Z : Set B) : Set B

The Z-atoms: minimal elements of Z⁺ (his ch. 2; relativized to Z, not Boolean atoms).

Equations

• Landman2020.atomsIn Z = {z : B | z ∈ Landman2020.plus Z ∧ ∀ y ∈ Landman2020.plus Z, y ≤ z → y = z}

def Landman2020.Atomistic {B : Type u_1} [CompleteBooleanAlgebra B] (Z : Set B) : Prop

Z is atomistic: every element of Z⁺ is the sum of the Z-atoms below it (his ATOM_{Z,b} = (b] ∩ ATOM_Z and b = ⊔ATOM_{Z,b}).

Equations

• Landman2020.Atomistic Z = ∀ b ∈ Landman2020.plus Z, b = sSup (Set.Iic b ∩ Landman2020.atomsIn Z)

theorem Landman2020.atomsIn_eq_of_disjoint {B : Type u_1} [CompleteBooleanAlgebra B] {Z : Set B} (hZ : Mereology.DisjointPred mOverlap Z) (hbot : ⊥ ∉ Z) : atomsIn Z = Z

In a ⊥-free disjoint set everything is minimal: ATOM_Z = Z (his §6.1.2 Lemma, step 2: a disjoint base is its own set of base-atoms).

Counting from disjointness (his ch. 5)

Mountain semantics counts in terms of Boolean atoms; Iceberg semantics observes that disjointness of the base is what makes counting correct. The distribution set D_Z(x) = (x] ∩ Z recovers x exactly when Z is disjoint — by frame distributivity, an element of a disjoint Z is below a sum of Z-elements only by being one of them.

def Landman2020.partsIn {B : Type u_1} [CompleteBooleanAlgebra B] (Z : Set B) (x : B) : Set B

The distribution set D_Z(x) = (x] ∩ Z (his §5.2).

Equations

• Landman2020.partsIn Z x = {z : B | z ∈ Z ∧ z ≤ x}

theorem Landman2020.mem_iff_le_sSup_of_disjoint {B : Type u_1} [CompleteBooleanAlgebra B] {Z Y : Set B} (hZ : Mereology.DisjointPred mOverlap Z) (hbot : ⊥ ∉ Z) (hY : Y ⊆ Z) {z : B} (hz : z ∈ Z) : z ≤ sSup Y ↔ z ∈ Y

Membership in a sum is membership in the summands (for disjoint, ⊥-free Z): z ≤ ⊔Y ↔ z ∈ Y. The frame law z ⊓ ⊔Y = ⨆ y ∈ Y, z ⊓ y reduces a stray z to a sum of nulls.

theorem Landman2020.partsIn_sSup {B : Type u_1} [CompleteBooleanAlgebra B] {Z Y : Set B} (hZ : Mereology.DisjointPred mOverlap Z) (hbot : ⊥ ∉ Z) (hY : Y ⊆ Z) : partsIn Z (sSup Y) = Y

The distribution set of a sum of Z-elements is exactly the set summed: counting reads the parts off correctly.

theorem Landman2020.sSup_partsIn {B : Type u_1} [CompleteBooleanAlgebra B] {Z : Set B} (hZ : Mereology.DisjointPred mOverlap Z) (hbot : ⊥ ∉ Z) {x : B} (hx : x ∈ star Z) : sSup (partsIn Z x) = x

Every element of *Z is the sum of its distribution set.

theorem Landman2020.partsIn_injOn {B : Type u_1} [CompleteBooleanAlgebra B] {Z : Set B} (hZ : Mereology.DisjointPred mOverlap Z) (hbot : ⊥ ∉ Z) : Set.InjOn (partsIn Z) (star Z)

Distribution is injective on *Z: a plurality is determined by what it distributes to. Disjointness, not atomicity, is what counting needs — the central claim of Iceberg semantics, as a theorem.

noncomputable def Landman2020.card {B : Type u_1} [CompleteBooleanAlgebra B] (Z : Set B) (x : B) : ℕ

card_Z(x) = |D_Z(x)| (his §5.2; presupposes Z disjoint, which is what partsIn_injOn certifies as sufficient).

Equations

• Landman2020.card Z x = (Landman2020.partsIn Z x).ncard

Exact numbers: the junction with [Har14a]

[Har14a] (30) characterizes the exact number values over a generating set of atoms as cardinality classes — singular |x| = 1, dual |x| = 2, trial |x| = 3 — with (31) the successor-like function that extends them. This book's card certifies precisely that counting: over a disjoint base, the cardinality of a sum is the number of generators summed. Two frameworks formalized from their own primary sources, agreeing on one counting operation by theorem.

theorem Landman2020.card_sSup {B : Type u_1} [CompleteBooleanAlgebra B] {Z Y : Set B} (hZ : Mereology.DisjointPred mOverlap Z) (hbot : ⊥ ∉ Z) (hY : Y ⊆ Z) : card Z (sSup Y) = Y.ncard

Over a disjoint base, the Landman cardinality of a sum is the number of generators summed — [Har14a]'s (30) cardinality classes are card-classes.

theorem Landman2020.card_self {B : Type u_1} [CompleteBooleanAlgebra B] {Z : Set B} (hZ : Mereology.DisjointPred mOverlap Z) (hbot : ⊥ ∉ Z) {z : B} (hz : z ∈ Z) : card Z z = 1

A generator counts as one (Harbour's singular: |x| = 1).

theorem Landman2020.card_pair {B : Type u_1} [CompleteBooleanAlgebra B] {Z : Set B} (hZ : Mereology.DisjointPred mOverlap Z) (hbot : ⊥ ∉ Z) {z₁ z₂ : B} (h₁ : z₁ ∈ Z) (h₂ : z₂ ∈ Z) (hne : z₁ ≠ z₂) : card Z (z₁ ⊔ z₂) = 2

A sum of two distinct generators counts as two (Harbour's dual: |x| = 2 — the value Number.interp assigns the minimal non-atoms).

I-sets and count – mass – neat – mess (his §6.1)

structure Landman2020.ISet (B : Type u_2) [CompleteBooleanAlgebra B] : Type u_2

An i-set: a body and a base that generates it under sum (his §5.1/§6.1.2: body(X) ⊆ *base(X) and ⊔body(X) = ⊔base(X)).

• body : Set B

  The standard denotation.

• base : Set B

  The generating set: the things that count as one.

• body_subset_star : self.body ⊆ star self.base
• sSup_body_eq : sSup self.body = sSup self.base

def Landman2020.ISet.nullEmpty {B : Type u_1} [CompleteBooleanAlgebra B] : ISet B

The singular null i-set ⟨∅, ∅⟩ (his §6.1.2 Lemma).

Equations

• Landman2020.ISet.nullEmpty = { body := ∅, base := ∅, body_subset_star := ⋯, sSup_body_eq := ⋯ }

def Landman2020.ISet.nullBot {B : Type u_1} [CompleteBooleanAlgebra B] : ISet B

The plural null i-set ⟨{⊥}, ∅⟩ (his §6.1.2 Lemma; *∅ = {⊥}).

Equations

• Landman2020.ISet.nullBot = { body := {⊥}, base := ∅, body_subset_star := ⋯, sSup_body_eq := ⋯ }

def Landman2020.ISet.IsNull {B : Type u_1} [CompleteBooleanAlgebra B] (X : ISet B) : Prop

An i-set is null iff its base is empty.

Equations

• X.IsNull = (X.base = ∅)

def Landman2020.ISet.IsCount {B : Type u_1} [CompleteBooleanAlgebra B] (X : ISet B) : Prop

Count: the base is disjoint (his §6.1.2).

Equations

• X.IsCount = Mereology.DisjointPred Landman2020.mOverlap X.base

def Landman2020.ISet.IsMass {B : Type u_1} [CompleteBooleanAlgebra B] (X : ISet B) : Prop

Mass: if non-null then not count (his §6.1.2; the null i-sets are both count and mass).

Equations

• X.IsMass = (¬X.IsNull → ¬X.IsCount)

def Landman2020.ISet.IsNeat {B : Type u_1} [CompleteBooleanAlgebra B] (X : ISet B) : Prop

Neat: the base is atomistic with disjoint base-atoms — the book's §6.1.2 definition, which explicitly replaces the base-atomicity of [Lan11]/[Lan16] by base-atomisticity.

Equations

• X.IsNeat = (Landman2020.Atomistic X.base ∧ Mereology.DisjointPred Landman2020.mOverlap (Landman2020.atomsIn X.base))

def Landman2020.ISet.IsMess {B : Type u_1} [CompleteBooleanAlgebra B] (X : ISet B) : Prop

Mess: if non-null then not neat.

Equations

• X.IsMess = (¬X.IsNull → ¬X.IsNeat)

theorem Landman2020.ISet.body_eq_of_base_empty {B : Type u_1} [CompleteBooleanAlgebra B] (X : ISet B) (h : X.base = ∅) : X.body = ∅ ∨ X.body = {⊥}

An empty-based i-set has body ∅ or {⊥}: the two null i-sets are the only ones (his §6.1.2 Lemma).

theorem Landman2020.ISet.IsCount.isNeat {B : Type u_1} [CompleteBooleanAlgebra B] {X : ISet B} (hX : X.IsCount) (hbot : ⊥ ∉ X.base) : X.IsNeat

Count i-sets are neat (his §6.1.2 Lemma, claim 2): a ⊥-free disjoint base is its own set of base-atoms, and trivially atomistic.

The Head Principle (his §5.3)

base(α) = (body(α)] ∩ base(H): the base of a complex NP is the base of its head, restricted to the parts of the complex's body. The accompanying Lemma is one line — base(α) ⊆ base(H) — and gives the compositionality of mass/count: a complex NP with a count head is count.

def Landman2020.ISet.headBase {B : Type u_1} [CompleteBooleanAlgebra B] (bodyC : Set B) (H : ISet B) : Set B

The head-principle base: the head's base elements that are parts of the complex's body.

Equations

• Landman2020.ISet.headBase bodyC H = {b : B | b ∈ H.base ∧ b ≤ sSup bodyC}

theorem Landman2020.ISet.headBase_disjoint {B : Type u_1} [CompleteBooleanAlgebra B] {bodyC : Set B} {H : ISet B} (hH : Mereology.DisjointPred mOverlap H.base) : Mereology.DisjointPred mOverlap (headBase bodyC H)

His §5.3 Lemma, verbatim: "If base(H) is disjoint then base(α) is disjoint. Proof: base(α) ⊆ base(H). ∎"

Pluralization (his §5.4)

plur(P) = ⟨*body(P), (*body(P)] ∩ base(P)⟩. Since ⊔*body(P) = ⊔body(P) = ⊔base(P), the head-principle restriction is vacuous: pluralization leaves the base fixed — in the worked white cats example, base(WHITE CATS) = base(WHITE CAT) = CAT ∩ WHITE.

def Landman2020.ISet.plur {B : Type u_1} [CompleteBooleanAlgebra B] (P : ISet B) : ISet B

Pluralization: close the body under sum; the base stays.

Equations

• P.plur = { body := Landman2020.star P.body, base := P.base, body_subset_star := ⋯, sSup_body_eq := ⋯ }

theorem Landman2020.ISet.plur_base_eq_headBase {B : Type u_1} [CompleteBooleanAlgebra B] (P : ISet B) : P.plur.base = headBase P.plur.body P

The book's (*body(P)] ∩ base(P) is just base(P): every base element is a part of the total body, so the head-principle restriction is vacuous under pluralization.

theorem Landman2020.ISet.plur_isCount {B : Type u_1} [CompleteBooleanAlgebra B] {P : ISet B} (hP : P.IsCount) : P.plur.IsCount

Pluralization preserves countness: the mass/count nature of a noun is unaffected by number morphology — it lives in the base.

The noun classes (his ch. 7–8)

Number-neutral neat mass nouns (poultry, livestock, §7.1): the singular/plural distinction is not articulated — ⟨*X₀, *X₀⟩ for a disjoint X₀ (his DOM-BIRD). The base overlaps (so: mass), but its atoms are exactly X₀ (so: neat). Mess mass nouns (water, §8.1.5): the base has no minimal elements at all, so atomisticity fails outright.

theorem Landman2020.star_overlapPred {B : Type u_1} [CompleteBooleanAlgebra B] {X₀ : Set B} (hbot : ⊥ ∉ X₀) (hdisj : Mereology.DisjointPred mOverlap X₀) {x₀ x₁ : B} (h₀ : x₀ ∈ X₀) (h₁ : x₁ ∈ X₀) (hne : x₀ ≠ x₁) : Mereology.OverlapPred mOverlap (star X₀)

A sum-closure properly overlaps once there are two distinct ⊥-free generators: x₀ and x₀ ⊔ x₁ are distinct members of *X₀ sharing the part x₀. Hence number-neutral nouns are mass.

def Landman2020.numberNeutral {B : Type u_1} [CompleteBooleanAlgebra B] (X₀ : Set B) : ISet B

The number-neutral neat mass i-set ⟨*X₀, *X₀⟩ (his §7.1: poultry with X₀ = DOM-BIRD).

Equations

• Landman2020.numberNeutral X₀ = { body := Landman2020.star X₀, base := Landman2020.star X₀, body_subset_star := ⋯, sSup_body_eq := ⋯ }

theorem Landman2020.atomsIn_star_of_disjoint {B : Type u_1} [CompleteBooleanAlgebra B] {X₀ : Set B} (hdisj : Mereology.DisjointPred mOverlap X₀) (hbot : ⊥ ∉ X₀) : atomsIn (star X₀) = X₀

The atoms of a sum-closure are the generators: for ⊥-free disjoint X₀, ATOM_{*X₀} = X₀.

theorem Landman2020.numberNeutral_isNeat {B : Type u_1} [CompleteBooleanAlgebra B] {X₀ : Set B} (hdisj : Mereology.DisjointPred mOverlap X₀) (hbot : ⊥ ∉ X₀) : (numberNeutral X₀).IsNeat

Number-neutral nouns are neat: the base *X₀ overlaps, but it is atomistic over the disjoint generator set X₀ (his §7.1: poultry is a neat mass i-set).

theorem Landman2020.not_neat_of_atomless {B : Type u_1} [CompleteBooleanAlgebra B] {X : ISet B} (h : atomsIn X.base = ∅) {b : B} (hb : b ∈ X.base) (hbne : b ≠ ⊥) : ¬X.IsNeat

A non-trivial atomless base is mess (his §8.1.5: water's base has no minimal elements — space can always be shaved off a region containing a molecule — so atomisticity fails).