ICDRT discourse referents

[Hof25], [Bra06]

Carrier types of Intensional CDRT ([Hof25]'s intensional extension of [Mus96]'s Compositional DRT, following [Bra06]'s Dynamic Ty2): entities extended with the universal falsifier ⋆ (Entity, [Bra06]'s dummy value for referent-less worlds), the two variable sorts (IVar for individuals, PVar for the propositional drefs that store local contexts), and the two-sorted assignment (ICDRT.Assignment — individual drefs as individual concepts W → Entity E, propositional drefs as Set W).

The system built over these types — updates, dynamic conditions, the veridicality typology — lives in ICDRT/Basic.lean; the paper-specific apparatus in Studies/Hofmann2025.lean. (The concept drefs of [Kri26] live with their consumer in Studies/Krifka2026.lean.)

inductive DynamicSemantics.ICDRT.Entity (E : Type u_1) : Type u_1

Entities extended with the universal falsifier ⋆ ([Bra06]; adopted by [Hof25]): individual drefs map to ⋆ in worlds where the referent does not exist — in "There's no bathroom", the bathroom variable maps to ⋆ in all worlds. Lexical relations are axiomatically false of ⋆.

Option E under a renaming, kept as its own inductive for the paper's ⋆ vocabulary and constructor-level pattern matching in consumers.

• some {E : Type u_1} : E → Entity E
• star {E : Type u_1} : Entity E

@[implicit_reducible]

instance DynamicSemantics.ICDRT.instDecidableEqEntity {E✝ : Type u_1} [DecidableEq E✝] : DecidableEq (Entity E✝)

Equations

• DynamicSemantics.ICDRT.instDecidableEqEntity = DynamicSemantics.ICDRT.instDecidableEqEntity.decEq

def DynamicSemantics.ICDRT.instDecidableEqEntity.decEq {E✝ : Type u_1} [DecidableEq E✝] (x✝ x✝¹ : Entity E✝) : Decidable (x✝ = x✝¹)

Equations

• DynamicSemantics.ICDRT.instDecidableEqEntity.decEq (DynamicSemantics.ICDRT.Entity.some a) (DynamicSemantics.ICDRT.Entity.some b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
• DynamicSemantics.ICDRT.instDecidableEqEntity.decEq (DynamicSemantics.ICDRT.Entity.some a) DynamicSemantics.ICDRT.Entity.star = isFalse ⋯
• DynamicSemantics.ICDRT.instDecidableEqEntity.decEq DynamicSemantics.ICDRT.Entity.star (DynamicSemantics.ICDRT.Entity.some a) = isFalse ⋯
• DynamicSemantics.ICDRT.instDecidableEqEntity.decEq DynamicSemantics.ICDRT.Entity.star DynamicSemantics.ICDRT.Entity.star = isTrue ⋯

def DynamicSemantics.ICDRT.instReprEntity.repr {E✝ : Type u_1} [Repr E✝] : Entity E✝ → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance DynamicSemantics.ICDRT.instReprEntity {E✝ : Type u_1} [Repr E✝] : Repr (Entity E✝)

Equations

• DynamicSemantics.ICDRT.instReprEntity = { reprPrec := DynamicSemantics.ICDRT.instReprEntity.repr }

def DynamicSemantics.ICDRT.Entity.isSome {E : Type u_1} : Entity E → Prop

Is this a real entity (not ⋆)?

Equations

• (DynamicSemantics.ICDRT.Entity.some a).isSome = True
• DynamicSemantics.ICDRT.Entity.star.isSome = False

@[implicit_reducible]

instance DynamicSemantics.ICDRT.Entity.instDecidablePredIsSome {E : Type u_1} : DecidablePred isSome

Equations

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

@[implicit_reducible]

instance DynamicSemantics.ICDRT.Entity.instInhabited {E : Type u_1} [Inhabited E] : Inhabited (Entity E)

Equations

• DynamicSemantics.ICDRT.Entity.instInhabited = { default := DynamicSemantics.ICDRT.Entity.star }

@[implicit_reducible]

instance DynamicSemantics.ICDRT.Entity.instFunctor : Functor Entity

Entity is a functor: f <$> .some e = .some (f e) and f <$> .star = .star — Option's functor structure under the renaming some ↔ Entity.some, none ↔ Entity.star. Used by the effect-functor-parameterized lookup interface in Semantics/Dynamic/Lookup.lean.

Equations

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

@[implicit_reducible]

instance DynamicSemantics.ICDRT.Entity.instFintype {E : Type u_1} [Fintype E] : Fintype (Entity E)

Equations

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

structure DynamicSemantics.ICDRT.PVar : Type

A propositional variable (names a propositional dref).

Propositional variables track local contexts - the set of worlds where an individual dref was introduced.

• idx : ℕ

@[implicit_reducible]

instance DynamicSemantics.ICDRT.instDecidableEqPVar : DecidableEq PVar

Equations

• DynamicSemantics.ICDRT.instDecidableEqPVar = DynamicSemantics.ICDRT.instDecidableEqPVar.decEq

def DynamicSemantics.ICDRT.instDecidableEqPVar.decEq (x✝ x✝¹ : PVar) : Decidable (x✝ = x✝¹)

Equations

• DynamicSemantics.ICDRT.instDecidableEqPVar.decEq { idx := a } { idx := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance DynamicSemantics.ICDRT.instReprPVar : Repr PVar

Equations

• DynamicSemantics.ICDRT.instReprPVar = { reprPrec := DynamicSemantics.ICDRT.instReprPVar.repr }

def DynamicSemantics.ICDRT.instReprPVar.repr : PVar → ℕ → Std.Format

Equations

• DynamicSemantics.ICDRT.instReprPVar.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "idx" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.idx)).group) " }"

def DynamicSemantics.ICDRT.instHashablePVar.hash : PVar → UInt64

Equations

• DynamicSemantics.ICDRT.instHashablePVar.hash { idx := a } = mixHash 0 (hash a)

@[implicit_reducible]

instance DynamicSemantics.ICDRT.instHashablePVar : Hashable PVar

Equations

• DynamicSemantics.ICDRT.instHashablePVar = { hash := DynamicSemantics.ICDRT.instHashablePVar.hash }

structure DynamicSemantics.ICDRT.IVar : Type

An individual variable (names an individual dref).

• idx : ℕ

def DynamicSemantics.ICDRT.instDecidableEqIVar.decEq (x✝ x✝¹ : IVar) : Decidable (x✝ = x✝¹)

Equations

• DynamicSemantics.ICDRT.instDecidableEqIVar.decEq { idx := a } { idx := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance DynamicSemantics.ICDRT.instDecidableEqIVar : DecidableEq IVar

Equations

• DynamicSemantics.ICDRT.instDecidableEqIVar = DynamicSemantics.ICDRT.instDecidableEqIVar.decEq

def DynamicSemantics.ICDRT.instReprIVar.repr : IVar → ℕ → Std.Format

Equations

• DynamicSemantics.ICDRT.instReprIVar.repr x✝ prec✝ = Std.Format.bracket "{ " (Std.Format.nil ++ Std.Format.text "idx" ++ Std.Format.text " := " ++ (Std.Format.nest 7 (repr x✝.idx)).group) " }"

@[implicit_reducible]

instance DynamicSemantics.ICDRT.instReprIVar : Repr IVar

Equations

• DynamicSemantics.ICDRT.instReprIVar = { reprPrec := DynamicSemantics.ICDRT.instReprIVar.repr }

@[implicit_reducible]

instance DynamicSemantics.ICDRT.instHashableIVar : Hashable IVar

Equations

• DynamicSemantics.ICDRT.instHashableIVar = { hash := DynamicSemantics.ICDRT.instHashableIVar.hash }

def DynamicSemantics.ICDRT.instHashableIVar.hash : IVar → UInt64

Equations

• DynamicSemantics.ICDRT.instHashableIVar.hash { idx := a } = mixHash 0 (hash a)

structure DynamicSemantics.ICDRT.Assignment (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

An ICDRT assignment maps variables to values.

In ICDRT, we need to track two kinds of assignments:

1. Individual variable assignments: IVar → Entity E
2. Propositional variable assignments: PVar → Set W

This is used by the ICDRT system (ICDRT/Basic.lean); simpler theories can use Nat → E.

• indiv : IVar → W → Entity E

  Individual variable assignment: intensional individual drefs (individual concepts). Each variable maps worlds to entities, possibly ⋆. In [Hof25]'s notation: type s(we), i.e., for each variable v, v(i) is a function from worlds to entities. v(i)(w) = ⋆ when v has no referent in w.

• prop : PVar → Set W

  Propositional variable assignment

def DynamicSemantics.ICDRT.Assignment.empty {W : Type u_1} {E : Type u_2} : Assignment W E

Empty assignment (all variables map to ⋆ / empty set)

Equations

• DynamicSemantics.ICDRT.Assignment.empty = { indiv := fun (x : DynamicSemantics.ICDRT.IVar) (x_1 : W) => DynamicSemantics.ICDRT.Entity.star, prop := fun (x : DynamicSemantics.ICDRT.PVar) => ∅ }

def DynamicSemantics.ICDRT.Assignment.updateIndiv {W : Type u_1} {E : Type u_2} (g : Assignment W E) (v : IVar) (e : W → Entity E) : Assignment W E

Update individual variable with an individual concept (world-dependent): mathlib's Function.update at the indiv field.

Equations

• g.updateIndiv v e = { indiv := Function.update g.indiv v e, prop := g.prop }

def DynamicSemantics.ICDRT.Assignment.updateIndivConst {W : Type u_1} {E : Type u_2} (g : Assignment W E) (v : IVar) (e : Entity E) : Assignment W E

Update individual variable with a constant entity (world-invariant). Convenience for cases where the entity is the same in all worlds.

Equations

• g.updateIndivConst v e = g.updateIndiv v fun (x : W) => e

def DynamicSemantics.ICDRT.Assignment.updateProp {W : Type u_1} {E : Type u_2} (g : Assignment W E) (p : PVar) (s : Set W) : Assignment W E

Update propositional variable: Function.update at the prop field.

Equations

• g.updateProp p s = { indiv := g.indiv, prop := Function.update g.prop p s }