Decidable proposition type
Equations
Instances For
The candidate proposition for sub-plurality z: "P holds of all atoms in z".
Equations
- Semantics.Lexical.Plural.Distributivity.candidateProp P z w = decide (∀ a ∈ z, P a w = true)
Instances For
Full candidate set: all sub-plurality propositions.
This is the set S from @cite{kriz-spector-2021} before relevance filtering.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Candidate set parameterized by tolerance.
With identity tolerance: only the maximal candidate. With full tolerance: all sub-plurality candidates.
Equations
- One or more equations did not get rendered due to their size.
Instances For
All candidates in the set are true at w
Equations
- Semantics.Lexical.Plural.Distributivity.trueOnAll candidates w = ∀ p ∈ candidates, p w = true
Instances For
All candidates in the set are false at w
Equations
- Semantics.Lexical.Plural.Distributivity.falseOnAll candidates w = ∀ p ∈ candidates, p w = false
Instances For
Some candidates true, some false (the gap)
Equations
Instances For
Theorem: The maximal candidate is exactly distMaximal.
Theorem: With identity tolerance, the candidate set is a singleton containing only the maximal candidate.
Theorem: With full tolerance, fullCandidateSet (nonempty sub-pluralities) is contained in the full-tolerance candidate set.
Theorem: trueOnAll for the full candidate set iff all atoms satisfy P.
This connects the candidate framework to the simple universal condition.
Theorem: falseOnAll for full candidates iff no atom satisfies P.
- (→): Singleton candidates {a} false → each P(a) fails.
- (←): No P(a) holds → for any nonempty z ⊆ x, some atom in z fails P.
Main Theorem: The trivalent semantics matches the candidate interpretation framework.
pluralTruthValue P x w equals: -.true iff trueOnAll (fullCandidateSet P x) w -.false iff falseOnAll (fullCandidateSet P x) w -.gap iff gapOnCandidates (fullCandidateSet P x) w
This is the central correspondence theorem of @cite{kriz-spector-2021}, showing that the simple trivalent semantics (based on all/some/none) coincides with the more sophisticated "truth on all readings" approach.
- TRUE: via
trueOnAll_full_iff_allSatisfy+pluralTruthValue_eq_true_iff - FALSE: via
falseOnAll_full_iff_noneSatisfy+pluralTruthValue_eq_false_iff - GAP: singleton witnesses for both true and false candidates
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.
This is the key filtering mechanism from @cite{kriz-spector-2021} Section 3.
Equations
- Semantics.Lexical.Plural.Distributivity.isStronglyRelevantProp q p = ∀ (w1 w2 : W), q.sameAnswer w1 w2 = true → p w1 = p w2
Instances For
Decidable version
Equations
- Semantics.Lexical.Plural.Distributivity.isStronglyRelevant q p = Fintype.elems.toList.all fun (w1 : W) => Fintype.elems.toList.all fun (w2 : W) => !q.sameAnswer w1 w2 || p w1 == p w2
Instances For
Theorem: With exact QUD, all propositions are strongly relevant.
The exact QUD distinguishes all worlds, so every proposition trivially respects the partition.
Corollary: With exact QUD, the filtered set equals the original set.
Theorem: With trivial QUD, only constant propositions are strongly relevant.
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.
This is the formal content of @cite{kriz-spector-2021} Section 3's relevance filtering.
Proof idea:
- If q groups w_all (where all satisfy P) with w_almost (where not all satisfy), then candidateProp P x has different values at these QUD-equivalent worlds.
- But strong relevance requires same values at QUD-equivalent worlds.
- Contradiction.
The proof is by contradiction: strong relevance + QUD equivalence forces the maximal candidate to agree on w_all and w_almost, but allSatisfy gives different values.
With identity tolerance, the only tolerant sub-plurality is x itself.
This is because z ⪯ x under identity tolerance iff z = x.
Identity tolerance candidate set contains exactly the maximal proposition.
NOTE: This is a variant of identity_candidateSet_eq_singleton, stating it in terms of the explicit proposition form.
Strong relevance (propositional version): respects QUD partition.
With exact QUD, all propositions are strongly relevant.
The exact QUD distinguishes all worlds, so every proposition aligns with it.
With trivial QUD, only constant propositions are strongly relevant.
The trivial QUD groups all worlds together, so a proposition is relevant iff it has the same value at all worlds.
Key Theorem: The maximal proposition is always strongly relevant to exact QUD.
This shows the connection between distMaximal and the truth-on-all-readings
approach: under the exact QUD, the maximal candidate is always relevant.
Correspondence Theorem: distMaximal characterizes truth on the maximal candidate.
The algebraic operator distMaximal equals the truth value of the unique candidate
generated by identity tolerance. This connects the operator-based approach
to the pragmatic truth-on-all-readings approach of Križ & @cite{kriz-spector-2021}.
Correspondence Theorem: distTolerant with full tolerance is always true.
With full tolerance, any sub-plurality (including the empty set) is tolerant, so distTolerant is true as long as x is in the powerset of itself (always true). The empty set vacuously satisfies the predicate.
Correspondence Theorem: distTolerant unfolds to existence of tolerant witness.
This connects the operator to the candidate interpretation framework.
The deepest compositional innovation of @cite{kriz-spector-2021}: interpretation is parameterized by H, which maps each argument position to a candidate denotation. For the Finset-based setting, H selects a sub-plurality z ⊆ x for each plurality x. The predicate is then evaluated on z instead of x.
The semantic effect of `all` is to *universally quantify* over admissible
values of H — not merely to collapse gaps. This explains:
- Why `all` removes homogeneity (∀H forces agreement across candidates)
- Why `all` interacts scopally with negation
- Why `all` selectively targets one argument position
The `removeGap` operation in `Homogeneity.lean` is a *consequence* of
∀H quantification, not a primitive.
A homogeneity parameter selects, for each plurality, a nonempty sub-plurality to serve as the effective argument. @cite{kriz-spector-2021} §5.3.1: H(n, x) ∈ Cand_x.
Equations
- Semantics.Lexical.Plural.Distributivity.HomParam Atom = (Finset Atom → Finset Atom)
Instances For
An admissible homogeneity parameter maps x to a nonempty sub-plurality of x. This is the Finset-level analog of H(n, x) ∈ Cand_x for distributive predicates, where the candidates are all nonempty sub-pluralities.
Equations
- Semantics.Lexical.Plural.Distributivity.isAdmissible H x = (H x ⊆ x ∧ (H x).Nonempty)
Instances For
The identity parameter: H(x) = x (universal/maximal reading).
Equations
Instances For
Interpretation of a distributive predicate parameterized by H: "P holds of all atoms in H(x)."
Equations
- Semantics.Lexical.Plural.Distributivity.interpWithH P H x w = decide (∀ a ∈ H x, P a w = true)
Instances For
With H = id, interpretation reduces to allSatisfy.
all as universal quantification over admissible H:
true iff for ALL admissible H, the predicate holds.
@cite{kriz-spector-2021} eq. 71.
Equations
- One or more equations did not get rendered due to their size.
Instances For
allViaForallH ↔ allSatisfy: universal quantification over H reduces
to the simple universal check on atoms.
Proof: (→) For each atom a ∈ x, the singleton parameter H_a(x) = {a} is admissible, and interpWithH forces P(a). (←) If all atoms satisfy P, then any sub-plurality does too.
This is the structural derivation of the removeGap effect: all
doesn't stipulate gap removal — it universally quantifies over H,
and the universal check is the only thing that survives.
The trivalent truth value via H quantification matches pluralTruthValue.
TRUE iff ∀H (admissible), interpWithH = true, i.e., allSatisfy. FALSE iff ∀H (admissible), interpWithH = false, i.e., noneSatisfy. GAP otherwise.
This shows that the H-parameterized semantics yields exactly the same
trivalent output as the supervaluation-based pluralTruthValue.
Derived: allPluralTV IS the ∀H quantification.
This replaces the removeGap-based definition with a deeper derivation:
all universally quantifies over homogeneity parameters, and the result
is a bivalent sentence because ∀H agreement leaves no room for gaps.
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. This yields homogeneity (true iff all true, false iff all false, gap iff mixed) and correct predictions in non-monotonic contexts.
The truth-on-all-readings principle determines a trivalent truth value from a set of Boolean candidates: TRUE iff all true, FALSE iff all false, GAP iff mixed. @cite{kriz-spector-2021} §3.2.
This is the Prop-level characterization (avoiding Decidable requirements on Set-quantified conditions).
Conjunction of candidates yields exactly the same three-way partition
as pluralTruthValue for the full candidate set. This IS the "truth
on all readings" ↔ supervaluation correspondence.