Assertion Types

Theory-neutral data types for assertion discourse phenomena.

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 ⋯

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

Equations

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

instance Interfaces.instReprAssertionOutcome : Repr AssertionOutcome

Equations

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

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 }

instance Interfaces.instInhabitedAssertionOutcome : Inhabited AssertionOutcome

Equations

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

def Interfaces.instInhabitedAssertionOutcome.default : AssertionOutcome

Equations

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

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 → Nat → 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 }

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

Equations

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

instance Interfaces.instBEqAssertionPhenomenon : BEq AssertionPhenomenon

Equations

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