van der Leer 2026: Speech Act Logic

Van der Leer's Speech Act Logic is a propositional dynamic logic of speech acts over the commitment states of Commitment.Frame, in which belief B_a and commitment C_{a,b} are modal operators. An assertion is the update c⌈π⌉_{a,b} that creates a commitment, Krifka's performative update, which Sincerity and Competence pass on to beliefs, so that common belief and commitment stay apart, as Bary demands. The projected discourse is a commitment space in the sense of Cohen and Krifka, a root state together with its cooperative continuations, which the speech acts transform: an assertion narrows the root and keeps the continuations in which the addressee confirms, a question keeps the root and the continuations in which the addressee answers, a denegation removes the continuations the denegated act reaches. Cooperativity, admissibility and possibility of a speech act are the three levels of the thesis's hierarchy of discourse expectations: a cooperative act is admissible and every act is possible, but not conversely.

Main statements

• committed_assert, committed_update: an assertion commits the speaker, and a commitment at the root survives every later speech act.
• committed_believes_of_sincere, exists_committed_believes_not_committed: under Sincerity a commitment entails a commitment to the corresponding belief, but not conversely, so Krifka's "The buffet is open" is stronger than "I believe the buffet is open".
• admissible_of_cooperative, exists_admissible_not_cooperative: cooperative speech acts are admissible, and not conversely.
• cooperative_assert_of_not_committed, not_cooperative_assert_compl: after an assertion, the addressee's confirming it is cooperative and denying it is not.

Implementation notes

Propositions are world-sets, so the thesis's side condition that a proposition be C_{a,b}-free holds vacuously, the antecedent of a conditional act holds at the root iff it is Set.univ, and the ⊨_SAL claims — for every space C, member c and world — are stated at the root, C_c (Definition 13) being again a space with root c. Theorem 32, possibility, is the totality of update.

TODO

• Theorem 36, the cooperativity of answering a question, and speech act entailment (Definition 11) as a relation between acts.
• Report to the author: the witness for Theorem 27(2), O_{a,b} = B_a ∪ {(w, w)}, is not Euclidean (buffet replaces it); Theorem 31(1) needs a ≠ b, since for a = b the confirming assertion is redundant; and the well-definedness of the assertion update, called easy, needs the root case of le_restrictCommitment_of_mem.

References

• T. van der Leer, Commitments, beliefs and expectations in conversation (2026)
• C. Bary, Speech acts, common ground and commitments (2025)
• M. Krifka, Performative updates and the modeling of speech acts (2024)
• M. Krifka, Structure and interpretation of declarative sentences (2024)
• A. Cohen and M. Krifka, Superlative quantifiers and meta-speech acts (2014)
• M. Krifka, Bias in Commitment Space Semantics: Declarative Questions, Negated Questions, and Question Tags (2015)

Beliefs and commitments

theorem VanDerLeer2026.committed_committed {W : Type u_1} {A : Type u_2} (c : Commitment.Frame W A) (a b : A) (π : Set W) (w : W) (h : c.Committed a b π w) : c.Committed a b {v : W | c.Committed a b π v} w

Commitment is positively introspective, C_{a,b} π → C_{a,b} C_{a,b} π.

theorem VanDerLeer2026.committed_not_committed {W : Type u_1} {A : Type u_2} (c : Commitment.Frame W A) (a b : A) (π : Set W) (w : W) (h : ¬c.Committed a b π w) : c.Committed a b {v : W | ¬c.Committed a b π v} w

Commitment is negatively introspective, ¬ C_{a,b} π → C_{a,b} ¬ C_{a,b} π.

theorem VanDerLeer2026.not_believes_empty {W : Type u_1} {A : Type u_2} (c : Commitment.Frame W A) (a : A) (w : W) : ¬c.Believes a ∅ w

Belief is consistent, in that no agent believes ⊥.

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

π is mutually believed at w when it holds at every world some agent's belief reaches (§2.2).

Equations

• VanDerLeer2026.MutuallyBelieved c π w = ModalLogic.Box (⋃ (a : A), c.belief a) (fun (x : W) => x ∈ π) w

theorem VanDerLeer2026.mutuallyBelieved_iff {W : Type u_1} {A : Type u_2} (c : Commitment.Frame W A) (π : Set W) (w : W) : MutuallyBelieved c π w ↔ ∀ (a : A), c.Believes a π w

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

π is mutually committed to at w when it holds at every world some commitment relation reaches (§2.2).

Equations

• VanDerLeer2026.MutuallyCommitted c π w = ModalLogic.Box (⋃ (p : A × A), c.commitment p.1 p.2) (fun (x : W) => x ∈ π) w

theorem VanDerLeer2026.mutuallyCommitted_iff {W : Type u_1} {A : Type u_2} (c : Commitment.Frame W A) (π : Set W) (w : W) : MutuallyCommitted c π w ↔ ∀ (a b : A), c.Committed a b π w

def VanDerLeer2026.sincereRestrict {W : Type u_1} {A : Type u_2} (c : Commitment.Frame W A) (a b : A) (π : Set W) (h : ∀ (w : W), ∃ (v : W), (w, v) ∈ c.belief a ∧ (w, v) ∈ c.commitment a b ∧ v ∈ π) : Commitment.Frame W A

The sincere update c⌈π⌉^sin_{a,b} is c⌈π⌉_{a,b} with a's belief narrowed to the new O_{a,b}-edges (Definition 6). It is partial, and h keeps the narrowed belief serial (footnote 18).

Equations

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

theorem VanDerLeer2026.sincere_sincereRestrict {W : Type u_1} {A : Type u_2} {c : Commitment.Frame W A} {a b : A} {π : Set W} (hs : c.Sincere) (h : ∀ (w : W), ∃ (v : W), (w, v) ∈ c.belief a ∧ (w, v) ∈ c.commitment a b ∧ v ∈ π) : (sincereRestrict c a b π h).Sincere

The sincere update preserves Sincerity — the reason Definition 6 exists.

theorem VanDerLeer2026.believes_sincereRestrict {W : Type u_1} {A : Type u_2} {c : Commitment.Frame W A} {a b : A} {π : Set W} (w : W) (h : ∀ (w : W), ∃ (v : W), (w, v) ∈ c.belief a ∧ (w, v) ∈ c.commitment a b ∧ v ∈ π) : (sincereRestrict c a b π h).Believes a π w

After the sincere update the speaker believes what was asserted.

theorem VanDerLeer2026.exists_sincere_not_sincere_restrictCommitment : ∃ (c : Commitment.Frame Bool Unit) (π : Set Bool), c.Sincere ∧ ¬(c.restrictCommitment () () π).Sincere

Definition 4 alone need not preserve Sincerity.

theorem VanDerLeer2026.committed_believes_of_sincere {W : Type u_1} {A : Type u_2} {c : Commitment.Frame W A} {a b : A} {π : Set W} {w : W} (hs : c.Sincere) (h : c.Committed a b π w) : c.Committed a b {v : W | c.Believes a π v} w

Under Sincerity, C_{a,b} π → C_{a,b} B_a π (Theorem 27(1)).

def VanDerLeer2026.buffet : Commitment.Frame Bool Bool

Both agents believe only true, at either world, and are committed to nothing. The state is sincere, and at false it satisfies C_{a,b} B_a {true} but not C_{a,b} {true}.

Equations

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

theorem VanDerLeer2026.exists_committed_believes_not_committed : ∃ (c : Commitment.Frame Bool Bool) (a : Bool) (b : Bool) (π : Set Bool) (w : Bool), c.Sincere ∧ c.Committed a b {v : Bool | c.Believes a π v} w ∧ ¬c.Committed a b π w

C_{a,b} B_a π → C_{a,b} π is not valid over sincere states (Theorem 27(2)).

Commitment spaces

structure VanDerLeer2026.CooperativeContinuation {W : Type u_1} {A : Type u_2} (c c' : Commitment.Frame W A) : Prop

c ⊏ c' says that c' is a cooperative continuation of c (Definition 7), in which beliefs and commitments narrow, every commitment relation of c' is non-empty, and some commitment relation narrows strictly.

• belief_le (a : A) : c'.belief a ⊆ c.belief a
• commitment_le (a b : A) : c'.commitment a b ⊆ c.commitment a b
• commitment_nonempty (a b : A) : ∃ (w : W) (v : W), (w, v) ∈ c'.commitment a b
• commitment_lt : ∃ (a : A) (b : A) (w : W) (v : W), (w, v) ∈ c.commitment a b ∧ (w, v) ∉ c'.commitment a b

def VanDerLeer2026.«term_⊏_» : Lean.TrailingParserDescr

c ⊏ c' says that c' is a cooperative continuation of c (Definition 7), in which beliefs and commitments narrow, every commitment relation of c' is non-empty, and some commitment relation narrows strictly.

Equations

• VanDerLeer2026.«term_⊏_» = Lean.ParserDescr.trailingNode `VanDerLeer2026.«term_⊏_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊏ ") (Lean.ParserDescr.cat `term 51))

def VanDerLeer2026.«term_⊑_» : Lean.TrailingParserDescr

c ⊑ c' says that c = c' or c ⊏ c'.

Equations

• VanDerLeer2026.«term_⊑_» = Lean.ParserDescr.trailingNode `VanDerLeer2026.«term_⊑_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⊑ ") (Lean.ParserDescr.cat `term 51))

theorem VanDerLeer2026.CooperativeContinuation.ne {W : Type u_1} {A : Type u_2} {c c' : Commitment.Frame W A} (h : CooperativeContinuation c c') : c ≠ c'

theorem VanDerLeer2026.CooperativeContinuation.of_le {W : Type u_1} {A : Type u_2} {c c' d : Commitment.Frame W A} (h : CooperativeContinuation c c') (hb : ∀ (a : A), c.belief a ⊆ d.belief a) (hc : ∀ (a b : A), c.commitment a b ⊆ d.commitment a b) : CooperativeContinuation d c'

Whatever c is below, any state above c in belief and commitment is below too.

theorem VanDerLeer2026.CooperativeContinuation.of_restrictCommitment {W : Type u_1} {A : Type u_2} {c c' : Commitment.Frame W A} {a b : A} {π : Set W} (h : CooperativeContinuation (c.restrictCommitment a b π) c') : CooperativeContinuation c c'

instance VanDerLeer2026.CooperativeContinuation.instIsTransFrame {W : Type u_1} {A : Type u_2} : IsTrans (Commitment.Frame W A) CooperativeContinuation

theorem VanDerLeer2026.commitment_le_of_le {W : Type u_1} {A : Type u_2} {c c' : Commitment.Frame W A} (h : Relation.ReflGen CooperativeContinuation c c') (a b : A) : c'.commitment a b ⊆ c.commitment a b

theorem VanDerLeer2026.eq_of_le_of_le {W : Type u_1} {A : Type u_2} {c c' : Commitment.Frame W A} (h : Relation.ReflGen CooperativeContinuation c c') (h' : Relation.ReflGen CooperativeContinuation c' c) : c = c'

@[instance_reducible]

def VanDerLeer2026.instPartialOrderFrame_studies {W : Type u_1} {A : Type u_2} : PartialOrder (Commitment.Frame W A)

The cooperative-continuation order on states, with ⊑ as ≤ and ⊏ as <. A commitment space (Definition 8) is then a Commitment.Space (Frame W A).

Equations

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

theorem VanDerLeer2026.le_restrictCommitment_of_mem {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) {x : Commitment.Frame W A} {d e : A} {σ : Set W} (hmem : x.restrictCommitment d e σ ∈ C) (hroot : x.restrictCommitment d e σ = C.root → x.restrictCommitment d e σ = x) : Relation.ReflGen CooperativeContinuation x (x.restrictCommitment d e σ)

A restriction x⌈σ⌉_{d,e} that belongs to C lies above x — unless it is the root and differs from x, since the root need not have non-empty commitment relations.

def VanDerLeer2026.assert {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) : Commitment.Space (Commitment.Frame W A)

In C[assert_{a,b}(π)] the root commits a to π towards b, and the continuations are the members of C above the state in which b has confirmed (Definition 10).

Equations

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

def VanDerLeer2026.question {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) : Commitment.Space (Commitment.Frame W A)

In C[question_{a,b}(π)] the root is kept, and the continuations are the members of C in which b has answered π or ¬π (Definition 19).

Equations

• VanDerLeer2026.question C a b π = C.restrict (Set.Ici (C.root.restrictCommitment b a π) ∪ Set.Ici (C.root.restrictCommitment b a πᶜ))

def VanDerLeer2026.Violation {W : Type u_1} {A : Type u_2} (c : Commitment.Frame W A) (a b : A) : Prop

V_{a,b} holds when a's commitment relation towards b is empty, so that a is committed to a contradiction (Definition 16).

Equations

• VanDerLeer2026.Violation c a b = ∀ (w v : W), (w, v) ∉ c.commitment a b

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

The language of actions has assertion, polar question, the empty act ⊖, denegation ∼α, composition α;β, and the conditional π ↪ α/β (Definition 20).

• 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
• empty {W : Type u_3} {A : Type u_4} : SpeechAct W A
• denegate {W : Type u_3} {A : Type u_4} (α : SpeechAct W A) : SpeechAct W A
• seq {W : Type u_3} {A : Type u_4} (α β : SpeechAct W A) : SpeechAct W A
• cond {W : Type u_3} {A : Type u_4} (π : Set W) (α β : SpeechAct W A) : SpeechAct W A

noncomputable def VanDerLeer2026.update {W : Type u_1} {A : Type u_2} : SpeechAct W A → Commitment.Space (Commitment.Frame W A) → Commitment.Space (Commitment.Frame W A)

C[α] (Definitions 10, 19, 21–24). The denegation C[∼α] removes the states of C[α] and keeps the root; the conditional tests its antecedent at the root, where a world-set holds iff it is Set.univ.

Equations

• VanDerLeer2026.update (VanDerLeer2026.SpeechAct.assert a b π) x✝ = VanDerLeer2026.assert x✝ a b π
• VanDerLeer2026.update (VanDerLeer2026.SpeechAct.question a b π) x✝ = VanDerLeer2026.question x✝ a b π
• VanDerLeer2026.update VanDerLeer2026.SpeechAct.empty x✝ = x✝
• VanDerLeer2026.update α.denegate x✝ = x✝.denegate ↑(VanDerLeer2026.update α x✝)
• VanDerLeer2026.update (α.seq β) x✝ = VanDerLeer2026.update β (VanDerLeer2026.update α x✝)
• VanDerLeer2026.update (VanDerLeer2026.SpeechAct.cond π α β) x✝ = if π = Set.univ then VanDerLeer2026.update α x✝ else VanDerLeer2026.update β x✝

@[simp]

theorem VanDerLeer2026.update_assert {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) : update (SpeechAct.assert a b π) C = assert C a b π

@[simp]

theorem VanDerLeer2026.update_question {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) : update (SpeechAct.question a b π) C = question C a b π

@[simp]

theorem VanDerLeer2026.update_empty {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) : update SpeechAct.empty C = C

@[simp]

theorem VanDerLeer2026.update_denegate {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (α : SpeechAct W A) : update α.denegate C = C.denegate ↑(update α C)

@[simp]

theorem VanDerLeer2026.update_seq {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (α β : SpeechAct W A) : update (α.seq β) C = update β (update α C)

@[simp]

theorem VanDerLeer2026.root_assert {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) : (assert C a b π).root = C.root.restrictCommitment a b π

@[simp]

theorem VanDerLeer2026.root_question {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) : (question C a b π).root = C.root

theorem VanDerLeer2026.root_update_commitment_le {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (α : SpeechAct W A) : (update α C).root.commitment a b ⊆ C.root.commitment a b

No speech act enlarges a commitment relation of the root (Lemma 28).

theorem VanDerLeer2026.committed_update {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) (w : W) (α : SpeechAct W A) (h : C.root.Committed a b π w) : (update α C).root.Committed a b π w

A commitment at the root survives every speech act (Theorem 30).

theorem VanDerLeer2026.committed_assert {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) (w : W) : (update (SpeechAct.assert a b π) C).root.Committed a b π w

After assert_{a,b}(π), a is committed towards b to π (Theorem 25).

theorem VanDerLeer2026.believes_committed_assert {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) (w : W) (x : A) : (update (SpeechAct.assert a b π) C).root.Believes x {v : W | (update (SpeechAct.assert a b π) C).root.Committed a b π v} w

After assert_{a,b}(π), everyone believes that the commitment was made.

theorem VanDerLeer2026.committed_committed_assert {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) (w : W) (x y : A) : (update (SpeechAct.assert a b π) C).root.Committed x y {v : W | (update (SpeechAct.assert a b π) C).root.Committed a b π v} w

After assert_{a,b}(π), everyone is committed to the commitment having been made.

theorem VanDerLeer2026.assert_assert_of_subset {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π τ : Set W) (h : π ⊆ τ) : update (SpeechAct.assert a b τ) (update (SpeechAct.assert a b π) C) = update (SpeechAct.assert a b π) C

Asserting π entails asserting any consequence τ (Theorem 29).

Possibility, admissibility, cooperativity

def VanDerLeer2026.Admissible {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (α : SpeechAct W A) : Prop

α is admissible in C when performing it violates no commitment (Definition 17). Every speech act is possible (Theorem 32), since update is total.

Equations

• VanDerLeer2026.Admissible C α = ∀ (x y : A), ¬VanDerLeer2026.Violation (VanDerLeer2026.update α C).root x y

def VanDerLeer2026.Cooperative {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (α : SpeechAct W A) : Prop

α is cooperative in C when it is not redundant and its result lies below a cooperative continuation of the root (Definition 15).

Equations

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

theorem VanDerLeer2026.violation_assert_empty {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) : Violation (update (SpeechAct.assert a b ∅) C).root a b

Inadmissibility of contradictions (Theorem 33).

theorem VanDerLeer2026.admissible_of_cooperative {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (α : SpeechAct W A) (h : Cooperative C α) : Admissible C α

Cooperative speech acts are admissible (Theorem 34(1)).

theorem VanDerLeer2026.exists_admissible_not_cooperative : ∃ (C : Commitment.Space (Commitment.Frame Bool Unit)) (α : SpeechAct Bool Unit), Admissible C α ∧ ¬Cooperative C α

Admissible speech acts need not be cooperative, since nothing is cooperative in a space without continuations (Theorem 34(3)).

theorem VanDerLeer2026.not_cooperative_assert_compl {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) : ¬Cooperative (update (SpeechAct.assert a b π) C) (SpeechAct.assert b a πᶜ)

After assert_{a,b}(π), b denying π is not cooperative (Theorem 31(2)).

theorem VanDerLeer2026.cooperative_assert_of_not_committed {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) [Nonempty W] (hab : a ≠ b) (hmem : (C.root.restrictCommitment a b π).restrictCommitment b a π ∈ C) (h : ∀ (w : W), ¬C.root.Committed b a π w) : Cooperative (update (SpeechAct.assert a b π) C) (SpeechAct.assert b a π)

After assert_{a,b}(π), b confirming π is cooperative, provided the confirmed state is projected in C and b was not yet committed to π (Theorem 31(1)). The thesis omits a ≠ b; for a = b the confirmation is redundant.

theorem VanDerLeer2026.question_assert {W : Type u_1} {A : Type u_2} (C : Commitment.Space (Commitment.Frame W A)) (a b : A) (π : Set W) : update (SpeechAct.question a b π) (update (SpeechAct.assert b a π) C) = update (SpeechAct.assert b a π) C

b asserting π entails a having asked whether π (Theorem 35).