Dynamic Semantics ↔ TTR: Truth-Conditional Equivalence

@cite{cooper-2023} @cite{groenendijk-stokhof-1991} @cite{muskens-1996} @cite{sutton-2024}

CDRT (Dynamic/) and TTR (TypeTheoretic/) handle overlapping phenomena — discourse referents, donkey anaphora, cross-sentential binding — with no connection. This file proves they have the same truth conditions for a core fragment, and identifies where they diverge.

The correspondence

Dynamic (CDRT)	Type-Theoretic (TTR)	Classical
DProp.ofStatic p	propT (p i)	p i
DProp.new n; test P	Σ (x : E), P x	∃ x, P x
DProp.impl (new;P) Q	Π (x : E), P x → Q x	∀ x, P x → Q x

The first column is state-threading (assignments as side effects). The second is type-dependency (witnesses as structure). Both reduce to the same classical truth conditions (third column).

The divergence

The systems agree on truth conditions but differ on anaphoric potential. In CDRT, ¬¬(∃x.P(x)) has the same truth conditions as ∃x.P(x) but different discourse effects: the dref x is inaccessible after double negation (negation resets the register). In TTR, anaphoric potential is carried by type structure, not side effects.

CDRT introduces a dref with DProp.new n, then tests a property on r(n). The truth condition is ∃ x, P x.

TTR represents the same thing as a Σ-type: (x : E) × P x, which is inhabited iff ∃ x, P x. This is purify applied to a parametric property with background E.

def Comparisons.DynamicTTR.cdrt_exists {E : Type} (n : ℕ) (P : E → Prop) : Semantics.Dynamic.CDRT.DProp E

CDRT existential: introduce dref n, test P on r(n).

Equations

• Comparisons.DynamicTTR.cdrt_exists n P = Semantics.Dynamic.CDRT.DProp.new n ;; Semantics.Dynamic.CDRT.DProp.ofStatic fun (r : Semantics.Dynamic.CDRT.Register E) => P (r n)

def Comparisons.DynamicTTR.ttr_exists {E : Type} (P : E → Prop) : Type

TTR existential: Σ-type with entity witness. This is purify ⟨E, λ e _ => propT (P e)⟩ a for any a, but since the result doesn't depend on a, we state it directly.

Equations

• Comparisons.DynamicTTR.ttr_exists P = ((x : E) × Semantics.TypeTheoretic.propT (P x))

theorem Comparisons.DynamicTTR.exists_equiv {E : Type} (n : ℕ) (P : E → Prop) (i : Semantics.Dynamic.CDRT.Register E) : (cdrt_exists n P).true_at i ↔ Nonempty (ttr_exists P)

Equivalence 1: CDRT dref introduction and TTR Σ-type have the same truth conditions. Both reduce to ∃ x, P x.

theorem Comparisons.DynamicTTR.exists_classical {E : Type} (P : E → Prop) : Nonempty (ttr_exists P) ↔ ∃ (x : E), P x

Both reduce to classical ∃.

CDRT handles donkey anaphora via DProp.impl: the antecedent introduces a dref, and the consequent refers back to it. The universal force ("every farmer...every donkey") comes from impl's ∀ over output registers.

TTR handles the same thing via universal purification (purifyUniv): a Π-type that universally quantifies over all background witnesses. Both reduce to ∀ x, P x → Q x.

def Comparisons.DynamicTTR.cdrt_donkey {E : Type} (n : ℕ) (P Q : E → Prop) : Semantics.Dynamic.CDRT.DProp E

CDRT donkey: impl(new n; test P, test Q). "For every way of extending the register with a P-entity at n, Q holds of that entity."

Equations

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

def Comparisons.DynamicTTR.ttr_donkey {E : Type} (P Q : E → Prop) : Type

TTR donkey: Π-type over witnesses. "For every P-witness, Q holds." This is purifyUniv on the parametric property with background {x : E // P x}.

Equations

• Comparisons.DynamicTTR.ttr_donkey P Q = ((x : E) → P x → Semantics.TypeTheoretic.propT (Q x))

theorem Comparisons.DynamicTTR.donkey_equiv {E : Type} (n : ℕ) (P Q : E → Prop) (i : Semantics.Dynamic.CDRT.Register E) : (cdrt_donkey n P Q).true_at i ↔ Nonempty (ttr_donkey P Q)

Equivalence 2: CDRT donkey implication and TTR Π-type have the same truth conditions. Both reduce to ∀ x, P x → Q x.

theorem Comparisons.DynamicTTR.donkey_classical {E : Type} (P Q : E → Prop) : Nonempty (ttr_donkey P Q) ↔ ∀ (x : E), P x → Q x

Both reduce to classical ∀→.

"Every farmer who owns a donkey beats it."

CDRT: impl(new 0; farmer(r0); new 1; donkey(r1); owns(r0,r1), beats(r0, r1))

TTR: ∀ x, farmer x → ∀ y, donkey y → owns x y → beats x y (= purifyUniv on a two-layer parametric property)

def Comparisons.DynamicTTR.cdrt_full_donkey {E : Type} (farmer donkey_ : E → Prop) (owns beats : E → E → Prop) : Semantics.Dynamic.CDRT.DProp E

Equations

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

def Comparisons.DynamicTTR.ttr_full_donkey {E : Type} (farmer donkey_ : E → Prop) (owns beats : E → E → Prop) : Type

Equations

• Comparisons.DynamicTTR.ttr_full_donkey farmer donkey_ owns beats = ((x : E) → farmer x → (y : E) → donkey_ y → owns x y → Semantics.TypeTheoretic.propT (beats x y))

theorem Comparisons.DynamicTTR.full_donkey_equiv {E : Type} (farmer donkey_ : E → Prop) (owns beats : E → E → Prop) (i : Semantics.Dynamic.CDRT.Register E) : (cdrt_full_donkey farmer donkey_ owns beats).true_at i ↔ Nonempty (ttr_full_donkey farmer donkey_ owns beats)

Equivalence 3: The full donkey sentence has the same truth conditions in CDRT and TTR.

The TTR existential and donkey types are instances of purify and purifyUniv from Quantification.lean. This makes the bridge connect to the existing TTR infrastructure, not just raw Σ/Π.

def Comparisons.DynamicTTR.ttr_exists_as_pppty {E : Type} (P : E → Prop) : Semantics.TypeTheoretic.PPpty E

The parametric property whose purification is ttr_exists P. Background: the entity domain. Foreground: test P at the witness.

Equations

• Comparisons.DynamicTTR.ttr_exists_as_pppty P = { Bg := E, fg := fun (x x_1 : E) => Semantics.TypeTheoretic.propT (P x) }

theorem Comparisons.DynamicTTR.purify_exists_eq {E : Type} (P : E → Prop) (a : E) : Semantics.TypeTheoretic.purify (ttr_exists_as_pppty P) a = ttr_exists P

purify of the existential parametric property is definitionally ttr_exists.

def Comparisons.DynamicTTR.ttr_donkey_as_pppty {E : Type} (P Q : E → Prop) : Semantics.TypeTheoretic.PPpty E

The parametric property whose universal purification is ttr_donkey. Background: P-witnesses. Foreground: test Q at the witness.

Equations

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

theorem Comparisons.DynamicTTR.purifyUniv_donkey_iff {E : Type} (P Q : E → Prop) (a : E) : Nonempty (Semantics.TypeTheoretic.purifyUniv (ttr_donkey_as_pppty P Q) a) ↔ ∀ (x : E), P x → Q x

purifyUniv of the donkey parametric property is inhabited iff the donkey universal holds.

The systems agree on truth conditions but differ on discourse effect. CDRT tracks anaphoric potential via the output register: after processing φ, the output register determines what drefs are available for subsequent sentences.

• new n; test P outputs a register with n bound → dref available
• neg (new n; test P) outputs i unchanged → dref lost

TTR tracks anaphoric potential via type structure: the Σ-type (x : E) × P x makes x available as a projection, regardless of how many negations wrap it.

This is the fundamental architectural difference: CDRT uses state for binding; TTR uses structure.

theorem Comparisons.DynamicTTR.neg_destroys_dref {E : Type} {φ : Semantics.Dynamic.CDRT.DProp E} (i o : Semantics.Dynamic.CDRT.Register E) (h : φ.neg i o) : o = i

In CDRT, negation destroys anaphoric potential. After ¬φ, the output register is unchanged from input — any drefs introduced by φ are inaccessible. This is a general property of DProp.neg, not specific to any particular φ.

theorem Comparisons.DynamicTTR.dne_same_truth {E : Type} (n : ℕ) (P : E → Prop) (i : Semantics.Dynamic.CDRT.Register E) : (cdrt_exists n P).neg.neg.true_at i ↔ (cdrt_exists n P).true_at i

Double negation preserves truth but not drefs. ¬¬(∃x.P(x)) has the same truth conditions as ∃x.P(x), but the output register is the input register (no binding).

theorem Comparisons.DynamicTTR.ttr_witness_survives {E : Type} (P : E → Prop) (w : ttr_exists P) : ∃ (x : E), P x

In TTR, there is no analogous destruction. The Σ-type (x : E) × P x carries its witness structurally. The projection Sigma.fst is always available, regardless of logical context.

inductive Comparisons.DynamicTTR.Ent : Type

• john : Ent
• bill : Ent
• fido : Ent

instance Comparisons.DynamicTTR.instDecidableEqEnt : DecidableEq Ent

Equations

• Comparisons.DynamicTTR.instDecidableEqEnt x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

theorem Comparisons.DynamicTTR.cdrt_donkey_concrete : (cdrt_full_donkey Comparisons.DynamicTTR.farmerP✝ Comparisons.DynamicTTR.donkeyP✝ Comparisons.DynamicTTR.ownsP✝ Comparisons.DynamicTTR.beatsP✝).true_at Comparisons.DynamicTTR.initReg✝

CDRT donkey sentence is true on this model.

theorem Comparisons.DynamicTTR.ttr_donkey_concrete : Nonempty (ttr_full_donkey Comparisons.DynamicTTR.farmerP✝ Comparisons.DynamicTTR.donkeyP✝ Comparisons.DynamicTTR.ownsP✝ Comparisons.DynamicTTR.beatsP✝)

TTR donkey sentence is true on this model.

theorem Comparisons.DynamicTTR.concrete_agreement : (cdrt_full_donkey Comparisons.DynamicTTR.farmerP✝ Comparisons.DynamicTTR.donkeyP✝ Comparisons.DynamicTTR.ownsP✝ Comparisons.DynamicTTR.beatsP✝).true_at Comparisons.DynamicTTR.initReg✝ ↔ Nonempty (ttr_full_donkey Comparisons.DynamicTTR.farmerP✝¹ Comparisons.DynamicTTR.donkeyP✝¹ Comparisons.DynamicTTR.ownsP✝¹ Comparisons.DynamicTTR.beatsP✝¹)

The two concrete results agree (by the equivalence theorem).