Mendia (2020): Reference to ad hoc kinds

Mendia analyzes kind reference through partitions. Carlson's Disjointness Condition, that a kind-referring expression ranges over subkinds sharing no realizations and jointly covering the kind, becomes the requirement that kind reference go through a partition of the kind's realizations into the cells of a contextually salient equivalence relation. Subkinds are referred to through the ι of the cells, and an ad hoc kind term such as the lions that eat people is the ι of κ+, the cells that contain every instance of the restrictor. Mendia's indistinguishability relation is Cresswell's degree construction, so an amount reading of a relative clause is the same definite under the partition of a preorder into its degrees.

Main statements

• ncard_realized_classes_le: under any partition, finitely many individuals realize at most as many subkinds as there are individuals, so two kinds of dog are sitting in the next room is false with only Fido there.
• the_kappaPlus_eq_some, the_kappaPlus_eq_none: the ad hoc kind term refers exactly when the restrictor's instances share a cell.
• amount_reading: an amount reading refers to the degree of the restrictor's instances.

Implementation notes

• The model is extensional. The type E collects the realizations of the kind under discussion, a salient kind formation is a Setoid E, the partition Π of (28) is its Setoid.classes, and a subkind is identified with its cell, as the paper does for its tables (p. 616: the members of a partition "are always objects, not kinds").
• (28b) as printed binds y_k in the antecedent and uses it in the consequent; it is read with y_k bound outside the implication. (33) prints Π(x_y) for Π(x_k).
• The ι of (31) and (36) is Reference.iota, undefined when no cell or several qualify.
• Dogs come in every combination of breed and role and lions in every combination of subspecies and diet, so there are people-eating lions of both subspecies. The restrictor lions that eat people is read as footnote 11's lions that eat only people, a value of the diet.

TODO

• The champagne partitions (64)–(66) of §4.3.2, the distribution of ad hoc kind terms (§3.3), the singular–plural contrast (§3.4), and the amount readings without degrees of §5.

References

• [Men20]
• [Car77b]
• [Cre76]

Partitions and the Disjointness Condition (§3.1)

theorem Mendia2020.cover_and_noOverlap_iff {E : Type u_1} {c : Set (Set E)} : ((∀ (x : E), ∃ y ∈ c, x ∈ y) ∧ ∀ (x : E), ∀ y ∈ c, x ∈ y → ¬∃ z ∈ c, y ≠ z ∧ x ∈ z) ↔ ∀ (x : E), ∃! y : Set E, y ∈ c ∧ x ∈ y

A family of subkinds ((16), (28)) covers the kind and has no overlap iff every realization lies in exactly one of them, the clause that makes a family a Setoid.IsPartition.

def Mendia2020.realized {E : Type u_1} (c : Set (Set E)) (X : Set E) : Set (Set E)

The subkinds of a family realized among the individuals X, those that n kinds of dog are in the next room counts.

Equations

• Mendia2020.realized c X = {y : Set E | y ∈ c ∧ (y ∩ X).Nonempty}

theorem Mendia2020.realized_classes {E : Type u_1} (s : Setoid E) (X : Set E) : realized s.classes X = (fun (x : E) => {z : E | s z x}) '' X

The subkinds of a partition realized among X are the cells of the members of X.

theorem Mendia2020.ncard_realized_classes_le {E : Type u_1} (s : Setoid E) {X : Set E} (hX : X.Finite) : (realized s.classes X).ncard ≤ X.ncard

Under any salient partition (14), finitely many individuals realize at most as many subkinds as there are individuals.

Fido, (14)

inductive Mendia2020.Breed : Type

Breeds of dog.

• borderCollie : Breed
• bulldog : Breed
• beagle : Breed

inductive Mendia2020.Role : Type

Roles of dog.

• watchDog : Role
• guideDog : Role

structure Mendia2020.Dog : Type

A dog has a breed, a role, and an index telling apart dogs alike in both.

• breed : Breed
• role : Role
• idx : ℕ

def Mendia2020.fido : Dog

Fido, a border collie and a watch-dog, (14b).

Equations

• Mendia2020.fido = { breed := Mendia2020.Breed.borderCollie, role := Mendia2020.Role.watchDog, idx := 0 }

theorem Mendia2020.ncard_realized_fido_le (s : Setoid Dog) : (realized s.classes {fido}).ncard ≤ 1

With only Fido in the room (14b), no partition of the dogs has two subkinds realized there, so two kinds of dog are sitting in the next room is false.

def Mendia2020.borderCollies : Set Dog

The border collies.

Equations

• Mendia2020.borderCollies = {d : Mendia2020.Dog | d.breed = Mendia2020.Breed.borderCollie}

def Mendia2020.watchDogs : Set Dog

The watch-dogs.

Equations

• Mendia2020.watchDogs = {d : Mendia2020.Dog | d.role = Mendia2020.Role.watchDog}

theorem Mendia2020.ncard_realized_borderCollies_watchDogs : (realized {borderCollies, watchDogs} {fido}).ncard = 2

Fido alone realizes both the border collies and the watch-dogs, so counting these two subkinds would make (14) true (14b).

theorem Mendia2020.not_partition_borderCollies_watchDogs : ¬∀ (x : Dog), ∃! y : Set Dog, y ∈ {borderCollies, watchDogs} ∧ x ∈ y

The border collies and the watch-dogs overlap in Fido (14b), so they form no partition and the Disjointness Condition excludes them.

def Mendia2020.room14a : Set Dog

The dogs of (14a) are three bulldogs and two beagles.

Equations

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

theorem Mendia2020.ncard_realized_room14a : (realized (Setoid.ker Dog.breed).classes room14a).ncard = 2

The dogs of the room (14a) realize two subkinds of the breed partition, so (14) is true.

Subkind reference (§3.2.2)

theorem Mendia2020.that_eq {E : Type u_1} (s : Setoid E) (a : E) : (Reference.iota fun (y : Set E) => y ∈ s.classes ∧ a ∈ y) = some {x : E | s x a}

The demonstrative that (kind of) dog (31b), the ι of the cells containing the demonstrated dog, always refers, to that dog's cell.

theorem Mendia2020.the_kind_eq_none {E : Type u_1} (s : Setoid E) {a b : E} (h : ¬s a b) : (Reference.iota fun (x : Set E) => x ∈ s.classes) = none

The kind of dog (32b), the ι of the cells alone, fails once the partition has two cells.

def Mendia2020.kappaPlus {E : Type u_1} (s : Setoid E) (P : Set E) : Set (Set E)

The operator κ+ (33) gives the cells of the partition that contain every instance of the restrictor P.

Equations

• Mendia2020.kappaPlus s P = {y : Set E | y ∈ s.classes ∧ P ⊆ y}

@[simp]

theorem Mendia2020.kappaPlus_empty {E : Type u_1} (s : Setoid E) : kappaPlus s ∅ = s.classes

With no restrictor κ+ is κ, the partition itself (footnote 9).

@[simp]

theorem Mendia2020.kappaPlus_singleton {E : Type u_1} (s : Setoid E) (a : E) : kappaPlus s {a} = {y : Set E | y ∈ s.classes ∧ a ∈ y}

Restricted to the demonstrated individual, κ+ gives the cells whose ι (31b) takes (footnote 9), so the demonstrative is the definite over κ+.

theorem Mendia2020.the_kappaPlus_eq_some {E : Type u_1} (s : Setoid E) {P : Set E} {a : E} (ha : a ∈ P) (hP : ∀ x ∈ P, s x a) : (Reference.iota fun (x : Set E) => x ∈ kappaPlus s P) = some {x : E | s x a}

When every instance of the restrictor shares the cell of a ∈ P, the definite over κ+ refers to that cell (36).

theorem Mendia2020.the_kappaPlus_eq_none {E : Type u_1} (s : Setoid E) {P : Set E} {a b : E} (ha : a ∈ P) (hb : b ∈ P) (h : ¬s a b) : (Reference.iota fun (x : Set E) => x ∈ kappaPlus s P) = none

When two instances of the restrictor lie in different cells, no cell contains them both and the definite fails (p. 604).

theorem Mendia2020.the_kappaPlus_ker {E : Type u_1} {β : Type u_2} (f : E → β) (a : E) : (Reference.iota fun (x : Set E) => x ∈ kappaPlus (Setoid.ker f) (f ⁻¹' {f a})) = some (f ⁻¹' {f a})

Under the partition by a function f ((36), (37), footnote 11), such as what each lion eats, the individuals on which f takes a given value form a cell, and the definite with that restrictor refers to exactly them, the second line of (36).

inductive Mendia2020.Subspecies : Type

Subspecies of lion.

• african : Subspecies
• asiatic : Subspecies

inductive Mendia2020.Diet : Type

What a lion eats, read as footnote 11 requires, is only people, only zebras, or only carrion.

• people : Diet
• zebras : Diet
• carrion : Diet

structure Mendia2020.Lion : Type

A lion has a subspecies, a diet, and an index telling apart lions alike in both.

• subspecies : Subspecies
• diet : Diet
• idx : ℕ

def Mendia2020.eatPeople : Set Lion

Lions that eat people, (21b), sharpened as footnote 11 requires.

Equations

• Mendia2020.eatPeople = Mendia2020.Lion.diet ⁻¹' {Mendia2020.Diet.people}

theorem Mendia2020.the_kappaPlus_subspecies : (Reference.iota fun (x : Set Lion) => x ∈ kappaPlus (Setoid.ker Lion.subspecies) eatPeople) = none

The partition of lions by subspecies cannot serve the lions that eat people, since there are people-eating lions of both subspecies (p. 604).

theorem Mendia2020.the_kappaPlus_diet : (Reference.iota fun (x : Set Lion) => x ∈ kappaPlus (Setoid.ker Lion.diet) eatPeople) = some eatPeople

The partition by what lions eat serves it (37), and the definite refers to the people-eating lions.

Amounts (§4.3)

theorem Mendia2020.amount_reading {E : Type u_1} [Preorder E] {P : Set E} {a : E} (ha : a ∈ P) (hP : ∀ x ∈ P, AntisymmRel (fun (x1 x2 : E) => x1 ≤ x2) x a) : (Reference.iota fun (x : Set E) => x ∈ kappaPlus (Degree.cresswellSetoid fun (x1 x2 : E) => x1 ≤ x2) P) = some {y : E | AntisymmRel (fun (x1 x2 : E) => x1 ≤ x2) a y}

An amount reading is ad hoc kind reference (§4.3) under the partition of a preorder into its degrees, (57)–(59), and needs only that the restrictor lie in one cell (p. 617). When every instance of the restrictor is as A as a, the definite over κ+ refers to the degree of a, the individuals exactly as A as a, (59).