Generalised homogeneity for collective predicates

[Kri16] §5.1's generalisation of the homogeneity gap to collective predicates via mereological overlap: a predicate is undefined of a plurality that fails it but overlaps a plurality satisfying it. For distributive predicates this reduces to supervaluation over atoms (generalisedTruthValue_distributive_reduction); for collectives like perform Hamlet the overlapping witness can be a larger group.

Main definitions

• overlaps: two pluralities share an individual (¬ Disjoint).
• generalisedTruthValue: trivalent truth over pluralities.

References

• M. Križ, Homogeneity, Non-Maximality, and All

def Semantics.Homogeneity.overlaps {Atom : Type u_1} (a b : Finset Atom) : Prop

Two pluralities overlap if they share at least one individual.

Equations

• Semantics.Homogeneity.overlaps a b = ¬Disjoint a b

@[instance_reducible]

instance Semantics.Homogeneity.instDecidableOverlaps {Atom : Type u_1} [DecidableEq Atom] (a b : Finset Atom) : Decidable (overlaps a b)

Equations

• Semantics.Homogeneity.instDecidableOverlaps a b = Semantics.Homogeneity.instDecidableOverlaps._aux_1 a b

def Semantics.Homogeneity.generalisedTruthValue {Atom : Type u_1} [DecidableEq Atom] (P : Finset Atom → Prop) [DecidablePred P] (domain : Finset (Finset Atom)) (a : Finset Atom) : Trivalent

Trivalent truth for predicates on pluralities: true if P holds of a, gapped if a fails P but overlaps a domain plurality satisfying it, false otherwise. domain is the set of relevant pluralities — singletons suffice for distributive predicates, collectives need larger groups.

Equations

• Semantics.Homogeneity.generalisedTruthValue P domain a = if P a then Trivalent.true else if ∃ b ∈ domain, Semantics.Homogeneity.overlaps a b ∧ P b then Trivalent.indet else Trivalent.false

theorem Semantics.Homogeneity.generalisedTruthValue_trichotomy {Atom : Type u_1} [DecidableEq Atom] (P : Finset Atom → Prop) [DecidablePred P] (domain : Finset (Finset Atom)) (a : Finset Atom) : generalisedTruthValue P domain a = Trivalent.true ∨ generalisedTruthValue P domain a = Trivalent.false ∨ generalisedTruthValue P domain a = Trivalent.indet

The generalised truth value is a genuine three-way partition.

theorem Semantics.Homogeneity.generalisedTruthValue_eq_true {Atom : Type u_1} [DecidableEq Atom] (P : Finset Atom → Prop) [DecidablePred P] (domain : Finset (Finset Atom)) (a : Finset Atom) (h : P a) : generalisedTruthValue P domain a = Trivalent.true

If P holds of a, the generalised truth value is true.

theorem Semantics.Homogeneity.generalisedTruthValue_distributive_reduction {Atom : Type u_1} [DecidableEq Atom] (pred : Atom → Prop) [DecidablePred pred] (a : Finset Atom) (hne : a.Nonempty) (domain : Finset (Finset Atom)) (hdomain : ∀ x ∈ a, {x} ∈ domain) : generalisedTruthValue (fun (s : Finset Atom) => ∀ x ∈ s, pred x) domain a = Supervaluation.superTrue pred { admissible := a, nonempty := hne }

For distributive predicates the generalised definition coincides with supervaluation over atoms, when the domain includes all member singletons.