Credence-Threshold Assertion

@cite{lauer-2013}

A credence-gated model of assertion: a proposition is assertable when the speaker's credence exceeds a context-dependent threshold. Lauer-adjacent in motivation but not the central @cite{lauer-2013} contribution.

⚠ Naming history (was Lauer.lean)

This file was previously named Lauer.lean but its content is a credence-threshold model, not @cite{lauer-2013}'s headline doxastic / preferential commitment split. The actual Lauer 2013 framework is substrate-supported elsewhere:

• The doxastic / preferential force distinction lives in Core/Discourse/Commitment.lean as CommitmentForce (with .doxastic and .preferential cases).
• Krifka-style commitment spaces consume it via Theories/Dialogue/CommitmentSpace.lean (the force parameter on IndexedWeightedCommitment.commit/refuse and the toDoxasticContextSet / toPreferentialContextSet projections).
• The @cite{condoravdi-lauer-2012} imperative-as-PEP study lives in Phenomena/Directives/Studies/CondoravdiLauer2012.lean.

Key properties of this file

• 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: credence maps to RSA's worldPrior, threshold maps to the rationality parameter

Closest to Stalnaker in structure (no explicit commitment/belief separation), but adds a probabilistic dimension that the bare CG model lacks.

structure Dialogue.CredenceThreshold.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 (Set W × ℚ)

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

• defaultProb : ℚ

  Default credence for propositions not in the list.

def Dialogue.CredenceThreshold.Credence.lookup {W : Type u_1} (c : Credence W) (p : Set W) [BEq (Set W)] : ℚ

Look up the credence for a proposition.

Equations

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

def Dialogue.CredenceThreshold.Credence.uniform {W : Type u_1} : Credence W

Uninformative credence: equal probability for everything.

Equations

• Dialogue.CredenceThreshold.Credence.uniform = { prob := [] }

structure Dialogue.CredenceThreshold.State (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 Dialogue.CredenceThreshold.State.empty {W : Type u_1} : State W

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

Equations

• Dialogue.CredenceThreshold.State.empty = { credence := Dialogue.CredenceThreshold.Credence.uniform, asserted := Core.Discourse.Commitment.CommitmentSlate.empty }

def Dialogue.CredenceThreshold.State.assert {W : Type u_1} (s : State W) (p : Set W) : State 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 Dialogue.CredenceThreshold.State.assertable {W : Type u_1} (s : State W) (p : Set W) [BEq (Set W)] : Prop

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

Equations

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

@[implicit_reducible]

instance Dialogue.CredenceThreshold.State.instDecidableAssertable {W : Type u_1} (s : State W) (p : Set W) [BEq (Set W)] : Decidable (s.assertable p)

Equations

• s.instDecidableAssertable p = Dialogue.CredenceThreshold.State.instDecidableAssertable._aux_1 s p

def Dialogue.CredenceThreshold.State.contextSet {W : Type u_1} (s : State W) : Core.CommonGround.ContextSet W

Context set: worlds compatible with all asserted propositions.

Equations

• s.contextSet w = s.asserted.toContextSet w

def Dialogue.CredenceThreshold.State.isStable {W : Type u_1} : State W → Prop

Stability: always stable (no table mechanism).

Equations

• x✝.isStable = True

@[implicit_reducible]

instance Dialogue.CredenceThreshold.State.instDecidableIsStable {W : Type u_1} (s : State W) : Decidable s.isStable

Equations

• s.instDecidableIsStable = isTrue ⋯

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 Dialogue.CredenceThreshold.always_stable {W : Type u_1} (s : State W) : s.isStable

Always stable (no pending issues mechanism).

@[implicit_reducible]

instance Dialogue.CredenceThreshold.instHasContextSetState {W : Type u_1} : Core.CommonGround.HasContextSet (State W) W

Credence-threshold states project to a context set via the asserted-list intersection (contextSet). The credence + threshold machinery gates which assertions can occur; once asserted, the propositional contribution to the context set is the same as Stalnakerian narrowing.

Equations

• Dialogue.CredenceThreshold.instHasContextSetState = { toContextSet := Dialogue.CredenceThreshold.State.contextSet }