Bilateral Denotations for ICDRT Contexts

Bilateral (positive/negative) update semantics instantiated for ICDRT contexts (@cite{krahmer-muskens-1995}). This captures the DN-DRT / BUS mechanism applied to ICDRT's IContext type.

This bilateral structure is NOT the same as @cite{hofmann-2025}'s full ICDRT analysis, which derives accessibility from veridicality + discourse consistency rather than bilateral negation (§5.1.1). The bilateral approach cannot handle disagreement or modal subordination contexts.

Cross-cutting smell: two competing approaches to cross-disjunct anaphora

This file and Phenomena/Anaphora/Studies/Hofmann2025.lean are two formalizations of the same empirical territory — cross-negation and cross-disjunct anaphora (the "bathroom sentence" pattern: Either there's no bathroom, or it's upstairs). They are not stacked extensions; they are competitors.

Approach	Mechanism	Solves	Doesn't solve
Bilateral (this file)	Two update channels; negation = swap	DNE, bathroom sentence	Disagreement, modal subordination, speaker-vs-hearer commitment
Full ICDRT (@cite{hofmann-2025})	Propositional drefs + per-speaker DiscContext + veridicality classification	All of the above + three-way veridical/hypothetical/counterfactual	Pays in intensional machinery

The bilateral approach is the lighter formalism — a single information state with two update polarities. The full ICDRT machinery (per-speaker commitment sets, three-way veridicality) is heavier but covers cases the bilateral approach structurally cannot. Choose by phenomenon: if disagreement or modal subordination are in scope, use the full ICDRT; if only the basic bathroom pattern matters, the bilateral apparatus here suffices.

The empirical comparison is formalized in Phenomena/Anaphora/Studies/Hofmann2025.lean §7, which proves both approaches solve the bathroom sentence and identifies the four cases (disagreement, modal subordination, three-way veridicality classification, negated existential truth conditions) where ICDRT is strictly more expressive.

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

Bilateral ICDRT denotation: positive and negative updates.

Following @cite{krahmer-muskens-1995}'s bilateral negation: formulas have both positive and negative interpretations, and negation swaps them. This gives double negation elimination (DNE), which Hofmann uses but does not require — ICDRT's flat update with propositional drefs handles double negation via complementation over propositional drefs (§4.1).

Note: this bilateral structure captures the DN-DRT / BUS mechanism (§5.1.1) but NOT the full ICDRT analysis. ICDRT derives accessibility from veridicality + discourse consistency, which covers cases (modal subordination, disagreement) that bilateral accounts cannot (§5.1.1).

• positive : Core.IContext W E → Core.IContext W E

  Positive update (assertion)

• negative : Core.IContext W E → Core.IContext W E

  Negative update (denial)

def Semantics.Dynamic.Bilateral.ICDRT.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.Bilateral.ICDRT.BilateralICDRT.neg_neg {W : Type u_1} {E : Type u_2} (φ : BilateralICDRT W E) : ∼∼φ = φ

Double negation elimination (definitional).

theorem Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.isBilateral {W : Type u_1} {E : Type u_2} : Core.Logic.Bilateral.IsBilateral (fun (x : BilateralICDRT W E) => x.positive) (fun (x : BilateralICDRT W E) => x.negative) neg

ICDRT-bilateral is a paraconsistent bilateral logic (Core.Logic.Bilateral.IsBilateral). The BilateralICDRT value IS the formula; positive and negative are field projections; neg swaps them by definition. Both axioms reduce to rfl.

def Semantics.Dynamic.Bilateral.ICDRT.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.Bilateral.ICDRT.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.Bilateral.ICDRT.BilateralICDRT.«term∼_» : Lean.ParserDescr

Notation

Equations

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

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

Equations

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

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

Extend context with random assignment for variable v.

Only assigns real entities (not ⋆), tracking assignments in all worlds (flat).

Equations

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

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

Bilateral existential with flat update.

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.

theorem Semantics.Dynamic.Bilateral.ICDRT.extendContext_mem {W : Type u_1} {E : Type u_2} (c : Core.IContext W E) (v : Core.IVar) (domain : Set E) (i : Core.ICDRTAssignment W E) (w : W) (e : E) (hc : (i, w) ∈ c) (he : e ∈ domain) : (i.updateIndivConst v (Core.Entity.some e), w) ∈ extendContext c v domain

Context extension includes witnesses: if (i, w) ∈ c and e ∈ domain, then the extended pair is in the extended context.

theorem Semantics.Dynamic.Bilateral.ICDRT.atom_complementary {W : Type u_1} {E : Type u_2} (prop : W → Prop) (c : Core.IContext W E) : (BilateralICDRT.atom prop).positive c ∪ (BilateralICDRT.atom prop).negative c = c

Atomic positive and negative updates cover the context: every assignment-world pair is either verified or falsified.

theorem Semantics.Dynamic.Bilateral.ICDRT.atom_disjoint {W : Type u_1} {E : Type u_2} (prop : W → Prop) (c : Core.IContext W E) : (BilateralICDRT.atom prop).positive c ∩ (BilateralICDRT.atom prop).negative c = ∅

Atomic positive and negative updates are disjoint: no pair is both verified and falsified.