Van der Leer 2026: Speech-Act Logic (SAL)

[van-der-leer-2026]

A propositional dynamic logic of speech acts over commitment-state Kripke frames. Speech acts are actions (α ::= assert | question | ~α | α;β | π ↪ α/β) interpreted as updates on commitment spaces (Definition 10+).

Main definitions

• CommitmentSpace — Definition 8: set of states with a ⊑-minimal root and projected continuations.
• SpeechAct — Definition 20: the PDL action language.
• apply — interpretation of SpeechAct as commitment-space update.
• Headline theorems T25, T26, T27, T30, T32, T33.
• FBProjection — F&B 2010 as a SAL projection.

§1 Commitment spaces (Definition 8)

structure VanDerLeer2026.CommitmentSpace (W : Type u_3) (A : Type u_4) : Type (max u_3 u_4)

Definition 8: a set of commitment states with a unique ⊑-minimal root. The root is the current state; non-root members are projected futures (admissible continuations under the Collaborative Principle).

• states : Set (Discourse.Commitment.Frame.CommitmentState W A)
• root : Discourse.Commitment.Frame.CommitmentState W A
• root_mem : self.root ∈ self.states
• root_minimal (c : Discourse.Commitment.Frame.CommitmentState W A) : c ∈ self.states → Discourse.Commitment.Frame.CooperativeExtRefl self.root c

def VanDerLeer2026.CommitmentSpace.singleton {W : Type u_1} {A : Type u_2} (root : Discourse.Commitment.Frame.CommitmentState W A) : CommitmentSpace W A

The trivial space: only the root state, no projected futures.

Equations

• VanDerLeer2026.CommitmentSpace.singleton root = { states := {root}, root := root, root_mem := ⋯, root_minimal := ⋯ }

@[simp]

theorem VanDerLeer2026.CommitmentSpace.singleton_root {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) : (singleton c).root = c

@[simp]

theorem VanDerLeer2026.CommitmentSpace.singleton_states {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) : (singleton c).states = {c}

def VanDerLeer2026.CommitmentSpace.MutuallyCommitted {W : Type u_1} {A : Type u_2} (C : CommitmentSpace W A) (π : Set W) : Prop

A proposition is mutually committed throughout the space (every state, every agent pair). Geurts 2019 fixed-point characterisation lifted to the space level.

Equations

• C.MutuallyCommitted π = ∀ c ∈ C.states, ∀ (w : W), Discourse.Commitment.Frame.MutuallyCommittedAt c π w

def VanDerLeer2026.CommitmentSpace.CommonlyBelieved {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) (group : List A) (π : Set W) (bound : ℕ) (w : W) : Prop

A proposition is commonly believed via the substrate's EpistemicLogic.commonBelief on the state's belief relation.

Equations

• VanDerLeer2026.CommitmentSpace.CommonlyBelieved c group π bound w = Semantics.Modality.EpistemicLogic.commonBelief c.belief group (fun (v : W) => v ∈ π) bound w

§2 Speech-act action language (Definitions 20-24)

inductive VanDerLeer2026.SpeechAct (W : Type u_3) (A : Type u_4) : Type (max u_3 u_4)

The action language: assert, question, sequential composition, denegation, empty.

• empty {W : Type u_3} {A : Type u_4} : SpeechAct W A
• assert {W : Type u_3} {A : Type u_4} (a b : A) (π : Set W) : SpeechAct W A
• question {W : Type u_3} {A : Type u_4} (a b : A) (π : Set W) : SpeechAct W A
• seq {W : Type u_3} {A : Type u_4} (α β : SpeechAct W A) : SpeechAct W A
• denegate {W : Type u_3} {A : Type u_4} (α : SpeechAct W A) : SpeechAct W A

def VanDerLeer2026.assertOnState {W : Type u_1} {A : Type u_2} (a b : A) (π : Set W) (c : Discourse.Commitment.Frame.CommitmentState W A) : Discourse.Commitment.Frame.CommitmentState W A

Update a commitment state with assert_{a,b}(π): restrict the (a, b) commitment relation to π-targets.

Equations

• VanDerLeer2026.assertOnState a b π c = c.restrictCommitment a b π

def VanDerLeer2026.applyAssert {W : Type u_1} {A : Type u_2} (a b : A) (π : Set W) (C : CommitmentSpace W A) : CommitmentSpace W A

The headline assert update: new root is assertOnState of the prior root; we expose the singleton form for the basic theorems.

Equations

• VanDerLeer2026.applyAssert a b π C = VanDerLeer2026.CommitmentSpace.singleton (VanDerLeer2026.assertOnState a b π C.root)

def VanDerLeer2026.apply {W : Type u_1} {A : Type u_2} : SpeechAct W A → CommitmentSpace W A → CommitmentSpace W A

Interpretation of SpeechAct as a commitment-space update. question, denegate are placeholders for the basic theorems.

Equations

• VanDerLeer2026.apply VanDerLeer2026.SpeechAct.empty x✝ = x✝
• VanDerLeer2026.apply (VanDerLeer2026.SpeechAct.assert a b π) x✝ = VanDerLeer2026.applyAssert a b π x✝
• VanDerLeer2026.apply (VanDerLeer2026.SpeechAct.question a b π) x✝ = x✝
• VanDerLeer2026.apply (α.seq β) x✝ = VanDerLeer2026.apply β (VanDerLeer2026.apply α x✝)
• VanDerLeer2026.apply α.denegate x✝ = x✝

@[simp]

theorem VanDerLeer2026.apply_empty {W : Type u_1} {A : Type u_2} (C : CommitmentSpace W A) : apply SpeechAct.empty C = C

@[simp]

theorem VanDerLeer2026.apply_assert {W : Type u_1} {A : Type u_2} (a b : A) (π : Set W) (C : CommitmentSpace W A) : apply (SpeechAct.assert a b π) C = applyAssert a b π C

@[simp]

theorem VanDerLeer2026.apply_seq {W : Type u_1} {A : Type u_2} (α β : SpeechAct W A) (C : CommitmentSpace W A) : apply (α.seq β) C = apply β (apply α C)

§3 Headline theorems T25-T33

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

T25 — after assert_{a,b}(π), a is committed to π at the new root.

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

T26 — under Sincerity + Competence, commitment transfers to the addressee's belief. The mediated CommonGround-update of [bary-2025].

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

T27.1 — under Sincerity, commitment to p entails commitment to "I believe p". The formal direction of [krifka-2024]'s "buffet is open" puzzle.

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

T27.2 — non-converse: there exist sincere states where C_{a,b} (B_a p) holds but C_{a,b} p does not. TODO: full countermodel construction.

theorem VanDerLeer2026.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 : Discourse.Commitment.Frame.Committed C.root a b π w) : Discourse.Commitment.Frame.Committed (apply (SpeechAct.assert a' b' π') C).root a b π w

T30 — commitment persists under unrelated assertion.

theorem VanDerLeer2026.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

T32 — every assertion update produces a non-empty space.

theorem VanDerLeer2026.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

T33 — asserting ∅ yields a violation state (empty O_{a,b}).

§4 Farkas-Bruce 2010 as a SAL projection

def VanDerLeer2026.FBProjection.discourseCommitment {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) (x : A) (w : W) (π : Set W) : Prop

F&B's DC_x: propositions x is publicly committed to, projected from a SAL state by ranging over all addressees.

Equations

• VanDerLeer2026.FBProjection.discourseCommitment c x w π = ∀ (y : A), Discourse.Commitment.Frame.Committed c x y π w

def VanDerLeer2026.FBProjection.commonGround {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) (w : W) (π : Set W) : Prop

F&B's cg (common ground) projected as universally-believed propositions.

Equations

• VanDerLeer2026.FBProjection.commonGround c w π = ∀ (a : A), Discourse.Commitment.Frame.Believes c a π w

theorem VanDerLeer2026.FBProjection.assert_adds_to_DC {W : Type u_1} {A : Type u_2} (a b : A) (π : Set W) (C : CommitmentSpace W A) (w : W) : Discourse.Commitment.Frame.Committed (apply (SpeechAct.assert a b π) C).root a b π w

After assert_{a,b}(π), a's F&B-style discourse commitment includes π (towards b).

theorem VanDerLeer2026.FBProjection.assert_enters_CG_under_sincerity_competence {W : Type u_1} {A : Type u_2} (a b : A) (π : Set W) (C : CommitmentSpace W A) (w : W) (hsin : Discourse.Commitment.Frame.Sincere (apply (SpeechAct.assert a b π) C).root) (hcomp : Discourse.Commitment.Frame.Competent (apply (SpeechAct.assert a b π) C).root) : Discourse.Commitment.Frame.Believes (apply (SpeechAct.assert a b π) C).root b π w

Under sincerity+competence, the addressee believes the asserted π — the F&B "ASSERT enters CommonGround" effect, mediated.

theorem VanDerLeer2026.FBProjection.dc_subset_cg_under_sincerity_competence {W : Type u_1} {A : Type u_2} (c : Discourse.Commitment.Frame.CommitmentState W A) (hsin : Discourse.Commitment.Frame.Sincere c) (hcomp : Discourse.Commitment.Frame.Competent c) (x : A) (w : W) (π : Set W) : discourseCommitment c x w π → commonGround c w π

The Bary 2025 critique made visible: under sincerity+competence, DC_x ⊆ cg — but in general they differ. F&B's conflation of the two sets works only in the ideal case.