Dynamic Propositions: The Semantic Algebra #

@cite{heim-1982} @cite{groenendijk-stokhof-1991} @cite{kamp-reyle-1993}

The relational type DRS 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:

@cite{heim-1982}: 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).
@cite{kamp-reyle-1993}: DRS 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.
@cite{groenendijk-stokhof-1991}: 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.

@cite{muskens-1996} unified these by parametrizing over the state type S, showing all systems embed into this algebra.

Operations #

Operation	Type	Origin
`DRS S`	`S → S → Prop`	G&S 1991, implicit in Heim 1982
`dseq`	`DRS S → DRS S → DRS S`	relational composition
`test`	`Condition S → DRS S`	identity + check
`dneg`	`DRS S → Condition S`	universal non-existence
`dimpl`	`DRS S → DRS S → Condition S`	K&R verification for ⇒
`ddisj`	`DRS S → DRS S → Condition S`	K&R verification for ∨
`closure`	`DRS 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, @cite{krahmer-muskens-1995}, @cite{elliott-sudo-2025})	Two update channels (positive/negative); negation = swap	`Dynamic/Bilateral/Basic.lean`, `Dynamic/Bilateral/ICDRT.lean`
ICDRT (@cite{hofmann-2025})	Propositional drefs + complementation under flat update	`Phenomena/Anaphora/Studies/Hofmann2025.lean`
TTR (@cite{cooper-2023})	Classical metalanguage reduction; negation is static	`Theories/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: Phenomena/Anaphora/Studies/Hofmann2025.lean §7 (bilateral vs ICDRT on the bathroom sentence), Phenomena/Anaphora/Studies/Cooper2023.lean §§ 4-5 (CDRT ↔ TTR truth-conditional equivalence + dynamic divergence under negation), and Phenomena/Anaphora/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.