Docs / Semantics / Reference / Kind

Kinds

import Linglib.Semantics.Reference.Kind · namespace Kind

Source

Chierchia models a kind as an individual concept: at each situation it picks out the sum of its instances, and it has no value where it has none. The operator 'down', ∩, takes a property to the concept of the largest member of its extension at each situation, which is the property's kind where that concept is a kind, and the operator 'up', ∪, takes a kind to the property of being one of its instances, the parts of its value. ∩ is ι applied at each situation, and ∪ its partial inverse, Set.Iic.

∩ undoes ∪, and ∪ undoes ∩ on a property closed downward wherever ∩ is defined, that is, wherever the property has instances its extension has a largest member. Closure under sums gives the largest member, not closure downward: over a complete semilattice ∩ is defined on a property closed under arbitrary sums, so ∪ undoes ∩ on one that is also closed downward (Kind.up_down_of_sSup_mem), and ∩ is defined on a finite property closed under binary sums (Kind.down_isSome_of_supClosed). On the plural of a singular property, ∪∩ restores the atoms beneath the pluralities. ∩ is undefined for a singular property when no kind is singular wherever it has a value. Derived kind predication, which applies a predicate of objects to a kind by quantifying existentially over its instances, is Quantifier.Det.some (Kind.up k s).

Main definitions

  • Kind.up: ∪, the instances of a kind at a situation.
  • Kind.down: ∩, the concept of the largest member of a property's extension.

Implementation notes

The set of kinds is a parameter K : Set (S → Option E) of the theorems that need it, primitive as in Chierchia. Chierchia states (17c) with AT_P "the set that generates P under PL", which is read here as the atoms beneath members of P. Read as the singular property whose plural P is, (17c) fails at a situation with exactly one instance, where the plural has no member and ∩ no value (Studies/Chierchia1998.lean).

References

Declarations

L61
L63
L65–66

∩: the concept of the largest member of a property's extension at each situation, which is the property's kind where it is a kind.

downL70–72
noncomputable def Kind.down {S : Type u_1} {E : Type u_2} [LE E] (P : S → Set E) (s : S) :
Option E

Used by down_eq_some_iff, down_isSome_iff, down_eq_none_iff, down_up, up_down, up_down_of_forall_atom, down_notMem_of_atom, down_isSome_of_supClosed, up_down_of_sSup_mem

Used in Chierchia1998, Dayal2004, Krifka2003, Krifka2026, LeBruynDeSwart2022

L78–79
L81–82
L84–85

∩∪d = d, Chierchia's (17a).

theorem down_upL87–89
{S : Type u_1} {E : Type u_2} [PartialOrder E] (k : S → Option E) :
down (up k) = k

Built from ,

∪∩P = P for a property closed downward wherever ∩P is defined, Chierchia's (17b): wherever the property has instances, its extension has a largest member.

theorem up_downL91–95
{S : Type u_1} {E : Type u_2} {P : S → Set E} [PartialOrder E] (hP : ∀ (s : S), IsLowerSet (P s)) (hdef : ∀ (s : S), (P s).Nonempty → (down P s).isSome = true) :
up (down P) = P

Built from ,

On the plural of a singular property F, true of what is not F and has only F-atoms, ∪∩ adds the atoms beneath the pluralities wherever ∩ is defined, Chierchia's (17c).

theorem up_down_of_forall_atomL97–116
{S : Type u_1} {E : Type u_2} {P F : S → Set E} [PartialOrder E] (hF : ∀ (s : S), ∀ x ∈ F s, Mereology.Atom x) (hP : ∀ (s : S) (x : E), x ∈ P s ↔ x ∉ F s ∧ ∀ y ≤ x, Mereology.Atom y → y ∈ F s) (hdef : ∀ (s : S), (P s).Nonempty → (down P s).isSome = true) (s : S) :
up (down P) s = P s ∪ {a : E | Mereology.Atom a ∧ ∃ x ∈ P s, a ≤ x}

Built from ,

∩ is undefined for a singular property when no kind is singular in every situation where it has a value: the concept of a singular property is singular wherever it has one.

theorem down_notMem_of_atomL118–122
{S : Type u_1} {E : Type u_2} {P : S → Set E} [PartialOrder E] {K : Set (S → Option E)} (hK : ∀ k ∈ K, ¬∀ (s : S), ∀ d ∈ k s, Mereology.Atom d) (hP : ∀ (s : S), ∀ x ∈ P s, Mereology.Atom x) :
down P ∉ K

Built from

theorem down_isSome_of_supClosedL126–128
{S : Type u_1} {E : Type u_2} {P : S → Set E} {s : S} [SemilatticeSup E] (hcum : SupClosed (P s)) (hfin : (P s).Finite) (hne : (P s).Nonempty) :
(down P s).isSome = true

Built from

theorem up_down_of_sSup_memL130–133
{S : Type u_1} {E : Type u_2} {P : S → Set E} [CompleteSemilatticeSup E] (hP : ∀ (s : S), IsLowerSet (P s)) (hsum : ∀ (s : S), ∀ T ⊆ P s, T.Nonempty → sSup T ∈ P s) :
up (down P) = P

Built from ,