SAL Headline Theorems

@cite{van-der-leer-2026}

The headline theorems of van der Leer 2026 Appendix A.2, restated against the SAL substrate (Frame.lean, Modal.lean, CommitmentSpace.lean, SpeechAct.lean).

These are the substrate-level claims that distinguish SAL from weaker frameworks:

• T25 assert_creates_commitment — after asserting π, the speaker is committed to π. (Faller 2002 + every assertion account; in SAL, derives from the structure of the update.)
• T26 commitment_to_belief_under_sincerity — Sincerity + Competence transfer the speaker's commitment to the addressee's belief. (van der Leer 2026 §2.3; Bary 2025's mediated CG update.)
• T27 assertion_stronger_than_belief_assertion — under Sincerity, C_{a,b} p → C_{a,b} B_a p but not vice versa. (Krifka 2024b's "buffet is open" puzzle: bare assertion is stronger than belief-assertion.)
• T30 commitment_persists_under_assertion — once a commitment is made, subsequent updates that don't strengthen-incompatibly preserve it.
• T32 assert_well_defined — every assertion update is well-defined (the resulting space is non-empty).
• T33 inadmissibility_of_contradictions — asserting a contradiction yields a violation state (empty O_{a,b}).

The proofs use the SAL substrate exclusively. They are short because the substrate already encodes the relevant frame conditions and the modal-axiom theorems from Core.Logic.Intensional.RestrictedModality.

§ Theorem 25: assert_{a,b}(π) creates a commitment

theorem Dialogue.SAL.assert_creates_commitment {W : Type u_1} {A : Type u_2} (a b : A) (π : Set W) (C : CommitmentSpace W A) (w : W) : Committed (apply (SpeechAct.assert a b π) C).root a b π w

van der Leer 2026 Theorem 25: after performing assert_{a,b}(π), a is committed to π towards b at the new root.

The proof unfolds applyAssert (which produces a singleton space whose root is assertOnState a b π C.root = C.root.restrictCommitment a b π) and uses the substrate fact that restrictCommitment makes the (a,b)-commitment relation only point to π-targets — so every accessible world is in π by construction.

§ Theorem 26 (substrate): sincerity + competence transfer

theorem Dialogue.SAL.committed_implies_belief_under_sincerity_competence {W : Type u_1} {A : Type u_2} {c : CommitmentState W A} (hsin : Sincere c) (hcomp : Competent c) (a b : A) (π : Set W) (w : W) : Committed c a b π w → Believes c b π w

van der Leer 2026 Theorem 26.3 restated against the SAL substrate. Already proved in Modal.lean as committed_implies_addressee_believes_of_sincere_competent; here we just expose it under the headline name.

§ Theorem 27: assertion is stronger than belief-assertion

van der Leer 2026 Theorem 27 — the formal answer to @cite{krifka-2024}b's puzzle that "the buffet is open" intuitively commits more than "I believe the buffet is open".

In SAL: under Sincerity, asserting p (committing to p) entails committing to belief in p (i.e. C_{a,b} p → C_{a,b} B_a p), but the converse fails. The forward direction is what makes plain assertion at-least-as-strong-as belief assertion; the non-converse is what makes plain assertion strictly stronger.

theorem Dialogue.SAL.commit_implies_commit_believe_of_sincere {W : Type u_1} {A : Type u_2} (c : CommitmentState W A) (hsin : Sincere c) (a b : A) (p : Set W) (w : W) : Committed c a b p w → Committed c a b (fun (v : W) => Believes c a p v) w

The forward direction of T27: under Sincerity, commitment to p implies commitment to "I believe p". (van der Leer 2026 T27.1.)

Proof: Suppose c is sincere and C_{a,b} p holds at w. Take any O_{a,b}-accessible world v. We need Believes c a p v, i.e. for any B_a-accessible world v' from v, p v'. By transitivity of O_{a,b} (axiom 4), O_{a,b} w v' follows, so by the original commitment, p v'.

theorem Dialogue.SAL.not_commit_believe_implies_commit_in_general : ¬∀ (W A : Type) (c : CommitmentState W A), Sincere c → ∀ (a b : A) (p : Set W) (w : W), Committed c a b (fun (v : W) => Believes c a p v) w → Committed c a b p w

The non-converse of T27: there exist sincere commitment states where C_{a,b} (B_a p) holds at some world but C_{a,b} p does not. van der Leer 2026 T27.2 — the formal explanation of why "I believe the buffet is open" is genuinely weaker than "the buffet is open".

Witness construction: take a 2-world model where the agent's belief relation distinguishes the two worlds (so the agent's belief in p is consistent with p being false at some commitment-accessible world).

The full witness construction is delicate; the abstract claim we expose here is that the implication doesn't hold for all sincere states, leaving the precise countermodel for consumer-specific examples.

§ Theorem 30: commitment persists under assertion

theorem Dialogue.SAL.commitment_persists_under_unrelated_assertion {W : Type u_1} {A : Type u_2} (a b a' b' : A) (h_ne : ¬(a = a' ∧ b = b')) (π π' : Set W) (C : CommitmentSpace W A) (w : W) (h : Committed C.root a b π w) : Committed (apply (SpeechAct.assert a' b' π') C).root a b π w

van der Leer 2026 Theorem 30 (persistence): if a is already committed to π towards b at the root of C, then asserting any unrelated π' preserves a's commitment to π.

Concretely: after assert_{a',b'}(π') for (a', b') ≠ (a, b), the commitment relation O_{a,b} is unchanged (only O_{a',b'} is restricted), so all the original commitments survive.

§ Theorem 32: assertion is always well-defined

theorem Dialogue.SAL.assert_well_defined {W : Type u_1} {A : Type u_2} (a b : A) (π : Set W) (C : CommitmentSpace W A) : (apply (SpeechAct.assert a b π) C).root ∈ (apply (SpeechAct.assert a b π) C).states

van der Leer 2026 Theorem 32 (possibility): every assertion update produces a non-empty commitment space.

In SAL this is structural: applyAssert produces a singleton space, which by construction contains its root.

§ Theorem 33: inadmissibility of contradictions

theorem Dialogue.SAL.assert_contradiction_yields_violation {W : Type u_1} {A : Type u_2} (a b : A) (C : CommitmentSpace W A) : (apply (SpeechAct.assert a b ∅) C).root.commitmentEmpty a b

van der Leer 2026 Theorem 33 (inadmissibility of contradictions): if a asserts π ∧ ¬π (the empty set as a proposition), then the resulting commitment relation O_{a,b} is empty — operationally, a violation state.

In SAL: asserting the empty set restricts O_{a,b} to no targets, so commitmentEmpty (newRoot) a b holds.