Intensional CDRT

[Mus96] [Sto99] [Bra06] [Hof25]

ICDRT ([Hof25]'s intensional extension of [Mus96]'s Compositional DRT): dynamic semantics built over ICDRT.Assignment (individual drefs as IVar → W → Entity E plus propositional drefs as PVar → Set W). This is a layer above ICDRT/Defs.lean (which owns the carrier types) and below paper-specific theories such as [Hof25] (whose paper apparatus lives in Studies/Hofmann2025.lean).

ICDRT's delta over the level-0 spine is exactly its carrier and its conditions: ICDRT.Update is the spine's relational Update at ICDRT assignments, sequencing is the spine's seq, and the static-to-dynamic bridge toUpdate is lift ∘ fiberDRS — by definition, not by theorem. fiberDRS embeds assignment-only relations into pair relations (passive worlds); lift is the spine's relational image. Consequently toUpdate is always distributive (lift_isDistributive) — the algebraic content of [Hof25]'s observation that ICDRT-style negation via propositional dref complementation stays distributive, unlike test-based dynamic negation that inspects whole states.

Main definitions

• ICDRT.Context: information states — sets of assignment-world pairs.
• ICDRT.Update (the spine's Update at ICDRT assignments), idUp, fiberDRS, and toUpdate := lift ∘ fiberDRS.
• propVarUp, indivVarUp, multiVarUp, relVarUp: variable updates.
• dynInclusion, isComplement: dynamic conditions on propositional drefs.
• dynPred, localEntailment: predication and local contextual entailment.
• veridicalIndiv, counterfactualIndiv, hypotheticalIndiv, counterfactualProp, accessible, subsetReq: the veridicality typology.

Information states

@[reducible, inline]

abbrev DynamicSemantics.ICDRT.Context (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

• DynamicSemantics.ICDRT.Context W E = Set (DynamicSemantics.ICDRT.Assignment W E × W)

def DynamicSemantics.ICDRT.Context.univ {W : Type u_1} {E : Type u_2} : Context W E

The trivial context (all possibilities)

Equations

• DynamicSemantics.ICDRT.Context.univ = Set.univ

Updates as static relations

@[reducible, inline]

abbrev DynamicSemantics.ICDRT.Update (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Static update relation between input and output assignments: the spine's relational Update at ICDRT assignments. Following [Mus96]'s Compositional DRT, dynamic updates are relations between assignments; sequencing is the spine's seq and the lift to context transformers is toUpdate below.

Equations

• DynamicSemantics.ICDRT.Update W E = DynamicSemantics.Update (DynamicSemantics.ICDRT.Assignment W E)

def DynamicSemantics.ICDRT.idUp {W : Type u_1} {E : Type u_2} : Update W E

Identity update: output equals input.

Equations

• DynamicSemantics.ICDRT.idUp = Eq

def DynamicSemantics.ICDRT.fiberDRS {W : Type u_1} {E : Type u_2} (D : Update W E) : DynamicSemantics.Update (Assignment 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 Update (Assignment W E × W).

Equations

• DynamicSemantics.ICDRT.fiberDRS D (j, w') (j_1, w'_1) = (w' = w'_1 ∧ D j j_1)

def DynamicSemantics.ICDRT.toUpdate {W : Type u_1} {E : Type u_2} (D : Update W E) : CCP (Assignment W E × W)

Lift a static update relation to a context transformer: the fiberwise embedding followed by the spine's relational image.

Equations

• DynamicSemantics.ICDRT.toUpdate D = DynamicSemantics.lift (DynamicSemantics.ICDRT.fiberDRS D)

theorem DynamicSemantics.ICDRT.mem_toUpdate {W : Type u_1} {E : Type u_2} (D : Update W E) (c : Context W E) {p : Assignment W E × W} : p ∈ toUpdate D c ↔ ∃ (i : Assignment W E), (i, p.2) ∈ c ∧ D i p.1

Membership in the lifted update.

theorem DynamicSemantics.ICDRT.idUp_toUpdate {W : Type u_1} {E : Type u_2} (c : Context W E) : toUpdate idUp c = c

Identity update lifts to identity on contexts.

theorem DynamicSemantics.ICDRT.fiberDRS_seq {W : Type u_1} {E : Type u_2} (D₁ D₂ : Update W E) : fiberDRS (Update.seq D₁ D₂) = (fiberDRS D₁).seq (fiberDRS D₂)

fiberDRS preserves sequential composition.

theorem DynamicSemantics.ICDRT.seq_toUpdate {W : Type u_1} {E : Type u_2} (D₁ D₂ : Update W E) (c : Context W E) : toUpdate (Update.seq D₁ D₂) c = toUpdate D₂ (toUpdate D₁ c)

Sequential composition lifts to function composition on contexts.

theorem DynamicSemantics.ICDRT.toUpdate_isDistributive {W : Type u_1} {E : Type u_2} (D : Update W E) : (toUpdate D).IsDistributive

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

theorem DynamicSemantics.ICDRT.toUpdate_test_eliminative {W : Type u_1} {E : Type u_2} (C : Assignment W E → Prop) : (toUpdate fun (i j : Assignment W E) => i = j ∧ C j).IsEliminative

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

Variable updates

def DynamicSemantics.ICDRT.propVarUp {W : Type u_1} {E : Type u_2} (p : PVar) (i j : Assignment W E) : Prop

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

Equations

• DynamicSemantics.ICDRT.propVarUp p i j = ((∀ (q : DynamicSemantics.ICDRT.PVar), q ≠ p → j.prop q = i.prop q) ∧ ∀ (v : DynamicSemantics.ICDRT.IVar), j.indiv v = i.indiv v)

def DynamicSemantics.ICDRT.indivVarUp {W : Type u_1} {E : Type u_2} (v : IVar) (i j : Assignment W E) : Prop

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

Equations

• DynamicSemantics.ICDRT.indivVarUp v i j = ((∀ (p : DynamicSemantics.ICDRT.PVar), j.prop p = i.prop p) ∧ ∀ (u : DynamicSemantics.ICDRT.IVar), u ≠ v → j.indiv u = i.indiv u)

def DynamicSemantics.ICDRT.multiVarUp {W : Type u_1} {E : Type u_2} (ps : List PVar) (vs : List IVar) (i j : Assignment W E) : Prop

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

Equations

• DynamicSemantics.ICDRT.multiVarUp ps vs i j = ((∀ p ∉ ps, j.prop p = i.prop p) ∧ ∀ v ∉ vs, j.indiv v = i.indiv v)

def DynamicSemantics.ICDRT.relVarUp {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) (i j : Assignment 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 [Hof25] Definition 25.

Equations

• DynamicSemantics.ICDRT.relVarUp φ v i j = (DynamicSemantics.ICDRT.indivVarUp v i j ∧ ∀ (w : W), w ∈ j.prop φ ↔ j.indiv v w ≠ DynamicSemantics.ICDRT.Entity.star)

Dynamic conditions on propositional drefs

def DynamicSemantics.ICDRT.dynInclusion {W : Type u_1} {E : Type u_2} (φ₁ φ₂ : PVar) (i : Assignment W E) : Prop

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

Equations

• DynamicSemantics.ICDRT.dynInclusion φ₁ φ₂ i = (i.prop φ₁ ⊆ i.prop φ₂)

def DynamicSemantics.ICDRT.isComplement {W : Type u_1} {E : Type u_2} (φ₁ φ₂ : PVar) (i : Assignment W E) : Prop

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

Equations

• DynamicSemantics.ICDRT.isComplement φ₁ φ₂ i = (i.prop φ₁ = (i.prop φ₂)ᶜ)

Predication and local entailment

def DynamicSemantics.ICDRT.dynPred {W : Type u_1} {E : Type u_2} (R : E → W → Prop) (φ : PVar) (v : IVar) (i : Assignment 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

• DynamicSemantics.ICDRT.dynPred R φ v i = ∀ w ∈ i.prop φ, match i.indiv v w with | DynamicSemantics.ICDRT.Entity.some e => R e w | DynamicSemantics.ICDRT.Entity.star => False

def DynamicSemantics.ICDRT.localEntailment {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) (i : Assignment 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

• DynamicSemantics.ICDRT.localEntailment φ v i = ∀ w ∈ i.prop φ, i.indiv v w ≠ DynamicSemantics.ICDRT.Entity.star

Veridicality typology

@[reducible, inline]

abbrev DynamicSemantics.ICDRT.veridicalIndiv {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : Assignment W E) : Prop

Veridical individual dref: v has a referent in all φ_DC-worlds — localEntailment read at the commitment set.

Equations

• DynamicSemantics.ICDRT.veridicalIndiv φ_DC v i = DynamicSemantics.ICDRT.localEntailment φ_DC v i

def DynamicSemantics.ICDRT.counterfactualIndiv {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : Assignment W E) : Prop

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

Equations

• DynamicSemantics.ICDRT.counterfactualIndiv φ_DC v i = ∀ w ∈ i.prop φ_DC, i.indiv v w = DynamicSemantics.ICDRT.Entity.star

def DynamicSemantics.ICDRT.counterfactualProp {W : Type u_1} {E : Type u_2} (φ_DC δ : PVar) (i : Assignment W E) : Prop

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

Equations

• DynamicSemantics.ICDRT.counterfactualProp φ_DC δ i = (i.prop φ_DC ∩ i.prop δ = ∅)

def DynamicSemantics.ICDRT.hypotheticalIndiv {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : Assignment W E) : Prop

Hypothetical individual dref: neither veridical nor counterfactual.

Equations

• DynamicSemantics.ICDRT.hypotheticalIndiv φ_DC v i = (¬DynamicSemantics.ICDRT.veridicalIndiv φ_DC v i ∧ ¬DynamicSemantics.ICDRT.counterfactualIndiv φ_DC v i)

def DynamicSemantics.ICDRT.accessible {W : Type u_1} {E : Type u_2} (φ_anaphor : PVar) (v : IVar) (φ_DC : PVar) (i : Assignment W E) : Prop

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

Equations

• DynamicSemantics.ICDRT.accessible φ_anaphor v φ_DC i = (DynamicSemantics.ICDRT.localEntailment φ_anaphor v i ∧ (i.prop φ_DC).Nonempty)

@[reducible, inline]

abbrev DynamicSemantics.ICDRT.subsetReq {W : Type u_1} {E : Type u_2} (φ_anaphor φ_antecedent : PVar) (i : Assignment W E) : Prop

Subset requirement: indefinite at φ_antecedent can antecede pronoun at φ_anaphor only when φ_anaphor(i) ⊆ φ_antecedent(i) — dynInclusion at the anaphor site.

Equations

• DynamicSemantics.ICDRT.subsetReq φ_anaphor φ_antecedent i = DynamicSemantics.ICDRT.dynInclusion φ_anaphor φ_antecedent i

Multi-agent discourse contexts

@[reducible, inline]

abbrev DynamicSemantics.ICDRT.decCondition {W : Type u_1} {E : Type u_2} (φ_DC φ : PVar) (j : Assignment W E) : Prop

Generic declarative-assertion subset condition: φ_DC(j) ⊆ φ(j) — dynInclusion under the speech-act reading "the speaker's commitment set is updated to a subset of the asserted content".

Equations

• DynamicSemantics.ICDRT.decCondition φ_DC φ j = DynamicSemantics.ICDRT.dynInclusion φ_DC φ j

theorem DynamicSemantics.ICDRT.counterfactual_blocks_veridical {W : Type u_1} {E : Type u_2} (i j : Assignment W E) (φ_DC φ_anaphor φ_neg : PVar) (h_extends_DC : j.prop φ_DC = i.prop φ_DC) (h_extends_neg : j.prop φ_neg = i.prop φ_neg) (h_disjoint : counterfactualProp φ_DC φ_neg i) (h_dec : decCondition φ_DC φ_anaphor j) (h_subset : subsetReq φ_anaphor φ_neg j) : ¬(j.prop φ_DC).Nonempty

Counterfactual antecedent blocks veridical anaphor ([Hof25]'s bathroom-sentence theorem: "There isn't a bathroom. #It is upstairs."). If j extends i keeping the commitment set and the negated content fixed, the antecedent is counterfactual (φ_DC(i) ∩ φ_neg(i) = ∅), and j satisfies both the DEC condition and the anaphor's subset requirement, then the discourse is inconsistent.

Frameworks without propositional-dref structure have no analogue — [Cha19b]'s State W E handles the same phenomenon by alternative-set filtering (Studies/Charlow2019.lean).

structure DynamicSemantics.ICDRT.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 : Assignment W E

  Current discourse state

• dcVar : Speaker → PVar

  Map from interlocutors to their commitment-set propositional variables

def DynamicSemantics.ICDRT.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.prop (c.dcVar x)).Nonempty

def DynamicSemantics.ICDRT.DiscContext.nullAssignment {W : Type u_1} {E : Type u_2} : Assignment 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 DynamicSemantics.ICDRT.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

• DynamicSemantics.ICDRT.DiscContext.initialContext dcVar = { state := DynamicSemantics.ICDRT.DiscContext.nullAssignment, dcVar := dcVar }

theorem DynamicSemantics.ICDRT.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.

Pragmatic and propositional maximization

def DynamicSemantics.ICDRT.pragMaxDC {W : Type u_1} {E : Type u_2} {Speaker : Type u_3} (dcVar : Speaker → PVar) (D : Update W E) (i j : Assignment 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

• DynamicSemantics.ICDRT.pragMaxDC dcVar D i j = (D i j ∧ ∀ (h : DynamicSemantics.ICDRT.Assignment W E), D i h → ∀ (x : Speaker), ¬j.prop (dcVar x) ⊂ h.prop (dcVar x))

def DynamicSemantics.ICDRT.propMaxOp {W : Type u_1} {E : Type u_2} (φ : PVar) (D : Update W E) (i j : Assignment 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

• DynamicSemantics.ICDRT.propMaxOp φ D i j = (D i j ∧ ∀ (k : DynamicSemantics.ICDRT.Assignment W E), D i k → ¬j.prop φ ⊂ k.prop φ)

def DynamicSemantics.ICDRT.believeCondition {W : Type u_1} {E : Type u_2} (φ_belief : PVar) (dox : Assignment W E → Set W) (j : Assignment 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

• DynamicSemantics.ICDRT.believeCondition φ_belief dox j = (dox j ⊆ j.prop φ_belief)

Structural theorems

theorem DynamicSemantics.ICDRT.relVarUp_implies_localEntailment {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) (i j : Assignment 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 DynamicSemantics.ICDRT.veridical_implies_accessible {W : Type u_1} {E : Type u_2} (φ_DC φ_anaphor : PVar) (v : IVar) (i : Assignment W E) (h_veridical : veridicalIndiv φ_DC v i) (h_subset : i.prop φ_anaphor ⊆ i.prop φ_DC) (h_consistent : (i.prop φ_DC).Nonempty) : accessible φ_anaphor v φ_DC i

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

theorem DynamicSemantics.ICDRT.counterfactual_veridical_fails {W : Type u_1} {E : Type u_2} (φ_DC φ_anaphor φ_antecedent : PVar) (v : IVar) (i : Assignment W E) (h_cf : counterfactualIndiv φ_DC v i) (h_dc_veridical : i.prop φ_DC ⊆ i.prop φ_anaphor) (h_subset : subsetReq φ_anaphor φ_antecedent i) (h_rel : ∀ (w : W), w ∈ i.prop φ_antecedent ↔ i.indiv v w ≠ Entity.star) : ¬accessible φ_anaphor v φ_DC i

Counterfactual dref in veridical anaphor context → inaccessibility.

theorem DynamicSemantics.ICDRT.double_complement_eq {W : Type u_1} {E : Type u_2} (φ₁ φ₂ φ₃ : PVar) (i : Assignment W E) (h1 : isComplement φ₁ φ₂ i) (h2 : isComplement φ₃ φ₁ i) : i.prop φ₃ = i.prop φ₂

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

theorem DynamicSemantics.ICDRT.disjunction_enables_anaphora {W : Type u_1} {E : Type u_2} (φ₃ φ_a : PVar) (v : IVar) (i : Assignment W E) (h_sub : i.prop φ_a ⊆ i.prop φ₃) (h_rel : ∀ w ∈ i.prop φ₃, i.indiv 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 DynamicSemantics.ICDRT.veridicality_trichotomy {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : Assignment 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 DynamicSemantics.ICDRT.veridical_counterfactual_exclusive {W : Type u_1} {E : Type u_2} (φ_DC : PVar) (v : IVar) (i : Assignment W E) (hv : veridicalIndiv φ_DC v i) (hc : counterfactualIndiv φ_DC v i) : ¬(i.prop φ_DC).Nonempty

Veridical and counterfactual are incompatible given a nonempty DC.

theorem DynamicSemantics.ICDRT.star_blocks_dynPred {W : Type u_1} {E : Type u_2} (R : E → W → Prop) (φ : PVar) (v : IVar) (i : Assignment W E) (w : W) (hw : w ∈ i.prop φ) (hstar : i.indiv 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 DynamicSemantics.ICDRT.dec_complement_counterfactual {W : Type u_1} {E : Type u_2} (φ_DC φ_outer φ_inner : PVar) (i : Assignment W E) (h_comp : isComplement φ_outer φ_inner i) (h_dec : dynInclusion φ_DC φ_outer 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 [Hof25]'s analysis of "there isn't a bathroom").

Fibered lookup instance

@[implicit_reducible]

instance DynamicSemantics.ICDRT.instHasFiberedLookupEntityAssignmentIVar {W : Type u_1} {E : Type u_2} : HasFiberedLookup Entity (Assignment W E) IVar W E

ICDRT contexts expose the shared lookup interface at M = Entity (Dynamic/Lookup.lean), making ICDRT lookups comparable with the extensional (M = Id) and [Cha19b] (M = Set) families.

Equations

• DynamicSemantics.ICDRT.instHasFiberedLookupEntityAssignmentIVar = { iLookup := fun (i : DynamicSemantics.ICDRT.Assignment W E) (v : DynamicSemantics.ICDRT.IVar) (w : W) => i.indiv v w }