Assertion Theory Interface

@cite{brandom-1994} @cite{farkas-bruce-2010} @cite{gunlogson-2001} @cite{krifka-2015} @cite{lauer-2013} @cite{stalnaker-1978}

Abstract interface for comparing theories of assertion, following the same interface-and-instantiation pattern used for ImplicatureTheory.

Each theory implements AssertionTheory by providing:

• A state type representing the discourse state
• Operations for assertion, context set extraction, and stability
• Boolean flags indicating which phenomena the theory models

Theories Compared

Theory	Commitment ≠ Belief	Retraction	Source Marking
Stalnaker	No	No	No
Farkas & Bruce	Yes (dcS/dcL ≠ cg)	No	No
Krifka	Yes	Yes	No
Brandom	Yes (entitlements)	Yes	No
Gunlogson	Yes	Yes	Yes
Lauer	Yes (credence)	No	No

inductive Interfaces.AssertionOutcome : Type

The possible outcomes of an assertion in discourse.

Not all theories distinguish all four outcomes:

• Stalnaker: only accepted (assertion = CG update)
• Farkas & Bruce: accepted vs pending (table model)
• Krifka/Brandom: all four (commitment space / scorekeeping)

• accepted : AssertionOutcome

  Proposition enters the common ground

• pending : AssertionOutcome

  Proposition on the table, awaiting resolution

• retracted : AssertionOutcome

  Previously accepted proposition withdrawn

• challenged : AssertionOutcome

  Assertion met with a demand for reasons

instance Interfaces.instDecidableEqAssertionOutcome : DecidableEq AssertionOutcome

Equations

• Interfaces.instDecidableEqAssertionOutcome x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Interfaces.instReprAssertionOutcome : Repr AssertionOutcome

Equations

• Interfaces.instReprAssertionOutcome = { reprPrec := Interfaces.instReprAssertionOutcome.repr }

def Interfaces.instReprAssertionOutcome.repr : AssertionOutcome → ℕ → Std.Format

Equations

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

def Interfaces.instBEqAssertionOutcome.beq : AssertionOutcome → AssertionOutcome → Bool

Equations

• Interfaces.instBEqAssertionOutcome.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Interfaces.instBEqAssertionOutcome : BEq AssertionOutcome

Equations

• Interfaces.instBEqAssertionOutcome = { beq := Interfaces.instBEqAssertionOutcome.beq }

def Interfaces.instInhabitedAssertionOutcome.default : AssertionOutcome

Equations

• Interfaces.instInhabitedAssertionOutcome.default = Interfaces.AssertionOutcome.accepted

instance Interfaces.instInhabitedAssertionOutcome : Inhabited AssertionOutcome

Equations

• Interfaces.instInhabitedAssertionOutcome = { default := Interfaces.instInhabitedAssertionOutcome.default }

class Interfaces.AssertionTheory (T : Type) : Type 1

Abstract interface for theories of assertion.

Each theory provides a state type, an assertion operation, and a way to extract the common ground. Boolean flags indicate which discourse phenomena the theory can model.

Following the ImplicatureTheory pattern: the interface is minimal, with rich comparison infrastructure built on top.

• State : Type → Type

  The theory's discourse state representation. Parameterized by world type (at Type level, matching BProp W).

• initial {W : Type} : State T W

  The initial (empty) discourse state.

• assert {W : Type} : State T W → BProp W → State T W

  Assert a proposition, updating the discourse state.

• contextSet {W : Type} : State T W → Core.CommonGround.ContextSet W

  Extract the context set (worlds compatible with common ground).

• isStable {W : Type} : State T W → Bool

  Is the discourse state stable (no pending issues)?

• separatesCommitmentFromBelief : Bool

  Does the theory separate public commitment from private belief?

  • false: Stalnaker (assertion = adding to shared beliefs)
  • true: Krifka, Brandom, Gunlogson (commitment ≠ belief)
• supportsRetraction : Bool

  Does the theory support retraction of prior commitments?

  • false: Stalnaker, Farkas & Bruce (monotonic CG)
  • true: Krifka, Brandom (commitment can be withdrawn)
• modelsSourceMarking : Bool

  Does the theory model source marking (who generated the commitment)?

  • false: all theories except Gunlogson
  • true: Gunlogson (self- vs other-generated)

def Interfaces.theoriesAgreeOnContextSet {T1 T2 : Type} [AssertionTheory T1] [AssertionTheory T2] {W : Type} (s1 : AssertionTheory.State T1 W) (s2 : AssertionTheory.State T2 W) (p : BProp W) : Prop

Two theories agree on the context set after asserting a proposition.

Equations

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

def Interfaces.theoriesAgreeOnStability {T1 T2 : Type} [AssertionTheory T1] [AssertionTheory T2] {W : Type} (s1 : AssertionTheory.State T1 W) (s2 : AssertionTheory.State T2 W) (p : BProp W) : Bool

Two theories agree on stability after asserting a proposition.

Equations

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

def Interfaces.bothSeparateCommitment {T1 T2 : Type} [AssertionTheory T1] [AssertionTheory T2] : Bool

Both theories separate commitment from belief.

Equations

• Interfaces.bothSeparateCommitment = (Interfaces.AssertionTheory.separatesCommitmentFromBelief T1 && Interfaces.AssertionTheory.separatesCommitmentFromBelief T2)

def Interfaces.bothSupportRetraction {T1 T2 : Type} [AssertionTheory T1] [AssertionTheory T2] : Bool

Both theories support retraction.

Equations

• Interfaces.bothSupportRetraction = (Interfaces.AssertionTheory.supportsRetraction T1 && Interfaces.AssertionTheory.supportsRetraction T2)

inductive Interfaces.AssertionPhenomenon : Type

Assertion-related phenomena that theories may handle.

• basicAssertion : AssertionPhenomenon

  Basic assertion adds to common ground

• hedging : AssertionPhenomenon

  Hedging reduces commitment strength

• oathFormulae : AssertionPhenomenon

  Oath formulae increase commitment strength

• risingDeclaratives : AssertionPhenomenon

  Rising declaratives shift commitment source

• retraction : AssertionPhenomenon

  Retraction / taking back a prior commitment

• lying : AssertionPhenomenon

  Lying: commitment without belief

• challenging : AssertionPhenomenon

  Challenging: demanding reasons for a commitment

instance Interfaces.instDecidableEqAssertionPhenomenon : DecidableEq AssertionPhenomenon

Equations

• Interfaces.instDecidableEqAssertionPhenomenon x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Interfaces.instReprAssertionPhenomenon.repr : AssertionPhenomenon → ℕ → Std.Format

Equations

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

instance Interfaces.instReprAssertionPhenomenon : Repr AssertionPhenomenon

Equations

• Interfaces.instReprAssertionPhenomenon = { reprPrec := Interfaces.instReprAssertionPhenomenon.repr }

instance Interfaces.instBEqAssertionPhenomenon : BEq AssertionPhenomenon

Equations

• Interfaces.instBEqAssertionPhenomenon = { beq := Interfaces.instBEqAssertionPhenomenon.beq }

def Interfaces.instBEqAssertionPhenomenon.beq : AssertionPhenomenon → AssertionPhenomenon → Bool

Equations

• Interfaces.instBEqAssertionPhenomenon.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

def Interfaces.handlesAssertion (T : Type) [AssertionTheory T] : AssertionPhenomenon → Bool

Whether a theory handles a given phenomenon.

Derived from the Boolean flags — not a separate configuration.

Equations

• Interfaces.handlesAssertion T Interfaces.AssertionPhenomenon.basicAssertion = true
• Interfaces.handlesAssertion T Interfaces.AssertionPhenomenon.hedging = Interfaces.AssertionTheory.separatesCommitmentFromBelief T
• Interfaces.handlesAssertion T Interfaces.AssertionPhenomenon.oathFormulae = Interfaces.AssertionTheory.separatesCommitmentFromBelief T
• Interfaces.handlesAssertion T Interfaces.AssertionPhenomenon.risingDeclaratives = Interfaces.AssertionTheory.modelsSourceMarking T
• Interfaces.handlesAssertion T Interfaces.AssertionPhenomenon.retraction = Interfaces.AssertionTheory.supportsRetraction T
• Interfaces.handlesAssertion T Interfaces.AssertionPhenomenon.lying = Interfaces.AssertionTheory.separatesCommitmentFromBelief T
• Interfaces.handlesAssertion T Interfaces.AssertionPhenomenon.challenging = Interfaces.AssertionTheory.supportsRetraction T