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

Landman interprets a noun phrase as an i-set, a body together with a base that generates the body under sum. Counting is relative to the base, and it is correct when the base is disjoint, whether or not the algebra has atoms. An i-set is count when its base is disjoint and neat when its base is generated by a disjoint set of base-atoms, and a non-null i-set is mass when it is not count and mess when it is not neat. The Head principle computes the base of a complex noun phrase from the base of its head, so modification, pluralization and numerals preserve count and neat.

Main definitions

• sumClosure: the closure *X of a set under arbitrary sums, as a closure operator.
• Generates X Y: X generates Y under sum.
• atomsIn Z, Atomistic Z: the Z-atoms and atomisticity relative to Z.
• card Z x: the number of Z-parts of x.
• ISet, with ISet.IsCount, ISet.IsMass, ISet.IsNeat and ISet.IsMess.
• ISet.restrict: the Head principle; ISet.sep, ISet.plur and ISet.number are its instances for modifiers, the plural and numerals.
• ISet.IsSumNeutral: the sum neutral i-sets of nouns like poultry.

Main results

• sumClosureOrderIso: over a disjoint base without ⊥, the sums of base elements correspond to the sets of base elements, so a sum counts as many as it sums (card_sSup).
• ISet.isNeat_iff: an i-set is neat iff its base is generated by a disjoint set of its objects.
• ISet.IsCount.isNeat, ISet.IsMess.isMass: count i-sets are neat, and mess i-sets are mass.
• ISet.IsCount.restrict, ISet.IsNeat.restrict: the Head principle preserves count and neat.
• ISet.mem_number_plur_sep_singular: three white cats denotes the sums of three white cats.
• Pottery.isNeat, Ironware.not_atomistic: a neat mass noun, and the atomic base that is not neat because it is not atomistic.

Implementation notes

Landman works in a complete Boolean algebra. The definitions need only a complete lattice and the counting results only the frame law, so they are stated at those levels. card is total; its presupposition that the base is disjoint is a hypothesis of the theorems about it, as is ⊥ ∉ Z, without which ⊥ would count as a base element. The pottery and ironware models take items to be singletons of a power set.

TODO

The intensional layer of §6.1.3–6.1.4 (count, neat and mess intensions, conceptual and contextual disjointness) and the i-objects that interpret definite DPs are not formalized.

References

• [Lan20]
• [Lan11], [Lan16]

Closure and generation under sum (ch. 2)

def Landman2020.sumClosure {B : Type u_1} [CompleteLattice B] : ClosureOperator (Set B)

The closure *X of X under sum is the set of sums of subsets of X. It contains ⊥ = ⊔∅.

Equations

• Landman2020.sumClosure = ClosureOperator.ofPred (fun (X : Set B) => sSup '' 𝒫 X) (fun (S : Set B) => ∀ T ⊆ S, sSup T ∈ S) ⋯ ⋯ ⋯

theorem Landman2020.mem_sumClosure {B : Type u_1} [CompleteLattice B] {X : Set B} {b : B} : b ∈ sumClosure X ↔ ∃ Y ⊆ X, sSup Y = b

theorem Landman2020.sSup_mem_sumClosure {B : Type u_1} [CompleteLattice B] {X Y : Set B} (h : Y ⊆ X) : sSup Y ∈ sumClosure X

@[simp]

theorem Landman2020.sumClosure_empty {B : Type u_1} [CompleteLattice B] : sumClosure ∅ = {⊥}

@[simp]

theorem Landman2020.sSup_sumClosure {B : Type u_1} [CompleteLattice B] (X : Set B) : sSup (sumClosure X) = sSup X

theorem Landman2020.sumClosure_sdiff_bot {B : Type u_1} [CompleteLattice B] (X : Set B) : sumClosure (X \ {⊥}) = sumClosure X

Discarding ⊥ from the generators does not change their sums.

structure Landman2020.Generates {B : Type u_1} [CompleteLattice B] (X Y : Set B) : Prop

X generates Y under sum if every element of Y is a sum of elements of X and Y and X have the same sum.

• subset_sumClosure : Y ⊆ sumClosure X
• sSup_eq : sSup Y = sSup X

theorem Landman2020.generates_self {B : Type u_1} [CompleteLattice B] (X : Set B) : Generates X X

theorem Landman2020.generates_sumClosure {B : Type u_1} [CompleteLattice B] (X : Set B) : Generates X (sumClosure X)

theorem Landman2020.Generates.of_subset {B : Type u_1} [CompleteLattice B] {X Y : Set B} (hXY : X ⊆ Y) (hY : Y ⊆ sumClosure X) : Generates X Y

A subset of Y that generates every element of Y generates Y.

theorem Landman2020.Generates.sumClosure_subset {B : Type u_1} [CompleteLattice B] {X Y : Set B} (h : Generates X Y) : sumClosure Y ⊆ sumClosure X

Sums of elements of X are sums of elements of any set that generates X.

Relative atoms (ch. 2)

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

The Z-atoms are the minimal elements of Z \ {⊥}, the objects of Z.

Equations

• Landman2020.atomsIn Z = {a : B | Minimal (fun (x : B) => x ∈ Z \ {⊥}) a}

theorem Landman2020.mem_atomsIn_of_isAtom {B : Type u_1} [CompleteLattice B] {Z : Set B} {b : B} (ha : IsAtom b) (h : b ∈ Z) : b ∈ atomsIn Z

An atom of the algebra that lies in Z is a Z-atom.

@[simp]

theorem Landman2020.atomsIn_univ {B : Type u_1} [CompleteLattice B] : atomsIn Set.univ = {a : B | IsAtom a}

Relative to the whole algebra, the Z-atoms are the atoms.

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

Z is atomistic if every element of Z is the sum of the Z-atoms below it.

Equations

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

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

Z is atomic if every object of Z has a Z-atom below it.

Equations

• Landman2020.Atomic Z = ∀ b ∈ Z \ {⊥}, (Set.Iic b ∩ Landman2020.atomsIn Z).Nonempty

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

Z is atomless if it has no Z-atoms.

Equations

• Landman2020.Atomless Z = (Landman2020.atomsIn Z = ∅)

theorem Landman2020.Atomistic.atomic {B : Type u_1} [CompleteLattice B] {Z : Set B} (h : Atomistic Z) : Atomic Z

theorem Landman2020.atomistic_iff_generates {B : Type u_1} [CompleteLattice B] {Z : Set B} : Atomistic Z ↔ Generates (atomsIn Z) Z

Z is atomistic iff its atoms generate it.

theorem Landman2020.atomsIn_eq_of_pairwiseDisjoint {B : Type u_1} [CompleteLattice B] {Z : Set B} (hZ : Z.PairwiseDisjoint id) : atomsIn Z = Z \ {⊥}

A disjoint set has its objects as atoms.

theorem Landman2020.atomsIn_eq_of_subset_sumClosure {B : Type u_1} [CompleteLattice B] {A Z : Set B} (hAZ : A ⊆ Z) (hA : A.PairwiseDisjoint id) (hbot : ⊥ ∉ A) (hZA : Z ⊆ sumClosure A) : atomsIn Z = A

A disjoint set of objects of Z that generates every element of Z is the set of Z-atoms.

theorem Landman2020.atomsIn_Iic_inter {B : Type u_1} [CompleteLattice B] {Z : Set B} {c : B} : atomsIn (Set.Iic c ∩ Z) = Set.Iic c ∩ atomsIn Z

Restricting Z to the parts of c keeps exactly the Z-atoms below c.

theorem Landman2020.Atomistic.Iic_inter {B : Type u_1} [CompleteLattice B] {Z : Set B} {c : B} (h : Atomistic Z) : Atomistic (Set.Iic c ∩ Z)

theorem Landman2020.Atomless.not_pairwiseDisjoint {B : Type u_1} [CompleteLattice B] {Z : Set B} {b : B} (h : Atomless Z) (hb : b ∈ Z) (hb0 : b ≠ ⊥) : ¬Z.PairwiseDisjoint id

An atomless set with an object is not disjoint.

Distribution sets and cardinality (§5.2)

The distribution set of x relative to Z is Iic x ∩ Z, the book's (x] ∩ Z.

theorem Landman2020.sSup_Iic_inter {B : Type u_1} [CompleteLattice B] {Z : Set B} {x : B} (hx : x ∈ sumClosure Z) : sSup (Set.Iic x ∩ Z) = x

Every sum of elements of Z is the sum of its distribution set.

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

card Z x is the cardinality of x relative to Z, the number of its Z-parts.

Equations

• Landman2020.card Z x = (Set.Iic x ∩ Z).ncard

theorem Landman2020.le_sSup_iff_mem {B : Type u_1} [Order.Frame B] {Y Z : Set B} {z : B} (hZ : Z.PairwiseDisjoint id) (hz : z ∈ Z) (hz0 : z ≠ ⊥) (hY : Y ⊆ Z) : z ≤ sSup Y ↔ z ∈ Y

Over a disjoint base, a base object lies below a sum of base elements only if it is one of them.

theorem Landman2020.Iic_sSup_inter {B : Type u_1} [Order.Frame B] {Y Z : Set B} (hZ : Z.PairwiseDisjoint id) (hbot : ⊥ ∉ Z) (hY : Y ⊆ Z) : Set.Iic (sSup Y) ∩ Z = Y

Over a disjoint base without ⊥, the distribution set of a sum of base elements is the set summed.

theorem Landman2020.sSup_injOn {B : Type u_1} [Order.Frame B] {Z : Set B} (hZ : Z.PairwiseDisjoint id) (hbot : ⊥ ∉ Z) : Set.InjOn sSup (𝒫 Z)

Over a disjoint base without ⊥, a sum determines its summands.

def Landman2020.sumClosureOrderIso {B : Type u_1} [Order.Frame B] {Z : Set B} (hZ : Z.PairwiseDisjoint id) (hbot : ⊥ ∉ Z) : ↑(sumClosure Z) ≃o ↑(𝒫 Z)

Over a disjoint base without ⊥, the sums of base elements are order-isomorphic to the sets of base elements, as the elements of a complete atomic Boolean algebra are to the sets of its atoms.

Equations

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

theorem Landman2020.card_sSup {B : Type u_1} [Order.Frame B] {Y Z : Set B} (hZ : Z.PairwiseDisjoint id) (hbot : ⊥ ∉ Z) (hY : Y ⊆ Z) : card Z (sSup Y) = Y.ncard

Over a disjoint base without ⊥, a sum counts as many as the base elements it sums.

theorem Landman2020.card_of_mem {B : Type u_1} [Order.Frame B] {Z : Set B} {z : B} (hZ : Z.PairwiseDisjoint id) (hbot : ⊥ ∉ Z) (hz : z ∈ Z) : card Z z = 1

A base element counts as one.

I-sets (§5.1, §6.1.2)

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

An i-set is a body together with a base that generates it under sum.

• body : Set B

  The body is the set the noun phrase denotes.

• base : Set B

  The base is the set in terms of which the body is counted.

• generates : Generates self.base self.body

theorem Landman2020.ISet.ext_iff {B : Type u_2} {inst✝ : CompleteLattice B} {x y : ISet B} : x = y ↔ x.body = y.body ∧ x.base = y.base

theorem Landman2020.ISet.ext {B : Type u_2} {inst✝ : CompleteLattice B} {x y : ISet B} (body : x.body = y.body) (base : x.base = y.base) : x = y

theorem Landman2020.ISet.body_subset {B : Type u_1} [CompleteLattice B] (X : ISet B) : X.body ⊆ sumClosure X.base

def Landman2020.ISet.singular {B : Type u_1} [CompleteLattice B] (Z : Set B) : ISet B

The i-set ⟨Z, Z⟩ of a singular noun, such as ⟨CAT, CAT⟩ for cat.

Equations

• Landman2020.ISet.singular Z = { body := Z, base := Z, generates := ⋯ }

def Landman2020.ISet.ofBase {B : Type u_1} [CompleteLattice B] (Z : Set B) : ISet B

The i-set ⟨*Z, Z⟩ generated by a base Z, such as ⟨*CAT, CAT⟩ for cats.

Equations

• Landman2020.ISet.ofBase Z = { body := Landman2020.sumClosure Z, base := Z, generates := ⋯ }

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

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

Equations

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

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

An i-set is count if its base is disjoint.

Equations

• X.IsCount = X.base.PairwiseDisjoint id

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

An i-set is mass if it is count only when null.

Equations

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

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

An i-set is neat if its base is atomistic with disjoint base-atoms.

Equations

• X.IsNeat = (Landman2020.Atomistic X.base ∧ (Landman2020.atomsIn X.base).PairwiseDisjoint id)

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

An i-set is mess if it is neat only when null.

Equations

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

theorem Landman2020.ISet.isNull_iff {B : Type u_1} [CompleteLattice B] {X : ISet B} : X.IsNull ↔ X = singular ∅ ∨ X = ofBase ∅

The null i-sets are the singular null i-set ⟨∅, ∅⟩ and the plural null i-set ⟨{⊥}, ∅⟩.

theorem Landman2020.ISet.IsNull.isCount {B : Type u_1} [CompleteLattice B] {X : ISet B} (h : X.IsNull) : X.IsCount

Null i-sets are count, and they are mass by definition.

theorem Landman2020.ISet.IsNull.isNeat {B : Type u_1} [CompleteLattice B] {X : ISet B} (h : X.IsNull) : X.IsNeat

Null i-sets are neat, and they are mess by definition.

theorem Landman2020.ISet.isNeat_iff {B : Type u_1} [CompleteLattice B] {X : ISet B} : X.IsNeat ↔ ∃ A ⊆ X.base, ⊥ ∉ A ∧ A.PairwiseDisjoint id ∧ Generates A X.base

An i-set is neat iff its base is generated by a disjoint set of its objects, which are then its base-atoms.

theorem Landman2020.ISet.IsCount.isNeat {B : Type u_1} [CompleteLattice B] {X : ISet B} (h : X.IsCount) : X.IsNeat

Count i-sets are neat.

theorem Landman2020.ISet.IsMess.isMass {B : Type u_1} [CompleteLattice B] {X : ISet B} (h : X.IsMess) : X.IsMass

Mess i-sets are mass.

theorem Landman2020.ISet.IsNeat.body_subset_sumClosure_atomsIn {B : Type u_1} [CompleteLattice B] {X : ISet B} (h : X.IsNeat) : X.body ⊆ sumClosure (atomsIn X.base)

The body of a neat i-set consists of sums of base-atoms.

theorem Landman2020.ISet.not_isNeat_of_atomless {B : Type u_1} [CompleteLattice B] {X : ISet B} {b : B} (h : Atomless X.base) (hb : b ∈ X.base) (hb0 : b ≠ ⊥) : ¬X.IsNeat

An i-set whose base is atomless but has an object is not neat, so it is mess mass.

The Head principle (§5.3, §5.4)

def Landman2020.ISet.restrict {B : Type u_1} [CompleteLattice B] (H : ISet B) (C : Set B) (hC : C ⊆ sumClosure H.base) : ISet B

By the Head principle, a body C generated by the base of a head H has as base the elements of H's base below its sum, (C] ∩ base(H).

Equations

• H.restrict C hC = { body := C, base := Set.Iic (sSup C) ∩ H.base, generates := ⋯ }

theorem Landman2020.ISet.restrict_base {B : Type u_1} [CompleteLattice B] {H : ISet B} {C : Set B} (hC : C ⊆ sumClosure H.base) : (H.restrict C hC).base = Set.Iic (sSup C) ∩ H.base

theorem Landman2020.ISet.IsCount.restrict {B : Type u_1} [CompleteLattice B] {H : ISet B} {C : Set B} (h : H.IsCount) (hC : C ⊆ sumClosure H.base) : (H.restrict C hC).IsCount

The Head principle preserves count.

theorem Landman2020.ISet.IsNeat.restrict {B : Type u_1} [CompleteLattice B] {H : ISet B} {C : Set B} (h : H.IsNeat) (hC : C ⊆ sumClosure H.base) : (H.restrict C hC).IsNeat

The Head principle preserves neat.

def Landman2020.ISet.sep {B : Type u_1} [CompleteLattice B] (P : ISet B) (p : B → Prop) : ISet B

Subsective modification by a property p, as by an adjective (white) or a numeral.

Equations

• P.sep p = P.restrict {x : B | x ∈ P.body ∧ p x} ⋯

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

Pluralization closes the body under sum.

Equations

• P.plur = P.restrict (Landman2020.sumClosure P.body) ⋯

@[simp]

theorem Landman2020.ISet.plur_base {B : Type u_1} [CompleteLattice B] (P : ISet B) : P.plur.base = P.base

Pluralization keeps the base.

theorem Landman2020.ISet.plur_singular {B : Type u_1} [CompleteLattice B] (Z : Set B) : (singular Z).plur = ofBase Z

Pluralizing a singular noun gives the i-set its base generates, as plur ⟨CAT, CAT⟩ is ⟨*CAT, CAT⟩.

noncomputable def Landman2020.ISet.number {B : Type u_1} [CompleteLattice B] (N : ℕ → Prop) (P : ISet B) : ISet B

The numeral schema keeps the body elements whose cardinality relative to the base satisfies the number predicate N.

Equations

• Landman2020.ISet.number N P = P.sep fun (x : B) => N (Landman2020.card P.base x)

theorem Landman2020.ISet.sep_singular {B : Type u_1} [Order.Frame B] {Z : Set B} (hZ : Z.PairwiseDisjoint id) (hbot : ⊥ ∉ Z) (p : B → Prop) : (singular Z).sep p = singular {z : B | z ∈ Z ∧ p z}

Modifying a singular count noun restricts its base, so white cat denotes ⟨CAT ∩ WHITE, CAT ∩ WHITE⟩.

theorem Landman2020.ISet.mem_number_ofBase {B : Type u_1} [Order.Frame B] {Z : Set B} {x : B} (hZ : Z.PairwiseDisjoint id) (hbot : ⊥ ∉ Z) (N : ℕ → Prop) : x ∈ (number N (ofBase Z)).body ↔ ∃ Y ⊆ Z, N Y.ncard ∧ sSup Y = x

A numeral counts the base elements of a count i-set generated by its base, so three cats denotes the sums of three cats.

theorem Landman2020.ISet.mem_number_plur_sep_singular {B : Type u_1} [Order.Frame B] {Z : Set B} {x : B} (hZ : Z.PairwiseDisjoint id) (hbot : ⊥ ∉ Z) (p : B → Prop) (N : ℕ → Prop) : x ∈ (number N ((singular Z).sep p).plur).body ↔ ∃ Y ⊆ {z : B | z ∈ Z ∧ p z}, N Y.ncard ∧ sSup Y = x

Three white cats denotes the sums of three white cats (§5.4).

Sum neutral neat mass nouns (§7.1)

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

The i-set ⟨*X₀, *X₀⟩, whose body and base are both the sums of X₀.

Equations

• Landman2020.ISet.sumNeutral X₀ = Landman2020.ISet.singular (Landman2020.sumClosure X₀)

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

An i-set is sum neutral, like poultry, if it is ⟨*X₀, *X₀⟩ for a disjoint set X₀.

Equations

• X.IsSumNeutral = ∃ (X₀ : Set B), X₀.PairwiseDisjoint id ∧ X = Landman2020.ISet.sumNeutral X₀

theorem Landman2020.ISet.IsSumNeutral.isNeat {B : Type u_1} [CompleteLattice B] {X : ISet B} (h : X.IsSumNeutral) : X.IsNeat

Sum neutral i-sets are neat.

theorem Landman2020.ISet.not_isCount_sumNeutral {B : Type u_1} [CompleteLattice B] {X₀ : Set B} {x y : B} (hx : x ∈ X₀) (hy : y ∈ X₀) (hxy : x ≠ y) (hx0 : x ≠ ⊥) (hy0 : y ≠ ⊥) : ¬(sumNeutral X₀).IsCount

An i-set ⟨*X₀, *X₀⟩ with two distinct objects in X₀ is not count, since its base contains both objects and their sum.

Pottery and ironware (§7.1)

Pottery is a group neutral neat mass noun. Its base adds the cup and saucer and the teaset to the basic items, so it overlaps, and the basic items generate it. The ironware of the Excursus to §7.1 has an atomic base with disjoint base-atoms, which is neat on the definition of [Lan11], but the hammer is not the sum of the base-atoms below it, so ironware is mess. The water of §8.1.5 has the same profile.

The basic items are the teapot, the cup, the saucer and the fruit bowl.

def Landman2020.Pottery.teapot : Set (Fin 4)

Equations

• Landman2020.Pottery.teapot = {0}

def Landman2020.Pottery.cup : Set (Fin 4)

Equations

• Landman2020.Pottery.cup = {1}

def Landman2020.Pottery.saucer : Set (Fin 4)

Equations

• Landman2020.Pottery.saucer = {2}

def Landman2020.Pottery.bowl : Set (Fin 4)

Equations

• Landman2020.Pottery.bowl = {3}

def Landman2020.Pottery.items : Set (Set (Fin 4))

The basic items are the singletons.

Equations

• Landman2020.Pottery.items = Set.range fun (i : Fin 4) => {i}

def Landman2020.Pottery.base : Set (Set (Fin 4))

The items sold as one are the basic items, the cup and saucer, and the teaset.

Equations

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

def Landman2020.Pottery.pottery : ISet (Set (Fin 4))

Pottery denotes ⟨*BP, BP⟩.

Equations

• Landman2020.Pottery.pottery = Landman2020.ISet.ofBase Landman2020.Pottery.base

theorem Landman2020.Pottery.isNeat : pottery.IsNeat

theorem Landman2020.Pottery.not_isCount : ¬pottery.IsCount

The teaset overlaps the teapot.

theorem Landman2020.Pottery.isMass : pottery.IsMass

theorem Landman2020.Pottery.not_isSumNeutral : ¬pottery.IsSumNeutral

Pottery is not sum neutral, since the teapot and the fruit bowl are not sold as one.

The ironware items are the pliers, the hammerhead, and the hammer, which is the hammerhead together with its wooden handle 2.

def Landman2020.Ironware.pliers : Set (Fin 3)

Equations

• Landman2020.Ironware.pliers = {0}

def Landman2020.Ironware.hammerhead : Set (Fin 3)

Equations

• Landman2020.Ironware.hammerhead = {1}

def Landman2020.Ironware.hammer : Set (Fin 3)

Equations

• Landman2020.Ironware.hammer = {1, 2}

def Landman2020.Ironware.base : Set (Set (Fin 3))

Equations

• Landman2020.Ironware.base = {Landman2020.Ironware.pliers, Landman2020.Ironware.hammerhead, Landman2020.Ironware.hammer}

def Landman2020.Ironware.ironware : ISet (Set (Fin 3))

Ironware denotes ⟨*base, base⟩.

Equations

• Landman2020.Ironware.ironware = Landman2020.ISet.ofBase Landman2020.Ironware.base

theorem Landman2020.Ironware.hammerhead_lt_hammer : hammerhead ⊂ hammer

theorem Landman2020.Ironware.atomsIn_base : atomsIn base = {pliers, hammerhead}

theorem Landman2020.Ironware.atomic : Atomic ironware.base

Every ironware item has a base-atom below it.

theorem Landman2020.Ironware.pairwiseDisjoint_atomsIn : (atomsIn ironware.base).PairwiseDisjoint id

theorem Landman2020.Ironware.not_atomistic : ¬Atomistic ironware.base

The hammer is not the sum of the base-atoms below it.

theorem Landman2020.Ironware.isMess : ironware.IsMess

theorem Landman2020.Ironware.isMass : ironware.IsMass