Assertion Theories: Cross-Theory Comparison

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

Compares assertion theories along structural dimensions.

Comparison Matrix

Theory	Commitment ≠ Belief	Retraction	Source	Entitlements	Probabilistic	Meta-speech-acts
Stalnaker	No	No	No	No	No	No
F&B	Yes	No	No	No	No	No
Krifka 2015	Yes	Yes	No	No	No	No
Krifka 2020 (JP/ComP)	Yes	Yes	No	No	No	No
Cohen-Krifka 2014	Yes	Yes	No	No	No	Yes
Brandom	Yes	Yes	No	Yes	No	No
Gunlogson	Yes	Yes	Yes	No	No	No
Lauer	Yes	No	No	No	Yes	No

The "Meta-speech-acts" column flags whether the framework supports denegation ~A and derived meta-speech-acts like GRANT (= ~ASSERT(¬·)). Cohen-Krifka 2014 introduced the apparatus; Krifka 2015 inherits it but this file's row for Krifka 2015 records what's actually formalized in its own study file (which scopes to §§1–5, denegation deferred to the Cohen-Krifka 2014 study).

Key Embeddings

1. Stalnaker embeds in Krifka: when commitment = belief (no lying, no hedging), Krifka's model collapses to Stalnaker's.
2. F&B's dcS/dcL are Krifka commitment states: dcS = speaker's commitment slate, dcL = addressee's commitment slate.
3. Krifka 2015 and Cohen-Krifka 2014 share the commitment-space substrate; Cohen-Krifka 2014 chronologically precedes and introduces denegation, which Krifka 2015 inherits (eq. 5).
4. Brandom strictly richer than Stalnaker: entitlements have no Stalnaker analog.
5. Gunlogson models rising declaratives; Stalnaker cannot.
6. Lying: Krifka and Brandom handle it (commitment without belief); Stalnaker struggles (assertion = belief update).

structure Phenomena.Assertion.Compare.AssertionComparison : Type

Summary comparison record for one theory.

• name : String

  Theory name

• separates : Bool

  Separates commitment from belief?

• retraction : Bool

  Supports retraction?

• source : Bool

  Models source marking?

• metaSpeechActs : Bool

  Supports meta-speech-acts (denegation, GRANT)?

def Phenomena.Assertion.Compare.instReprAssertionComparison.repr : AssertionComparison → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Phenomena.Assertion.Compare.instReprAssertionComparison : Repr AssertionComparison

Equations

• Phenomena.Assertion.Compare.instReprAssertionComparison = { reprPrec := Phenomena.Assertion.Compare.instReprAssertionComparison.repr }

def Phenomena.Assertion.Compare.comparisonMatrix : List AssertionComparison

The full comparison matrix.

Equations

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

theorem Phenomena.Assertion.Compare.matrix_correct : comparisonMatrix.length = 8

The matrix length pin.

theorem Phenomena.Assertion.Compare.only_cohen_krifka_has_meta_speech_acts : List.map (fun (x : AssertionComparison) => x.name) (List.filter (fun (x : AssertionComparison) => x.metaSpeechActs) comparisonMatrix) = ["Cohen-Krifka 2014"]

Cohen-Krifka 2014 is the only listed theory with substrate-level meta-speech-act support (denegation ~A, GRANT). Krifka 2015 inherits the apparatus but its Studies/Krifka2015.lean formalization scopes to §§1–5; the denegation worked example lives in Studies/CohenKrifka2014.lean.

The matrix in §1 is hand-stipulated. The substrate's Dialogue.Assertable typeclass lets us derive cross-framework agreement structurally: any framework satisfying the speakerAssert_subset_prior and speakerAssert_narrows laws must agree with every other such framework on the projected context set after assertion.

Two frameworks currently instantiate Assertable: Dialogue.Stalnaker.StalnakerState and Dialogue.Krifka.KrifkaState. The theorems below show the value of polymorphism: write the proof once against the typeclass, apply to both concrete frameworks.

This is the consumer the audit (CHANGELOG 0.230.677) flagged as missing — without it, the typeclass's cross-framework theorems (speakerAssert_initial_subset, speakerAssert_twice_narrows, speakerAssert_twice_subset_prior) were dead code.

theorem Phenomena.Assertion.Compare.any_assertable_narrows_initial {S : Type u_1} {W : Type u_2} [Dialogue.Assertable S W] (φ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert Dialogue.Assertable.initial φ) ⊆ {w : W | φ w}

Polymorphic assertion-narrowing: any Assertable framework narrows the context set by the asserted proposition. The headline polymorphic theorem from Assertable.lean, restated here as a Phenomena-level claim about ANY assertion theory in the Assertable family.

theorem Phenomena.Assertion.Compare.stalnaker_assertion_narrows {W : Type u_1} (φ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert Dialogue.Assertable.initial φ) ⊆ {w : W | φ w}

Stalnaker satisfies the polymorphic theorem: applying any_assertable_narrows_initial at the Stalnaker instance. The fact that this typechecks is the structural witness that Stalnaker's set-intersection assertion semantics genuinely fits the Assertable shape.

theorem Phenomena.Assertion.Compare.krifka_assertion_narrows {W : Type u_1} (φ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert Dialogue.Assertable.initial φ) ⊆ {w : W | φ w}

Krifka satisfies the polymorphic theorem: applying any_assertable_narrows_initial at the Krifka instance. Krifka's commitment-space assertion (prepending commit speaker doxastic φ to the root) gives the same structural narrowing despite the radically different state representation.

theorem Phenomena.Assertion.Compare.any_assertable_twice_narrows {S : Type u_1} {W : Type u_2} [Dialogue.Assertable S W] (s : S) (φ ψ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert (Dialogue.Assertable.speakerAssert s φ) ψ) ⊆ {w : W | φ w ∧ ψ w}

Cross-framework two-step narrowing: asserting φ then ψ in ANY Assertable framework yields a context set ⊆ {φ ∧ ψ}. Polymorphic version of speakerAssert_twice_narrows.

theorem Phenomena.Assertion.Compare.stalnaker_twice_narrows {W : Type u_1} (s : Dialogue.Stalnaker.StalnakerState W) (φ ψ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert (Dialogue.Assertable.speakerAssert s φ) ψ) ⊆ {w : W | φ w ∧ ψ w}

Stalnaker satisfies two-step narrowing.

theorem Phenomena.Assertion.Compare.krifka_twice_narrows {W : Type u_1} (s : Dialogue.Krifka.KrifkaState W) (φ ψ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert (Dialogue.Assertable.speakerAssert s φ) ψ) ⊆ {w : W | φ w ∧ ψ w}

Krifka satisfies two-step narrowing.

theorem Phenomena.Assertion.Compare.stalnaker_krifka_agree_on_initial_assertion {W : Type u_1} (φ : W → Prop) : Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert Dialogue.Assertable.initial φ) ⊆ {w : W | φ w} ∧ Core.CommonGround.HasContextSet.toContextSet (Dialogue.Assertable.speakerAssert Dialogue.Assertable.initial φ) ⊆ {w : W | φ w}

Cross-framework agreement on initial-state assertion: starting from initial in two different Assertable frameworks and asserting the same φ yields context sets that BOTH narrow to the same φ-witnesses. The polymorphic theorem fires twice with the same conclusion shape. The instances may have wildly different intermediate representations (Stalnaker = list of propositions; Krifka = root + continuations of indexed commitments), but their projected context sets agree on the φ-narrowing constraint.

This is the substrate-level "cross-framework agreement" structural fact that the §1 matrix's "Stalnaker no separation / Krifka separates" rows are silent about. The matrix tracks representational differences; this theorem tracks observational agreement at the context-set level.