inductive Semantics.Dynamic.Core.Entity (E : Type u_1) : Type u_1

Entities extended with the universal falsifier ⋆.

In Hofmann's system, individual drefs map to ⋆ in worlds where the referent doesn't exist. For example, in "There's no bathroom", the bathroom variable maps to ⋆ in all worlds.

The falsifier ⋆ satisfies: R(⋆) = false for all predicates R.

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

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

Equations

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

instance Semantics.Dynamic.Core.instDecidableEqEntity {E✝ : Type u_1} [DecidableEq E✝] : DecidableEq (Entity E✝)

Equations

• Semantics.Dynamic.Core.instDecidableEqEntity = Semantics.Dynamic.Core.instDecidableEqEntity.decEq

instance Semantics.Dynamic.Core.instReprEntity {E✝ : Type u_1} [Repr E✝] : Repr (Entity E✝)

Equations

• Semantics.Dynamic.Core.instReprEntity = { reprPrec := Semantics.Dynamic.Core.instReprEntity.repr }

def Semantics.Dynamic.Core.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.

def Semantics.Dynamic.Core.Entity.liftPred {E : Type u_1} (p : E → Bool) : Entity E → Bool

Lift a predicate to handle ⋆ (false for ⋆)

Equations

• Semantics.Dynamic.Core.Entity.liftPred p (Semantics.Dynamic.Core.Entity.some a) = p a
• Semantics.Dynamic.Core.Entity.liftPred p Semantics.Dynamic.Core.Entity.star = false

def Semantics.Dynamic.Core.Entity.liftPred₂ {E : Type u_1} (p : E → E → Bool) : Entity E → Entity E → Bool

Lift a binary predicate (false if either is ⋆)

Equations

• Semantics.Dynamic.Core.Entity.liftPred₂ p (Semantics.Dynamic.Core.Entity.some e₁) (Semantics.Dynamic.Core.Entity.some e₂) = p e₁ e₂
• Semantics.Dynamic.Core.Entity.liftPred₂ p x✝¹ x✝ = false

def Semantics.Dynamic.Core.Entity.inject {E : Type u_1} (e : E) : Entity E

Inject regular entity

Equations

• Semantics.Dynamic.Core.Entity.inject e = Semantics.Dynamic.Core.Entity.some e

def Semantics.Dynamic.Core.Entity.isSome {E : Type u_1} : Entity E → Bool

Is this a real entity (not ⋆)?

Equations

• (Semantics.Dynamic.Core.Entity.some a).isSome = true
• Semantics.Dynamic.Core.Entity.star.isSome = false

def Semantics.Dynamic.Core.Entity.toOption {E : Type u_1} : Entity E → Option E

Extract entity if present

Equations

• (Semantics.Dynamic.Core.Entity.some a).toOption = some a
• Semantics.Dynamic.Core.Entity.star.toOption = none

instance Semantics.Dynamic.Core.Entity.instInhabited {E : Type u_1} [Inhabited E] : Inhabited (Entity E)

Equations

• Semantics.Dynamic.Core.Entity.instInhabited = { default := Semantics.Dynamic.Core.Entity.star }

instance Semantics.Dynamic.Core.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 Semantics.Dynamic.Core.ConceptDRef (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A concept discourse referent value: a property annotated with a morphosyntactic count feature.

Introduced by the NP of an antecedent DP. For example, dog in John owns a dog introduces a concept dref anchored to the property λi.λx[dog(i)(x)] with feature [COUNT].

Kind anaphors pick up concept drefs and derive kind individuals via Chierchia's ∩ (down) operator:

• ⟦it⟧ = λP[MASS]. λi. ∩P(i)
• ⟦they⟧ = λP[COUNT]. λi. ∩(⊔P)(i)

The ⊔-closure for count nouns introduces pluralization, allowing for the number mismatch between a spider (singular) and they (plural). For mass nouns, ⊔-closure is vacuous (mass predicates are already cumulative), so the singular it is used.

• property : W → E → Bool

  The property this concept is anchored to: λi.λx[P(i)(x)]

• feature : MassCount

  Morphosyntactic count feature

inductive Semantics.Dynamic.Core.DRefVal (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Values that discourse referent indices can map to.

Standard dynamic semantics restricts assignments to map indices to entities. @cite{krifka-2026} §4 extends this: assignments are partial functions from ℕ to a heterogeneous universe including entities, concepts (properties with count features), and world-time indices.

• .entity e: an individual referent (standard entity dref)
• .concept c: a concept dref — the NP property with [MASS]/[COUNT]
• .index w: a world-time index dref
• .undef: index not in the domain (models assignment partiality)

Key property: concept drefs project past operators like negation, disjunction, and modals — they are introduced in the global assignment, not in local sub-assignments. This is what licenses kind anaphora out of anaphoric islands:

John doesn't own a dog. He is afraid of them.

The entity dref for a dog is trapped under negation, but the concept dref for 'dog' projects to the global context.

• entity {W : Type u_1} {E : Type u_2} : E → DRefVal W E
• concept {W : Type u_1} {E : Type u_2} : ConceptDRef W E → DRefVal W E
• index {W : Type u_1} {E : Type u_2} : W → DRefVal W E
• undef {W : Type u_1} {E : Type u_2} : DRefVal W E

def Semantics.Dynamic.Core.DRefVal.getEntity {W : Type u_1} {E : Type u_2} : DRefVal W E → Option E

Extract entity value, if present.

Equations

• (Semantics.Dynamic.Core.DRefVal.entity e).getEntity = some e
• x✝.getEntity = none

def Semantics.Dynamic.Core.DRefVal.getConcept {W : Type u_1} {E : Type u_2} : DRefVal W E → Option (ConceptDRef W E)

Extract concept dref, if present.

Equations

• (Semantics.Dynamic.Core.DRefVal.concept c).getConcept = some c
• x✝.getConcept = none

def Semantics.Dynamic.Core.DRefVal.getIndex {W : Type u_1} {E : Type u_2} : DRefVal W E → Option W

Extract world-time index, if present.

Equations

• (Semantics.Dynamic.Core.DRefVal.index w).getIndex = some w
• x✝.getIndex = none

def Semantics.Dynamic.Core.DRefVal.isDefined {W : Type u_1} {E : Type u_2} : DRefVal W E → Bool

Is this index in the domain of the assignment?

Equations

• Semantics.Dynamic.Core.DRefVal.undef.isDefined = false
• x✝.isDefined = true

def Semantics.Dynamic.Core.DRefVal.liftEntityPred {W : Type u_1} {E : Type u_2} (p : E → Bool) : DRefVal W E → Bool

Lift a predicate on entities to DRefVal (false for non-entities).

Equations

• Semantics.Dynamic.Core.DRefVal.liftEntityPred p (Semantics.Dynamic.Core.DRefVal.entity e) = p e
• Semantics.Dynamic.Core.DRefVal.liftEntityPred p x✝ = false

def Semantics.Dynamic.Core.DRefVal.liftConceptPred {W : Type u_1} {E : Type u_2} (p : ConceptDRef W E → Bool) : DRefVal W E → Bool

Lift a predicate on concepts to DRefVal (false for non-concepts).

Equations

• Semantics.Dynamic.Core.DRefVal.liftConceptPred p (Semantics.Dynamic.Core.DRefVal.concept c) = p c
• Semantics.Dynamic.Core.DRefVal.liftConceptPred p x✝ = false

@[reducible, inline]

abbrev Semantics.Dynamic.Core.Var : Type

Variable indices for discourse referents.

We use natural numbers but provide type wrappers for clarity.

Equations

• Semantics.Dynamic.Core.Var = ℕ

structure Semantics.Dynamic.Core.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 : ℕ

def Semantics.Dynamic.Core.instDecidableEqPVar.decEq (x✝ x✝¹ : PVar) : Decidable (x✝ = x✝¹)

Equations

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

instance Semantics.Dynamic.Core.instDecidableEqPVar : DecidableEq PVar

Equations

• Semantics.Dynamic.Core.instDecidableEqPVar = Semantics.Dynamic.Core.instDecidableEqPVar.decEq

def Semantics.Dynamic.Core.instBEqPVar.beq : PVar → PVar → Bool

Equations

• Semantics.Dynamic.Core.instBEqPVar.beq { idx := a } { idx := b } = (a == b)
• Semantics.Dynamic.Core.instBEqPVar.beq x✝¹ x✝ = false

instance Semantics.Dynamic.Core.instBEqPVar : BEq PVar

Equations

• Semantics.Dynamic.Core.instBEqPVar = { beq := Semantics.Dynamic.Core.instBEqPVar.beq }

def Semantics.Dynamic.Core.instReprPVar.repr : PVar → ℕ → Std.Format

Equations

• Semantics.Dynamic.Core.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) " }"

instance Semantics.Dynamic.Core.instReprPVar : Repr PVar

Equations

• Semantics.Dynamic.Core.instReprPVar = { reprPrec := Semantics.Dynamic.Core.instReprPVar.repr }

def Semantics.Dynamic.Core.instHashablePVar.hash : PVar → UInt64

Equations

• Semantics.Dynamic.Core.instHashablePVar.hash { idx := a } = mixHash 0 (hash a)

instance Semantics.Dynamic.Core.instHashablePVar : Hashable PVar

Equations

• Semantics.Dynamic.Core.instHashablePVar = { hash := Semantics.Dynamic.Core.instHashablePVar.hash }

structure Semantics.Dynamic.Core.IVar : Type

An individual variable (names an individual dref).

• idx : ℕ

instance Semantics.Dynamic.Core.instDecidableEqIVar : DecidableEq IVar

Equations

• Semantics.Dynamic.Core.instDecidableEqIVar = Semantics.Dynamic.Core.instDecidableEqIVar.decEq

def Semantics.Dynamic.Core.instDecidableEqIVar.decEq (x✝ x✝¹ : IVar) : Decidable (x✝ = x✝¹)

Equations

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

def Semantics.Dynamic.Core.instBEqIVar.beq : IVar → IVar → Bool

Equations

• Semantics.Dynamic.Core.instBEqIVar.beq { idx := a } { idx := b } = (a == b)
• Semantics.Dynamic.Core.instBEqIVar.beq x✝¹ x✝ = false

instance Semantics.Dynamic.Core.instBEqIVar : BEq IVar

Equations

• Semantics.Dynamic.Core.instBEqIVar = { beq := Semantics.Dynamic.Core.instBEqIVar.beq }

instance Semantics.Dynamic.Core.instReprIVar : Repr IVar

Equations

• Semantics.Dynamic.Core.instReprIVar = { reprPrec := Semantics.Dynamic.Core.instReprIVar.repr }

def Semantics.Dynamic.Core.instReprIVar.repr : IVar → ℕ → Std.Format

Equations

• Semantics.Dynamic.Core.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) " }"

def Semantics.Dynamic.Core.instHashableIVar.hash : IVar → UInt64

Equations

• Semantics.Dynamic.Core.instHashableIVar.hash { idx := a } = mixHash 0 (hash a)

instance Semantics.Dynamic.Core.instHashableIVar : Hashable IVar

Equations

• Semantics.Dynamic.Core.instHashableIVar = { hash := Semantics.Dynamic.Core.instHashableIVar.hash }

structure Semantics.Dynamic.Core.CVar : Type

A concept variable (names a concept dref).

Concept variables are indices into the assignment that map to ConceptDRef values — properties annotated with [MASS]/[COUNT].

• idx : ℕ

def Semantics.Dynamic.Core.instDecidableEqCVar.decEq (x✝ x✝¹ : CVar) : Decidable (x✝ = x✝¹)

Equations

• Semantics.Dynamic.Core.instDecidableEqCVar.decEq { idx := a } { idx := b } = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯

instance Semantics.Dynamic.Core.instDecidableEqCVar : DecidableEq CVar

Equations

• Semantics.Dynamic.Core.instDecidableEqCVar = Semantics.Dynamic.Core.instDecidableEqCVar.decEq

def Semantics.Dynamic.Core.instBEqCVar.beq : CVar → CVar → Bool

Equations

• Semantics.Dynamic.Core.instBEqCVar.beq { idx := a } { idx := b } = (a == b)
• Semantics.Dynamic.Core.instBEqCVar.beq x✝¹ x✝ = false

instance Semantics.Dynamic.Core.instBEqCVar : BEq CVar

Equations

• Semantics.Dynamic.Core.instBEqCVar = { beq := Semantics.Dynamic.Core.instBEqCVar.beq }

instance Semantics.Dynamic.Core.instReprCVar : Repr CVar

Equations

• Semantics.Dynamic.Core.instReprCVar = { reprPrec := Semantics.Dynamic.Core.instReprCVar.repr }

def Semantics.Dynamic.Core.instReprCVar.repr : CVar → ℕ → Std.Format

Equations

• Semantics.Dynamic.Core.instReprCVar.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 Semantics.Dynamic.Core.instHashableCVar.hash : CVar → UInt64

Equations

• Semantics.Dynamic.Core.instHashableCVar.hash { idx := a } = mixHash 0 (hash a)

instance Semantics.Dynamic.Core.instHashableCVar : Hashable CVar

Equations

• Semantics.Dynamic.Core.instHashableCVar = { hash := Semantics.Dynamic.Core.instHashableCVar.hash }

structure Semantics.Dynamic.Core.ICDRTAssignment (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 IntensionalCDRT; simpler theories can use Nat → E.

• indiv : IVar → Entity E

  Individual variable assignment

• prop : PVar → Set W

  Propositional variable assignment

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

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

Equations

• Semantics.Dynamic.Core.ICDRTAssignment.empty = { indiv := fun (x : Semantics.Dynamic.Core.IVar) => Semantics.Dynamic.Core.Entity.star, prop := fun (x : Semantics.Dynamic.Core.PVar) => ∅ }

def Semantics.Dynamic.Core.ICDRTAssignment.updateIndiv {W : Type u_1} {E : Type u_2} (g : ICDRTAssignment W E) (v : IVar) (e : Entity E) : ICDRTAssignment W E

Update individual variable

Equations

• g.updateIndiv v e = { indiv := fun (v' : Semantics.Dynamic.Core.IVar) => if (v' == v) = true then e else g.indiv v', prop := g.prop }

def Semantics.Dynamic.Core.ICDRTAssignment.updateProp {W : Type u_1} {E : Type u_2} (g : ICDRTAssignment W E) (p : PVar) (s : Set W) : ICDRTAssignment W E

Update propositional variable

Equations

• g.updateProp p s = { indiv := g.indiv, prop := fun (p' : Semantics.Dynamic.Core.PVar) => if (p' == p) = true then s else g.prop p' }

def Semantics.Dynamic.Core.PDref (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

A propositional discourse referent: s(wt) in Hofmann's notation.

Maps each assignment to a set of worlds (the "local context" where the associated individual dref has a referent).

In Hofmann's notation: type s(wt) = s → wt = assignment → (world → truth)

For simpler dynamic theories that don't distinguish propositional drefs, this can be instantiated with a trivial assignment type.

Equations

• Semantics.Dynamic.Core.PDref W E = (Semantics.Dynamic.Core.ICDRTAssignment W E → Set W)

def Semantics.Dynamic.Core.SimplePDref (W : Type u_1) : Type u_1

Simpler propositional dref without assignment dependence.

Equations

• Semantics.Dynamic.Core.SimplePDref W = Set W

def Semantics.Dynamic.Core.PDref.top {W : Type u_1} {E : Type u_2} : PDref W E

The tautological propositional dref (all worlds)

Equations

• Semantics.Dynamic.Core.PDref.top x✝ = Set.univ

def Semantics.Dynamic.Core.PDref.bot {W : Type u_1} {E : Type u_2} : PDref W E

The contradictory propositional dref (no worlds)

Equations

• Semantics.Dynamic.Core.PDref.bot x✝ = ∅

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

Propositional dref from a classical proposition

Equations

• Semantics.Dynamic.Core.PDref.ofProp p x✝ = {w : W | p w}

def Semantics.Dynamic.Core.PDref.inter {W : Type u_1} {E : Type u_2} (φ ψ : PDref W E) : PDref W E

Intersection of propositional drefs

Equations

• φ.inter ψ g = φ g ∩ ψ g

def Semantics.Dynamic.Core.PDref.union {W : Type u_1} {E : Type u_2} (φ ψ : PDref W E) : PDref W E

Union of propositional drefs

Equations

• φ.union ψ g = φ g ∪ ψ g

def Semantics.Dynamic.Core.IDref (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

An individual discourse referent: s(we) in Hofmann's notation.

Maps each assignment and world to an entity (possibly ⋆).

In Hofmann's notation: type s(we) = s → we = assignment → world → entity

Equations

• Semantics.Dynamic.Core.IDref W E = (Semantics.Dynamic.Core.ICDRTAssignment W E → W → Semantics.Dynamic.Core.Entity E)

def Semantics.Dynamic.Core.SimpleIDref (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Simpler individual dref using Nat → E assignments (for standard dynamic semantics).

Equations

• Semantics.Dynamic.Core.SimpleIDref W E = ((ℕ → E) → W → E)

def Semantics.Dynamic.Core.IDref.const {W : Type u_1} {E : Type u_2} (e : Entity E) : IDref W E

Constant individual dref (same entity in all contexts)

Equations

• Semantics.Dynamic.Core.IDref.const e x✝¹ x✝ = e

def Semantics.Dynamic.Core.IDref.undef {W : Type u_1} {E : Type u_2} : IDref W E

The undefined individual dref (always ⋆)

Equations

• Semantics.Dynamic.Core.IDref.undef x✝¹ x✝ = Semantics.Dynamic.Core.Entity.star

def Semantics.Dynamic.Core.IDref.ofVar {W : Type u_1} {E : Type u_2} (v : IVar) : IDref W E

Variable lookup dref

Equations

• Semantics.Dynamic.Core.IDref.ofVar v g x✝ = g.indiv v

def Semantics.Dynamic.Core.IDref.satisfies {W : Type u_1} {E : Type u_2} (d : IDref W E) (p : E → W → Bool) : ICDRTAssignment W E → W → Bool

Apply predicate to individual dref

Equations

• d.satisfies p g w = Semantics.Dynamic.Core.Entity.liftPred (fun (e : E) => p e w) (d g w)

@[reducible, inline]

abbrev Semantics.Dynamic.Core.LocalContext (W : Type u_1) (E : Type u_2) : Type (max u_2 u_1)

A local context is a propositional dref that tracks WHERE an individual dref was introduced.

In "Either there's no bathroom, or it's upstairs", the bathroom is introduced in the local context of the first disjunct. The propositional dref p_bathroom tracks: "worlds where there is a bathroom" (the local context of the positive update).

Equations

• Semantics.Dynamic.Core.LocalContext W E = Semantics.Dynamic.Core.PDref W E

def Semantics.Dynamic.Core.dynamicPredication {W : Type u_1} {E : Type u_2} (R : E → W → Prop) (φ : LocalContext W E) (v : IDref W E) : ICDRTAssignment W E → W → Prop

Dynamic predication relative to a local context.

R_φ(v) is true iff R(v) holds in all worlds of the local context φ.

In Hofmann's system: ⟦R_φ(v)⟧^g,w = 1 iff ∀w' ∈ φ^g: R(v^g(w'))

This ensures anaphora is only felicitous when the referent exists throughout the relevant local context.

Equations

• Semantics.Dynamic.Core.dynamicPredication R φ v g x✝ = ∀ w' ∈ φ g, match v g w' with | Semantics.Dynamic.Core.Entity.some e => R e w' | Semantics.Dynamic.Core.Entity.star => False

def Semantics.Dynamic.Core.entityDomain {W : Type u_1} {E : Type u_2} (p : Set W) (dref : W → Entity E) : Set E

The entity domain in a local context.

DOM_e(p) = { e | e is defined throughout p }

For individual drefs that map to ⋆ in some worlds of p, those drefs are not in the entity domain of p.

Equations

• Semantics.Dynamic.Core.entityDomain p dref = {e : E | ∀ w ∈ p, dref w = Semantics.Dynamic.Core.Entity.some e}

def Semantics.Dynamic.Core.accessibleIn {W : Type u_1} {E : Type u_2} (e : E) (p : Set W) (dref : W → Entity E) : Prop

An entity is accessible in a local context if it exists throughout.

Equations

• Semantics.Dynamic.Core.accessibleIn e p dref = ∀ w ∈ p, dref w = Semantics.Dynamic.Core.Entity.some e