Intensional CDRT

Muskens's compositional DRT with intensional discourse referents. An individual dref is an individual concept, a function from worlds to individuals or the universal falsifier ⋆ (type s(we)); a propositional dref is a set of worlds (type s(wt)) and stores the local context of some embedded content. This is the flat update of Stone and Brasoveanu in Hofmann's formulation: a discourse state is a single assignment, updated relationally, and an individual dref has a referent only at the worlds of its local context.

A state has two sorts of registers, IVar and PVar, each with its RegisterStructure, so the variable update [δ] is CDRT's Update.randomAssign at either sort and a DRS [δ | C] is Update.box {δ} C. Over these sit the relative variable update [φ : υ], after which υ has a referent at exactly the φ-worlds, predication relative to a local context, local entailment, and maximization over a propositional dref, CDRT's Update.maxAt.

Main definitions

• ICDRT.State: individual concepts for IVars and propositions for PVars.
• ICDRT.relUpdate: relative variable update [φ : υ].
• ICDRT.pred: predication R_φ(υ) relative to a local context.
• ICDRT.incl, ICDRT.eqCompl: the conditions φ₁ ⋐ φ₂ and φ₁ ≡ φ̄₂.
• ICDRT.localEntailment: υ has a referent throughout φ.

Main results

• ICDRT.mem_randomAssign_indiv, ICDRT.mem_randomAssign_prop: a variable update changes one register of one sort and nothing else.
• ICDRT.mem_localEntailment_of_mem_pred: predication entails local entailment, since ⋆ satisfies no relation.
• ICDRT.mem_localEntailment_iff_of_relUpdate: after [φ : υ], υ is entailed in a local context exactly when that context lies within φ.
• ICDRT.mem_maxAt_prop: CDRT's maxAt at a propositional dref is maximization max_φ.

Implementation notes

⋆ is none. The typed drefs are two register sorts rather than one register carrier, since a RegisterStructure has one value type. The relative variable update is Hofmann's biconditional form; Stone's has only the implication from φ-worlds to referents.

References

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

structure ICDRT.PVar : Type

A propositional variable, the name of a propositional dref.

• idx : ℕ

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

Equations

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

@[instance_reducible]

instance ICDRT.instDecidableEqPVar : DecidableEq PVar

Equations

• ICDRT.instDecidableEqPVar = ICDRT.instDecidableEqPVar.decEq

@[instance_reducible]

instance ICDRT.instReprPVar : Repr PVar

Equations

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

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

Equations

• 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) " }"

structure ICDRT.IVar : Type

An individual variable, the name of an individual dref.

• idx : ℕ

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

Equations

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

@[instance_reducible]

instance ICDRT.instDecidableEqIVar : DecidableEq IVar

Equations

• ICDRT.instDecidableEqIVar = ICDRT.instDecidableEqIVar.decEq

@[instance_reducible]

instance ICDRT.instReprIVar : Repr IVar

Equations

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

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

Equations

• 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) " }"

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

A discourse state assigns an individual concept to each individual dref and a proposition to each propositional dref. An individual dref is none, the falsifier ⋆, at the worlds where it has no referent.

• indiv : IVar → W → Option E
• prop : PVar → Set W

theorem ICDRT.State.ext_iff {W : Type u_1} {E : Type u_2} {x y : State W E} : x = y ↔ x.indiv = y.indiv ∧ x.prop = y.prop

theorem ICDRT.State.ext {W : Type u_1} {E : Type u_2} {x y : State W E} (indiv : x.indiv = y.indiv) (prop : x.prop = y.prop) : x = y

def ICDRT.State.updateIndiv {W : Type u_1} {E : Type u_2} (g : State W E) (v : IVar) (e : W → Option E) : State W E

Reassign an individual dref.

Equations

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

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

Reassign a propositional dref.

Equations

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

@[simp]

theorem ICDRT.State.updateProp_prop_self {W : Type u_1} {E : Type u_2} (g : State W E) (p : PVar) (s : Set W) : (g.updateProp p s).prop p = s

@[simp]

theorem ICDRT.State.updateProp_prop_of_ne {W : Type u_1} {E : Type u_2} (g : State W E) {p q : PVar} (h : q ≠ p) (s : Set W) : (g.updateProp p s).prop q = g.prop q

@[simp]

theorem ICDRT.State.updateProp_indiv {W : Type u_1} {E : Type u_2} (g : State W E) (p : PVar) (s : Set W) : (g.updateProp p s).indiv = g.indiv

@[simp]

theorem ICDRT.State.updateIndiv_prop {W : Type u_1} {E : Type u_2} (g : State W E) (v : IVar) (e : W → Option E) : (g.updateIndiv v e).prop = g.prop

@[simp]

theorem ICDRT.State.updateIndiv_indiv_self {W : Type u_1} {E : Type u_2} (g : State W E) (v : IVar) (e : W → Option E) : (g.updateIndiv v e).indiv v = e

@[simp]

theorem ICDRT.State.updateIndiv_indiv_of_ne {W : Type u_1} {E : Type u_2} (g : State W E) {v u : IVar} (h : u ≠ v) (e : W → Option E) : (g.updateIndiv v e).indiv u = g.indiv u

Registers and variable update

@[instance_reducible]

instance ICDRT.instRegisterStructureIVarStateForallOption {W : Type u_1} {E : Type u_2} : DynamicSemantics.RegisterStructure IVar (State W E) (W → Option E)

Individual drefs are registers holding individual concepts.

Equations

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

@[instance_reducible]

instance ICDRT.instRegisterStructurePVarStateSet {W : Type u_1} {E : Type u_2} : DynamicSemantics.RegisterStructure PVar (State W E) (Set W)

Propositional drefs are registers holding propositions.

Equations

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

@[simp]

theorem ICDRT.val_ivar {W : Type u_1} {E : Type u_2} (i : State W E) (v : IVar) : DynamicSemantics.RegisterStructure.val v i = i.indiv v

@[simp]

theorem ICDRT.val_pvar {W : Type u_1} {E : Type u_2} (i : State W E) (p : PVar) : DynamicSemantics.RegisterStructure.val p i = i.prop p

theorem ICDRT.updateIndiv_mem_randomAssign {W : Type u_1} {E : Type u_2} (i : State W E) (v : IVar) (e : W → Option E) : (i, i.updateIndiv v e) ∈ DynamicSemantics.Update.randomAssign v

theorem ICDRT.updateProp_mem_randomAssign {W : Type u_1} {E : Type u_2} (i : State W E) (p : PVar) (s : Set W) : (i, i.updateProp p s) ∈ DynamicSemantics.Update.randomAssign p

theorem ICDRT.mem_randomAssign_indiv {W : Type u_1} {E : Type u_2} {i j : State W E} {v : IVar} : (i, j) ∈ DynamicSemantics.Update.randomAssign v ↔ (∀ (p : PVar), j.prop p = i.prop p) ∧ ∀ (u : IVar), u ≠ v → j.indiv u = i.indiv u

The update [υ] relates i to the states j that differ from it at most in the value of υ ([Hof25] App. B (9a)).

theorem ICDRT.mem_randomAssign_prop {W : Type u_1} {E : Type u_2} {i j : State W E} {φ : PVar} : (i, j) ∈ DynamicSemantics.Update.randomAssign φ ↔ (∀ (q : PVar), q ≠ φ → j.prop q = i.prop q) ∧ ∀ (u : IVar), j.indiv u = i.indiv u

The update [φ] relates i to the states j that differ from it at most in the value of φ ([Hof25] App. B (9a)).

theorem DynamicSemantics.Update.Fixes.prop_eq {W : Type u_1} {E : Type u_2} {i j : ICDRT.State W E} {φ : ICDRT.PVar} {D : Update (ICDRT.State W E)} (h : Fixes φ D) (hD : (i, j) ∈ D) : j.prop φ = i.prop φ

A fixed propositional dref keeps its value across the update.

theorem ICDRT.updateProp_mem_box {W : Type u_1} {E : Type u_2} {i : State W E} {C : DynamicSemantics.Condition (State W E)} (p : PVar) (s : Set W) (h : i.updateProp p s ∈ C) : (i, i.updateProp p s) ∈ DynamicSemantics.Update.box {p} C

Introducing p with the value s runs the DRS [p | C] when the result satisfies C.

theorem ICDRT.fixes_randomAssign_ivar {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) : DynamicSemantics.Update.Fixes φ (DynamicSemantics.Update.randomAssign v)

An individual variable update fixes every propositional dref.

theorem ICDRT.mem_maxAt_prop {W : Type u_1} {E : Type u_2} {i j : State W E} {φ : PVar} {D : DynamicSemantics.Update (State W E)} : (i, j) ∈ DynamicSemantics.Update.maxAt φ D ↔ (i, j) ∈ D ∧ ∀ (k : State W E), (i, k) ∈ D → ¬j.prop φ ⊂ k.prop φ

Maximization max_φ(D) over a propositional dref ([Hof25] (40)) is CDRT's maxAt, keeping the outputs of D at which no other output gives φ a proper superset.

Relative variable update

def ICDRT.relUpdate {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) : DynamicSemantics.Update (State W E)

The relative variable update [φ : υ] ([Hof25] (25), App. B (9b)) updates υ so that it has a referent at all and only the φ-worlds.

Equations

• ICDRT.relUpdate φ v = DynamicSemantics.Update.box {v} {j : ICDRT.State W E | ∀ (w : W), w ∈ j.prop φ ↔ j.indiv v w ≠ none}

theorem ICDRT.mem_relUpdate {W : Type u_1} {E : Type u_2} {i j : State W E} {v : IVar} {φ : PVar} : (i, j) ∈ relUpdate φ v ↔ (i, j) ∈ DynamicSemantics.Update.randomAssign v ∧ ∀ (w : W), w ∈ j.prop φ ↔ j.indiv v w ≠ none

theorem ICDRT.updateIndiv_mem_relUpdate {W : Type u_1} {E : Type u_2} {i : State W E} {v : IVar} {φ : PVar} (e : W → Option E) (h : ∀ (w : W), w ∈ i.prop φ ↔ e w ≠ none) : (i, i.updateIndiv v e) ∈ relUpdate φ v

Introducing υ as the concept e is a relative update [φ : υ] when e has a referent at exactly the φ-worlds.

theorem ICDRT.fixes_relUpdate {W : Type u_1} {E : Type u_2} (ψ φ : PVar) (v : IVar) : DynamicSemantics.Update.Fixes ψ (relUpdate φ v)

Conditions

def ICDRT.pred {W : Type u_1} {E : Type u_2} (R : E → W → Prop) (φ : PVar) (v : IVar) : DynamicSemantics.Condition (State W E)

Predication R_φ(υ) ([Hof25] (27), App. B (7a)) holds if R holds of υ's referent at every world of the local context φ; ⋆ satisfies no relation.

Equations

• ICDRT.pred R φ v = {i : ICDRT.State W E | ∀ w ∈ i.prop φ, match i.indiv v w with | some e => R e w | none => False}

def ICDRT.incl {W : Type u_1} {E : Type u_2} (φ₁ φ₂ : PVar) : DynamicSemantics.Condition (State W E)

Inclusion φ₁ ⋐ φ₂ (App. B (7c)).

Equations

• ICDRT.incl φ₁ φ₂ = {i : ICDRT.State W E | i.prop φ₁ ⊆ i.prop φ₂}

def ICDRT.eqCompl {W : Type u_1} {E : Type u_2} (φ₁ φ₂ : PVar) : DynamicSemantics.Condition (State W E)

φ₁ ≡ φ̄₂ (App. B (7b), (8a)), the condition negation places on its context.

Equations

• ICDRT.eqCompl φ₁ φ₂ = {i : ICDRT.State W E | i.prop φ₁ = (i.prop φ₂)ᶜ}

def ICDRT.localEntailment {W : Type u_1} {E : Type u_2} (φ : PVar) (v : IVar) : DynamicSemantics.Condition (State W E)

A dref υ is entailed in the local context φ ([Hof25] (28)) if it has a referent at every φ-world.

Equations

• ICDRT.localEntailment φ v = {i : ICDRT.State W E | ∀ w ∈ i.prop φ, i.indiv v w ≠ none}

theorem ICDRT.not_mem_pred_of_eq_none {W : Type u_1} {E : Type u_2} {i : State W E} {v : IVar} {φ : PVar} {R : E → W → Prop} {w : W} (hw : w ∈ i.prop φ) (h : i.indiv v w = none) : i ∉ pred R φ v

⋆ falsifies predication ((29a)).

theorem ICDRT.mem_localEntailment_of_mem_pred {W : Type u_1} {E : Type u_2} {i : State W E} {v : IVar} {φ : PVar} {R : E → W → Prop} (h : i ∈ pred R φ v) : i ∈ localEntailment φ v

Predication entails local entailment ((29b)), since a referent satisfying R is not ⋆.

theorem ICDRT.mem_localEntailment_iff_of_relUpdate {W : Type u_1} {E : Type u_2} {i j : State W E} {v : IVar} {φ ψ : PVar} (h : (i, j) ∈ relUpdate φ v) : j ∈ localEntailment ψ v ↔ j.prop ψ ⊆ j.prop φ

After [φ : υ], υ is entailed in a local context exactly when the context lies within φ, the subset requirement of [Hof25] (39).