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

DNE holds definitionally: ¬¬φ = φ.

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

Negation preserves context consistency.

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

Standard disjunction without cross-disjunct anaphora.

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.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.IntensionalCDRT.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.IntensionalCDRT.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.IntensionalCDRT.BilateralICDRT.«term_⟹_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.impl_as_disj {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) (c : 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.IntensionalCDRT.BilateralICDRT.de_morgan_conj_positive {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) (c : 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.IntensionalCDRT.BilateralICDRT.de_morgan_disj_positive {W : Type u_1} {E : Type u_2} (φ ψ : BilateralICDRT W E) (c : IContext W E) : (∼(φ ⊕ ψ)).positive c = φ.negative c ∩ ψ.negative c

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

def Semantics.Dynamic.IntensionalCDRT.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.IntensionalCDRT.BilateralICDRT.existsWideDisj p v domain φ ψ = Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.exists_ p v domain (φ.disjBathroom ψ)

def Semantics.Dynamic.IntensionalCDRT.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.IntensionalCDRT.BilateralICDRT.existsNarrowFirstDisj p v domain φ ψ = (Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.exists_ p v domain φ).disjBathroom ψ

def Semantics.Dynamic.IntensionalCDRT.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.IntensionalCDRT.BilateralICDRT.forall_ p v domain φ = ∼(Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.exists_ p v domain ∼φ)

def Semantics.Dynamic.IntensionalCDRT.BilateralICDRT.donkeyConditional {W : Type u_1} {E : Type u_2} (pFarmer pDonkey : Core.PVar) (vFarmer vDonkey : Core.IVar) (farmers donkeys : Set E) (owns beats : E → E → W → Prop) : BilateralICDRT W E

Donkey conditional: "If a farmer owns a donkey, he beats it."

In Hofmann's flat update:

1. "a farmer" introduces dref f
2. "a donkey" introduces dref d
3. These are accessible in the consequent via propositional drefs

Structure: ∃f.∃d.(owns(f,d) → beats(f,d))

The indefinites take widest scope (flat), but propositional drefs track that they're introduced in the antecedent context.

Equations

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

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

The classic bathroom sentence: "Either there's no bathroom, or it's upstairs."

Analysis:

1. First disjunct: ¬∃x.bathroom(x)
2. Second disjunct: upstairs(x)
3. Bathroom disjunction: x from ¬∃ is accessible in second disjunct

The negative of ∃x.bathroom(x) still introduces x (flatly), but with local context where bathroom(x) is false.

Equations

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

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

More detailed 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.