structure Phenomena.ScalarImplicatures.CompareSauerland.EpistemicState (W : Type u_1) : Type u_1

An epistemic state represents what the speaker knows. We model this as a set of worlds the speaker considers possible.

• possible : List W

  Worlds compatible with speaker's knowledge

• nonempty : self.possible ≠ []

  Non-empty (speaker knows something is true)

def Phenomena.ScalarImplicatures.CompareSauerland.knows {W : Type u_1} (e : EpistemicState W) (φ : BProp W) : Bool

K operator: speaker knows φ iff φ is true in all epistemically possible worlds.

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.knows e φ = e.possible.all φ

def Phenomena.ScalarImplicatures.CompareSauerland.possible {W : Type u_1} (e : EpistemicState W) (φ : BProp W) : Bool

P operator: speaker considers φ possible.

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.possible e φ = e.possible.any φ

theorem Phenomena.ScalarImplicatures.CompareSauerland.duality {W : Type u_1} (e : EpistemicState W) (φ : BProp W) : (knows e fun (w : W) => !φ w) = false ↔ possible e φ = true

Standard epistemic duality: ¬K¬φ ↔ Pφ

structure Phenomena.ScalarImplicatures.CompareSauerland.ScalarScenario (W : Type u_1) : Type u_1

A scalar scenario specifies an assertion and its alternatives.

• assertion : BProp W

  The asserted proposition

• alternatives : List (BProp W)

  The scalar alternatives (stronger propositions)

def Phenomena.ScalarImplicatures.CompareSauerland.hasPrimaryImplicature {W : Type u_1} (S : ScalarScenario W) (e : EpistemicState W) (ψ : BProp W) : Prop

Primary implicature: speaker doesn't know the stronger alternative.

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.hasPrimaryImplicature S e ψ = (ψ ∈ S.alternatives ∧ Phenomena.ScalarImplicatures.CompareSauerland.knows e ψ = false)

def Phenomena.ScalarImplicatures.CompareSauerland.hasSecondaryImplicature {W : Type u_1} (e : EpistemicState W) (ψ : BProp W) : Prop

Secondary implicature: speaker knows the alternative is false.

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.hasSecondaryImplicature e ψ = ((Phenomena.ScalarImplicatures.CompareSauerland.knows e fun (w : W) => !ψ w) = true)

theorem Phenomena.ScalarImplicatures.CompareSauerland.secondary_blocked_if_possible {W : Type u_1} (e : EpistemicState W) (ψ : BProp W) : possible e ψ = true → (knows e fun (w : W) => !ψ w) = false

Key insight: if ψ is possible, then K¬ψ is blocked.

inductive Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld : Type

Worlds for the disjunction scenario: A∨B with 4 possible truth combinations.

• neither : DisjWorld
• onlyA : DisjWorld
• onlyB : DisjWorld
• both : DisjWorld

instance Phenomena.ScalarImplicatures.CompareSauerland.instDecidableEqDisjWorld : DecidableEq DisjWorld

Equations

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

instance Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjWorld : BEq DisjWorld

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjWorld = { beq := Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjWorld.beq }

def Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjWorld.beq : DisjWorld → DisjWorld → Bool

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.CompareSauerland.instReprDisjWorld : Repr DisjWorld

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instReprDisjWorld = { reprPrec := Phenomena.ScalarImplicatures.CompareSauerland.instReprDisjWorld.repr }

def Phenomena.ScalarImplicatures.CompareSauerland.instReprDisjWorld.repr : DisjWorld → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjWorld : Inhabited DisjWorld

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjWorld = { default := Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjWorld.default }

def Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjWorld.default : DisjWorld

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjWorld.default = Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.neither

def Phenomena.ScalarImplicatures.CompareSauerland.propA : BProp DisjWorld

Proposition A is true

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.propA Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.onlyA = true
• Phenomena.ScalarImplicatures.CompareSauerland.propA Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.both = true
• Phenomena.ScalarImplicatures.CompareSauerland.propA x✝ = false

def Phenomena.ScalarImplicatures.CompareSauerland.propB : BProp DisjWorld

Proposition B is true

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.propB Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.onlyB = true
• Phenomena.ScalarImplicatures.CompareSauerland.propB Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.both = true
• Phenomena.ScalarImplicatures.CompareSauerland.propB x✝ = false

def Phenomena.ScalarImplicatures.CompareSauerland.propAorB : BProp DisjWorld

A ∨ B

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.propAorB Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.neither = false
• Phenomena.ScalarImplicatures.CompareSauerland.propAorB x✝ = true

def Phenomena.ScalarImplicatures.CompareSauerland.propAandB : BProp DisjWorld

A ∧ B

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.propAandB Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.both = true
• Phenomena.ScalarImplicatures.CompareSauerland.propAandB x✝ = false

theorem Phenomena.ScalarImplicatures.CompareSauerland.primary_possibility_correspondence {W : Type u_1} (e : EpistemicState W) (ψ : BProp W) : knows e ψ = false → (possible e fun (w : W) => !ψ w) = true

Theorem (Primary-Possibility Correspondence):

Sauerland: ¬Kψ (speaker doesn't know ψ) RSA: P(¬ψ worlds) > 0 (positive probability on ¬ψ worlds)

These are equivalent when the epistemic state corresponds to the support of the probability distribution.

theorem Phenomena.ScalarImplicatures.CompareSauerland.blocking_correspondence {W : Type u_1} (e : EpistemicState W) (ψ : BProp W) : possible e ψ = true → ¬hasSecondaryImplicature e ψ

Theorem (Blocking Correspondence): Secondary K¬ψ is blocked when Pψ holds.

inductive Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance : Type

Utterances for disjunction scenario

• AorB : DisjUtterance
• A : DisjUtterance
• B : DisjUtterance
• AandB : DisjUtterance

instance Phenomena.ScalarImplicatures.CompareSauerland.instDecidableEqDisjUtterance : DecidableEq DisjUtterance

Equations

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

def Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjUtterance.beq : DisjUtterance → DisjUtterance → Bool

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjUtterance : BEq DisjUtterance

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjUtterance = { beq := Phenomena.ScalarImplicatures.CompareSauerland.instBEqDisjUtterance.beq }

def Phenomena.ScalarImplicatures.CompareSauerland.instReprDisjUtterance.repr : DisjUtterance → ℕ → Std.Format

Equations

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

instance Phenomena.ScalarImplicatures.CompareSauerland.instReprDisjUtterance : Repr DisjUtterance

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instReprDisjUtterance = { reprPrec := Phenomena.ScalarImplicatures.CompareSauerland.instReprDisjUtterance.repr }

def Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjUtterance.default : DisjUtterance

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjUtterance.default = Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance.AorB

instance Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjUtterance : Inhabited DisjUtterance

Equations

• Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjUtterance = { default := Phenomena.ScalarImplicatures.CompareSauerland.instInhabitedDisjUtterance.default }

def Phenomena.ScalarImplicatures.CompareSauerland.disjMeaning : DisjUtterance → DisjWorld → Bool

Literal semantics for disjunction utterances

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.ScalarImplicatures.CompareSauerland.disjMeaning Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance.AorB x✝ = true
• Phenomena.ScalarImplicatures.CompareSauerland.disjMeaning Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance.A Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.onlyA = true
• Phenomena.ScalarImplicatures.CompareSauerland.disjMeaning Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance.A Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.both = true
• Phenomena.ScalarImplicatures.CompareSauerland.disjMeaning Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance.A x✝ = false
• Phenomena.ScalarImplicatures.CompareSauerland.disjMeaning Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance.B Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.onlyB = true
• Phenomena.ScalarImplicatures.CompareSauerland.disjMeaning Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance.B Phenomena.ScalarImplicatures.CompareSauerland.DisjWorld.both = true
• Phenomena.ScalarImplicatures.CompareSauerland.disjMeaning Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance.B x✝ = false
• Phenomena.ScalarImplicatures.CompareSauerland.disjMeaning Phenomena.ScalarImplicatures.CompareSauerland.DisjUtterance.AandB x✝ = false

RSA Graded Exclusivity (Stubs)

RSA evaluation infrastructure (RSA.Eval.L1_world, boolToRat, getScore) has been removed. The RSA L1 computation (disjL1) and graded exclusivity theorems need reimplementation with the new RSAConfig framework.

The key results to reimplement:

• rsa_disjunction_graded_exclusivity: L1("A or B") assigns higher probability to exclusive worlds (onlyA, onlyB) than inclusive (both)
• rsa_both_has_positive_probability: RSA assigns positive (but lower) probability to "both" world (unlike Sauerland's categorical K¬(A∧B))
• p_both_decreases_with_alpha: As α increases, P(both) decreases, approaching Sauerland's categorical framework in the limit
• sauerland_is_rsa_limit: Sauerland's categorical framework is the α → ∞ limit of RSA