Candidate Interpretations for Plural Predication

Formalizes @cite{kriz-spector-2021}'s candidate interpretation framework: the set of sub-plurality propositions, truth-on-all-readings, QUD-based strong relevance filtering, the H parameter, and candidate conjunction.

Dependency

Imports Distributivity.lean for basic plural predicates (allSatisfy, noneSatisfy, pluralTruthValue, Tolerance, distMaximal, distTolerant).

def Semantics.Plurality.Distributivity.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 all atoms in z".

Equations

• Semantics.Plurality.Distributivity.candidateProp P z w = ∀ a ∈ z, P a w

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.candidateProp.instDecidable {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.Distributivity.candidateProp.instDecidable P z w = id inferInstance

def Semantics.Plurality.Distributivity.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 sub-plurality propositions.

This is the set S from @cite{kriz-spector-2021} before relevance filtering.

Equations

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

def Semantics.Plurality.Distributivity.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 parameterized by tolerance.

With identity tolerance: only the maximal candidate. With trivial tolerance: all nonempty sub-plurality candidates.

Equations

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

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

All candidates in the set hold at w

Equations

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

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

All candidates in the set fail at w

Equations

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

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

Some candidates true, some false (the gap)

Equations

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

theorem Semantics.Plurality.Distributivity.candidateProp_x_eq_distMaximal {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) : candidateProp P x = distMaximal P x

Theorem: The maximal candidate is exactly distMaximal.

theorem Semantics.Plurality.Distributivity.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: With identity tolerance, the candidate set is a singleton containing only the maximal candidate.

theorem Semantics.Plurality.Distributivity.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

With trivial tolerance, fullCandidateSet = candidateSet.

theorem Semantics.Plurality.Distributivity.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: trueOnAll for the full candidate set iff all atoms satisfy P.

theorem Semantics.Plurality.Distributivity.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: falseOnAll for full candidates iff no atom satisfies P (when x is nonempty).

theorem Semantics.Plurality.Distributivity.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)

Main Theorem: The trivalent semantics matches the candidate interpretation framework.

def Semantics.Plurality.Distributivity.isStronglyRelevantProp {W : Type u_2} (q : QUD W) (p : W → Prop) [DecidablePred p] : Prop

Strong relevance: a proposition aligns with a QUD's partition.

A proposition p is strongly relevant to QUD q iff p respects the partition: if two worlds are q-equivalent, then p has the same truth value at both.

Equations

• Semantics.Plurality.Distributivity.isStronglyRelevantProp q p = ∀ (w1 w2 : W), q.r w1 w2 → (p w1 ↔ p w2)

def Semantics.Plurality.Distributivity.stronglyRelevantSet {W : Type u_2} (q : QUD W) (candidates : Set (W → Prop)) : Set (W → Prop)

Filter candidate set to strongly relevant propositions. Decidability is handled per-call by the consumer; we keep the membership Set-based.

Equations

• Semantics.Plurality.Distributivity.stronglyRelevantSet q candidates = {p : W → Prop | p ∈ candidates ∧ ∀ (w1 w2 : W), q.r w1 w2 → (p w1 ↔ p w2)}

theorem Semantics.Plurality.Distributivity.exact_all_relevant {W : Type u_2} [Fintype W] [DecidableEq W] [LawfulBEq W] (p : W → Prop) [DecidablePred p] : isStronglyRelevantProp QUD.exact p

With exact QUD, all propositions are strongly relevant.

theorem Semantics.Plurality.Distributivity.exact_stronglyRelevantSet_eq {W : Type u_2} [Fintype W] [DecidableEq W] [LawfulBEq W] (candidates : Set (W → Prop)) : stronglyRelevantSet QUD.exact candidates = candidates

With exact QUD, the filtered set equals the original set.

theorem Semantics.Plurality.Distributivity.trivial_relevant_iff_constant {W : Type u_2} [Fintype W] [DecidableEq W] (p : W → Prop) [DecidablePred p] : isStronglyRelevantProp QUD.trivial p ↔ ∀ (w1 w2 : W), p w1 ↔ p w2

With trivial QUD, only constant propositions are strongly relevant.

theorem Semantics.Plurality.Distributivity.nonMaximality_from_coarse_qud {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype W] [DecidableEq W] (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) : ¬isStronglyRelevantProp q (candidateProp P x)

Non-Maximality Theorem: With a coarse QUD that groups "all P" with "almost all P", the maximal candidate may not be strongly relevant, allowing non-maximal readings.

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

With identity tolerance, the only tolerant sub-plurality is x itself.

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

Maximal proposition is always strongly relevant to exact QUD.

theorem Semantics.Plurality.Distributivity.distMaximal_eq_maximal_candidate {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype W] [DecidableEq W] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : distMaximal P x w ↔ candidateProp P x w

distMaximal IS the maximal candidate proposition.

theorem Semantics.Plurality.Distributivity.distTolerant_iff_exists_tolerant {Atom : Type u_1} {W : Type u_2} [DecidableEq Atom] [Fintype W] [DecidableEq W] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (tol : Tolerance Atom) (x : Finset Atom) (w : W) : distTolerant P tol x w ↔ ∃ z ∈ x.powerset, z.Nonempty ∧ tol.rel z x ∧ ∀ a ∈ z, P a w

distTolerant unfolds to existence of a nonempty tolerant witness.

The deepest compositional innovation of @cite{kriz-spector-2021}: interpretation is parameterized by H, which maps each argument position to a candidate denotation.

@[reducible, inline]

abbrev Semantics.Plurality.Distributivity.HomParam (Atom : Type u_5) : Type u_5

A homogeneity parameter selects, for each plurality, a nonempty sub-plurality to serve as the effective argument.

Equations

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

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

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

Equations

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

def Semantics.Plurality.Distributivity.HomParam.id {Atom : Type u_3} : HomParam Atom

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

Equations

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

theorem Semantics.Plurality.Distributivity.HomParam.id_admissible {Atom : Type u_3} [DecidableEq Atom] [Fintype Atom] (x : Finset Atom) (hne : x.Nonempty) : isAdmissible id x

def Semantics.Plurality.Distributivity.interpWithH {Atom : Type u_3} {W : Type u_4} (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 parameterized by H: "P holds of all atoms in H(x)."

Equations

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

@[implicit_reducible]

instance Semantics.Plurality.Distributivity.interpWithH.instDecidable {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] [Fintype Atom] (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.Distributivity.interpWithH.instDecidable P H x w = id inferInstance

theorem Semantics.Plurality.Distributivity.interpWithH_id {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] [Fintype Atom] (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : interpWithH P HomParam.id x w ↔ allSatisfy P x w

With H = id, interpretation reduces to allSatisfy.

def Semantics.Plurality.Distributivity.allViaForallH {Atom : Type u_3} {W : Type u_4} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (w : W) : Prop

all as universal quantification over admissible H.

Equations

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

theorem Semantics.Plurality.Distributivity.allViaForallH_iff_allSatisfy {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] [Fintype 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

allViaForallH ↔ allSatisfy: universal quantification over H reduces to the simple universal check on atoms.

theorem Semantics.Plurality.Distributivity.forallH_true_iff_pluralTrue {Atom : Type u_3} {W : Type u_4} [DecidableEq Atom] [Fintype 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

The trivalent truth value via H quantification matches pluralTruthValue.

K&S 2021's key departure from @cite{malamud-2012}: the overall meaning of a sentence is the CONJUNCTION of all strongly relevant candidate interpretations, not the disjunction.

theorem Semantics.Plurality.Distributivity.candidateConjunction_trichotomy {W : Type u_3} (candidates : Set (W → Prop)) (w : W) (decAll : Decidable (trueOnAll candidates w)) (decNone : Decidable (falseOnAll candidates w)) : trueOnAll candidates w ∨ falseOnAll candidates w ∨ gapOnCandidates candidates w

The truth-on-all-readings principle: TRUE iff all hold, FALSE iff none hold, GAP iff mixed. (Classical logic + Decidable per-candidate.)

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

Conjunction of candidates yields exactly the same three-way partition as pluralTruthValue for the full candidate set.