Bilateral Connectives (DN-DRT / BUS)

Bilateral connectives enabling cross-disjunct anaphora (bathroom sentences), following the DN-DRT / BUS mechanism (@cite{krahmer-muskens-1995}).

This bilateral approach is NOT the same as @cite{hofmann-2025}'s full ICDRT analysis. ICDRT uses static operators over propositional discourse referents to derive accessibility from veridicality + discourse consistency, covering cases (modal subordination, disagreement) that bilateral accounts cannot (§5.1.1).

Main definitions

BilateralICDRT.neg, disjBathroom, impl, bathroomSentenceFull

theorem Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.dne_equality {W : Type u_1} {E : Type u_2} (φ : BilateralICDRT W E) (c : Core.IContext W E) : (∼∼φ).positive c = φ.positive c ∧ (∼∼φ).negative c = φ.negative c

DNE for BilateralICDRT: pointwise positive and negative interpretations of ¬¬φ agree with φ. Routed through the substrate's Core.Logic.Bilateral.IsBilateral.{positive,negative}_negate_negate, via BilateralICDRT.isBilateral (parent file).

theorem Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.neg_consistent_iff {W : Type u_1} {E : Type u_2} (φ : BilateralICDRT W E) (c : Core.IContext W E) : Set.Nonempty ((∼φ).positive c) ↔ Set.Nonempty (φ.negative c)

Negation preserves context consistency.

def Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.disjStd {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) : BilateralICDRT W E

Standard disjunction without cross-disjunct anaphora.

Equations

• φ ⊕ ψ = { positive := fun (c : Semantics.Dynamic.Core.IContext W E) => φ.positive c ∪ ψ.positive c, negative := fun (c : Semantics.Dynamic.Core.IContext W E) => φ.negative c ∩ ψ.negative c }

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.BilateralICDRT.disjBathroom {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) : BilateralICDRT W E

Bathroom disjunction: ψ evaluated in context where φ failed, enabling cross-disjunct anaphora.

Equations

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

def Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.disjBathroom' {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) : BilateralICDRT W E

Alternative formulation making the sequencing clearer.

The second disjunct "sees" the context where the first disjunct failed.

Equations

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

def Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.impl {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) : BilateralICDRT W E

Conditional: if φ then ψ.

In the bathroom analysis, conditionals work similarly: "If there's a bathroom, it's upstairs."

The antecedent introduces drefs accessible in the consequent.

⟦φ → ψ⟧^+ = ⟦φ⟧^- ∪ (⟦φ⟧^+ ∩ ⟦ψ⟧^+) ⟦φ → ψ⟧^- = ⟦φ⟧^+ ∩ ⟦ψ⟧^-

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.

theorem Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.impl_as_disj {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) (c : Core.IContext W E) (hψ_subsetting : ψ.positive (φ.positive c) ⊆ φ.positive c) : (φ ⟹ ψ).positive c = ((∼φ).disjBathroom ψ).positive c

Material conditional equivalence: φ → ψ ≡ ¬φ ∨ ψ

Using bathroom disjunction, this gives anaphora from antecedent to consequent.

Note: This equivalence requires that ψ's positive update is a subsetting operation (i.e., ψ.positive c' ⊆ c' for any context c'). This is standard in dynamic semantics where updates can only eliminate possibilities, not add them.

theorem Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.de_morgan_conj_positive {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) (c : Core.IContext W E) : (∼(φ ⊗ ψ)).positive c = (φ ⊗ ψ).negative c

De Morgan: ¬(φ ∧ ψ) ≡ ¬φ ∨ ¬ψ

In bilateral semantics, this holds because:

• Negation swaps positive/negative
• Conjunction sequences, disjunction chooses

theorem Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.de_morgan_disj_positive {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) (c : Core.IContext W E) : (∼(φ ⊕ ψ)).positive c = φ.negative c ∩ ψ.negative c

De Morgan: ¬(φ ∨ ψ) ≡ ¬φ ∧ ¬ψ

def Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.existsWideDisj {W : Type u_1} {E : Type u_2} (p : Core.PVar) (v : Core.IVar) (domain : Set E) (φ ψ : BilateralICDRT W E) : BilateralICDRT W E

Wide-scope existential: ∃x.(φ ∨ ψ)

The variable x is introduced before the disjunction, so it's accessible in both disjuncts.

Equations

• Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.existsWideDisj p v domain φ ψ = Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.exists_ p v domain (φ.disjBathroom ψ)

def Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.existsNarrowFirstDisj {W : Type u_1} {E : Type u_2} (p : Core.PVar) (v : Core.IVar) (domain : Set E) (φ ψ : BilateralICDRT W E) : BilateralICDRT W E

Narrow-scope existential in first disjunct: (∃x.φ) ∨ ψ

With bathroom disjunction, x introduced in ∃x.φ is accessible in ψ because ψ is evaluated in the negative of ∃x.φ, which still introduces x.

Equations

• Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.existsNarrowFirstDisj p v domain φ ψ = (Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.exists_ p v domain φ).disjBathroom ψ

def Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.forall_ {W : Type u_1} {E : Type u_2} (p : Core.PVar) (v : Core.IVar) (domain : Set E) (φ : BilateralICDRT W E) : BilateralICDRT W E

Universal quantifier via de Morgan: ∀x.φ ≡ ¬∃x.¬φ

Equations

• Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.forall_ p v domain φ = ∼(Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.exists_ p v domain ∼φ)

def Semantics.Dynamic.Bilateral.ICDRT.BilateralICDRT.bathroomSentenceFull {W : Type u_1} {E : Type u_2} (p : Core.PVar) (v : Core.IVar) (domain : Set E) (bathroom upstairs : Core.Entity E → W → Prop) : BilateralICDRT W E

Bathroom sentence with proper variable reference.

In full ICDRT, "it" in the second disjunct looks up variable v, and the propositional dref p tracks where v has a referent.

Equations

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