The update algebra

Dynamic meanings come in two forms: a relational update Update S relates input states to output states, and a context change potential CCP S transforms sets of states as wholes. lift sends an update to its image transformer, lower recovers it, and the distributive transformers are exactly the relational images. A satisfaction relation induces the standard eliminative fragment (updateFromSat), which PLA, DRT, and DPL instantiate. The monadic reading of the pair is in Collapse.lean.

Main definitions

• Update S, Condition S: relations on states, properties of states.
• Update.test, Update.neg, Update.seq, Update.impl, Update.disj, Update.closure: the relational connectives.
• Update.IsTest: updates that never change the state.
• CCP.guard, CCP.might, CCP.must, CCP.negTest: whole-state tests.
• CCP.IsEliminative, CCP.IsTest, CCP.IsDistributive, CCP.IsClassical: the classification of transformers.
• CCP.up, CCP.down: the content–update coercions.
• lift, lower: the bridge between the two forms.
• supportOf, contentOf, updateFromSat, dynamicEntailsOf: the layer a satisfaction relation induces.

Main results

• Update S is a Monoid and an IsQuantale under sequencing (scoped); tests are its subidentities (Update.isTest_iff_le_one).
• Update.IsTest.eq_test_closure, CCP.IsTest.eq_guard: a test is the test of its truth condition, a guard of its acceptance condition.
• lower_lift, lift_lower: lift and lower are mutually inverse on distributive transformers.
• CCP.isClassical_iff_up_down_eq, exists_eq_lift_test_iff: the classical transformers are exactly the static ones — up of their own content, the lifted test filters; CCP.might_not_isDistributive separates.
• support_iff_update_eq: support is being a fixed point of the update.

Implementation notes

The algebraic instances are scoped: Update S and CCP S abbreviate function types. updateFromSat is the literal filter rather than lift (test _) so that instantiating frameworks connect to it by rfl. Update.neg does not validate double-negation elimination and CCP.negTest is not CCP.neg; the framework-specific repairs and comparisons live in the studies. [GS91a]'s entailment notions live in Studies/GroenendijkStokhof1991.lean.

References

• J. Groenendijk and M. Stokhof, Dynamic Predicate Logic
• H. Kamp and U. Reyle, From Discourse to Logic
• R. Muskens, Combining Montague Semantics and Discourse Representation
• I. Heim, The Semantics of Definite and Indefinite Noun Phrases
• I. Heim, On the Projection Problem for Presuppositions
• J. Groenendijk and M. Stokhof, Two Theories of Dynamic Semantics
• F. Veltman, Defaults in Update Semantics
• R. Muskens, J. van Benthem, and A. Visser, Dynamics
• J. van Benthem, Essays in Logical Semantics
• D. Rothschild and S. Yalcin, Three Notions of Dynamicness in Language
• A. Gillies, On Groenendijk and Stokhof's "Dynamic Predicate Logic"

The relational face

@[reducible, inline]

abbrev DynamicSemantics.Update (S : Type u_1) : Type u_1

A dynamic meaning as a binary relation between input and output states.

Equations

• DynamicSemantics.Update S = (S → S → Prop)

@[reducible, inline]

abbrev DynamicSemantics.Condition (S : Type u_1) : Type u_1

A static property of a single state; test embeds conditions into updates.

Equations

• DynamicSemantics.Condition S = (S → Prop)

The connectives

def DynamicSemantics.Update.test {S : Type u_1} (C : Condition S) : Update S

test C checks C without changing the state.

Equations

• DynamicSemantics.Update.test C i j = (i = j ∧ C j)

def DynamicSemantics.Update.neg {S : Type u_1} (D : Update S) : Condition S

neg D holds at i iff no output k satisfies D.

Equations

• D.neg i = ¬∃ (k : S), D i k

def DynamicSemantics.Update.seq {S : Type u_1} (D₁ D₂ : Update S) : Update S

seq D₁ D₂ relates i to k iff some intermediate j has D₁ i j and D₂ j k.

Equations

• D₁.seq D₂ = Relation.Comp D₁ D₂

def DynamicSemantics.Update.impl {S : Type u_1} (D₁ D₂ : Update S) : Condition S

impl D₁ D₂ holds at i iff every D₁-output from i has a D₂-output.

Equations

• D₁.impl D₂ i = ∀ (h : S), D₁ i h → ∃ (k : S), D₂ h k

def DynamicSemantics.Update.disj {S : Type u_1} (D₁ D₂ : Update S) : Condition S

disj D₁ D₂ holds at i iff some disjunct has an output from i.

Equations

• D₁.disj D₂ i = ∃ (k : S), D₁ i k ∨ D₂ i k

def DynamicSemantics.Update.closure {S : Type u_1} (D : Update S) : Condition S

closure D holds at i iff D has an output from i — [Hei82]'s truth definition.

Equations

• D.closure i = ∃ (k : S), D i k

The update quantale

@[implicit_reducible]

def DynamicSemantics.Update.instMonoid {S : Type u_1} : Monoid (Update S)

Update S is a monoid under seq with the trivial test as unit (scoped; see the implementation notes).

Equations

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

theorem DynamicSemantics.Update.instIsQuantale {S : Type u_1} : IsQuantale (Update S)

Update S is a quantale: sequencing distributes over arbitrary unions of updates, so mathlib's residuation vocabulary applies (scoped).

Tests are the subidentities

def DynamicSemantics.Update.IsTest {S : Type u_1} (D : Update S) : Prop

An update is a test if it never changes the state ([GS91a], Definition 11).

Equations

• D.IsTest = ∀ ⦃i j : S⦄, D i j → i = j

theorem DynamicSemantics.Update.isTest_test {S : Type u_1} (C : Condition S) : (test C).IsTest

test C is a test.

theorem DynamicSemantics.Update.isTest_iff_le_one {S : Type u_1} {D : Update S} : D.IsTest ↔ D ≤ 1

Tests are the subidentities of the update monoid: the coreflexives D ≤ 1.

theorem DynamicSemantics.Update.IsTest.eq_test_closure {S : Type u_1} {D : Update S} (h : D.IsTest) : D = test D.closure

A test is the test of its own closure ([GS91a]'s Fact 6); the transformer-face mirror is CCP.IsTest.eq_guard.

The transformer face

@[reducible, inline]

abbrev DynamicSemantics.CCP (S : Type u_1) : Type u_1

A context change potential: a transformer of whole information states.

Equations

• DynamicSemantics.CCP S = (Set S → Set S)

def DynamicSemantics.CCP.seq {S : Type u_1} (u v : CCP S) : CCP S

Sequential composition of CCPs, in diagrammatic order.

Equations

• u.seq v s = v (u s)

@[implicit_reducible]

def DynamicSemantics.CCP.instMonoid {S : Type u_1} : Monoid (CCP S)

CCP S is a monoid under seq (scoped; see the implementation notes).

Equations

• DynamicSemantics.CCP.instMonoid = { mul := DynamicSemantics.CCP.seq, mul_assoc := ⋯, one := id, one_mul := ⋯, mul_one := ⋯, npow_zero := ⋯, npow_succ := ⋯ }

def DynamicSemantics.CCP.neg {S : Type u_1} (φ : CCP S) : CCP S

Dynamic negation by set difference: the states that do not survive φ ([Hei82]; [Vel96]).

Equations

• φ.neg s = s \ φ s

Whole-state tests

def DynamicSemantics.CCP.guard {S : Type u_1} (C : Set S → Prop) : CCP S

guard C passes a state through iff it satisfies C, else crashes to ∅.

Equations

• DynamicSemantics.CCP.guard C s = {p : S | p ∈ s ∧ C s}

@[simp]

theorem DynamicSemantics.CCP.guard_pos {S : Type u_1} {C : Set S → Prop} {s : Set S} (h : C s) : guard C s = s

A guard whose condition holds passes the state through.

@[simp]

theorem DynamicSemantics.CCP.guard_neg {S : Type u_1} {C : Set S → Prop} {s : Set S} (h : ¬C s) : guard C s = ∅

A guard whose condition fails crashes to ∅.

@[simp]

theorem DynamicSemantics.CCP.mem_guard {S : Type u_1} {C : Set S → Prop} {s : Set S} {p : S} : p ∈ guard C s ↔ p ∈ s ∧ C s

def DynamicSemantics.CCP.negTest {S : Type u_1} (φ : CCP S) : CCP S

negTest φ passes iff φ crashes — a whole-state consistency test, not the set-difference neg (see the implementation notes).

Equations

• φ.negTest = DynamicSemantics.CCP.guard fun (s : Set S) => ¬(φ s).Nonempty

def DynamicSemantics.CCP.might {S : Type u_1} (φ : CCP S) : CCP S

might φ passes iff φ yields a nonempty result ([Vel96]).

Equations

• φ.might = DynamicSemantics.CCP.guard fun (s : Set S) => (φ s).Nonempty

def DynamicSemantics.CCP.must {S : Type u_1} (φ : CCP S) : CCP S

must φ passes iff φ returns its input unchanged ([Vel96]).

Equations

• φ.must = DynamicSemantics.CCP.guard fun (s : Set S) => φ s = s

def DynamicSemantics.CCP.entails {S : Type u_1} (φ ψ : CCP S) : Prop

Acceptance consequence: every φ-output is a fixed point of ψ ([Vel96]'s acceptance validity; [Bea01]'s D45).

Equations

• φ.entails ψ = ∀ (s : Set S), ψ (φ s) = φ s

Classification

def DynamicSemantics.CCP.IsEliminative {S : Type u_1} (u : CCP S) : Prop

A transformer is eliminative if it never adds possibilities.

Equations

• u.IsEliminative = (u ≤ id)

theorem DynamicSemantics.CCP.isEliminative_id {S : Type u_1} : IsEliminative id

The identity is eliminative.

theorem DynamicSemantics.CCP.IsEliminative.seq {S : Type u_1} {u v : CCP S} (hu : u.IsEliminative) (hv : v.IsEliminative) : (u.seq v).IsEliminative

Sequencing preserves eliminativity.

def DynamicSemantics.CCP.IsTest {S : Type u_1} (u : CCP S) : Prop

A transformer is a test if it passes its input through or crashes to ∅ — [Vel96]'s tests, Update.IsTest one carrier up.

Equations

• u.IsTest = ∀ (s : Set S), u s = s ∨ u s = ∅

theorem DynamicSemantics.CCP.IsTest.isEliminative {S : Type u_1} {u : CCP S} (h : u.IsTest) : u.IsEliminative

Tests are eliminative.

theorem DynamicSemantics.CCP.guard_isTest {S : Type u_1} (C : Set S → Prop) : (guard C).IsTest

Guards are tests.

theorem DynamicSemantics.CCP.IsTest.eq_guard {S : Type u_1} {u : CCP S} (h : u.IsTest) : u = guard fun (s : Set S) => u s = s

A test is the guard of its own acceptance condition — the mirror of Update.IsTest.eq_test_closure.

theorem DynamicSemantics.CCP.isTest_iff_exists_guard {S : Type u_1} {u : CCP S} : u.IsTest ↔ ∃ (C : Set S → Prop), u = guard C

The tests are exactly the guards.

def DynamicSemantics.CCP.IsDistributive {S : Type u_1} (φ : CCP S) : Prop

A transformer is distributive if it acts per-element: φ s = ⋃ i ∈ s, φ {i} — equivalently, it preserves arbitrary joins (Collapse.lean's isDistributive_iff_map_sSup).

Equations

• φ.IsDistributive = ∀ (s : Set S), φ s = {p : S | ∃ i ∈ s, p ∈ φ {i}}

The classical fragment

def DynamicSemantics.CCP.up {S : Type u_1} (c : Set S) : CCP S

The static update a content determines: intersection with it.

Equations

• DynamicSemantics.CCP.up c s = s ∩ c

def DynamicSemantics.CCP.down {S : Type u_1} (u : CCP S) : Set S

The content an update determines: the indices whose singleton it updates successfully.

Equations

• u.down = {i : S | (u {i}).Nonempty}

@[simp]

theorem DynamicSemantics.CCP.down_up {S : Type u_1} (c : Set S) : (up c).down = c

down retracts up.

theorem DynamicSemantics.CCP.IsEliminative.down_eq {S : Type u_1} {u : CCP S} (he : u.IsEliminative) : u.down = {i : S | u {i} = {i}}

On eliminative updates, content is acceptance on singletons.

def DynamicSemantics.CCP.IsClassical {S : Type u_1} (u : CCP S) : Prop

An update is classical if it is eliminative and distributive.

Equations

• u.IsClassical = (u.IsEliminative ∧ u.IsDistributive)

theorem DynamicSemantics.CCP.isClassical_up {S : Type u_1} (c : Set S) : (up c).IsClassical

Static updates are classical.

theorem DynamicSemantics.CCP.might_not_isDistributive : ∃ (S : Type) (φ : CCP S), ¬φ.might.IsDistributive

might is not distributive: a whole-state test can pass where every per-singleton test fails.

The bridge

def DynamicSemantics.lift {S : Type u_1} (R : Update S) : CCP S

The relational image: lift R σ collects the R-outputs of the elements of σ — the strongest postcondition of [MvBV11].

Equations

• DynamicSemantics.lift R σ = {j : S | ∃ i ∈ σ, R i j}

def DynamicSemantics.lower {S : Type u_1} (φ : CCP S) : Update S

lower φ i j holds iff j is an output of φ on the singleton {i}.

Equations

• DynamicSemantics.lower φ i j = (j ∈ φ {i})

theorem DynamicSemantics.mem_lift {S : Type u_1} {R : Update S} {σ : Set S} {j : S} : j ∈ lift R σ ↔ ∃ i ∈ σ, R i j

theorem DynamicSemantics.lift_seq {S : Type u_1} (R₁ R₂ : Update S) : lift (R₁.seq R₂) = (lift R₁).seq (lift R₂)

lift sends sequencing to composition.

theorem DynamicSemantics.lift_test {S : Type u_1} (C : Condition S) : lift (Update.test C) = fun (σ : Set S) => {i : S | i ∈ σ ∧ C i}

lift (test C) is the filter by C.

theorem DynamicSemantics.lift_isDistributive {S : Type u_1} (R : Update S) : (lift R).IsDistributive

Lifted transformers are distributive.

theorem DynamicSemantics.lower_lift {S : Type u_1} (R : Update S) : lower (lift R) = R

lower is a left inverse of lift: the relational face loses nothing.

theorem DynamicSemantics.lift_lower {S : Type u_1} (φ : CCP S) (hd : φ.IsDistributive) : lift (lower φ) = φ

lift is a right inverse of lower on distributive transformers.

theorem DynamicSemantics.lift_le_lift_iff {S : Type u_1} {R R' : Update S} : lift R ≤ lift R' ↔ R ≤ R'

lift reflects (and preserves) the pointwise order.

Test filters

@[simp]

theorem DynamicSemantics.mem_lift_test {S : Type u_1} {C : Condition S} {σ : Set S} {i : S} : i ∈ lift (Update.test C) σ ↔ i ∈ σ ∧ C i

theorem DynamicSemantics.lift_test_isEliminative {S : Type u_1} (C : Condition S) : (lift (Update.test C)).IsEliminative

lift (test C) is eliminative: it only removes elements.

theorem DynamicSemantics.lift_test_lift_test {S : Type u_1} (C₁ C₂ : Condition S) (σ : Set S) : lift (Update.test C₂) (lift (Update.test C₁) σ) = lift (Update.test fun (i : S) => C₁ i ∧ C₂ i) σ

Composing test filters conjoins the conditions.

theorem DynamicSemantics.lift_test_idem {S : Type u_1} (C : Condition S) (σ : Set S) : lift (Update.test C) (lift (Update.test C) σ) = lift (Update.test C) σ

Test filters are idempotent.

theorem DynamicSemantics.lift_test_disjoint {S : Type u_1} (C₁ C₂ : Condition S) (h : ∀ (i : S), C₁ i → C₂ i → False) (σ : Set S) : lift (Update.test C₂) (lift (Update.test C₁) σ) = ∅

Contradictory test filters compose to the empty state.

theorem DynamicSemantics.lift_test_cover₃ {S : Type u_1} (C₁ C₂ C₃ : Condition S) (h : ∀ (i : S), C₁ i ∨ C₂ i ∨ C₃ i) (σ : Set S) : lift (Update.test C₁) σ ∪ lift (Update.test C₂) σ ∪ lift (Update.test C₃) σ = σ

Covering test filters partition the state.

The static fragment

Van Benthem's additivity ([vB86]; [RY16]; [Gil22]): the classical transformers are exactly the lifted test filters. Update semantics keeps eliminativity but its whole-state tests break distributivity; DPL's random reassignment does the reverse ([GS91b], §4).

theorem DynamicSemantics.up_eq_lift_test {S : Type u_1} (C : Condition S) : CCP.up {i : S | C i} = lift (Update.test C)

up of a condition's extension is its lifted test filter.

theorem DynamicSemantics.exists_eq_lift_test_iff {S : Type u_1} {φ : CCP S} : (∃ (C : Condition S), φ = lift (Update.test C)) ↔ φ.IsClassical

A transformer is a lifted test filter iff it is classical.

theorem DynamicSemantics.CCP.isClassical_iff_up_down_eq {S : Type u_1} {φ : CCP S} : φ.IsClassical ↔ up φ.down = φ

The classical updates are exactly the static ones: up ∘ down is their normal form.

The satisfaction layer

A satisfaction relation sat : S → φ → Prop induces the standard eliminative fragment, and the layer reduces to mathlib's intersection–subset API: the induced update intersects with content (definitionally), support is inclusion in content, and dynamic entailment is content inclusion (dynamicEntailsOf_iff_content_subset). PLA, DRT, and DPL instantiate sat.

def DynamicSemantics.contentOf {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) : Set S

The content of a formula: all possibilities satisfying it.

Equations

• DynamicSemantics.contentOf sat ψ = {p : S | sat p ψ}

def DynamicSemantics.supportOf {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (s : Set S) (ψ : φ) : Prop

s supports ψ when every possibility in s satisfies ψ: inclusion in content.

Equations

• DynamicSemantics.supportOf sat s ψ = (s ⊆ DynamicSemantics.contentOf sat ψ)

theorem DynamicSemantics.support_mono {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (s t : Set S) (ψ : φ) (h : t ⊆ s) (hs : supportOf sat s ψ) : supportOf sat t ψ

Support is downward closed: smaller states support more.

theorem DynamicSemantics.empty_supports {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) : supportOf sat ∅ ψ

The empty state supports everything (vacuously).

theorem DynamicSemantics.content_mono {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ₁ ψ₂ : φ) (h : ∀ (p : S), sat p ψ₁ → sat p ψ₂) : contentOf sat ψ₁ ⊆ contentOf sat ψ₂

Content is monotone in pointwise entailment.

theorem DynamicSemantics.sep_monotone {S : Type u_1} (pred : S → Prop) : Monotone fun (s : Set S) => {p : S | p ∈ s ∧ pred p}

Filtering a set by a predicate is monotone.

theorem DynamicSemantics.sep_eliminative {S : Type u_1} (pred : S → Prop) : CCP.IsEliminative fun (s : Set S) => {p : S | p ∈ s ∧ pred p}

Filtering a set by a predicate is eliminative.

def DynamicSemantics.updateFromSat {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) : CCP S

The update a satisfaction relation induces: filter to the satisfying possibilities (see the implementation notes on the choice of body).

Equations

• DynamicSemantics.updateFromSat sat ψ s = {p : S | p ∈ s ∧ sat p ψ}

@[simp]

theorem DynamicSemantics.mem_updateFromSat {S : Type u_1} {φ : Type u_2} {sat : S → φ → Prop} {ψ : φ} {s : Set S} {p : S} : p ∈ updateFromSat sat ψ s ↔ p ∈ s ∧ sat p ψ

theorem DynamicSemantics.updateFromSat_eliminative {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) : (updateFromSat sat ψ).IsEliminative

Induced updates are eliminative.

theorem DynamicSemantics.updateFromSat_monotone {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) : Monotone (updateFromSat sat ψ)

updateFromSat is monotone in the state argument.

theorem DynamicSemantics.updateFromSat_eq_inter_content {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) (s : Set S) : updateFromSat sat ψ s = s ∩ contentOf sat ψ

Updating is intersecting with the content.

theorem DynamicSemantics.updateFromSat_eq_lift_test {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) : updateFromSat sat ψ = lift (Update.test fun (p : S) => sat p ψ)

The induced update is the lift of the satisfaction test.

theorem DynamicSemantics.updateFromSat_isDistributive {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) : (updateFromSat sat ψ).IsDistributive

Induced updates are distributive.

theorem DynamicSemantics.support_iff_update_eq {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) (s : Set S) : supportOf sat s ψ ↔ updateFromSat sat ψ s = s

Support is being a fixed point of the update ([Dek12]'s Proper Support).

def DynamicSemantics.dynamicEntailsOf {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ₁ ψ₂ : φ) : Prop

Dynamic entailment: updating with ψ₁ always yields a state supporting ψ₂.

Equations

• DynamicSemantics.dynamicEntailsOf sat ψ₁ ψ₂ = ∀ (s : Set S), DynamicSemantics.supportOf sat (DynamicSemantics.updateFromSat sat ψ₁ s) ψ₂

theorem DynamicSemantics.dynamicEntailsOf_iff_content_subset {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ₁ ψ₂ : φ) : dynamicEntailsOf sat ψ₁ ψ₂ ↔ contentOf sat ψ₁ ⊆ contentOf sat ψ₂

Dynamic entailment is content inclusion — the layer's consequence relation is classical entailment on contents.

theorem DynamicSemantics.dynamicEntailsOf_iff_entails {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ₁ ψ₂ : φ) : dynamicEntailsOf sat ψ₁ ψ₂ ↔ (updateFromSat sat ψ₁).entails (updateFromSat sat ψ₂)

Dynamic entailment is acceptance consequence of the induced updates.

theorem DynamicSemantics.dynamicEntails_refl {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ : φ) : dynamicEntailsOf sat ψ ψ

Dynamic entailment is reflexive.

theorem DynamicSemantics.dynamicEntails_trans {S : Type u_1} {φ : Type u_2} (sat : S → φ → Prop) (ψ₁ ψ₂ ψ₃ : φ) (h1 : dynamicEntailsOf sat ψ₁ ψ₂) (h2 : dynamicEntailsOf sat ψ₂ ψ₃) : dynamicEntailsOf sat ψ₁ ψ₃

Dynamic entailment is transitive.