Intensional Dynamic Semantics — Generic Substrate

@cite{muskens-1996} @cite{stone-1999} @cite{brasoveanu-2006} @cite{hofmann-2025}

Generic infrastructure for dynamic semantics built over ICDRTAssignment (individual drefs as IVar → W → Entity E plus propositional drefs as PVar → Set W). This is a layer above Dynamic/Core/DiscourseRef.lean (which owns the assignment type) and below paper-specific theories such as @cite{hofmann-2025} (whose paper apparatus lives in Phenomena/Anaphora/Studies/Hofmann2025.lean).

Main definitions

Layer	Names
Information state	IContext (set of assignment-world pairs), DynProp (context transformer)
Update relations	ICDRTUpdate, ICDRTUpdate.{seq, idUp, toDynProp}
Variable updates	propVarUp, indivVarUp, multiVarUp, relVarUp
Dynamic conditions	dynInclusion, dynIdentity, dynComplement, isComplement, dynUnion
Predication	dynPred, localEntailment
Veridicality typology	veridicalIndiv/Prop, counterfactualIndiv/Prop, hypotheticalIndiv/Prop, accessible, subsetReq
Static-to-dynamic bridge	fiberDRS, toDynProp_eq_lift_fiberDRS

Architecture

ICDRTUpdate W E ──fiberDRS──→ DRS (ICDRTAssignment W E × W) ──lift──→ CCP (... × W)
       ‖                              ‖                                    ‖
   DRS (Assign)              DRS (Assign × World)                 DynProp W E
       │                              │                                    │
    seq = dseq              dseq (fiber level)                    CCP.seq

The factorization toDynProp = lift ∘ fiberDRS separates two concerns:

• fiberDRS: embed assignment-only relations into pair relations (passive worlds)
• lift: convert relational meanings to set-transformer meanings

toDynProp is always distributive (corollary of lift_isDistributive). This is the algebraic content of @cite{hofmann-2025}'s observation that ICDRT-style negation via propositional dref complementation stays distributive — unlike test-based dynamic negation that inspects whole states.

def Semantics.Dynamic.Core.ICDRTAssignment.«term_⟦_⟧ᵢ» : Lean.TrailingParserDescr

Notation for individual variable lookup

Equations

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

def Semantics.Dynamic.Core.ICDRTAssignment.«term_⟦_⟧ₚ» : Lean.TrailingParserDescr

Notation for propositional variable lookup

Equations

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

@[reducible, inline]

abbrev Semantics.Dynamic.Core.IContext (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Set of assignment-world pairs (information state in flat update).

Kept as abbrev so it inherits Set α's Membership, EmptyCollection, HasSubset, Union, Inter, and Singleton instances (and the corresponding Set API) directly.

Equations

• Semantics.Dynamic.Core.IContext W E = Set (Semantics.Dynamic.Core.ICDRTAssignment W E × W)

def Semantics.Dynamic.Core.IContext.univ {W : Type u_1} {E : Type u_2} : IContext W E

The trivial context (all possibilities)

Equations

• Semantics.Dynamic.Core.IContext.univ = Set.univ

def Semantics.Dynamic.Core.IContext.empty {W : Type u_1} {E : Type u_2} : IContext W E

The absurd context (no possibilities)

Equations

• Semantics.Dynamic.Core.IContext.empty = ∅

def Semantics.Dynamic.Core.IContext.consistent {W : Type u_1} {E : Type u_2} (c : IContext W E) : Prop

Context is consistent (non-empty)

Equations

• c.consistent = Set.Nonempty c

def Semantics.Dynamic.Core.IContext.worlds {W : Type u_1} {E : Type u_2} (c : IContext W E) : Set W

Worlds in the context (projection)

Equations

• c.worlds = {w : W | ∃ (g : Semantics.Dynamic.Core.ICDRTAssignment W E), (g, w) ∈ c}

def Semantics.Dynamic.Core.IContext.update {W : Type u_1} {E : Type u_2} (c : IContext W E) (p : W → Prop) : IContext W E

Update with a world-predicate

Equations

• c⟦p⟧ = {gw : Semantics.Dynamic.Core.ICDRTAssignment W E × W | gw ∈ c ∧ p gw.2}

def Semantics.Dynamic.Core.IContext.updateFull {W : Type u_1} {E : Type u_2} (c : IContext W E) (p : ICDRTAssignment W E → W → Prop) : IContext W E

Update with an assignment-world predicate

Equations

• c.updateFull p = {gw : Semantics.Dynamic.Core.ICDRTAssignment W E × W | gw ∈ c ∧ p gw.1 gw.2}

def Semantics.Dynamic.Core.IContext.«term_⟦_⟧» : Lean.TrailingParserDescr

Equations

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

def Semantics.Dynamic.Core.DynProp (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Context-to-context transformer (sentence denotation).

Equations

• Semantics.Dynamic.Core.DynProp W E = (Semantics.Dynamic.Core.IContext W E → Semantics.Dynamic.Core.IContext W E)

def Semantics.Dynamic.Core.DynProp.id {W : Type u_1} {E : Type u_2} : DynProp W E

Identity (says nothing). Aliases CCP.id.

Equations

• Semantics.Dynamic.Core.DynProp.id c = c

def Semantics.Dynamic.Core.DynProp.absurd {W : Type u_1} {E : Type u_2} : DynProp W E

Absurd (contradiction). Aliases CCP.absurd.

Equations

• Semantics.Dynamic.Core.DynProp.absurd x✝ = ∅

def Semantics.Dynamic.Core.DynProp.ofProp {W : Type u_1} {E : Type u_2} (p : W → Prop) : DynProp W E

Lift a classical proposition to a context filter.

Equations

• Semantics.Dynamic.Core.DynProp.ofProp p c = c⟦p⟧

def Semantics.Dynamic.Core.ICDRTUpdate (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Static update relation between input and output assignments.

Following @cite{muskens-1996}'s Compositional DRT, dynamic updates are relations between assignments rather than operations on sets of assignment-world pairs. The lift to context transformers is done by toDynProp below.

Equations

• Semantics.Dynamic.Core.ICDRTUpdate W E = (Semantics.Dynamic.Core.ICDRTAssignment W E → Semantics.Dynamic.Core.ICDRTAssignment W E → Prop)

def Semantics.Dynamic.Core.ICDRTUpdate.seq {W : Type u_1} {E : Type u_2} (D₁ D₂ : ICDRTUpdate W E) : ICDRTUpdate W E

Sequencing (;): relational composition. (D₁ ; D₂)(i)(j) ↔ ∃k, D₁(i)(k) ∧ D₂(k)(j)

Equations

• (D₁ ⨟ D₂) i j = ∃ (k : Semantics.Dynamic.Core.ICDRTAssignment W E), D₁ i k ∧ D₂ k j

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

Equations

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

def Semantics.Dynamic.Core.ICDRTUpdate.idUp {W : Type u_1} {E : Type u_2} : ICDRTUpdate W E

Identity update: output equals input.

Equations

• Semantics.Dynamic.Core.ICDRTUpdate.idUp i j = (i = j)

def Semantics.Dynamic.Core.ICDRTUpdate.successful {W : Type u_1} {E : Type u_2} (D : ICDRTUpdate W E) (i : ICDRTAssignment W E) : Prop

An update is successful from i if some output j exists.

Equations

• D.successful i = ∃ (j : Semantics.Dynamic.Core.ICDRTAssignment W E), D i j

def Semantics.Dynamic.Core.ICDRTUpdate.toDynProp {W : Type u_1} {E : Type u_2} (D : ICDRTUpdate W E) : DynProp W E

Lift a static update relation to a context update on information states.

Equations

• D.toDynProp c = {p : Semantics.Dynamic.Core.ICDRTAssignment W E × W | ∃ (i : Semantics.Dynamic.Core.ICDRTAssignment W E), (i, p.2) ∈ c ∧ D i p.1}

theorem Semantics.Dynamic.Core.ICDRTUpdate.idUp_toDynProp {W : Type u_1} {E : Type u_2} (c : IContext W E) : idUp.toDynProp c = c

Identity update lifts to identity on contexts.

theorem Semantics.Dynamic.Core.ICDRTUpdate.seq_toDynProp {W : Type u_1} {E : Type u_2} (D₁ D₂ : ICDRTUpdate W E) (c : IContext W E) : (D₁ ⨟ D₂).toDynProp c = D₂.toDynProp (D₁.toDynProp c)

Sequential composition lifts to function composition on contexts.

def Semantics.Dynamic.Core.propVarUp {W : Type u_1} {E : Type u_2} (p : PVar) (i j : ICDRTAssignment W E) : Prop

Propositional variable update: j differs from i at most in the value of p. i[p]j

Equations

• Semantics.Dynamic.Core.propVarUp p i j = ((∀ (q : Semantics.Dynamic.Core.PVar), q ≠ p → j⟦q⟧ₚ = i⟦q⟧ₚ) ∧ ∀ (v : Semantics.Dynamic.Core.IVar), j⟦v⟧ᵢ = i⟦v⟧ᵢ)

def Semantics.Dynamic.Core.indivVarUp {W : Type u_1} {E : Type u_2} (v : IVar) (i j : ICDRTAssignment W E) : Prop

Individual variable update: j differs from i at most in the value of v. i[v]j

Equations

• Semantics.Dynamic.Core.indivVarUp v i j = ((∀ (p : Semantics.Dynamic.Core.PVar), j⟦p⟧ₚ = i⟦p⟧ₚ) ∧ ∀ (u : Semantics.Dynamic.Core.IVar), u ≠ v → j⟦u⟧ᵢ = i⟦u⟧ᵢ)

def Semantics.Dynamic.Core.multiVarUp {W : Type u_1} {E : Type u_2} (ps : List PVar) (vs : List IVar) (i j : ICDRTAssignment W E) : Prop

Multi-variable update: j differs from i at most in the listed prop/indiv vars.

Equations

• Semantics.Dynamic.Core.multiVarUp ps vs i j = ((∀ p ∉ ps, j⟦p⟧ₚ = i⟦p⟧ₚ) ∧ ∀ v ∉ vs, j⟦v⟧ᵢ = i⟦v⟧ᵢ)

def Semantics.Dynamic.Core.relVarUp {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) (i j : ICDRTAssignment W E) : Prop

Relative variable update: i[φ : v]j.

j differs from i at most in v, AND for every world w, φ(j)(w) ↔ v(j)(w) ≠ ⋆.

The biconditional (not just implication) is crucial: it ensures that v has a referent in all and only the φ-worlds, preventing drefs under negation from having global referents. Following @cite{hofmann-2025} Definition 25.

Equations

• Semantics.Dynamic.Core.relVarUp φ v i j = (Semantics.Dynamic.Core.indivVarUp v i j ∧ ∀ (w : W), w ∈ j⟦φ⟧ₚ ↔ (j⟦v⟧ᵢ) w ≠ Semantics.Dynamic.Core.Entity.star)

def Semantics.Dynamic.Core.dynInclusion {W : Type u_1} {E : Type u_2} (φ₁ φ₂ : PVar) (i : ICDRTAssignment W E) : Prop

Dynamic inclusion: φ₁(i) ⊆ φ₂(i).

Equations

• (φ₁ ∈ₚ φ₂ at i) = (i⟦φ₁⟧ₚ ⊆ i⟦φ₂⟧ₚ)

def Semantics.Dynamic.Core.«term_∈ₚ_At_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Dynamic.Core.dynIdentity {W : Type u_1} {E : Type u_2} (α β : PVar) (i : ICDRTAssignment W E) : Prop

Dynamic identity: α(i) = β(i).

Equations

• Semantics.Dynamic.Core.dynIdentity α β i = (i⟦α⟧ₚ = i⟦β⟧ₚ)

def Semantics.Dynamic.Core.dynComplement {W : Type u_1} {E : Type u_2} (φ : PVar) (i : ICDRTAssignment W E) : Set W

Dynamic complementation: set-theoretic complement of a propositional dref.

Equations

• Semantics.Dynamic.Core.dynComplement φ i = (i⟦φ⟧ₚ)ᶜ

def Semantics.Dynamic.Core.isComplement {W : Type u_1} {E : Type u_2} (φ₁ φ₂ : PVar) (i : ICDRTAssignment W E) : Prop

Condition: φ₁ is the complement of φ₂ at state i. The negation condition φ₁ ≡ φ̄₂.

Equations

• Semantics.Dynamic.Core.isComplement φ₁ φ₂ i = (i⟦φ₁⟧ₚ = (i⟦φ₂⟧ₚ)ᶜ)

def Semantics.Dynamic.Core.dynUnion {W : Type u_1} {E : Type u_2} (φ₁ φ₂ : PVar) (i : ICDRTAssignment W E) : Set W

Dynamic union: φ₁(i) ∪ φ₂(i).

Equations

• Semantics.Dynamic.Core.dynUnion φ₁ φ₂ i = i⟦φ₁⟧ₚ ∪ i⟦φ₂⟧ₚ

def Semantics.Dynamic.Core.dynPred {W : Type u_1} {E : Type u_2} (R : E → W → Prop) (φ : PVar) (v : IVar) (i : ICDRTAssignment W E) : Prop

Dynamic predication: R_φ(v).

A unary predicate R interpreted relative to a propositional dref φ (the local context):

R_φ(v) := λi. ∀w.(φ(i)(w) → R(v(i)(w))(w))

Holds when the predicate R applies to v's referent in every world of the local context φ. The universal falsifier ⋆ never satisfies R, so a ⋆-valued referent in any φ-world makes dynPred fail.

Equations

• Semantics.Dynamic.Core.dynPred R φ v i = ∀ w ∈ i⟦φ⟧ₚ, match (i⟦v⟧ᵢ) w with | Semantics.Dynamic.Core.Entity.some e => R e w | Semantics.Dynamic.Core.Entity.star => False

def Semantics.Dynamic.Core.localEntailment {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) (i : ICDRTAssignment W E) : Prop

Local contextual entailment: v has a defined referent throughout φ(i).

∀w.(φ(i)(w) → v(i)(w) ≠ ⋆_e)

A precondition for anaphora to v resolved in local context φ.

Equations

• Semantics.Dynamic.Core.localEntailment φ v i = ∀ w ∈ i⟦φ⟧ₚ, (i⟦v⟧ᵢ) w ≠ Semantics.Dynamic.Core.Entity.star

theorem Semantics.Dynamic.Core.pred_entails_existence {W : Type u_1} {E : Type u_2} (v : IVar) (i : ICDRTAssignment W E) (w : W) (e : E) (hv : (i⟦v⟧ᵢ) w = Entity.some e) : (i⟦v⟧ᵢ) w ≠ Entity.star

Predication entails existence: a successful predication of R to v implies v(i)(w) ≠ ⋆.

def Semantics.Dynamic.Core.veridicalIndiv {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : ICDRTAssignment W E) : Prop

Veridical individual dref: v has a referent in all φ_DC-worlds.

Equations

• Semantics.Dynamic.Core.veridicalIndiv φ_DC v i = ∀ w ∈ i⟦φ_DC⟧ₚ, (i⟦v⟧ᵢ) w ≠ Semantics.Dynamic.Core.Entity.star

def Semantics.Dynamic.Core.veridicalProp {W : Type u_1} {E : Type u_2} (φ_DC δ : PVar) (i : ICDRTAssignment W E) : Prop

Veridical propositional dref: φ_DC(i) ⊆ δ(i).

Equations

• Semantics.Dynamic.Core.veridicalProp φ_DC δ i = (i⟦φ_DC⟧ₚ ⊆ i⟦δ⟧ₚ)

def Semantics.Dynamic.Core.counterfactualIndiv {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : ICDRTAssignment W E) : Prop

Counterfactual individual dref: v maps to ⋆ in all φ_DC-worlds.

Equations

• Semantics.Dynamic.Core.counterfactualIndiv φ_DC v i = ∀ w ∈ i⟦φ_DC⟧ₚ, (i⟦v⟧ᵢ) w = Semantics.Dynamic.Core.Entity.star

def Semantics.Dynamic.Core.counterfactualProp {W : Type u_1} {E : Type u_2} (φ_DC δ : PVar) (i : ICDRTAssignment W E) : Prop

Counterfactual propositional dref: φ_DC(i) ∩ δ(i) = ∅.

Equations

• Semantics.Dynamic.Core.counterfactualProp φ_DC δ i = (i⟦φ_DC⟧ₚ ∩ i⟦δ⟧ₚ = ∅)

def Semantics.Dynamic.Core.hypotheticalIndiv {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : ICDRTAssignment W E) : Prop

Hypothetical individual dref: neither veridical nor counterfactual.

Equations

• Semantics.Dynamic.Core.hypotheticalIndiv φ_DC v i = (¬Semantics.Dynamic.Core.veridicalIndiv φ_DC v i ∧ ¬Semantics.Dynamic.Core.counterfactualIndiv φ_DC v i)

def Semantics.Dynamic.Core.hypotheticalProp {W : Type u_1} {E : Type u_2} (φ_DC δ : PVar) (i : ICDRTAssignment W E) : Prop

Hypothetical propositional dref: neither veridical nor counterfactual.

Equations

• Semantics.Dynamic.Core.hypotheticalProp φ_DC δ i = (¬Semantics.Dynamic.Core.veridicalProp φ_DC δ i ∧ ¬Semantics.Dynamic.Core.counterfactualProp φ_DC δ i)

def Semantics.Dynamic.Core.accessible {W : Type u_1} {E : Type u_2} (φ_anaphor : PVar) (v : IVar) (φ_DC : PVar) (i : ICDRTAssignment W E) : Prop

Accessibility: v is accessible at the anaphor site φ_anaphor iff it is locally entailed there and the discourse is consistent.

Equations

• Semantics.Dynamic.Core.accessible φ_anaphor v φ_DC i = (Semantics.Dynamic.Core.localEntailment φ_anaphor v i ∧ i⟦φ_DC⟧ₚ.Nonempty)

def Semantics.Dynamic.Core.subsetReq {W : Type u_1} {E : Type u_2} (φ_anaphor φ_antecedent : PVar) (i : ICDRTAssignment W E) : Prop

Subset requirement: indefinite at φ_antecedent can antecede pronoun at φ_anaphor only when φ_anaphor(i) ⊆ φ_antecedent(i).

Equations

• Semantics.Dynamic.Core.subsetReq φ_anaphor φ_antecedent i = (i⟦φ_anaphor⟧ₚ ⊆ i⟦φ_antecedent⟧ₚ)

def Semantics.Dynamic.Core.decCondition {W : Type u_1} {E : Type u_2} (φ_DC φ : PVar) (j : ICDRTAssignment W E) : Prop

Generic declarative-assertion subset condition: φ_DC(j) ⊆ φ(j).

Definitionally identical to dynInclusion φ_DC φ j; kept as a separate name because the speech-act literature reads it as "the speaker's commitment set is updated to a subset of the asserted content".

Equations

• Semantics.Dynamic.Core.decCondition φ_DC φ j = (j⟦φ_DC⟧ₚ ⊆ j⟦φ⟧ₚ)

structure Semantics.Dynamic.Core.DiscContext (W : Type u_3) (E : Type u_4) (Speaker : Type u_5) : Type (max (max u_3 u_4) u_5)

A multi-agent discourse context: a current discourse state plus an assignment from interlocutors to commitment-set propositional variables.

Each interlocutor x has their own commitment-set dref dcVar x. This is the multi-agent generalization of single-state dynamic semantics — distinct interlocutors can carry contradictory commitments simultaneously without making the discourse inconsistent.

• state : ICDRTAssignment W E

  Current discourse state

• dcVar : Speaker → PVar

  Map from interlocutors to their commitment-set propositional variables

def Semantics.Dynamic.Core.DiscContext.consistent {W : Type u_1} {E : Type u_2} {Speaker : Type u_3} (c : DiscContext W E Speaker) : Prop

Discourse consistency: every interlocutor's commitment set is nonempty. ∀x ∈ INT, φ_{DC_x}(i) ≠ ∅

Equations

• c.consistent = ∀ (x : Speaker), c.state⟦c.dcVar x⟧ₚ.Nonempty

def Semantics.Dynamic.Core.DiscContext.updateSuccessful {W : Type u_1} {E : Type u_2} {Speaker : Type u_3} (c : DiscContext W E Speaker) (D : ICDRTUpdate W E) : Prop

An update D is successful in context C iff some output assignment exists.

Equations

• c.updateSuccessful D = ∃ (j : Semantics.Dynamic.Core.ICDRTAssignment W E), D c.state j

def Semantics.Dynamic.Core.DiscContext.updateAcceptable {W : Type u_1} {E : Type u_2} {Speaker : Type u_3} (c : DiscContext W E Speaker) (D : ICDRTUpdate W E) : Prop

An update is acceptable iff it is successful AND leaves all commitment sets nonempty (preserves discourse consistency).

Equations

• c.updateAcceptable D = ∃ (j : Semantics.Dynamic.Core.ICDRTAssignment W E), D c.state j ∧ ∀ (x : Speaker), j⟦c.dcVar x⟧ₚ.Nonempty

def Semantics.Dynamic.Core.DiscContext.nullAssignment {W : Type u_1} {E : Type u_2} : ICDRTAssignment W E

Null assignment: every propositional dref maps to all worlds; every individual dref maps to ⋆ in every world. The "no information yet" state.

Equations

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

def Semantics.Dynamic.Core.DiscContext.initialContext {W : Type u_1} {E : Type u_2} {Speaker : Type u_3} (dcVar : Speaker → PVar) : DiscContext W E Speaker

Initial discourse context: null assignment, every commitment set equal to the full set of worlds.

Equations

• Semantics.Dynamic.Core.DiscContext.initialContext dcVar = { state := Semantics.Dynamic.Core.DiscContext.nullAssignment, dcVar := dcVar }

theorem Semantics.Dynamic.Core.DiscContext.initialContext_consistent {W : Type u_1} {E : Type u_2} [Nonempty W] {Speaker : Type u_3} {dcVar : Speaker → PVar} : (initialContext dcVar).consistent

The initial context is always consistent.

def Semantics.Dynamic.Core.pragMaxDC {W : Type u_1} {E : Type u_2} {Speaker : Type u_3} (dcVar : Speaker → PVar) (D : ICDRTUpdate W E) (i j : ICDRTAssignment W E) : Prop

Pragmatic maximization for commitment sets.

Output j is pragmatically privileged when no other possible output h assigns a proper superset to any interlocutor's commitment-set dref:

max_DC(D)(i)(j) := D(i)(j) ∧ ∀h x. D(i)(h) → ¬(φ_{DC_x}(j) ⊊ φ_{DC_x}(h))

A formal articulation of the Gricean Quantity maxim: speakers commit to the strongest claim supported by the evidence.

Equations

• Semantics.Dynamic.Core.pragMaxDC dcVar D i j = (D i j ∧ ∀ (h : Semantics.Dynamic.Core.ICDRTAssignment W E), D i h → ∀ (x : Speaker), ¬j⟦dcVar x⟧ₚ ⊂ h⟦dcVar x⟧ₚ)

def Semantics.Dynamic.Core.propMaxOp {W : Type u_1} {E : Type u_2} (φ : PVar) (D : ICDRTUpdate W E) (i j : ICDRTAssignment W E) : Prop

Propositional maximization: max_φ(D).

Restricts outputs to those where propositional dref φ is maximal — no other successful output k assigns a proper superset to φ:

max_φ(D)(i)(j) := D(i)(j) ∧ ∀k. D(i)(k) → ¬(φ(j) ⊊ φ(k))

Used to ensure local contexts are as wide as the truth conditions allow, e.g. for the inner content of a negated existential.

Equations

• Semantics.Dynamic.Core.propMaxOp φ D i j = (D i j ∧ ∀ (k : Semantics.Dynamic.Core.ICDRTAssignment W E), D i k → ¬j⟦φ⟧ₚ ⊂ k⟦φ⟧ₚ)

def Semantics.Dynamic.Core.believeCondition {W : Type u_1} {E : Type u_2} (φ_belief : PVar) (dox : ICDRTAssignment W E → Set W) (j : ICDRTAssignment W E) : Prop

Doxastic accessibility condition for an attitude verb's local context.

believe_φ'(δ^v) ≡ [φ' | DOX(δ,φ) ⊆ φ']

dox j returns the set of worlds compatible with the agent's beliefs at assignment j; the condition asserts that φ' contains them.

Equations

• Semantics.Dynamic.Core.believeCondition φ_belief dox j = (dox j ⊆ j⟦φ_belief⟧ₚ)

theorem Semantics.Dynamic.Core.relVarUp_implies_localEntailment {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) (i j : ICDRTAssignment W E) (h : relVarUp φ v i j) : localEntailment φ v j

Local entailment follows from relative variable update. The biconditional in relVarUp (Definition 25ii) directly yields local contextual entailment at the output assignment.

theorem Semantics.Dynamic.Core.veridical_implies_accessible {W : Type u_1} {E : Type u_2} (φ_DC φ_anaphor : PVar) (v : IVar) (i : ICDRTAssignment W E) (h_veridical : veridicalIndiv φ_DC v i) (h_subset : i⟦φ_anaphor⟧ₚ ⊆ i⟦φ_DC⟧ₚ) (h_consistent : i⟦φ_DC⟧ₚ.Nonempty) : accessible φ_anaphor v φ_DC i

Veridical dref + DC-subsumed anaphor context + consistency → accessibility.

theorem Semantics.Dynamic.Core.counterfactual_veridical_fails {W : Type u_1} {E : Type u_2} (φ_DC φ_anaphor φ_antecedent : PVar) (v : IVar) (i : ICDRTAssignment W E) (h_cf : counterfactualIndiv φ_DC v i) (h_dc_veridical : i⟦φ_DC⟧ₚ ⊆ i⟦φ_anaphor⟧ₚ) (h_subset : subsetReq φ_anaphor φ_antecedent i) (h_rel : ∀ (w : W), w ∈ i⟦φ_antecedent⟧ₚ ↔ (i⟦v⟧ᵢ) w ≠ Entity.star) : ¬accessible φ_anaphor v φ_DC i

Counterfactual dref in veridical anaphor context → inaccessibility.

theorem Semantics.Dynamic.Core.double_complement_eq {W : Type u_1} {E : Type u_2} (φ₁ φ₂ φ₃ : PVar) (i : ICDRTAssignment W E) (h1 : isComplement φ₁ φ₂ i) (h2 : isComplement φ₃ φ₁ i) : i⟦φ₃⟧ₚ = i⟦φ₂⟧ₚ

Double complementation collapses: φ₁ ≡ φ̄₂ and φ₃ ≡ φ̄₁ give φ₃ = φ₂.

theorem Semantics.Dynamic.Core.disjunction_enables_anaphora {W : Type u_1} {E : Type u_2} (φ₃ φ_a : PVar) (v : IVar) (i : ICDRTAssignment W E) (h_sub : i⟦φ_a⟧ₚ ⊆ i⟦φ₃⟧ₚ) (h_rel : ∀ w ∈ i⟦φ₃⟧ₚ, (i⟦v⟧ᵢ) w ≠ Entity.star) : localEntailment φ_a v i

Disjunction enables anaphora across disjuncts: if v is defined in all φ₃-worlds and the anaphor's local context is contained in φ₃, then v is locally entailed at the anaphor site.

theorem Semantics.Dynamic.Core.veridicality_trichotomy {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : ICDRTAssignment W E) : veridicalIndiv φ_DC v i ∨ counterfactualIndiv φ_DC v i ∨ hypotheticalIndiv φ_DC v i

Veridicality trichotomy: every individual dref is veridical, counterfactual, or hypothetical relative to any speaker.

theorem Semantics.Dynamic.Core.veridical_counterfactual_exclusive {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : ICDRTAssignment W E) (hv : veridicalIndiv φ_DC v i) (hc : counterfactualIndiv φ_DC v i) : ¬i⟦φ_DC⟧ₚ.Nonempty

Veridical and counterfactual are incompatible given a nonempty DC.

theorem Semantics.Dynamic.Core.star_blocks_dynPred {W : Type u_1} {E : Type u_2} (R : E → W → Prop) (φ : PVar) (v : IVar) (i : ICDRTAssignment W E) (w : W) (hw : w ∈ i⟦φ⟧ₚ) (hstar : (i⟦v⟧ᵢ) w = Entity.star) (hpred : dynPred R φ v i) : False

The universal falsifier blocks dynamic predication: if v maps to ⋆ at some w ∈ φ, then R_φ(v) fails.

theorem Semantics.Dynamic.Core.dec_complement_counterfactual {W : Type u_1} {E : Type u_2} (φ_DC φ_outer φ_inner : PVar) (i : ICDRTAssignment W E) (h_comp : isComplement φ_outer φ_inner i) (h_dec : φ_DC ∈ₚ φ_outer at i) : counterfactualProp φ_DC φ_inner i

Subset condition + complementation derive counterfactuality of the inner content. The shape DC ⊆ φ_outer ∧ φ_outer = φ̄_inner ⟹ DC ∩ φ_inner = ∅ is the core algebraic move that turns negation into commitment-set counterfactuality (the recipe used by @cite{hofmann-2025}'s analysis of "there isn't a bathroom").

def Semantics.Dynamic.Core.fiberDRS {W : Type u_1} {E : Type u_2} (D : ICDRTUpdate W E) : DynProp.DRS (ICDRTAssignment W E × W)

Embed an assignment-only relation into a pair relation with passive worlds.

fiberDRS D (i, w) (j, w') ↔ w = w' ∧ D i j

ICDRT updates operate on assignments only and worlds are inert fibers. fiberDRS makes this structure explicit at the type level of DRS (ICDRTAssignment W E × W).

Equations

• Semantics.Dynamic.Core.fiberDRS D (j, w') (j_1, w'_1) = (w' = w'_1 ∧ D j j_1)

theorem Semantics.Dynamic.Core.toDynProp_eq_lift_fiberDRS {W : Type u_1} {E : Type u_2} (D : ICDRTUpdate W E) : D.toDynProp = lift (fiberDRS D)

toDynProp = lift ∘ fiberDRS: the static-to-dynamic bridge factors through fiberwise embedding followed by relational image.

theorem Semantics.Dynamic.Core.fiberDRS_seq {W : Type u_1} {E : Type u_2} (D₁ D₂ : ICDRTUpdate W E) : fiberDRS (D₁ ⨟ D₂) = fiberDRS D₁ ⨟ fiberDRS D₂

fiberDRS preserves sequential composition.

theorem Semantics.Dynamic.Core.fiberDRS_idUp {W : Type u_1} {E : Type u_2} : fiberDRS ICDRTUpdate.idUp = fun (p q : ICDRTAssignment W E × W) => p = q

fiberDRS preserves identity.

theorem Semantics.Dynamic.Core.fiberDRS_homomorphism {W : Type u_1} {E : Type u_2} : (∀ (D₁ D₂ : ICDRTUpdate W E), fiberDRS (D₁ ⨟ D₂) = fiberDRS D₁ ⨟ fiberDRS D₂) ∧ fiberDRS ICDRTUpdate.idUp = fun (p q : ICDRTAssignment W E × W) => p = q

fiberDRS is a monoid homomorphism (ICDRTUpdate, seq, idUp) → (DRS, dseq, id).

theorem Semantics.Dynamic.Core.toDynProp_isDistributive {W : Type u_1} {E : Type u_2} (D : ICDRTUpdate W E) : IsDistributive D.toDynProp

toDynProp D is always distributive: it processes each assignment-world pair independently. Corollary of lift_isDistributive.

theorem Semantics.Dynamic.Core.toDynProp_test_eliminative {W : Type u_1} {E : Type u_2} (C : ICDRTAssignment W E → Prop) : IsEliminative (ICDRTUpdate.toDynProp fun (i j : ICDRTAssignment W E) => i = j ∧ C j)

A test update — one that preserves the assignment — lifts to an eliminative CCP: it can only shrink the context, never grow it.

theorem Semantics.Dynamic.Core.toDynProp_dec_eliminative {W : Type u_1} {E : Type u_2} (φ_DC φ : PVar) : IsEliminative (ICDRTUpdate.toDynProp fun (i j : ICDRTAssignment W E) => i = j ∧ decCondition φ_DC φ j)

The DEC condition lifts to an eliminative CCP: assertion narrows the context (removes worlds from the commitment set).

theorem Semantics.Dynamic.Core.complement_update_distributive {W : Type u_1} {E : Type u_2} (φ_outer φ_inner : PVar) : IsDistributive (ICDRTUpdate.toDynProp fun (i j : ICDRTAssignment W E) => i = j ∧ isComplement φ_outer φ_inner j)

ICDRT-style negation via complementation stays distributive — unlike test-based dynamic negation that inspects the whole input state.

theorem Semantics.Dynamic.Core.lower_toDynProp {W : Type u_1} {E : Type u_2} (D : ICDRTUpdate W E) : lower D.toDynProp = fiberDRS D

Round-trip: lowering the CCP back to a relation recovers the fiberwise embedding. Combined with lower_lift, this shows no information is lost in the fiberDRS/lift factorization.

theorem Semantics.Dynamic.Core.toDynProp_seq_algebraic {W : Type u_1} {E : Type u_2} (D₁ D₂ : ICDRTUpdate W E) (c : IContext W E) : (D₁ ⨟ D₂).toDynProp c = CCP.seq D₁.toDynProp D₂.toDynProp c

toDynProp preserves sequential composition — algebraic derivation via fiberDRS_seq + lift_dseq.

theorem Semantics.Dynamic.Core.toDynProp_id_algebraic {W : Type u_1} {E : Type u_2} (c : IContext W E) : ICDRTUpdate.idUp.toDynProp c = CCP.id c

toDynProp preserves identity — algebraic derivation via fiberDRS_idUp.

Register ICDRTAssignment W E as an instance of the abstract Dynamic.Context typeclass family. With these instances, every predicate and theorem in Dynamic.Context (e.g. counterfactual_blocks_veridical, multi_counterfactual_blocks_veridical) applies to ICDRT contexts without re-proof.

@[implicit_reducible]

instance Semantics.Dynamic.Core.instHasIndivDrefs_ICDRT {W : Type u_1} {E : Type u_2} : Context.HasIndivDrefs (ICDRTAssignment W E) IVar W E

Equations

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

@[implicit_reducible]

instance Semantics.Dynamic.Core.instHasPropDrefs_ICDRT {W : Type u_1} {E : Type u_2} : Context.HasPropDrefs (ICDRTAssignment W E) PVar W

Equations

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

theorem Semantics.Dynamic.Core.localEntailment_eq_context {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) (i : ICDRTAssignment W E) : Context.localEntailment φ v i ↔ localEntailment φ v i

The generic Dynamic.Context.localEntailment agrees definitionally with the concrete localEntailment on ICDRT.

theorem Semantics.Dynamic.Core.veridicalIndiv_eq_context {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : ICDRTAssignment W E) : Context.veridicalIndiv φ_DC v i ↔ veridicalIndiv φ_DC v i

The generic Dynamic.Context.veridicalIndiv agrees definitionally with the concrete veridicalIndiv on ICDRT.

theorem Semantics.Dynamic.Core.subsetReq_eq_context {W : Type u_1} {E : Type u_2} (a b : PVar) (i : ICDRTAssignment W E) : Context.subsetReq a b i ↔ subsetReq a b i

The generic Dynamic.Context.subsetReq agrees definitionally with the concrete subsetReq on ICDRT.

theorem Semantics.Dynamic.Core.decCondition_eq_context {W : Type u_1} {E : Type u_2} (φ_DC φ : PVar) (i : ICDRTAssignment W E) : Context.decCondition φ_DC φ i ↔ decCondition φ_DC φ i

The generic Dynamic.Context.decCondition agrees definitionally with the concrete decCondition on ICDRT.

theorem Semantics.Dynamic.Core.relVarUp_eq_context {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) (i j : ICDRTAssignment W E) : relVarUp φ v i j ↔ Context.relVarUp φ v i j

Hofmann's relVarUp agrees with the generic Dynamic.Context.relVarUp (modulo set-extensionality on the biconditional). The cross-field operation is a definition over the basic typeclass operations, not a separate axiom.