Documentation

Linglib.Semantics.Homogeneity.Usable

Pragmatic usability of trivalent propositions #

[Kri16]'s pragmatics over Trivalent.Prop3: a proposition is sufficientlyTrue at a world when its issue cell contains a literally-true world, addressesIssue when no cell straddles the true/false boundary, and usable when it is not false, sufficiently true, and addresses the issue. Non-maximal readings are exactly usability at gap-worlds (gap_enables_nonmax); gap removal blocks them (metaAssert_prevents_nonmax); tolerated exceptions cannot be mentioned (exception_unaddressable). communicatedContent is what the hearer learns; strong relevance ([KS21b]) is the bivalent counterpart of Addressing.

Main definitions #

References #

source
def Semantics.Homogeneity.sufficientlyTrue {W : Type u_1} (q : QUD W) (p : Trivalent.Prop3 W) (w : W) :
Prop

p is "true enough" at w relative to issue q: some q-equivalent world makes p literally true. This weakens the maxim of Quality — a speaker need only assert something equivalent, for current purposes, to something true.

Equations
Instances For
    source
    @[instance_reducible]
    instance Semantics.Homogeneity.sufficientlyTrue.instDecidable {W : Type u_1} [Fintype W] (q : QUD W) (p : Trivalent.Prop3 W) (w : W) :
    Decidable (sufficientlyTrue q p w)
    Equations
    source
    theorem Semantics.Homogeneity.literal_imp_sufficient {W : Type u_1} (q : QUD W) (p : Trivalent.Prop3 W) (w : W) (h : p w = Trivalent.true) :
    sufficientlyTrue q p w

    Literal truth implies sufficient truth, for any issue.

    source
    def Semantics.Homogeneity.addressesIssue {W : Type u_1} (q : QUD W) (p : Trivalent.Prop3 W) :
    Prop

    p addresses issue q when no cell of q overlaps both the positive and the negative extension. Gap-worlds are invisible: only cells straddling the true/false boundary disqualify.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance Semantics.Homogeneity.addressesIssue.instDecidable {W : Type u_1} [Fintype W] (q : QUD W) (p : Trivalent.Prop3 W) :
      Decidable (addressesIssue q p)
      Equations
      source
      def Semantics.Homogeneity.usable {W : Type u_1} (q : QUD W) (p : Trivalent.Prop3 W) (w : W) :
      Prop

      p may be used at w: it is not false at w, sufficiently true at w, and addresses the issue.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance Semantics.Homogeneity.usable.instDecidable {W : Type u_1} [Fintype W] (q : QUD W) (p : Trivalent.Prop3 W) (w : W) :
        Decidable (usable q p w)
        Equations
        source
        theorem Semantics.Homogeneity.usable_iff_of_isBivalent {W : Type u_1} {p : Trivalent.Prop3 W} (hbiv : p.isBivalent) (q : QUD W) (w : W) :
        usable q p w ↔ p w = Trivalent.true ∧ addressesIssue q p

        For a bivalent proposition, usability is literal truth plus addressing: sufficient truth adds nothing without gap-worlds.

        Usability at gap-worlds #

        source
        theorem Semantics.Homogeneity.gap_enables_nonmax {W : Type u_1} (q : QUD W) (p : Trivalent.Prop3 W) (w w' : W) (hGap : p w = Trivalent.indet) (hEquiv : q.r w w') (hTrue : p w' = Trivalent.true) (hAddr : addressesIssue q p) :
        usable q p w

        The gap enables non-maximal use: a gapped world whose cell contains a true-world is usable, given addressing.

        source
        theorem Semantics.Homogeneity.metaAssert_prevents_nonmax {W : Type u_1} (q : QUD W) (p : Trivalent.Prop3 W) (w : W) (h : usable q p.metaAssert w) :
        p.metaAssert w = Trivalent.true

        Gap removal forces literal truth for usability: the general form of the headline result that homogeneity removers prevent non-maximal use.

        source
        theorem Semantics.Homogeneity.exception_unaddressable {W : Type u_1} (q : QUD W) (p e : Trivalent.Prop3 W) (w : W) (hUse : usable q p w) (hEw : e w = Trivalent.true) (hEfalse : ∀ (w' : W), p w' = Trivalent.true → e w' = Trivalent.false) :
        ¬addressesIssue q e

        Unmentionability of exceptions ([Kri16] §4.1): when p is used at w under issue q, an exception-mentioning sentence e — true at w but false wherever p is literally true — cannot address the same issue. w's cell contains a literally-true world, and e straddles the true/false boundary between w and that world.

        Communicated content #

        source
        def Semantics.Homogeneity.communicatedContent {W : Type u_1} (q : QUD W) (p : Trivalent.Prop3 W) :
        Set W

        The worlds the hearer considers possible after hearing p under issue q: those indistinguishable, for current purposes, from a world where p is literally true.

        Equations
        Instances For
          source
          @[simp]
          theorem Semantics.Homogeneity.mem_communicatedContent {W : Type u_1} {q : QUD W} {p : Trivalent.Prop3 W} {w : W} :
          w ∈ communicatedContent q p ↔ sufficientlyTrue q p w
          source
          @[instance_reducible]
          instance Semantics.Homogeneity.communicatedContent.instDecidableMem {W : Type u_1} [Fintype W] (q : QUD W) (p : Trivalent.Prop3 W) (w : W) :
          Decidable (w ∈ communicatedContent q p)
          Equations
          source
          theorem Semantics.Homogeneity.posExt_subset_communicated {W : Type u_1} (q : QUD W) (p : Trivalent.Prop3 W) :
          p.posExt ⊆ communicatedContent q p

          Literal truth is always communicated.

          source
          theorem Semantics.Homogeneity.communicatedContent_eq_posExt {W : Type u_1} {p : Trivalent.Prop3 W} (hbiv : p.isBivalent) (q : QUD W) (hAddr : addressesIssue q p) :
          communicatedContent q p = p.posExt

          For a bivalent proposition that addresses the issue, communicated content is exactly the positive extension: no pragmatic weakening.

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

          Coarser issues communicate more: if q' refines q, everything communicated under q' is communicated under q. This is [Kri16]'s key prediction that coarse issues enable non-maximal use.

          Strong relevance #

          Bivalent counterpart of addressesIssue, from [KS21b]: a W → Prop is strongly relevant to an issue when it is constant on each cell. The bivalent bridge to addressesIssue is KrizSpector2021.bivalent_addressing_iff_stronglyRelevant.

          source
          def Semantics.Homogeneity.isStronglyRelevantProp {W : Type u_1} (q : QUD W) (p : W → Prop) :
          Prop

          A proposition is strongly relevant to an issue iff it is constant on each cell of the partition.

          Equations
          Instances For
            source
            def Semantics.Homogeneity.stronglyRelevantSet {W : Type u_1} (q : QUD W) (candidates : Set (W → Prop)) :
            Set (W → Prop)

            Filter a set of propositions to those strongly relevant to q.

            Equations
            Instances For
              source
              theorem Semantics.Homogeneity.trivial_relevant_iff_constant {W : Type u_1} (p : W → Prop) :
              isStronglyRelevantProp QUD.trivial p ↔ ∀ (w₁ w₂ : W), p w₁ ↔ p w₂

              With the trivial QUD, strong relevance is constancy on W.

              source
              theorem Semantics.Homogeneity.exact_all_relevant {W : Type u_1} [BEq W] [LawfulBEq W] (p : W → Prop) :
              isStronglyRelevantProp QUD.exact p

              With the exact QUD, every proposition is strongly relevant.

              source
              theorem Semantics.Homogeneity.exact_stronglyRelevantSet_eq {W : Type u_1} [BEq W] [LawfulBEq W] (candidates : Set (W → Prop)) :
              stronglyRelevantSet QUD.exact candidates = candidates

              With the exact QUD, the strongly-relevant filter is the identity.

              source
              def Semantics.Homogeneity.bivalentPred {W : Type u_1} (p : Trivalent.Prop3 W) :
              W → Bool

              The Bool truth predicate of a proposition. Bridges the trivalent Addressing constraint to bivalent strong-relevance filtering ([KS21b]).

              Equations
              Instances For