Assertion Phenomena: Theory-Neutral Data

@cite{gunlogson-2001} @cite{lauer-2013} @cite{searle-1969}

Empirical observations about assertion that any theory should account for. These data points are theory-neutral: they describe observable patterns without importing from Theories/.

Data Points

1. Hedged assertions reduce commitment strength
2. Oath formulae increase commitment strength
3. Rising declaratives shift commitment source
4. Retraction withdraws a prior commitment
5. Lying involves commitment without belief

structure Phenomena.Assertion.HedgedAssertionDatum : Type

Hedged assertion datum: hedging expressions reduce commitment.

"I think it's raining" commits the speaker less strongly than "It's raining." The propositional content is the same; the commitment profile differs.

• hedge : String

  The hedge expression ("I think", "maybe", "probably")

• content : String

  The propositional content

• reducesCommitment : Bool

  Does the hedge reduce commitment? (always true empirically)

def Phenomena.Assertion.instReprHedgedAssertionDatum.repr : HedgedAssertionDatum → Nat → Std.Format

Equations

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

instance Phenomena.Assertion.instReprHedgedAssertionDatum : Repr HedgedAssertionDatum

Equations

• Phenomena.Assertion.instReprHedgedAssertionDatum = { reprPrec := Phenomena.Assertion.instReprHedgedAssertionDatum.repr }

def Phenomena.Assertion.hedgeExamples : List HedgedAssertionDatum

Canonical hedging examples.

Equations

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

theorem Phenomena.Assertion.all_hedges_reduce : (hedgeExamples.all fun (x : HedgedAssertionDatum) => x.reducesCommitment) = true

All canonical hedges reduce commitment.

structure Phenomena.Assertion.OathFormulaDatum : Type

Oath formula datum: oath expressions increase commitment.

"I swear it's raining" commits the speaker more strongly than "It's raining." The speaker stakes their credibility on the content.

• oath : String

  The oath expression ("I swear", "I promise", "I guarantee")

• content : String

  The propositional content

• increasesCommitment : Bool

  Does the oath increase commitment? (always true empirically)

def Phenomena.Assertion.instReprOathFormulaDatum.repr : OathFormulaDatum → Nat → Std.Format

Equations

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

instance Phenomena.Assertion.instReprOathFormulaDatum : Repr OathFormulaDatum

Equations

• Phenomena.Assertion.instReprOathFormulaDatum = { reprPrec := Phenomena.Assertion.instReprOathFormulaDatum.repr }

def Phenomena.Assertion.oathExamples : List OathFormulaDatum

Canonical oath examples.

Equations

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

theorem Phenomena.Assertion.all_oaths_increase : (oathExamples.all fun (x : OathFormulaDatum) => x.increasesCommitment) = true

All canonical oaths increase commitment.

structure Phenomena.Assertion.RisingDeclarativeDatum : Type

Rising declarative datum: intonation shifts commitment source.

"It's raining?" (rising) attributes the content to the addressee, while "It's raining." (falling) commits the speaker. Same words, different intonation, different commitment profile.

• content : String

  The content

• isRising : Bool

  Is the intonation rising?

• speakerCommits : Bool

  Does the speaker commit?

• attributedToAddressee : Bool

  Is the content attributed to the addressee?

instance Phenomena.Assertion.instReprRisingDeclarativeDatum : Repr RisingDeclarativeDatum

Equations

• Phenomena.Assertion.instReprRisingDeclarativeDatum = { reprPrec := Phenomena.Assertion.instReprRisingDeclarativeDatum.repr }

def Phenomena.Assertion.instReprRisingDeclarativeDatum.repr : RisingDeclarativeDatum → Nat → Std.Format

Equations

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

def Phenomena.Assertion.risingExamples : List RisingDeclarativeDatum

Falling vs rising contrast.

Equations

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

theorem Phenomena.Assertion.rising_no_speaker_commitment : ((List.filter (fun (x : RisingDeclarativeDatum) => x.isRising) risingExamples).all fun (x : RisingDeclarativeDatum) => !x.speakerCommits) = true

Rising declaratives do not commit the speaker.

theorem Phenomena.Assertion.falling_speaker_commits : ((List.filter (fun (x : RisingDeclarativeDatum) => !x.isRising) risingExamples).all fun (x : RisingDeclarativeDatum) => x.speakerCommits) = true

Falling declaratives commit the speaker.

structure Phenomena.Assertion.RetractionDatum : Type

Retraction datum: withdrawing a prior commitment.

"I take that back" / "Actually, never mind" removes a previously asserted proposition from the speaker's commitments. Not all theories support this operation.

• content : String

  The retracted content

• retraction : String

  The retraction expression

• isFelicitous : Bool

  Is the retraction felicitous?

def Phenomena.Assertion.instReprRetractionDatum.repr : RetractionDatum → Nat → Std.Format

Equations

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

instance Phenomena.Assertion.instReprRetractionDatum : Repr RetractionDatum

Equations

• Phenomena.Assertion.instReprRetractionDatum = { reprPrec := Phenomena.Assertion.instReprRetractionDatum.repr }

def Phenomena.Assertion.retractionExamples : List RetractionDatum

Retraction examples.

Equations

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

structure Phenomena.Assertion.LyingDatum : Type

Lying datum: commitment without belief.

A liar publicly commits to p while privately believing ¬p. The assertion has the same surface form as a sincere assertion, but the speaker's internal state diverges from their public commitment.

• asserted : String

  What the speaker asserts (public commitment)

• believed : String

  What the speaker believes (private state)

• commitmentBeliefDiverge : Bool

  Do commitment and belief diverge?

instance Phenomena.Assertion.instReprLyingDatum : Repr LyingDatum

Equations

• Phenomena.Assertion.instReprLyingDatum = { reprPrec := Phenomena.Assertion.instReprLyingDatum.repr }

def Phenomena.Assertion.instReprLyingDatum.repr : LyingDatum → Nat → Std.Format

Equations

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

def Phenomena.Assertion.lyingExamples : List LyingDatum

Lying involves commitment-belief divergence.

Equations

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

theorem Phenomena.Assertion.lying_diverges : (lyingExamples.all fun (x : LyingDatum) => x.commitmentBeliefDiverge) = true

All lying examples show commitment-belief divergence.