Candidate Interpretations for Plural Predication

[KS21b]

Formalises a cover-cell simplification of [KS21b]'s candidate interpretation framework. The simplification treats each candidate as a subset-universal proposition λ w => ∀ a ∈ z, P a w for some sub-plurality z ⊆ x. This captures K&S's predictions in monotonic contexts but is not their actual Cand_x: K&S build candidates from convex closures of sub-plurality bundles (substrate at ordConnectedHull), yielding generalised-quantifier candidates that pattern with [Sch96b]-style covers and [Bri98]'s ill-fitting covers but diverge in non-monotonic contexts. For the cases formalised here the two predictions coincide; the divergent non-monotonic cases are flagged in the Todo.

The contrast with [Mal12]'s earlier disjunctive aggregation is made kernel-checked in malamud_strictly_weaker_when_mixed.

Main declarations

• pluralTruthValue — trivalent K&S denotation via Core.Duality.dist.
• inGap, homogeneity_gap_symmetric, pluralTruthValue_neg — the homogeneity theorem.
• candidateProp, fullCandidateSet, candidateSet — the (cover-cell) candidate-set machinery.
• trueOnAll, falseOnAll, gapOnCandidates — the truth-on-all-readings trichotomy.
• pluralTruthValue_{true,false,indet}_iff_* — correspondence between trivalent denotation and candidate semantics.
• HomParam, isAdmissible, interpWithH, allViaForallH — homogeneity parameter machinery (single-argument, sub-plurality-valued simplification of K&S's multi-argument GQ-valued H).
• malamudDisjunction, malamud_strictly_weaker_when_mixed — the [Mal12] contrast made kernel-checked.

Implementation notes

Strong relevance (constancy on QUD cells) is defined at the substrate level in Semantics/Homogeneity/Basic.lean as Semantics.Homogeneity.isStronglyRelevantProp and re-exported here. The bivalent bridge to [Kri16]'s addressesIssue is proved in Studies/KrizSpector2021.lean.

Todo

• Replace candidateProp with K&S's faithful Cand_x (def. 21 in [KS21b] — UNVERIFIED definition number) via ordConnectedHull. Current simplification matches K&S predictions only in monotonic contexts; non-monotonic cases (e.g. the "exactly one student read the books" example, see Studies/KrizSpector2021.lean) require the enriched generalised quantifiers.
• Re-type HomParam as ArgIdx × Finset Atom → Cand_x to support K&S's multi-argument candidate selection (their Desideratum B on co-referential plurals).
• Bridge to [BL21]'s Exh^{IE+II} + ∃-PL rival implicature account.

Trivalent truth values

@[reducible]

def Semantics.Plurality.Trivalent.pluralTruthValue {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) : Core.Duality.Truth3

The trivalent truth value for plural predication "the Xs are P".

• TRUE: all atoms satisfy P (vacuously on ∅)
• FALSE: nonempty plurality with no atoms satisfying P
• GAP: witnesses on both sides

This is the core of [KS21b]: predication on a plurality is super-true iff the predicate holds at every atom, super-false iff it fails at every atom, gap otherwise. The [vF66] supervaluation framing (each atom as a specification point) is documented by Semantics.Supervaluation.superTrue_eq_dist.

Equations

• Semantics.Plurality.Trivalent.pluralTruthValue P x w = Core.Duality.dist x fun (a : Atom) => P a w

@[simp]

theorem Semantics.Plurality.Trivalent.pluralTruthValue_eq_true_iff {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.true ↔ allSatisfy P x w

@[simp]

theorem Semantics.Plurality.Trivalent.pluralTruthValue_eq_false_iff {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.false ↔ x.Nonempty ∧ noneSatisfy P x w

@[simp]

theorem Semantics.Plurality.Trivalent.pluralTruthValue_eq_gap_iff {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.indet ↔ (∃ a ∈ x, P a w) ∧ ∃ a ∈ x, ¬P a w

theorem Semantics.Plurality.Trivalent.allSatisfy_imp_noneSatisfy_neg {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : allSatisfy P x w → noneSatisfy (fun (a : Atom) (w : W) => ¬P a w) x w

theorem Semantics.Plurality.Trivalent.noneSatisfy_imp_allSatisfy_neg {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : noneSatisfy P x w → allSatisfy (fun (a : Atom) (w : W) => ¬P a w) x w

The homogeneity theorem

def Semantics.Plurality.Trivalent.inGap {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) : Prop

The gap condition: some but not all atoms satisfy P.

Equations

• Semantics.Plurality.Trivalent.inGap P x w = ((∃ a ∈ x, P a w) ∧ ∃ a ∈ x, ¬P a w)

theorem Semantics.Plurality.Trivalent.homogeneity_gap_symmetric {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : inGap P x w ↔ inGap (fun (a : Atom) (w : W) => ¬P a w) x w

Homogeneity Theorem ([KS21b]). The gap is symmetric under negation: a world is in the gap for P iff it is in the gap for ¬P. This explains why "the Xs are P" and "the Xs aren't P" are both undefined in exactly the same worlds.

theorem Semantics.Plurality.Trivalent.pluralTruthValue_gap_iff_neg_gap {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (_hne : x.Nonempty) : pluralTruthValue P x w = Core.Duality.Truth3.indet ↔ pluralTruthValue (fun (a : Atom) (w : W) => ¬P a w) x w = Core.Duality.Truth3.indet

Corollary: pluralTruthValue is gap iff the negated version is gap.

theorem Semantics.Plurality.Trivalent.pluralTruthValue_neg {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hne : x.Nonempty) : pluralTruthValue (fun (a : Atom) (w : W) => ¬P a w) x w = match pluralTruthValue P x w with | Core.Duality.Truth3.true => Core.Duality.Truth3.false | Core.Duality.Truth3.false => Core.Duality.Truth3.true | Core.Duality.Truth3.indet => Core.Duality.Truth3.indet

Homogeneity Polarity: truth and falsity swap under negation on nonempty pluralities; the gap is preserved. Empty x makes both allSatisfy P and allSatisfy ¬P vacuously true, so the theorem requires x.Nonempty.

Candidate interpretations

def Semantics.Plurality.Trivalent.candidateProp {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (z : Finset Atom) : W → Prop

The candidate proposition for sub-plurality z: P holds of every atom in z. This is the cover-cell simplification of [KS21b]'s candidate; see module-level Todo for the convex-closure-enriched faithful version. Definitionally equal to distMaximal P z.

Equations

• Semantics.Plurality.Trivalent.candidateProp P z = Semantics.Plurality.distMaximal P z

@[implicit_reducible]

instance Semantics.Plurality.Trivalent.instDecidableCandidateProp {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (z : Finset Atom) (w : W) : Decidable (candidateProp P z w)

Equations

• Semantics.Plurality.Trivalent.instDecidableCandidateProp P z w = Semantics.Plurality.Trivalent.instDecidableCandidateProp._aux_1 P z w

def Semantics.Plurality.Trivalent.fullCandidateSet {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Set (W → Prop)

Full candidate set: all nonempty sub-plurality propositions.

Equations

• Semantics.Plurality.Trivalent.fullCandidateSet P x = {p : W → Prop | ∃ z ∈ x.powerset, z.Nonempty ∧ p = Semantics.Plurality.Trivalent.candidateProp P z}

def Semantics.Plurality.Trivalent.candidateSet {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (tol : Tolerance Atom) (x : Finset Atom) : Set (W → Prop)

Candidate set filtered by a tolerance relation. With identity tolerance only the maximal candidate survives; with trivial tolerance every nonempty sub-plurality candidate is included.

Equations

• Semantics.Plurality.Trivalent.candidateSet P tol x = {p : W → Prop | ∃ z ∈ x.powerset, z.Nonempty ∧ tol.rel z x ∧ p = Semantics.Plurality.Trivalent.candidateProp P z}

Truth-on-all-readings trichotomy

def Semantics.Plurality.Trivalent.trueOnAll {W : Type u_2} (candidates : Set (W → Prop)) (w : W) : Prop

All candidates in the set hold at w.

Equations

• Semantics.Plurality.Trivalent.trueOnAll candidates w = ∀ p ∈ candidates, p w

def Semantics.Plurality.Trivalent.falseOnAll {W : Type u_2} (candidates : Set (W → Prop)) (w : W) : Prop

All candidates in the set fail at w.

Equations

• Semantics.Plurality.Trivalent.falseOnAll candidates w = ∀ p ∈ candidates, ¬p w

def Semantics.Plurality.Trivalent.gapOnCandidates {W : Type u_2} (candidates : Set (W → Prop)) (w : W) : Prop

Some candidates true, some false at w (the homogeneity gap).

Equations

• Semantics.Plurality.Trivalent.gapOnCandidates candidates w = ((∃ p ∈ candidates, p w) ∧ ∃ p ∈ candidates, ¬p w)

Identity- and trivial-tolerance reductions

theorem Semantics.Plurality.Trivalent.identity_candidateSet_eq_singleton {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (hne : x.Nonempty) : candidateSet P Tolerance.identity x = {candidateProp P x}

theorem Semantics.Plurality.Trivalent.fullCandidateSet_eq_candidateSet_trivial {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : fullCandidateSet P x = candidateSet P Tolerance.trivial x

theorem Semantics.Plurality.Trivalent.identity_tolerant_iff_eq {Atom : Type u_1} [DecidableEq Atom] (x z : Finset Atom) : Tolerance.identity.rel z x ↔ z = x

Identity tolerance is just plurality equality.

Truth-on-all ↔ trivalent semantics

Three correspondence lemmas connecting trueOnAll / falseOnAll / gapOnCandidates over the (cover-cell) candidate set to the trivalent pluralTruthValue.

theorem Semantics.Plurality.Trivalent.trueOnAll_full_iff_allSatisfy {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : trueOnAll (fullCandidateSet P x) w ↔ allSatisfy P x w

theorem Semantics.Plurality.Trivalent.falseOnAll_full_iff_noneSatisfy {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (_hne : x.Nonempty) : falseOnAll (fullCandidateSet P x) w ↔ noneSatisfy P x w

theorem Semantics.Plurality.Trivalent.pluralTruthValue_true_iff_trueOnAll {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.true ↔ trueOnAll (fullCandidateSet P x) w

theorem Semantics.Plurality.Trivalent.pluralTruthValue_false_iff_falseOnAll {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hne : x.Nonempty) : pluralTruthValue P x w = Core.Duality.Truth3.false ↔ falseOnAll (fullCandidateSet P x) w

theorem Semantics.Plurality.Trivalent.pluralTruthValue_indet_iff_gapOnCandidates {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : pluralTruthValue P x w = Core.Duality.Truth3.indet ↔ gapOnCandidates (fullCandidateSet P x) w

theorem Semantics.Plurality.Trivalent.pluralTruthValue_eq_candidateSemantics {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (hne : x.Nonempty) : (pluralTruthValue P x w = Core.Duality.Truth3.true ↔ trueOnAll (fullCandidateSet P x) w) ∧ (pluralTruthValue P x w = Core.Duality.Truth3.false ↔ falseOnAll (fullCandidateSet P x) w) ∧ (pluralTruthValue P x w = Core.Duality.Truth3.indet ↔ gapOnCandidates (fullCandidateSet P x) w)

Consolidated form bundling the three correspondence lemmas.

QUD relevance for K&S candidates

isStronglyRelevantProp lives in Semantics.Homogeneity (substrate); these are the K&S-specific specialisations applied to candidateProp.

theorem Semantics.Plurality.Trivalent.maximal_relevant_to_exact {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [BEq W] [LawfulBEq W] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) : Homogeneity.isStronglyRelevantProp QUD.exact (candidateProp P x)

The maximal candidate is always strongly relevant to the exact QUD.

theorem Semantics.Plurality.Trivalent.nonMaximality_from_coarse_qud {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (q : QUD W) (w_all w_almost : W) (h_equiv : q.r w_all w_almost) (h_all : allSatisfy P x w_all) (h_not_all : ¬allSatisfy P x w_almost) : ¬Homogeneity.isStronglyRelevantProp q (candidateProp P x)

Non-Maximality from a coarse QUD: when the QUD groups an all-true world with a not-all-true world, the maximal candidate is not strongly relevant — opening the door to a non-maximal interpretation.

The homogeneity parameter H

K&S parameterise interpretation by H, mapping each argument position to a candidate denotation. The formalisation here treats H as a single-argument sub-plurality selector — a simplification of K&S's multi-argument candidate-GQ-valued H (their H is morally ArgIdx × Plurality → Cand_x, supporting their Desideratum B on co-referential plural arguments). The reductive allViaForallH_iff_allSatisfy below reflects this simplification: K&S's actual H does not collapse to atom-universal in non-monotonic positions.

def Semantics.Plurality.Trivalent.HomParam (Atom : Type u_3) : Type u_3

A homogeneity parameter selects, for each plurality, a sub-plurality.

Equations

• Semantics.Plurality.Trivalent.HomParam Atom = (Finset Atom → Finset Atom)

def Semantics.Plurality.Trivalent.isAdmissible {Atom : Type u_1} (H : HomParam Atom) (x : Finset Atom) : Prop

An admissible homogeneity parameter maps x to a nonempty sub-plurality.

Equations

• Semantics.Plurality.Trivalent.isAdmissible H x = (H x ⊆ x ∧ (H x).Nonempty)

def Semantics.Plurality.Trivalent.HomParam.id {Atom : Type u_1} : HomParam Atom

The identity parameter H(x) = x (universal/maximal reading).

Equations

• Semantics.Plurality.Trivalent.HomParam.id x = x

theorem Semantics.Plurality.Trivalent.isAdmissible_id {Atom : Type u_1} [DecidableEq Atom] (x : Finset Atom) (hne : x.Nonempty) : isAdmissible HomParam.id x

def Semantics.Plurality.Trivalent.interpWithH {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (H : HomParam Atom) (x : Finset Atom) (w : W) : Prop

Interpretation of a distributive predicate parameterised by H.

Equations

• Semantics.Plurality.Trivalent.interpWithH P H x w = ∀ a ∈ H x, P a w

@[implicit_reducible]

instance Semantics.Plurality.Trivalent.instDecidableInterpWithH {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (H : HomParam Atom) (x : Finset Atom) (w : W) : Decidable (interpWithH P H x w)

Equations

• Semantics.Plurality.Trivalent.instDecidableInterpWithH P H x w = Semantics.Plurality.Trivalent.instDecidableInterpWithH._aux_1 P H x w

def Semantics.Plurality.Trivalent.allViaForallH {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) : Prop

Universal quantification over admissible H.

Equations

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

theorem Semantics.Plurality.Trivalent.allViaForallH_iff_allSatisfy {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : allViaForallH P x w ↔ allSatisfy P x w

Universal H-quantification reduces to atom-wise universal, in the file's simplified H typing. K&S's actual H, valued in candidate GQs, does not collapse this way in non-monotonic positions.

theorem Semantics.Plurality.Trivalent.forallH_true_iff_pluralTrue {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : allViaForallH P x w ↔ pluralTruthValue P x w = Core.Duality.Truth3.true

Trivalent truth via H-quantification matches pluralTruthValue.

Candidate conjunction vs Malamud's disjunction

K&S compute sentence meaning as the conjunction of all strongly relevant candidate interpretations. [Mal12]'s earlier proposal used disjunction: a sentence is true iff some candidate is. The contrast is empirically critical in non-monotonic contexts and was K&S's headline departure from Malamud; the divergence theorem below makes the prose claim kernel-checked.

theorem Semantics.Plurality.Trivalent.candidateConjunction_trichotomy {W : Type u_2} (candidates : Set (W → Prop)) (w : W) [Decidable (trueOnAll candidates w)] [Decidable (falseOnAll candidates w)] : trueOnAll candidates w ∨ falseOnAll candidates w ∨ gapOnCandidates candidates w

Truth-on-all trichotomy: a candidate set is true-on-all, false-on-all, or mixed (gap). Classical disjunction over decidable cases.

def Semantics.Plurality.Trivalent.malamudDisjunction {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) : Prop

[Mal12]'s disjunctive aggregation: a sentence is true iff some candidate is. Contrasts with trueOnAll's conjunctive aggregation.

Equations

• Semantics.Plurality.Trivalent.malamudDisjunction P x w = ∃ p ∈ Semantics.Plurality.Trivalent.fullCandidateSet P x, p w

theorem Semantics.Plurality.Trivalent.trueOnAll_imp_malamud {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (a : Atom) (ha : a ∈ x) : trueOnAll (fullCandidateSet P x) w → malamudDisjunction P x w

K&S's conjunction entails Malamud's disjunction, given any atom witness to make the candidate set inhabited.

theorem Semantics.Plurality.Trivalent.malamud_strictly_weaker_when_mixed {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (h_some : ∃ a ∈ x, P a w) (h_other : ∃ b ∈ x, ¬P b w) : malamudDisjunction P x w ∧ ¬trueOnAll (fullCandidateSet P x) w

Divergence theorem. When P has mixed truth values on x at w — at least one atom satisfies P and at least one does not — Malamud's disjunction holds at w while K&S's conjunction fails. K&S's prose departure from [Mal12] made kernel-checked.

Bridge to Bar-Lev's existPL

[Mal12]'s disjunctive aggregation collapses to [BL21]'s existPL with full domain: both express "some atom satisfies P". This makes the prior Bar-Lev / K&S silent-divergence connection kernel-checked. The K&S divergence theorem (malamud_strictly_weaker_when_mixed) immediately yields the polarity-asymmetric existPL divergence corollary below.

theorem Semantics.Plurality.Trivalent.malamudDisjunction_eq_existPL_full {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : malamudDisjunction P x w ↔ Implicature.existPL x P x w

Malamud's disjunctive aggregation IS Bar-Lev's existPL on the full domain. Establishes that the two prose-cited rival frameworks coincide on this primitive.

theorem Semantics.Plurality.Trivalent.existPL_not_eq_pluralTruthValue_true {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) (h_some : ∃ a ∈ x, P a w) (h_other : ∃ b ∈ x, ¬P b w) : Implicature.existPL x P x w ∧ pluralTruthValue P x w ≠ Core.Duality.Truth3.true

Divergence theorem (Bar-Lev vs K&S). On mixed-truth data, Bar-Lev's existPL (bivalent existential) holds while K&S's pluralTruthValue is not .true. This is the polarity-asymmetric contrast that distinguishes implicature-strengthening accounts from trivalent-gap accounts in non-monotonic contexts.

Bridge to [Sch96b] covers

Cover and Trivalent operate at different conceptual levels — Cover is a relation on Set (Finset Atom) × Finset Atom ("these parts cover that whole"), Trivalent's candidate is a function Finset Atom → (W → Prop) ("this sub-plurality produces this proposition"). They share the substrate of "non-empty sub-pluralities of x" but the operations remain distinct. The bridge below makes the forward direction explicit: every cell of a finite cover produces a candidate in fullCandidateSet.

theorem Semantics.Plurality.Trivalent.mem_fullCandidateSet_of_cover_cell {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) {parts : Finset (Finset Atom)} {hne : parts.Nonempty} (hCover : Cover.IsFinCover parts hne x) {z : Finset Atom} (hz : z ∈ parts) (hzNe : z.Nonempty) : candidateProp P z ∈ fullCandidateSet P x

Cover cells are candidates: any non-empty cell of a finite cover of x (in the [Sch96b] sense) corresponds to a candidate in fullCandidateSet P x. The cover relation constrains how parts join to x; the candidate function lifts each part to its sub-plurality-universal proposition.