Documentation

Linglib.Phenomena.ScalarImplicatures.ExhaustivityLimit

RSA L1 at α → ∞ recovers Fox's exh @cite{fox-2007} #

This file proves the concrete connection between RSA pragmatic inference and Neo-Gricean exhaustification for the simplest non-trivial case: the Horn scale ⟨some, all⟩.

Setup. Two utterances (weak = "some", strong = "all") and two worlds (weakOnly = "some but not all", both = "all"). A belief-based RSA speaker S1 chooses utterances proportional to L0(w|u)^α, where L0 is the literal listener posterior under a uniform prior.

Main result (l1_weak_weakOnly_tendsto_one): The pragmatic listener L1, hearing "some", assigns probability converging to 1 to the "some but not all" world as α → ∞. This IS the scalar implicature: some ∧ ¬all.

Connection to Fox 2007 (§5): Fox's innocent-exclusion computation on the same scale yields exh(some) = some ∧ ¬all — true at weakOnly, false at both. The RSA limit concentrates on exactly the worlds where exh returns true.

The proof factors through two key steps:

  1. At the weakOnly world, "all" is false so S1(some|weakOnly) = 1 exactly (for any α > 0), since rpow(0, α) = 0.
  2. At the both world, "all" is strictly more informative (L0 = 1 vs 1/2), so rpow_luce_eq_softmax converts the rpow ratio to a softmax, and tendsto_softmax_infty_not_max gives S1(some|both) → 0.

Position in the limit chain #

The general RSA→IBR limit theorem (rsa_speaker_to_ibr in IBR/RSABridge.lean) shows that RSA S1 concentrates on the IBR-optimal message as α → ∞ for any InterpGame. This file instantiates that general result for the specific Horn scale ⟨some, all⟩.

Combined with ibr_equals_exhMW (ScalarGames.lean) and @cite{denic-2023}'s entailment_invariant_across_domain_size (Denic2023.lean), the chain shows that RSA cannot escape domain-size blindness in the high-rationality limit — probabilistic mechanisms (like informativeness-based pruning) are the only way out.

source
inductive Phenomena.ScalarImplicatures.ExhaustivityLimit.ScaleU :
Type
Instances For
    source
    @[implicit_reducible]
    instance Phenomena.ScalarImplicatures.ExhaustivityLimit.instDecidableEqScaleU :
    DecidableEq ScaleU
    Equations
    source
    @[implicit_reducible]
    instance Phenomena.ScalarImplicatures.ExhaustivityLimit.instFintypeScaleU :
    Fintype ScaleU
    Equations
    • One or more equations did not get rendered due to their size.
    source
    inductive Phenomena.ScalarImplicatures.ExhaustivityLimit.ScaleW :
    Type
    Instances For
      source
      @[implicit_reducible]
      instance Phenomena.ScalarImplicatures.ExhaustivityLimit.instDecidableEqScaleW :
      DecidableEq ScaleW
      Equations
      source
      @[implicit_reducible]
      instance Phenomena.ScalarImplicatures.ExhaustivityLimit.instFintypeScaleW :
      Fintype ScaleW
      Equations
      • One or more equations did not get rendered due to their size.
      source
      instance Phenomena.ScalarImplicatures.ExhaustivityLimit.instNonemptyScaleU :
      Nonempty ScaleU
      source
      instance Phenomena.ScalarImplicatures.ExhaustivityLimit.instNonemptyScaleW :
      Nonempty ScaleW
      source
      def Phenomena.ScalarImplicatures.ExhaustivityLimit.meaning :
      ScaleU → ScaleW → Bool

      Literal meaning: weak is true everywhere, strong only at "both".

      Equations
      Instances For
        source
        noncomputable def Phenomena.ScalarImplicatures.ExhaustivityLimit.l0 :
        ScaleU → ScaleW → ℝ

        L0(w|u): uniform prior, so 1/|⟦u⟧| if true, 0 if false.

        Equations
        Instances For
          source
          noncomputable def Phenomena.ScalarImplicatures.ExhaustivityLimit.s1 (α : ℝ) (w : ScaleW) (u : ScaleU) :
          ℝ

          S1(u|w, α) = rpow(L0(w|u), α) / Σ_u' rpow(L0(w|u'), α).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            theorem Phenomena.ScalarImplicatures.ExhaustivityLimit.s1_weak_weakOnly (α : ℝ) (hα : 0 < α) :
            s1 α ScaleW.weakOnly ScaleU.weak = 1

            At weakOnly: s1(weak) = 1 for α > 0. "strong" is false, so rpow(0, α) = 0 — "weak" is the only live option.

            source
            theorem Phenomena.ScalarImplicatures.ExhaustivityLimit.s1_weak_both_tendsto_zero :
            Filter.Tendsto (fun (α : ℝ) => s1 α ScaleW.both ScaleU.weak) Filter.atTop (nhds 0)

            S1(weak | both, α) → 0 as α → ∞. "strong" (L0 = 1) is more informative than "weak" (L0 = 1/2), so the softmax speaker concentrates on "strong".

            source
            theorem Phenomena.ScalarImplicatures.ExhaustivityLimit.l1_weak_weakOnly_tendsto_one :
            Filter.Tendsto (fun (α : ℝ) => s1 α ScaleW.weakOnly ScaleU.weak / (s1 α ScaleW.weakOnly ScaleU.weak + s1 α ScaleW.both ScaleU.weak)) Filter.atTop (nhds 1)

            Scalar implicature limit: L1(weakOnly | weak, α) → 1 as α → ∞.

            The pragmatic listener hearing "some" concentrates on worlds where "all" is false. This IS the scalar implicature: some ∧ ¬all.

            source
            def Phenomena.ScalarImplicatures.ExhaustivityLimit.weakMeaning :
            ScaleW → Bool
            Equations
            Instances For
              source
              def Phenomena.ScalarImplicatures.ExhaustivityLimit.strongMeaning :
              ScaleW → Bool
              Equations
              Instances For
                source
                def Phenomena.ScalarImplicatures.ExhaustivityLimit.scaleAlts :
                Finset (Finset ScaleW)

                Alternative set as a Finset (Finset ScaleW): the prejacent and the strong scalemate, each represented by its world support.

                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  def Phenomena.ScalarImplicatures.ExhaustivityLimit.scaleExh :
                  Finset ScaleW

                  The exhaustified prejacent as a Finset ScaleW.

                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    theorem Phenomena.ScalarImplicatures.ExhaustivityLimit.scale_exhIE_eq :
                    scaleExh = {ScaleW.weakOnly}

                    Fox's innocent exclusion concentrates the meaning on weakOnly: exh(some) = some ∧ ¬all, true exactly at the world where the strong alternative fails.

                    source
                    theorem Phenomena.ScalarImplicatures.ExhaustivityLimit.exh_true_at_weakOnly :
                    ScaleW.weakOnly ∈ scaleExh

                    The world where L1 concentrates is exactly where exhIE returns true.

                    source
                    theorem Phenomena.ScalarImplicatures.ExhaustivityLimit.exh_false_at_both :
                    ScaleW.both ∉ scaleExh

                    exhIE excludes the "both" world — L1 assigns probability 0 there.

                    source
                    @[implicit_reducible]
                    instance Phenomena.ScalarImplicatures.ExhaustivityLimit.instAlternativeSourceScaleU :
                    Alternatives.AlternativeSource ScaleU

                    AlternativeSource instance for the {weak, strong} scale.

                    Equations
                    • One or more equations did not get rendered due to their size.
                    source
                    theorem Phenomena.ScalarImplicatures.ExhaustivityLimit.exh_via_alternativeSource :
                    Exhaustification.innocent.exh (Exhaustification.altsFromPreds (List.map meaning (Alternatives.AlternativeSource.alternatives ScaleU.weak))) (Exhaustification.predToFinset (meaning ScaleU.weak)) = scaleExh

                    Exhaustifying via AlternativeSource agrees with the hand-crafted alternative set.

                    This validates the full pipeline: AlternativeSource instance → meanings (via interp = meaning) → exhIE → exhaustified meaning.