@cite{lauer-2013}: Probabilistic Assertion

@cite{lauer-2013}

Models assertion as a speech act governed by probabilistic thresholds. A proposition is assertable when the speaker's credence exceeds a context-dependent threshold. This bridges traditional assertion theories to RSA's probabilistic pragmatic reasoning.

Key Properties

• Credence function: the speaker's subjective probability over worlds (rational-valued, matching RSA's worldPrior)
• Assertability threshold: a credence threshold above which assertion is licensed (matching RSA's alpha parameter)
• Bridge to RSA: Lauer's credence maps to RSA's worldPrior, and the threshold maps to the rationality parameter

Relation to Other Theories

Lauer's model is closest to Stalnaker in structure (no explicit commitment/belief separation), but adds a probabilistic dimension that the CG model lacks. The threshold mechanism provides a quantitative handle on hedging and commitment strength that Krifka's ComP layer models categorically.

structure Theories.Pragmatics.Assertion.Lauer.Credence (W : Type u_1) : Type u_1

A credence function: the speaker's subjective probability assignment to propositions.

Rational-valued (ℚ) for exact computation, matching RSA convention. The function takes a proposition and returns a probability in [0,1].

• prob : List (BProp W × ℚ)

  Probability assignment for a proposition (given as a list of proposition-probability pairs).

• defaultProb : ℚ

  Default credence for propositions not in the list.

def Theories.Pragmatics.Assertion.Lauer.Credence.lookup {W : Type u_1} (c : Credence W) (p : BProp W) [BEq (BProp W)] : ℚ

Look up the credence for a proposition.

Equations

• c.lookup p = match List.find? (fun (x : BProp W × ℚ) => match x with | (q, snd) => q == p) c.prob with | some (fst, v) => v | none => c.defaultProb

def Theories.Pragmatics.Assertion.Lauer.Credence.uniform {W : Type u_1} : Credence W

Uninformative credence: equal probability for everything.

Equations

• Theories.Pragmatics.Assertion.Lauer.Credence.uniform = { prob := [] }

structure Theories.Pragmatics.Assertion.Lauer.LauerState (W : Type u_1) : Type u_1

Lauer's discourse state: speaker credence + assertability threshold

• history of assertions.

The threshold is context-dependent: formal contexts (courtrooms) have higher thresholds than casual conversation.

• credence : Credence W

  Speaker's credence function

• threshold : ℚ

  Assertability threshold (credence must exceed this)

• asserted : Core.Discourse.Commitment.CommitmentSlate W

  List of asserted propositions (for tracking)

def Theories.Pragmatics.Assertion.Lauer.LauerState.empty {W : Type u_1} : LauerState W

Initial state: uniform credence, default threshold, no assertions.

Equations

• Theories.Pragmatics.Assertion.Lauer.LauerState.empty = { credence := Theories.Pragmatics.Assertion.Lauer.Credence.uniform, asserted := Core.Discourse.Commitment.CommitmentSlate.empty }

def Theories.Pragmatics.Assertion.Lauer.LauerState.assert {W : Type u_1} (s : LauerState W) (p : BProp W) : LauerState W

Assert a proposition: add it to the asserted list.

Assertability is a precondition (the speaker SHOULD have credence ≥ threshold), but the operation succeeds regardless — modeling that assertion can occur even when the norm is violated (as in lying).

Equations

• s.assert p = { credence := s.credence, threshold := s.threshold, asserted := s.asserted.add p }

def Theories.Pragmatics.Assertion.Lauer.LauerState.assertable {W : Type u_1} (s : LauerState W) (p : BProp W) [BEq (BProp W)] : Bool

Check if a proposition is assertable (credence ≥ threshold).

Equations

• s.assertable p = decide (s.credence.lookup p ≥ s.threshold)

def Theories.Pragmatics.Assertion.Lauer.LauerState.contextSet {W : Type u_1} (s : LauerState W) : Core.CommonGround.ContextSet W

Context set: worlds compatible with all asserted propositions.

Equations

• s.contextSet w = (s.asserted.toContextSet w = true)

def Theories.Pragmatics.Assertion.Lauer.LauerState.isStable {W : Type u_1} : LauerState W → Bool

Stability: always stable (no table mechanism).

Equations

• x✝.isStable = true

RSA Correspondence

Lauer's probabilistic model maps naturally to RSA parameters:

Lauer	RSA	Role
credence	worldPrior	probability over worlds
threshold	alpha	rationality / commitment level
asserted	utterance history	discourse context

The mapping is conceptual, not formal: RSA's worldPrior is a distribution over worlds (P(w)), while Lauer's credence is a probability over propositions (P(p)). The connection is:

P_Lauer(p) = Σ_{w: p(w)} P_RSA(w)

This lifts RSA's world-level prior to Lauer's proposition-level credence.

theorem Theories.Pragmatics.Assertion.Lauer.always_stable {W : Type u_1} (s : LauerState W) : s.isStable = true

Lauer is always stable (no pending issues mechanism).