structure SauerlandRSA.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 SauerlandRSA.knows {W : Type u_1} (e : EpistemicState W) (φ : BProp W) : Bool

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

Equations

• SauerlandRSA.knows e φ = e.possible.all φ

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

P operator: speaker considers φ possible.

Equations

• SauerlandRSA.possible e φ = e.possible.any φ

theorem SauerlandRSA.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 SauerlandRSA.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 SauerlandRSA.hasPrimaryImplicature {W : Type u_1} (S : ScalarScenario W) (e : EpistemicState W) (ψ : BProp W) : Prop

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

Equations

• SauerlandRSA.hasPrimaryImplicature S e ψ = (ψ ∈ S.alternatives ∧ SauerlandRSA.knows e ψ = false)

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

Secondary implicature: speaker knows the alternative is false.

Equations

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

theorem SauerlandRSA.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 SauerlandRSA.DisjWorld : Type

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

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

instance SauerlandRSA.instDecidableEqDisjWorld : DecidableEq DisjWorld

Equations

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

def SauerlandRSA.instBEqDisjWorld.beq : DisjWorld → DisjWorld → Bool

Equations

• SauerlandRSA.instBEqDisjWorld.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance SauerlandRSA.instBEqDisjWorld : BEq DisjWorld

Equations

• SauerlandRSA.instBEqDisjWorld = { beq := SauerlandRSA.instBEqDisjWorld.beq }

instance SauerlandRSA.instReprDisjWorld : Repr DisjWorld

Equations

• SauerlandRSA.instReprDisjWorld = { reprPrec := SauerlandRSA.instReprDisjWorld.repr }

def SauerlandRSA.instReprDisjWorld.repr : DisjWorld → ℕ → Std.Format

Equations

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

instance SauerlandRSA.instInhabitedDisjWorld : Inhabited DisjWorld

Equations

• SauerlandRSA.instInhabitedDisjWorld = { default := SauerlandRSA.instInhabitedDisjWorld.default }

def SauerlandRSA.instInhabitedDisjWorld.default : DisjWorld

Equations

• SauerlandRSA.instInhabitedDisjWorld.default = SauerlandRSA.DisjWorld.neither

def SauerlandRSA.propA : BProp DisjWorld

Proposition A is true

Equations

• SauerlandRSA.propA SauerlandRSA.DisjWorld.onlyA = true
• SauerlandRSA.propA SauerlandRSA.DisjWorld.both = true
• SauerlandRSA.propA x✝ = false

def SauerlandRSA.propB : BProp DisjWorld

Proposition B is true

Equations

• SauerlandRSA.propB SauerlandRSA.DisjWorld.onlyB = true
• SauerlandRSA.propB SauerlandRSA.DisjWorld.both = true
• SauerlandRSA.propB x✝ = false

def SauerlandRSA.propAorB : BProp DisjWorld

A ∨ B

Equations

• SauerlandRSA.propAorB SauerlandRSA.DisjWorld.neither = false
• SauerlandRSA.propAorB x✝ = true

def SauerlandRSA.propAandB : BProp DisjWorld

A ∧ B

Equations

• SauerlandRSA.propAandB SauerlandRSA.DisjWorld.both = true
• SauerlandRSA.propAandB x✝ = false

theorem SauerlandRSA.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 SauerlandRSA.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 SauerlandRSA.DisjUtterance : Type

Utterances for disjunction scenario

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

instance SauerlandRSA.instDecidableEqDisjUtterance : DecidableEq DisjUtterance

Equations

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

def SauerlandRSA.instBEqDisjUtterance.beq : DisjUtterance → DisjUtterance → Bool

Equations

• SauerlandRSA.instBEqDisjUtterance.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance SauerlandRSA.instBEqDisjUtterance : BEq DisjUtterance

Equations

• SauerlandRSA.instBEqDisjUtterance = { beq := SauerlandRSA.instBEqDisjUtterance.beq }

def SauerlandRSA.instReprDisjUtterance.repr : DisjUtterance → ℕ → Std.Format

Equations

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

instance SauerlandRSA.instReprDisjUtterance : Repr DisjUtterance

Equations

• SauerlandRSA.instReprDisjUtterance = { reprPrec := SauerlandRSA.instReprDisjUtterance.repr }

instance SauerlandRSA.instInhabitedDisjUtterance : Inhabited DisjUtterance

Equations

• SauerlandRSA.instInhabitedDisjUtterance = { default := SauerlandRSA.instInhabitedDisjUtterance.default }

def SauerlandRSA.instInhabitedDisjUtterance.default : DisjUtterance

Equations

• SauerlandRSA.instInhabitedDisjUtterance.default = SauerlandRSA.DisjUtterance.AorB

def SauerlandRSA.disjMeaning : DisjUtterance → DisjWorld → Bool

Literal semantics for disjunction utterances

Equations

• SauerlandRSA.disjMeaning SauerlandRSA.DisjUtterance.AorB SauerlandRSA.DisjWorld.neither = false
• SauerlandRSA.disjMeaning SauerlandRSA.DisjUtterance.AorB x✝ = true
• SauerlandRSA.disjMeaning SauerlandRSA.DisjUtterance.A SauerlandRSA.DisjWorld.onlyA = true
• SauerlandRSA.disjMeaning SauerlandRSA.DisjUtterance.A SauerlandRSA.DisjWorld.both = true
• SauerlandRSA.disjMeaning SauerlandRSA.DisjUtterance.A x✝ = false
• SauerlandRSA.disjMeaning SauerlandRSA.DisjUtterance.B SauerlandRSA.DisjWorld.onlyB = true
• SauerlandRSA.disjMeaning SauerlandRSA.DisjUtterance.B SauerlandRSA.DisjWorld.both = true
• SauerlandRSA.disjMeaning SauerlandRSA.DisjUtterance.B x✝ = false
• SauerlandRSA.disjMeaning SauerlandRSA.DisjUtterance.AandB SauerlandRSA.DisjWorld.both = true
• SauerlandRSA.disjMeaning SauerlandRSA.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