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)

@[reducible, inline]

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

DRS 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 @cite{heim-1982}'s file change potentials, @cite{kamp-reyle-1993}'s DRS verification, and @cite{groenendijk-stokhof-1991}'s DPL meanings all instantiate.

Equations

• Semantics.Dynamic.Core.DynProp.DRS 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 DRS meanings via test.

Equations

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

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

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

Corresponds to @cite{kamp-reyle-1993} Def 1.4.4 (negation verification) and @cite{groenendijk-stokhof-1991} DPL negation.

Equations

• (∼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) : DRS S

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

Corresponds to @cite{heim-1982}'s intersection with the satisfaction set: SAT(F') = SAT(F) ∩ {a : C(a)}.

Equations

• [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.

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

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

Relational composition: there exists an intermediate state h witnessing both transitions. This is @cite{heim-1982}'s successive file change, @cite{kamp-reyle-1993}'s DRS sequencing, and @cite{groenendijk-stokhof-1991}'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₂ : DRS S) : Condition S

Dynamic implication: D₁ → D₂.

Every way of satisfying the antecedent can be extended to satisfy the consequent. Corresponds to @cite{kamp-reyle-1993} 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₂ : DRS S) : Condition S

Dynamic disjunction: D₁ ∨ D₂.

Corresponds to @cite{kamp-reyle-1993} 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 : DRS S) : Condition S

Anaphoric closure: ∃ output state.

@cite{heim-1982}'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 : DRS S) (i : S) : Prop

A DRS 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 : DRS S) : Prop

A DRS 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₂ : DRS S) : Prop

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

Equations

• (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₃ : DRS 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 : DRS S) (hC : ∀ (i : S), C i) : [C] ⨟ D = D

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

theorem Semantics.Dynamic.Core.DynProp.dneg_dneg_test {S : Type u_1} (C : Condition S) : (∼[∼[C]]) = C

Double negation for tests.

theorem Semantics.Dynamic.Core.DynProp.closure_closure {S : Type u_1} (D : DRS S) : closure [closure D] = closure D

Closure is idempotent.

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

Sequencing distributes over closure.