Dynamic Propositions: The Semantic Algebra

[Hei82] [GS91] [KR93]

The relational type Update S = S → S → Prop and its core operations form the semantic algebra shared by all dynamic semantic systems: DRT, DPL, File Change Semantics, PLA, CDRT, BUS, and others.

Intellectual Origins

Three independent but converging lines of work arrive at essentially the same algebraic structure:

• [Hei82]: Sentence meanings are file change potentials — functions from files to files. Her principle (A), SAT(F + φ) = SAT(F) ∩ {a : a SAT φ}, decomposes update into the operations formalized here as test (intersection) and dseq (successive file change).

• [KR93]: Update verification clauses (Def 1.4.4) define when an embedding can be extended to satisfy each connective. These clauses correspond exactly to test, dseq, dneg, dimpl, and ddisj.

• [GS91]: Dynamic Predicate Logic makes the relational type explicit: meanings ARE binary relations on assignments. Their DPL conjunction = relational composition (dseq), DPL negation = universal non-existence (dneg), etc.

[Mus96] unified these by parametrizing over the state type S, showing all systems embed into this algebra.

Operations

Operation	Type	Origin
Update S	S → S → Prop	G&S 1991, implicit in Heim 1982
dseq	Update S → Update S → Update S	relational composition
test	Condition S → Update S	identity + check
dneg	Update S → Condition S	universal non-existence
dimpl	Update S → Update S → Condition S	K&R verification for ⇒
ddisj	Update S → Update S → Condition S	K&R verification for ∨
closure	Update S → Condition S	existential closure (Heim's truth)

Cross-cutting smell: three incompatible DNE solutions

dneg (above) gives the standard relational negation ¬D i ⟺ ¬∃k, D i k, which fails double-negation elimination — dneg (dneg D) ≢ D because positive update information is destroyed when negation collapses to a state predicate. Three downstream frameworks repair DNE in mutually incompatible ways:

Framework	DNE mechanism	File
Bilateral (BUS, [KM95], [ES25a])	Two update channels (positive/negative); negation = swap	Dynamic/Bilateral/Basic.lean, Dynamic/Bilateral/ICDRT.lean
ICDRT ([Hof25])	Propositional drefs + complementation under flat update	Studies/Hofmann2025.lean
TTR ([Coo23])	Classical metalanguage reduction; negation is static	Semantics/TypeTheoretic/

These are not mere notational variants. Bilateral DNE is structural (swap is involutive by definition); ICDRT DNE is derived (complementation of a propositional dref); TTR DNE is inherited (the metalanguage is classical so ¬¬p ↔ p holds at the static layer). Each repair pays for itself with different downstream costs — bilateral cannot distinguish speaker-vs-hearer commitments; ICDRT requires intensional contexts; TTR loses dynamic state-threading at the negation site.

The cross-framework comparisons are formalized at the phenomenon level: Studies/Hofmann2025.lean §7 (bilateral vs ICDRT on the bathroom sentence), Studies/Cooper2023.lean §§ 4-5 (CDRT ↔ TTR truth-conditional equivalence + dynamic divergence under negation), and Studies/Dekker2012.lean (PLA vs BUS on the bathroom sentence: eliminative test vs structural swap). New dynamic frameworks should declare which DNE strategy they adopt and link to one of these comparisons.

@[reducible, inline]

abbrev Semantics.Dynamic.Core.DynProp.Update (S : Type u_1) : Type u_1

Update meaning: type s(st) — binary relation on states.

A proposition in dynamic semantics is a relation between an input state and an output state. This is the type that [Hei82]'s file change potentials, [KR93]'s Update verification, and [GS91]'s DPL meanings all instantiate.

Equations

• Semantics.Dynamic.Core.DynProp.Update S = (S → S → Prop)

@[reducible, inline]

abbrev Semantics.Dynamic.Core.DynProp.Condition (S : Type u_1) : Type u_1

Condition: type st — property of a single state.

Static conditions that do not change the state. Conditions are lifted to Update meanings via test.

Equations

• Semantics.Dynamic.Core.DynProp.Condition S = (S → Prop)

def Semantics.Dynamic.Core.DynProp.dneg {S : Type u_1} (D : Update S) : Condition S

Dynamic negation: ¬D holds at i iff no output k satisfies D.

Corresponds to [KR93] Def 1.4.4 (negation verification) and [GS91] DPL negation.

Equations

• Semantics.Dynamic.Core.DynProp.dneg D i = ¬∃ (k : S), D i k

def Semantics.Dynamic.Core.DynProp.«term∼_» : Lean.ParserDescr

Equations

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

def Semantics.Dynamic.Core.DynProp.test {S : Type u_1} (C : Condition S) : Update S

Test: lift a condition to an Update that checks C without changing state.

Corresponds to [Hei82]'s intersection with the satisfaction set: SAT(F') = SAT(F) ∩ {a : C(a)}.

Equations

• Semantics.Dynamic.Core.DynProp.test C i j = (i = j ∧ C j)

def Semantics.Dynamic.Core.DynProp.«term[_]» : Lean.ParserDescr

Equations

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

theorem Semantics.Dynamic.Core.DynProp.eq_of_test {S : Type u_1} {C : Condition S} {i j : S} (h : test C i j) : i = j

A test relates a state only to itself. Operators that return a Condition (dneg, dimpl, ddisj) re-enter the update algebra via test, so updates factoring through test cannot modify the state — the algebraic core of anaphoric-island facts.

def Semantics.Dynamic.Core.DynProp.dseq {S : Type u_1} (D₁ D₂ : Update S) : Update S

Dynamic conjunction (sequencing): D₁ ; D₂.

Relational composition: there exists an intermediate state h witnessing both transitions. This is [Hei82]'s successive file change, [KR93]'s Update sequencing, and [GS91]'s DPL conjunction.

Equations

• (D₁ ⨟ D₂) i j = ∃ (h : S), D₁ i h ∧ D₂ h j

def Semantics.Dynamic.Core.DynProp.«term_⨟_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Dynamic.Core.DynProp.dimpl {S : Type u_1} (D₁ D₂ : Update S) : Condition S

Dynamic implication: D₁ → D₂.

Every way of satisfying the antecedent can be extended to satisfy the consequent. Corresponds to [KR93] Def 1.4.4 (implication verification): for all h, if D₁ i h then ∃ k, D₂ h k.

Equations

• Semantics.Dynamic.Core.DynProp.dimpl D₁ D₂ i = ∀ (h : S), D₁ i h → ∃ (k : S), D₂ h k

def Semantics.Dynamic.Core.DynProp.ddisj {S : Type u_1} (D₁ D₂ : Update S) : Condition S

Dynamic disjunction: D₁ ∨ D₂.

Corresponds to [KR93] Def 1.4.4 (disjunction verification): there exists an output via either disjunct.

Equations

• Semantics.Dynamic.Core.DynProp.ddisj D₁ D₂ i = ∃ (k : S), D₁ i k ∨ D₂ i k

def Semantics.Dynamic.Core.DynProp.closure {S : Type u_1} (D : Update S) : Condition S

Anaphoric closure: ∃ output state.

[Hei82]'s truth definition: a file is true iff its satisfaction set is non-empty, i.e., some assignment satisfies it.

Equations

• Semantics.Dynamic.Core.DynProp.closure D i = ∃ (k : S), D i k

def Semantics.Dynamic.Core.DynProp.term!_ : Lean.ParserDescr

Equations

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

def Semantics.Dynamic.Core.DynProp.trueAt {S : Type u_1} (D : Update S) (i : S) : Prop

A Update D is true relative to input i iff some output j satisfies D.

Equations

• Semantics.Dynamic.Core.DynProp.trueAt D i = ∃ (j : S), D i j

def Semantics.Dynamic.Core.DynProp.valid {S : Type u_1} (D : Update S) : Prop

A Update D is valid iff true at all inputs.

Equations

• Semantics.Dynamic.Core.DynProp.valid D = ∀ (i : S), Semantics.Dynamic.Core.DynProp.trueAt D i

def Semantics.Dynamic.Core.DynProp.entails {S : Type u_1} (D₁ D₂ : Update S) : Prop

Dynamic entailment: D₁ ⊨ D₂ iff every output of D₁ can be extended by D₂.

Equations

• Semantics.Dynamic.Core.DynProp.entails D₁ D₂ = ∀ (i : S), (∃ (j : S), D₁ i j) → ∀ (j : S), D₁ i j → ∃ (k : S), D₂ j k

def Semantics.Dynamic.Core.DynProp.«term_⊨_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.DynProp.dseq_assoc {S : Type u_1} (D₁ D₂ D₃ : Update S) : D₁ ⨟ D₂ ⨟ D₃ = D₁ ⨟ (D₂ ⨟ D₃)

Sequencing is associative.

theorem Semantics.Dynamic.Core.DynProp.test_dseq {S : Type u_1} (C : Condition S) (D : Update S) (hC : ∀ (i : S), C i) : test C ⨟ D = D

Test is left identity for sequencing (when condition holds everywhere).

theorem Semantics.Dynamic.Core.DynProp.dseq_test {S : Type u_1} (D : Update S) (C : Condition S) (hC : ∀ (i : S), C i) : D ⨟ test C = D

Test is right identity for sequencing (when condition holds everywhere). Together with test_dseq and dseq_assoc, this makes (Update S, ⨟, test ⊤) a monoid.

@[implicit_reducible]

def Semantics.Dynamic.Core.DynProp.instMonoidUpdate {S : Type u_1} : Monoid (Update S)

Update S is a monoid under dynamic conjunction ⨟ with the trivial test as unit (dseq_assoc, test_dseq, dseq_test). Scoped because Update S is an abbreviation for S → S → Prop: a global instance would attach */1 to the bare function type. Activate with open scoped Semantics.Dynamic.Core.DynProp; mathlib's WriterT (Update S) Id then gets Monad/LawfulMonad for free.

Equations

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

theorem Semantics.Dynamic.Core.DynProp.dneg_dneg_test {S : Type u_1} (C : Condition S) : dneg (test (dneg (test C))) = C

Double negation for tests.

theorem Semantics.Dynamic.Core.DynProp.closure_closure {S : Type u_1} (D : Update S) : closure (test (closure D)) = closure D

Closure is idempotent.

theorem Semantics.Dynamic.Core.DynProp.dseq_closure {S : Type u_1} (D₁ D₂ : Update S) : closure (D₁ ⨟ D₂) = fun (i : S) => ∃ (h : S), D₁ i h ∧ closure D₂ h

Sequencing distributes over closure.