Documentation

Linglib.Semantics.Homogeneity.Plural

Homogeneity: the plural instantiation #

Plural definite predication as the atoms-instantiation of the homogeneity substrate, after [Kri16]: barePlural P x is the trivalent sentence "the Xs are P" (supervaluation over the atoms of the plurality), and allPlural P x is its gap removal — all's semantic contribution. Originates with [Kri16]; consumed by Studies/Kriz2016.lean, Studies/BarLev2021.lean, and Studies/KrizSpector2021.lean.

Main definitions #

Main results #

References #

source
def Semantics.Homogeneity.barePlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :
Trivalent.Prop3 W

The bare plural sentence "the Xs are P" as a trivalent sentence.

Equations
Instances For
    source
    def Semantics.Homogeneity.allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :
    Trivalent.Prop3 W

    The all-sentence "all the Xs are P". Per [Kri16] §3.1, all's semantic contribution is gap removal, so the semantics is derived from the bare plural via Prop3.metaAssert rather than stipulated.

    Equations
    Instances For
      source
      theorem Semantics.Homogeneity.gapExt_allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :
      (allPlural P x).gapExt = ∅

      all eliminates the extension gap.

      source
      theorem Semantics.Homogeneity.not_isHomogeneous_allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :
      ¬isHomogeneous (allPlural P x)

      An all-sentence is never homogeneous.

      source
      theorem Semantics.Homogeneity.posExt_allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :
      (allPlural P x).posExt = (barePlural P x).posExt

      The bare plural and the all-sentence are true in the same worlds.

      source
      theorem Semantics.Homogeneity.negExt_allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :
      (allPlural P x).negExt = (barePlural P x).negExt ∪ (barePlural P x).gapExt

      all absorbs the gap into the negative extension.

      source
      theorem Semantics.Homogeneity.isBivalent_allPlural {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) :
      (allPlural P x).isBivalent

      all-sentences are bivalent.

      source
      theorem Semantics.Homogeneity.allPlural_eq_true_iff {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) :
      allPlural P x w = Trivalent.true ↔ Plurality.allSatisfy P x w

      An all-sentence is true iff all atoms satisfy P.

      source
      theorem Semantics.Homogeneity.bivalentPred_allPlural_eq_allSatisfy {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) :
      bivalentPred (allPlural P x) w = true ↔ Plurality.allSatisfy P x w

      bivalentPred of an all-sentence is true iff allSatisfy holds. Cf. KrizSpector2021.all_addressing_iff_relevant.

      source
      theorem Semantics.Homogeneity.allPlural_prevents_nonmax {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (q : QUD W) (w : W) (h : usable q (allPlural P x) w) :
      Plurality.allSatisfy P x w

      If an all-sentence is usable at w, all atoms satisfy P at w: bivalence turns usability's not-false clause into literal truth. Cf. allPlural_blocked_by_wide_issue for the complementary Addressing direction.

      source
      theorem Semantics.Homogeneity.allPlural_blocked_by_wide_issue {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (q : QUD W) (hWide : ∃ (w₁ : W) (w₂ : W), q.r w₁ w₂ ∧ Plurality.allSatisfy P x w₁ ∧ ¬Plurality.allSatisfy P x w₂) :
      ¬addressesIssue q (allPlural P x)

      An all-sentence cannot address a "wide" issue — one with a cell straddling the all/not-all boundary ([Kri16] §3.4).

      source
      theorem Semantics.Homogeneity.allPlural_exceptions_unmentionable {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (q : QUD W) (w : W) (a : Atom) (ha : a ∈ x) (h : usable q (allPlural P x) w) :
      P a w

      A usable all-sentence leaves no exceptions to mention: "#Although all the professors smiled, Smith didn't" is contradictory. The bare-plural unmentionability result proper ([Kri16] §4.1) is exception_unaddressable.

      source
      theorem Semantics.Homogeneity.barePlural_eq_superTrue {Atom : Type u_1} {W : Type u_2} (P : Atom → W → Prop) [(a : Atom) → (w : W) → Decidable (P a w)] (x : Finset Atom) (hne : x.Nonempty) (w : W) :
      barePlural P x w = Supervaluation.superTrue (fun (a : Atom) => P a w) { admissible := x, nonempty := hne }

      The bare plural at w equals superTrue with atoms as specification points and P(·, w) as the evaluation function — plural predication is supervaluation over atoms ([Fin75]).

      source
      theorem Semantics.Homogeneity.allPlural_ne_indet {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) :
      allPlural P x w ≠ Trivalent.indet

      An all-sentence is never indefinite.