Semantics.Homogeneity — Substrate for Trivalent Predication and Pragmatic Usability

@cite{kriz-2015} @cite{kriz-2016} @cite{fine-1975} @cite{beaver-krahmer-2001}

Domain-independent substrate for theories of homogeneity and non-maximality. The framework is anchored on @cite{kriz-2015} (Križ's dissertation); the published @cite{kriz-2016} is the first detailed application to plural definites and all. Both rely on Fine's supervaluation (@cite{fine-1975}) and Beaver-Krahmer's assertion operator (@cite{beaver-krahmer-2001}, encoded here as Truth3.metaAssert).

Layered structure

This file is the substrate for Phenomena.Plurals.Studies.Kriz2016 (the plural-specific instantiation) and for downstream consumers across plurals, conditionals, modality, generics, and summative predicates that exhibit homogeneity gaps.

Spec-point instantiations

Domain	Spec points	Remover	Anchored at
Plural definites	atoms	all	Phenomena.Plurals.Studies.Kriz2016
Conditionals	closest P-worlds	necessarily	§6 below + Conditionals.Counterfactual
Summative (spatial)	spatial parts	completely / whole	not yet formalized
Generics	subkinds	all	not yet formalized; cf. Cohen1999 (different equation)
Modal	best worlds	necessarily	Phenomena.Modality.Studies.AghaJeretic2022

The shared structure is supervaluation over specification points.

Contents

• §1 Trivalent Sentence Denotations: SentenceTV, posExt/negExt/gapExt, isHomogeneous, isBivalent.
• §2 Supervaluation as Homogeneity Source: supervaluationTV via SpecSpace.
• §3 Homogeneity Removal: removeGap = Truth3.metaAssert ∘ · lifted pointwise; preserves the positive extension while collapsing the gap into the negative.
• §4 Pragmatic Usability: sufficientlyTrue, addressesIssue, usable.
• §5 Communicated Content: communicatedContent + bivalentPred bridge.
• §6 Conditional Homogeneity (CEM): conditionalTV / strictConditionalTV. See Conditionals.Counterfactual.selectional_as_supervaluation for the equivalence with the selectional formulation.
• §7 Generalised Homogeneity (Collective Predicates): generalisedTV via Finset overlap (¬ Disjoint), uniformly handling distributive and collective predicates.
• §8 Cross-Domain: domain-independent consequences (gap_enables_nonmax, removed_prevents_nonmax, gap_not_false).

@[reducible, inline]

abbrev Semantics.Homogeneity.SentenceTV (W : Type u_2) : Type u_2

A trivalent sentence denotation: maps worlds to truth values. This is the general type for any sentence that may exhibit homogeneity.

Equations

• Semantics.Homogeneity.SentenceTV W = (W → Core.Duality.Truth3)

def Semantics.Homogeneity.posExt {W : Type u_1} (S : SentenceTV W) : Set W

Positive extension: worlds where the sentence is true.

Equations

• Semantics.Homogeneity.posExt S = {w : W | S w = Core.Duality.Truth3.true}

def Semantics.Homogeneity.negExt {W : Type u_1} (S : SentenceTV W) : Set W

Negative extension: worlds where the sentence is false.

Equations

• Semantics.Homogeneity.negExt S = {w : W | S w = Core.Duality.Truth3.false}

def Semantics.Homogeneity.gapExt {W : Type u_1} (S : SentenceTV W) : Set W

Extension gap: worlds where the sentence is neither true nor false.

Equations

• Semantics.Homogeneity.gapExt S = {w : W | S w = Core.Duality.Truth3.indet}

theorem Semantics.Homogeneity.extensions_partition {W : Type u_1} (S : SentenceTV W) (w : W) : w ∈ posExt S ∨ w ∈ negExt S ∨ w ∈ gapExt S

The three extensions partition the world space.

theorem Semantics.Homogeneity.posExt_negExt_disjoint {W : Type u_1} (S : SentenceTV W) : posExt S ∩ negExt S = ∅

The positive and negative extensions are disjoint.

def Semantics.Homogeneity.isHomogeneous {W : Type u_1} (S : SentenceTV W) : Prop

A sentence is homogeneous if its extension gap is non-empty. The gap is what enables non-maximal readings.

Equations

• Semantics.Homogeneity.isHomogeneous S = (Semantics.Homogeneity.gapExt S ≠ ∅)

def Semantics.Homogeneity.isBivalent {W : Type u_1} (S : SentenceTV W) : Prop

A sentence is bivalent if it has no extension gap. all, necessarily, and completely make sentences bivalent.

Equations

• Semantics.Homogeneity.isBivalent S = ∀ (w : W), S w = Core.Duality.Truth3.true ∨ S w = Core.Duality.Truth3.false

theorem Semantics.Homogeneity.isBivalent_iff_not_homogeneous {W : Type u_1} (S : SentenceTV W) : isBivalent S ↔ ¬isHomogeneous S

Bivalence and homogeneity are complementary: a sentence is bivalent iff it has no extension gap.

Every supervaluation instance gives rise to a trivalent sentence. The specification points can be: - Atoms of a plurality (plural definites) - Accessible worlds (conditionals) - Spatial parts (summative predicates) - Subkinds (generics)

The shared structure: TRUE iff the predicate holds at ALL spec points,
FALSE iff it fails at ALL, GAP iff it holds at some but not all. 

def Semantics.Homogeneity.supervaluationTV {Spec : Type u_2} {W : Type u_3} (eval : W → Spec → Prop) [(w : W) → (s : Spec) → Decidable (eval w s)] (space : W → Supervaluation.SpecSpace Spec) : SentenceTV W

Construct a trivalent sentence from a supervaluation instance. eval w gives the Prop predicate over spec points at world w, and space w gives the spec space at world w.

Equations

• Semantics.Homogeneity.supervaluationTV eval space w = Semantics.Supervaluation.superTrue (eval w) (space w)

theorem Semantics.Homogeneity.supervaluationTV_true_iff {Spec : Type u_2} {W : Type u_3} (eval : W → Spec → Prop) [(w : W) → (s : Spec) → Decidable (eval w s)] (space : W → Supervaluation.SpecSpace Spec) (w : W) : supervaluationTV eval space w = Core.Duality.Truth3.true ↔ ∀ s ∈ (space w).admissible, eval w s

A supervaluation sentence is true iff the predicate holds at all specs.

theorem Semantics.Homogeneity.supervaluationTV_false_iff {Spec : Type u_2} {W : Type u_3} (eval : W → Spec → Prop) [(w : W) → (s : Spec) → Decidable (eval w s)] (space : W → Supervaluation.SpecSpace Spec) (w : W) : supervaluationTV eval space w = Core.Duality.Truth3.false ↔ ∀ s ∈ (space w).admissible, ¬eval w s

A supervaluation sentence is false iff the predicate fails at all specs.

theorem Semantics.Homogeneity.supervaluationTV_gap_iff {Spec : Type u_2} {W : Type u_3} (eval : W → Spec → Prop) [(w : W) → (s : Spec) → Decidable (eval w s)] (space : W → Supervaluation.SpecSpace Spec) (w : W) : supervaluationTV eval space w = Core.Duality.Truth3.indet ↔ (∃ s ∈ (space w).admissible, eval w s) ∧ ∃ s ∈ (space w).admissible, ¬eval w s

A supervaluation sentence is gapped iff witnesses exist on both sides.

A homogeneity remover is any operation that eliminates the extension gap, making the sentence bivalent. Linguistically:

| Domain      | Remover         | Example                          |
|-------------|-----------------|----------------------------------|
| Plurals     | `all`           | "All the professors smiled"      |
| Conditionals| `necessarily`   | "If Mary comes, John will nec…"  |
| Spatial     | `completely`    | "The flag is completely blue"    |
| Spatial     | `whole`         | "The whole wall is painted"      |

Semantically, removal collapses the gap into the negative extension:
gap-worlds become false-worlds, preserving the positive extension. The
pointwise operator is exactly the assertion operator 𝒜 of
@cite{beaver-krahmer-2001}, available as `Truth3.metaAssert`. 

def Semantics.Homogeneity.removeGap {W : Type u_1} (S : SentenceTV W) : SentenceTV W

Remove homogeneity: collapse gap into negative extension. Defined as Truth3.metaAssert lifted pointwise — see Truth3.lean for the underlying assertion operator.

Equations

• Semantics.Homogeneity.removeGap S w = (S w).metaAssert

theorem Semantics.Homogeneity.removeGap_bivalent {W : Type u_1} (S : SentenceTV W) : isBivalent (removeGap S)

Removal produces a bivalent sentence.

theorem Semantics.Homogeneity.removeGap_posExt_eq {W : Type u_1} (S : SentenceTV W) : posExt (removeGap S) = posExt S

Removal preserves the positive extension.

theorem Semantics.Homogeneity.removeGap_negExt_eq {W : Type u_1} (S : SentenceTV W) : negExt (removeGap S) = negExt S ∪ gapExt S

Removal absorbs the gap into the negative extension.

theorem Semantics.Homogeneity.removeGap_not_homogeneous {W : Type u_1} (S : SentenceTV W) : ¬isHomogeneous (removeGap S)

Removed sentences are never homogeneous.

The pragmatic mechanism that derives non-maximal readings from the homogeneity gap. Two independent principles interact:

1. **Sufficient Truth**: weakens Quality to "true enough for current purposes"
2. **Addressing an Question**: restricts which sentences can be used for which
   issues, based on alignment between truth-value boundaries and issue cells

Together, they predict that a sentence can be used at a gap-world iff
(i) a literally-true world is in the same issue cell, and (ii) no cell
straddles the true/false boundary. 

def Semantics.Homogeneity.sufficientlyTrue {W : Type u_1} (q : QUD W) (S : SentenceTV W) (w : W) : Prop

Sufficient Truth: S is "true enough" at world w relative to issue I iff there is a world w' that is I-equivalent to w where S is literally true.

This weakens the standard maxim of quality: a speaker need not assert something literally true, only something equivalent to something true for current purposes.

Equations

• Semantics.Homogeneity.sufficientlyTrue q S w = ∃ (w' : W), q.r w w' ∧ S w' = Core.Duality.Truth3.true

theorem Semantics.Homogeneity.literal_imp_sufficient {W : Type u_1} (q : QUD W) (S : SentenceTV W) (w : W) (h : S w = Core.Duality.Truth3.true) : sufficientlyTrue q S w

Literal truth implies sufficient truth (for any issue).

def Semantics.Homogeneity.addressesIssue {W : Type u_1} (q : QUD W) (S : SentenceTV W) : Prop

Addressing an Question: S may be used to address issue I only if no cell of I overlaps with both the positive and the negative extension.

Gap-worlds are invisible: a cell containing true-worlds and gap-worlds is fine. Only a cell straddling the true/false boundary is problematic.

Equations

• Semantics.Homogeneity.addressesIssue q S = ¬∃ (w₁ : W) (w₂ : W), q.r w₁ w₂ ∧ S w₁ = Core.Duality.Truth3.true ∧ S w₂ = Core.Duality.Truth3.false

def Semantics.Homogeneity.usable {W : Type u_1} (q : QUD W) (S : SentenceTV W) (w : W) : Prop

A sentence may be used at w iff: (1) S is not false at w, (2) S is sufficiently true at w, and (3) S addresses the issue.

Equations

• Semantics.Homogeneity.usable q S w = (S w ≠ Core.Duality.Truth3.false ∧ Semantics.Homogeneity.sufficientlyTrue q S w ∧ Semantics.Homogeneity.addressesIssue q S)

theorem Semantics.Homogeneity.bivalent_usable_iff_true {W : Type u_1} (q : QUD W) (S : SentenceTV W) (hbiv : isBivalent S) (w : W) : usable q S w ↔ S w = Core.Duality.Truth3.true ∧ addressesIssue q S

For bivalent sentences, usability reduces to literal truth + addressing. Sufficient Truth adds nothing because there are no gap-worlds.

def Semantics.Homogeneity.communicatedContent {W : Type u_1} (q : QUD W) (S : SentenceTV W) : Set W

The communicated content of S relative to issue I: the set of worlds the hearer considers possible after hearing S.

This is the union of all issue cells that overlap with ⟦S⟧⁺. The hearer infers not that S is literally true, but that the actual world is indistinguishable (relative to current purposes) from one where S is literally true.

Equations

• Semantics.Homogeneity.communicatedContent q S = {w : W | Semantics.Homogeneity.sufficientlyTrue q S w}

theorem Semantics.Homogeneity.posExt_subset_communicated {W : Type u_1} (q : QUD W) (S : SentenceTV W) : posExt S ⊆ communicatedContent q S

Literal truth is always communicated.

theorem Semantics.Homogeneity.bivalent_communicated_eq_posExt {W : Type u_1} (q : QUD W) (S : SentenceTV W) (hbiv : isBivalent S) (hAddr : addressesIssue q S) : communicatedContent q S = posExt S

For bivalent sentences that address the issue, communicated content equals the positive extension — no pragmatic weakening is possible.

This is the key consequence of gap removal: all/necessarily/completely force literal truth to be communicated.

theorem Semantics.Homogeneity.communicatedContent_antitone {W : Type u_1} (q q' : QUD W) (S : SentenceTV W) (hRef : ∀ (w₁ w₂ : W), q'.r w₁ w₂ → q.r w₁ w₂) : communicatedContent q' S ⊆ communicatedContent q S

Communicated content is antitone in issue refinement: coarser issues (bigger cells) communicate more content. If q' refines q (q' is finer), then everything communicated under q' is also communicated under q.

This is @cite{kriz-2016}'s key prediction: coarser QUDs enable more non-maximal use. The finite model in Phenomena.Plurals.Studies.Kriz2016 demonstrates this: coarseQ communicates smithNeutral but fineQ does not.

def Semantics.Homogeneity.bivalentPred {W : Type u_1} (S : SentenceTV W) : W → Bool

Extract the Bool truth predicate from a bivalent sentence. Used to bridge between the trivalent Addressing constraint and bivalent strong-relevance filtering (Križ & Spector 2021).

Equations

• Semantics.Homogeneity.bivalentPred S w = (S w == Core.Duality.Truth3.true)

@cite{kriz-2016} §6.4: Conditionals are the modal analogue of plural definites. "If P, Q" universally quantifies over closest P-worlds, just as "the Xs are Q" universally quantifies over atoms. The conditional excluded middle (CEM) — the observation that "if P, Q" seems neither true nor false when Q holds at some but not all closest P-worlds — IS homogeneity.

| Plural domain | Conditional domain  |
|---------------|---------------------|
| atoms         | closest P-worlds    |
| `all`         | `necessarily`       |
| bare plural   | bare conditional    |
| gap (some)    | CEM (some worlds)   |

@cite{stalnaker-1981} @cite{von-fintel-1999} 

def Semantics.Homogeneity.conditionalTV {W : Type u_2} (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] : SentenceTV W

A bare conditional "if P, Q" as a trivalent sentence. The spec points are the closest P-worlds; the eval function is Q. TRUE if Q holds at all closest P-worlds, FALSE if Q fails at all, GAP otherwise (conditional excluded middle).

This is the same computation as selectionalCounterfactual in Theories.Semantics.Conditionals.Counterfactual, which proves the equivalence with superTrue via selectional_as_supervaluation. The two formalizations use different input representations (Finset vs SimilarityOrdering) but compute the same three-valued truth value.

Equations

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

def Semantics.Homogeneity.strictConditionalTV {W : Type u_2} (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] : SentenceTV W

A strict conditional "if P, necessarily Q" — the all of conditionals. Defined as gap removal on the bare conditional: necessarily collapses the homogeneity gap, just as all does for plurals.

Equations

• Semantics.Homogeneity.strictConditionalTV closestPWorlds Q = Semantics.Homogeneity.removeGap (Semantics.Homogeneity.conditionalTV closestPWorlds Q)

theorem Semantics.Homogeneity.strictConditionalTV_bivalent {W : Type u_2} (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] : isBivalent (strictConditionalTV closestPWorlds Q)

Strict conditionals are bivalent — necessarily removes the gap, just as all removes homogeneity for plurals.

theorem Semantics.Homogeneity.conditionalTV_posExt_eq {W : Type u_2} (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] : posExt (conditionalTV closestPWorlds Q) = posExt (strictConditionalTV closestPWorlds Q)

Positive extensions agree: the bare conditional and the strict conditional are true in the same worlds. Parallel to all_posExt_eq for plurals.

theorem Semantics.Homogeneity.necessarily_prevents_nonmax {W : Type u_2} (q : QUD W) (closestPWorlds : W → Finset W) (Q : W → Prop) [DecidablePred Q] (w : W) (h : usable q (strictConditionalTV closestPWorlds Q) w) (hne : (closestPWorlds w).Nonempty) (w' : W) : w' ∈ closestPWorlds w → Q w'

necessarily prevents non-maximal use of conditionals, just as all does for plurals. If a strict conditional is usable at w, Q holds at all closest P-worlds (when they exist).

@cite{kriz-2016} §5.1: Homogeneity for collective predicates is defined via mereological overlap, not individual atoms. A predicate P is undefined of plurality a if a is not in P's positive extension but overlaps with some plurality that is.

For distributive predicates, this reduces to the atom-based definition
in `Distributivity.lean`: the overlapping witness is a singleton {x}
where x ∈ a and P(x).

For collective predicates like "perform Hamlet", the overlapping witness
can be a larger group: "the boys" overlaps with "all the students", and
if all the students are performing Hamlet, the boys' predication is
undefined (not false). 

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

Two pluralities overlap if they share at least one individual. Defined as ¬ Disjoint, the mathlib idiom.

Equations

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

@[implicit_reducible]

instance Semantics.Homogeneity.instDecidableOverlaps {Atom : Type u_2} [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.generalisedTV {Atom : Type u_2} [DecidableEq Atom] (P : Finset Atom → Prop) [DecidablePred P] (domain : Finset (Finset Atom)) (a : Finset Atom) : Core.Duality.Truth3

Generalised homogeneity: trivalent truth for predicates on pluralities. Handles both distributive and collective predicates uniformly.

• TRUE: P holds of a
• GAP: P doesn't hold of a, but some overlapping plurality in domain satisfies P
• FALSE: no overlapping plurality in domain satisfies P

domain is the set of all relevant pluralities (e.g., all subgroups of the universe of discourse). For distributive predicates, singletons suffice; for collective predicates, larger groups are needed.

Equations

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

theorem Semantics.Homogeneity.generalisedTV_trichotomy {Atom : Type u_2} [DecidableEq Atom] (P : Finset Atom → Prop) [DecidablePred P] (domain : Finset (Finset Atom)) (a : Finset Atom) : generalisedTV P domain a = Core.Duality.Truth3.true ∨ generalisedTV P domain a = Core.Duality.Truth3.false ∨ generalisedTV P domain a = Core.Duality.Truth3.indet

Generalised homogeneity is a genuine three-way partition.

theorem Semantics.Homogeneity.generalisedTV_true_of_holds {Atom : Type u_2} [DecidableEq Atom] (P : Finset Atom → Prop) [DecidablePred P] (domain : Finset (Finset Atom)) (a : Finset Atom) (h : P a) : generalisedTV P domain a = Core.Duality.Truth3.true

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

theorem Semantics.Homogeneity.generalisedTV_distributive_reduction {Atom : Type u_2} [DecidableEq Atom] (pred : Atom → Prop) [DecidablePred pred] (a : Finset Atom) (hne : a.Nonempty) (domain : Finset (Finset Atom)) (hdomain : ∀ x ∈ a, {x} ∈ domain) : generalisedTV (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 singletons of members. The distributive predicate ∀ x ∈ s, pred x is checked against each sub-plurality; the overlap condition reduces to checking individual atoms of a.

The central insight of @cite{kriz-2016}: all homogeneity phenomena share the same pragmatic mechanism. Once a domain has been identified as exhibiting homogeneity (via any of the sources above), the SAME sufficientlyTrue + addressesIssue mechanism derives non-maximal readings, and the SAME removeGap operation explains why removers (all, necessarily, completely, whole) block them.

The following theorems are domain-independent consequences. 

theorem Semantics.Homogeneity.removed_prevents_nonmax {W : Type u_2} (q : QUD W) (S : SentenceTV W) (w : W) (h : usable q (removeGap S) w) : removeGap S w = Core.Duality.Truth3.true

Any bivalent sentence (one whose gap has been removed) forces literal truth for usability. This is the general form of the headline result: homogeneity removers prevent non-maximal use.

theorem Semantics.Homogeneity.gap_enables_nonmax {W : Type u_2} (q : QUD W) (S : SentenceTV W) (w w' : W) (hGap : S w = Core.Duality.Truth3.indet) (hEquiv : q.r w w') (hTrue : S w' = Core.Duality.Truth3.true) (hAddr : addressesIssue q S) : usable q S w

The gap enables non-maximal use: if S is gapped at w and w's cell contains a true-world, then S is usable at w (assuming addressing).

theorem Semantics.Homogeneity.gap_not_false {W : Type u_2} (S : SentenceTV W) (w : W) (h : S w = Core.Duality.Truth3.indet) : S w ≠ Core.Duality.Truth3.false

Gap-worlds are never false, so they satisfy the first usability condition.