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

Relative variable update: i[φ : v]j

Given propositional dref φ (the local context) and individual variable v, assignment j is a "φ-v extension" of assignment i iff:

1. j agrees with i on all propositional variables
2. j agrees with i on all individual variables except possibly v
3. j(v) is some entity e such that e exists in all worlds of φ^j

In Hofmann's notation (Definition 1, p.11): i[φ : v]j iff ∃e: j = i[v ↦ e] and j(v) ∈ DOM_e(φ^j) where DOM_e(p) = { e | ∀w ∈ p: e ≠ ⋆ }

Note: j(v) must be a real entity (not ⋆) that exists throughout φ^j.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.«term_[_:_]_» : Lean.TrailingParserDescr

Equations

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

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

Alternative formulation: 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.IntensionalCDRT.entityDomain p dref = {e : E | ∀ w ∈ p, dref w = Semantics.Dynamic.Core.Entity.some e}

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

Relative variable update with existential witness made explicit.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.flatExists {W : Type u_1} {E : Type u_2} (p : Core.PVar) (v : Core.IVar) (body : IContext W E → IContext W E) (c : IContext W E) : IContext W E

Flat existential update: ∃v.φ

The existential introduces v globally, but the propositional dref tracks the local context.

In Hofmann's system: ⟦∃v.φ⟧^+ c = { (j, w) | ∃i: (i,w) ∈ c and i[p:v]j and (j,w) ∈ ⟦φ⟧^+ }

where p is a fresh propositional variable that will track the local context where v has a referent.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.flatExistsExplicit {W : Type u_1} {E : Type u_2} (p : Core.PVar) (v : Core.IVar) (localCtx : Core.ICDRTAssignment W E → Set W) (body : IContext W E → IContext W E) (c : IContext W E) : IContext W E

Flat existential with explicit entity quantification.

This version makes clear that we quantify over entities e, extend the assignment, and track the local context.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.extendContext {W : Type u_1} {E : Type u_2} (c : IContext W E) (v : Core.IVar) (domain : Set E) : IContext W E

Extend context with random assignment for variable v.

Unlike standard randomAssign, this:

1. Only assigns real entities (not ⋆)
2. Tracks assignments in all worlds (flat)

Equations

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

def Semantics.Dynamic.IntensionalCDRT.extendContextWithLocal {W : Type u_1} {E : Type u_2} (c : IContext W E) (v : Core.IVar) (p : Core.PVar) (domain : Set E) (localCtx : Set W) : IContext W E

Extend context and track local context in propositional variable.

Equations

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

def Semantics.Dynamic.IntensionalCDRT.updateWithProposition {W : Type u_1} {E : Type u_2} (c : IContext W E) (prop : W → Prop) : IContext W E × Set W

Update context with proposition, yielding local context.

The local context is the set of worlds where the proposition holds.

Equations

• Semantics.Dynamic.IntensionalCDRT.updateWithProposition c prop = (c⟦prop⟧, {w : W | ∃ (g : Semantics.Dynamic.Core.ICDRTAssignment W E), (g, w) ∈ c⟦prop⟧})

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

Update relative to a propositional dref (local context).

⟦φ⟧_p evaluates φ in the local context p, not the global context.

Equations

• Semantics.Dynamic.IntensionalCDRT.updateInLocalContext c p prop = {gw : Semantics.Dynamic.Core.ICDRTAssignment W E × W | gw ∈ c ∧ ∀ w' ∈ gw.1⟦p⟧ₚ, prop gw.1 w'}

def Semantics.Dynamic.IntensionalCDRT.initPropDref {W : Type u_1} {E : Type u_2} (c : IContext W E) (p : Core.PVar) (g : Core.ICDRTAssignment W E) : Set W

Initialize propositional dref to the current context's worlds.

When introducing an existential, the propositional dref is set to the current local context (worlds where the indefinite is introduced).

Equations

• Semantics.Dynamic.IntensionalCDRT.initPropDref c p g = {w : W | (g, w) ∈ c}

def Semantics.Dynamic.IntensionalCDRT.narrowPropDref {W : Type u_1} {E : Type u_2} (g : Core.ICDRTAssignment W E) (p : Core.PVar) (prop : W → Prop) : Core.ICDRTAssignment W E

Narrow propositional dref after update.

When updating with a proposition, propositional drefs that track local contexts should be narrowed accordingly.

Equations

• Semantics.Dynamic.IntensionalCDRT.narrowPropDref g p prop = g.updateProp p {w : W | w ∈ g⟦p⟧ₚ ∧ prop w}

structure Semantics.Dynamic.IntensionalCDRT.BilateralICDRT (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Bilateral ICDRT denotation: positive and negative updates.

Following Hofmann's bilateral approach (building on Elliott & Sudo):

• Positive update: what survives assertion
• Negative update: what survives denial

The key property: negation swaps positive and negative.

• positive : IContext W E → IContext W E

  Positive update (assertion)

• negative : IContext W E → IContext W E

  Negative update (denial)

def Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.neg {W : Type u_1} {E : Type u_2} (φ : BilateralICDRT W E) : BilateralICDRT W E

Negation: swap positive and negative

Equations

• ∼φ = { positive := φ.negative, negative := φ.positive }

@[simp]

theorem Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.neg_neg {W : Type u_1} {E : Type u_2} (φ : BilateralICDRT W E) : ∼∼φ = φ

Double negation elimination (definitional).

def Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.atom {W : Type u_1} {E : Type u_2} (prop : W → Prop) : BilateralICDRT W E

Atomic proposition

Equations

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

def Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.conj {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) : BilateralICDRT W E

Conjunction: sequence positive updates

Equations

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

def Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.«term∼_» : Lean.ParserDescr

Notation

Equations

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

def Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.«term_⊗_» : Lean.TrailingParserDescr

Equations

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

def Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.exists_ {W : Type u_1} {E : Type u_2} (p : Core.PVar) (v : Core.IVar) (domain : Set E) (body : BilateralICDRT W E) : BilateralICDRT W E

Flat existential with bilateral structure.

The existential introduces drefs in both positive and negative updates. This is what makes double negation accessible:

⟦¬¬∃x.P(x)⟧^+ = ⟦∃x.P(x)⟧^+ (by DNE)

The dref x introduced in the inner scope is accessible in the outer scope because flat update introduces it globally.

Equations

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