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.

inductive Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleU : Type

• weak : ScaleU
• strong : ScaleU

instance Phenomena.ScalarImplicatures.CompareExhaustivity.instDecidableEqScaleU : DecidableEq ScaleU

Equations

• Phenomena.ScalarImplicatures.CompareExhaustivity.instDecidableEqScaleU x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ScalarImplicatures.CompareExhaustivity.instFintypeScaleU : Fintype ScaleU

Equations

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

inductive Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleW : Type

• weakOnly : ScaleW
• both : ScaleW

instance Phenomena.ScalarImplicatures.CompareExhaustivity.instDecidableEqScaleW : DecidableEq ScaleW

Equations

• Phenomena.ScalarImplicatures.CompareExhaustivity.instDecidableEqScaleW x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.ScalarImplicatures.CompareExhaustivity.instFintypeScaleW : Fintype ScaleW

Equations

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

instance Phenomena.ScalarImplicatures.CompareExhaustivity.instNonemptyScaleU : Nonempty ScaleU

instance Phenomena.ScalarImplicatures.CompareExhaustivity.instNonemptyScaleW : Nonempty ScaleW

def Phenomena.ScalarImplicatures.CompareExhaustivity.meaning : ScaleU → ScaleW → Bool

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

Equations

• Phenomena.ScalarImplicatures.CompareExhaustivity.meaning Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleU.weak x✝ = true
• Phenomena.ScalarImplicatures.CompareExhaustivity.meaning Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleU.strong Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleW.both = true
• Phenomena.ScalarImplicatures.CompareExhaustivity.meaning Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleU.strong Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleW.weakOnly = false

noncomputable def Phenomena.ScalarImplicatures.CompareExhaustivity.l0 : ScaleU → ScaleW → ℝ

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

Equations

• Phenomena.ScalarImplicatures.CompareExhaustivity.l0 Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleU.weak x✝ = 1 / 2
• Phenomena.ScalarImplicatures.CompareExhaustivity.l0 Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleU.strong Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleW.both = 1
• Phenomena.ScalarImplicatures.CompareExhaustivity.l0 Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleU.strong Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleW.weakOnly = 0

noncomputable def Phenomena.ScalarImplicatures.CompareExhaustivity.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.

theorem Phenomena.ScalarImplicatures.CompareExhaustivity.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.

theorem Phenomena.ScalarImplicatures.CompareExhaustivity.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".

theorem Phenomena.ScalarImplicatures.CompareExhaustivity.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.

def Phenomena.ScalarImplicatures.CompareExhaustivity.scaleDomain : List ScaleW

Equations

• Phenomena.ScalarImplicatures.CompareExhaustivity.scaleDomain = [Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleW.weakOnly, Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleW.both]

def Phenomena.ScalarImplicatures.CompareExhaustivity.weakMeaning : ScaleW → Bool

Equations

• Phenomena.ScalarImplicatures.CompareExhaustivity.weakMeaning = Phenomena.ScalarImplicatures.CompareExhaustivity.meaning Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleU.weak

def Phenomena.ScalarImplicatures.CompareExhaustivity.strongMeaning : ScaleW → Bool

Equations

• Phenomena.ScalarImplicatures.CompareExhaustivity.strongMeaning = Phenomena.ScalarImplicatures.CompareExhaustivity.meaning Phenomena.ScalarImplicatures.CompareExhaustivity.ScaleU.strong

def Phenomena.ScalarImplicatures.CompareExhaustivity.scaleAlts : List (ScaleW → Bool)

Equations

• Phenomena.ScalarImplicatures.CompareExhaustivity.scaleAlts = [Phenomena.ScalarImplicatures.CompareExhaustivity.weakMeaning, Phenomena.ScalarImplicatures.CompareExhaustivity.strongMeaning]

theorem Phenomena.ScalarImplicatures.CompareExhaustivity.scale_ie : Exhaustification.InnocentExclusion.ieIndices scaleDomain weakMeaning scaleAlts = [1]

Fox's innocent exclusion: "strong" is the only excludable alternative.

theorem Phenomena.ScalarImplicatures.CompareExhaustivity.exh_weak (w : ScaleW) : Exhaustification.InnocentExclusion.exhB scaleDomain scaleAlts weakMeaning w = (weakMeaning w && !strongMeaning w)

exh(weak) = weak ∧ ¬strong.

theorem Phenomena.ScalarImplicatures.CompareExhaustivity.exh_true_at_weakOnly : Exhaustification.InnocentExclusion.exhB scaleDomain scaleAlts weakMeaning ScaleW.weakOnly = true

The world where L1 concentrates is exactly where exh(weak) = true.

theorem Phenomena.ScalarImplicatures.CompareExhaustivity.exh_false_at_both : Exhaustification.InnocentExclusion.exhB scaleDomain scaleAlts weakMeaning ScaleW.both = false

exh(weak) is false at the "both" world — L1 assigns probability 0 there.

instance Phenomena.ScalarImplicatures.CompareExhaustivity.instAlternativeSourceScaleU : Alternatives.AlternativeSource ScaleU

AlternativeSource instance for the {weak, strong} scale.

Equations

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

theorem Phenomena.ScalarImplicatures.CompareExhaustivity.exh_via_alternativeSource (w : ScaleW) : Exhaustification.InnocentExclusion.exhB scaleDomain (List.map meaning (Alternatives.AlternativeSource.alternatives ScaleU.weak)) (meaning ScaleU.weak) w = Exhaustification.InnocentExclusion.exhB scaleDomain scaleAlts weakMeaning w

Exhaustifying via AlternativeSource agrees with the hand-crafted exhB call.

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