Homogeneity: plural predication

A plural predication has many readings, one for each choice of the parts of the plurality that count as close enough to it, as Križ and Spector propose. For every upper set U containing the plurality x, the predicate is read as holding of some non-bottom part of x in U. The readings run from the universal one, where U holds only what lies above x, to the existential one, where U holds everything. A sentence is therefore true on all of its readings when the predicate holds of x and false on all of them when it holds of no part of x. The readings are closed under union, and under intersection when the predicate is cumulative; for a distributive predicate they are exactly the lattice generated by the predications of the atoms of x, with the universal reading at the bottom and the existential one at the top. On a distributive predicate this is Križ's trivalent plural barePlural, supervaluation over the atoms, and allPlural removes its gap, which is the contribution of all.

Main definitions

• readings Q x: the readings of predicating Q of the plurality x.
• barePlural, allPlural: the bare plural sentence and the all-sentence.

Main results

• sInter_readings, sUnion_readings: true on every reading iff true of the whole, and on some reading iff true of some part.
• readings_eq_latticeClosure: the readings of a distributive predication are the lattice generated by the predications of the atoms.
• barePlural_eq_one_iff, barePlural_eq_neg_one_iff: the bare plural is true where every reading of the distributive predicate is, and false where none is.
• allPlural_prevents_nonmax: all forces literal truth and blocks non-maximal use.

Implementation notes

The readings are indexed by upper sets of the whole order, not by sets of parts of x, since only the trace of U on the parts of x matters. Križ and Spector's convex candidate domains, Haslinger and colleagues' tolerance relations and Bar-Lev's subdomain alternatives are all choices of U; the subdomain alternatives are the closure of the atoms under disjunction, a supClosure inside the latticeClosure of the readings. Bottom elements are not parts, so that the vacuous truth of a distributive predicate at the empty plurality yields no reading.

References

• [KS21b]
• [Kri16]
• [HRSW25]
• [BL21]

The readings of a plural predication

def Homogeneity.readings {α : Type u_1} {W : Type u_2} [PartialOrder α] (Q : α → Set W) (x : α) : Set (Set W)

The readings of predicating Q of x ([KS21b]'s (21)) say, for each upper set U containing x, that some non-bottom part of x in U is Q.

Equations

• Homogeneity.readings Q x = {p : Set W | ∃ (U : UpperSet α), x ∈ U ∧ p = {w : W | ∃ z ∈ U, z ≤ x ∧ ¬IsBot z ∧ w ∈ Q z}}

theorem Homogeneity.sInter_readings {α : Type u_1} {W : Type u_2} [PartialOrder α] {Q : α → Set W} {x : α} (hx : ¬IsBot x) : ⋂₀ readings Q x = Q x

True on every reading is true of the whole.

theorem Homogeneity.sUnion_readings {α : Type u_1} {W : Type u_2} [PartialOrder α] {Q : α → Set W} {x : α} : ⋃₀ readings Q x = {w : W | ∃ z ≤ x, ¬IsBot z ∧ w ∈ Q z}

True on some reading is true of some non-bottom part.

theorem Homogeneity.readings_of_minimal {α : Type u_1} {W : Type u_2} [PartialOrder α] {Q : α → Set W} {x : α} (hx : Minimal (fun (x : α) => ¬IsBot x) x) : readings Q x = {Q x}

An atom has a single reading, since nothing short of it is a part.

theorem Homogeneity.supClosed_readings {α : Type u_1} {W : Type u_2} [PartialOrder α] {Q : α → Set W} {x : α} : SupClosed (readings Q x)

The union of two readings is the reading of the union of their upper sets.

theorem Homogeneity.infClosed_readings {α : Type u_1} {W : Type u_2} [SemilatticeSup α] {Q : α → Set W} {x : α} (hQ : ∀ (w : W), SupClosed {z : α | w ∈ Q z}) : InfClosed (readings Q x)

For a cumulative predicate the intersection of two readings is the reading of the intersection of their upper sets, since the sum of two parts that are Q is Q.

theorem Homogeneity.readings_eq_latticeClosure {Atom : Type u_1} {W : Type u_2} {P : Atom → W → Prop} {x : Finset Atom} (hx : x.Nonempty) : readings (fun (z : Finset Atom) => {w : W | ∀ a ∈ z, P a w}) x = latticeClosure ((fun (a : Atom) => {w : W | P a w}) '' ↑x)

The readings of a distributive predication are the lattice generated by the predications of the atoms, each reading being a union of conjunctions of atomic predications and every such combination a reading.

The bare plural and all

def Homogeneity.barePlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : W → SignType

The bare plural sentence "the Xs are P" as a trivalent sentence.

Equations

• Homogeneity.barePlural P x w = SignType.supervaluation x fun (x : Atom) => P x w

def Homogeneity.allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : W → SignType

The all-sentence "all the Xs are P" asserts the bare plural pointwise. Per [Kri16] §3.1, all's semantic contribution is gap removal, so its semantics is derived from the bare plural rather than stipulated.

Equations

• Homogeneity.allPlural P x w = SignType.ofProp (Homogeneity.barePlural P x w = 1)

theorem Homogeneity.gapExt_allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Trivalent.gapExt (allPlural P x) = ∅

all eliminates the extension gap.

theorem Homogeneity.posExt_allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Trivalent.posExt (allPlural P x) = Trivalent.posExt (barePlural P x)

The bare plural and the all-sentence are true in the same worlds.

theorem Homogeneity.negExt_allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Trivalent.negExt (allPlural P x) = Trivalent.negExt (barePlural P x) ∪ Trivalent.gapExt (barePlural P x)

all absorbs the gap into the negative extension.

theorem Homogeneity.isBivalent_allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Trivalent.IsBivalent (allPlural P x)

all-sentences are bivalent.

theorem Homogeneity.allPlural_eq_one_iff {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : allPlural P x w = 1 ↔ ∀ a ∈ x, P a w

An all-sentence is true iff all atoms satisfy P.

theorem Homogeneity.allPlural_eq_neg_one_iff {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : allPlural P x w = -1 ↔ ¬∀ a ∈ x, P a w

An all-sentence is false iff some atom fails P.

theorem Homogeneity.bivalentPred_allPlural_iff {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : bivalentPred (allPlural P x) w = true ↔ ∀ a ∈ x, P a w

bivalentPred of an all-sentence is true iff all atoms satisfy P.

theorem Homogeneity.allPlural_prevents_nonmax {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (q : Setoid W) (w : W) (h : usable q (allPlural P x) w) (a : Atom) : a ∈ x → P a w

If an all-sentence is usable at w, all atoms satisfy P at w, since bivalence turns usability's not-false clause into literal truth.

theorem Homogeneity.allPlural_blocked_by_wide_issue {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (q : Setoid W) (hWide : ∃ (w₁ : W) (w₂ : W), q w₁ w₂ ∧ (∀ a ∈ x, P a w₁) ∧ ¬∀ a ∈ x, P a w₂) : ¬addressesIssue q (allPlural P x)

An all-sentence cannot address a "wide" issue — one with a cell straddling the all/not-all boundary ([Kri16] §3.4).

theorem Homogeneity.allPlural_exceptions_unmentionable {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (q : Setoid W) (w : W) (a : Atom) (ha : a ∈ x) (h : usable q (allPlural P x) w) : P a w

A usable all-sentence leaves no exceptions to mention — "#Although all the professors smiled, Smith didn't" is contradictory. The bare-plural unmentionability result proper ([Kri16] §4.1) is exception_unaddressable.

theorem Homogeneity.allPlural_ne_zero {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : allPlural P x w ≠ 0

An all-sentence is never indefinite.

theorem Homogeneity.barePlural_eq_one_iff {Atom : Type u_1} {W : Type u_2} {P : Atom → W → Prop} [(a : Atom) → (w : W) → Decidable (P a w)] {x : Finset Atom} (hx : x.Nonempty) (w : W) : barePlural P x w = 1 ↔ w ∈ ⋂₀ readings (fun (z : Finset Atom) => {w : W | ∀ a ∈ z, P a w}) x

The bare plural is true where every reading of the distributive predicate is.

theorem Homogeneity.barePlural_eq_neg_one_iff {Atom : Type u_1} {W : Type u_2} {P : Atom → W → Prop} [(a : Atom) → (w : W) → Decidable (P a w)] {x : Finset Atom} (hx : x.Nonempty) (w : W) : barePlural P x w = -1 ↔ w ∉ ⋃₀ readings (fun (z : Finset Atom) => {w : W | ∀ a ∈ z, P a w}) x

The bare plural is false where no reading of the distributive predicate is true.