structure Semantics.Dynamic.Core.BilateralDen (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

A bilateral denotation: positive and negative update functions.

In bilateral semantics, a sentence φ denotes a pair of update functions:

• positive: s[φ]⁺ - the result of asserting φ in state s
• negative: s[φ]⁻ - the result of denying φ in state s

Standard dynamic semantics only has positive updates. The negative dimension is what enables DNE and proper treatment of cross-disjunct anaphora.

• positive : InfoState W E → InfoState W E

  Positive update: result of asserting the sentence

• negative : InfoState W E → InfoState W E

  Negative update: result of denying the sentence

theorem Semantics.Dynamic.Core.BilateralDen.ext {W : Type u_1} {E : Type u_2} {φ ψ : BilateralDen W E} (hp : φ.positive = ψ.positive) (hn : φ.negative = ψ.negative) : φ = ψ

theorem Semantics.Dynamic.Core.BilateralDen.ext_iff {W : Type u_1} {E : Type u_2} {φ ψ : BilateralDen W E} : φ = ψ ↔ φ.positive = ψ.positive ∧ φ.negative = ψ.negative

def Semantics.Dynamic.Core.BilateralDen.atom {W : Type u_1} {E : Type u_2} (pred : W → Bool) : BilateralDen W E

Atomic proposition: lift a classical proposition to bilateral form.

For an atomic proposition p:

• s[p]⁺ = { w ∈ s | p(w) } (keep worlds where p holds)
• s[p]⁻ = { w ∈ s | ¬p(w) } (keep worlds where p fails)

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.atom_complementary {W : Type u_1} {E : Type u_2} (pred : W → Bool) (s : InfoState W E) : (atom pred).positive s ∪ (atom pred).negative s = s

Atomic positive and negative are complementary

theorem Semantics.Dynamic.Core.BilateralDen.atom_disjoint {W : Type u_1} {E : Type u_2} (pred : W → Bool) (s : InfoState W E) : (atom pred).positive s ∩ (atom pred).negative s = ∅

Atomic positive and negative are disjoint

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

Negation: swap positive and negative updates.

This is the key insight of bilateral semantics. Negation doesn't "push in" - it simply swaps which update is positive and which is negative.

s[¬φ]⁺ = s[φ]⁻ s[¬φ]⁻ = s[φ]⁺

Equations

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

def Semantics.Dynamic.Core.BilateralDen.«term~_» : Lean.ParserDescr

Notation for negation

Equations

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

@[simp]

theorem Semantics.Dynamic.Core.BilateralDen.neg_neg {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : ~~φ = φ

Double negation is identity (DNE).

theorem Semantics.Dynamic.Core.BilateralDen.dne_positive {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) (s : InfoState W E) : (~~φ).positive s = φ.positive s

DNE for positive updates

theorem Semantics.Dynamic.Core.BilateralDen.dne_negative {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) (s : InfoState W E) : (~~φ).negative s = φ.negative s

DNE for negative updates

theorem Semantics.Dynamic.Core.BilateralDen.neg_involutive {W : Type u_1} {E : Type u_2} : Function.Involutive neg

Negation is involutive

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

Conjunction: sequence positive updates, combine negative updates.

For conjunction φ ∧ ψ:

• s[φ ∧ ψ]⁺ = s[φ]⁺[ψ]⁺ (sequence: first assert φ, then ψ)
• s[φ ∧ ψ]⁻ = s[φ]⁻ ∪ (s[φ]⁺ ∩ s[ψ]⁻) (fail if φ fails OR φ succeeds but ψ fails)

The negative update reflects: a conjunction is denied if either conjunct could be denied.

Equations

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

def Semantics.Dynamic.Core.BilateralDen.«term_⊙_» : Lean.TrailingParserDescr

Notation for conjunction

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.conj_assoc_positive {W : Type u_1} {E : Type u_2} (φ ψ χ : BilateralDen W E) (s : InfoState W E) : (φ ⊙ ψ ⊙ χ).positive s = (φ ⊙ (ψ ⊙ χ)).positive s

Conjunction associates (for positive updates)

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

Standard disjunction: choice between updates.

For standard disjunction φ ∨ ψ:

• s[φ ∨ ψ]⁺ = s[φ]⁺ ∪ s[ψ]⁺ (either disjunct holds)
• s[φ ∨ ψ]⁻ = s[φ]⁻ ∩ s[ψ]⁻ (both must fail to deny)

Equations

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

def Semantics.Dynamic.Core.BilateralDen.«term_⊕_» : Lean.TrailingParserDescr

Notation for disjunction

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.de_morgan_disj {W : Type u_1} {E : Type u_2} (φ ψ : BilateralDen W E) (s : InfoState W E) : (~(φ ⊕ ψ)).positive s = φ.negative s ∩ ψ.negative s

De Morgan: negated disjunction swaps to conjunction of negations

def Semantics.Dynamic.Core.BilateralDen.exists_ {W : Type u_1} {E : Type u_2} (x : ℕ) (domain : Set E) (φ : BilateralDen W E) : BilateralDen W E

Existential quantification: introduce a discourse referent.

For ∃x.φ:

• s[∃x.φ]⁺ = s[x:=?][φ]⁺ (introduce x, then assert φ)
• s[∃x.φ]⁻ = { p ∈ s | ∀e, p[x↦e] ∉ s[x:=?][φ]⁺ } (no witness makes φ true)

Equations

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

def Semantics.Dynamic.Core.BilateralDen.existsFull {W : Type u_1} {E : Type u_2} (x : ℕ) (φ : BilateralDen W E) : BilateralDen W E

Existential with full domain

Equations

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

def Semantics.Dynamic.Core.BilateralDen.forall_ {W : Type u_1} {E : Type u_2} (x : ℕ) (domain : Set E) (φ : BilateralDen W E) : BilateralDen W E

Universal quantification: ∀x.φ = ¬∃x.¬φ

In bilateral semantics, universal quantification is defined via de Morgan duality. This ensures proper interaction with negation.

Equations

• Semantics.Dynamic.Core.BilateralDen.forall_ x domain φ = ~(Semantics.Dynamic.Core.BilateralDen.exists_ x domain ~φ)

def Semantics.Dynamic.Core.BilateralDen.supports {W : Type u_1} {E : Type u_2} (s : InfoState W E) (φ : BilateralDen W E) : Prop

Bilateral support: state s supports φ iff positive update is non-empty and s subsists in s[φ]⁺.

Equations

• Semantics.Dynamic.Core.BilateralDen.supports s φ = ((φ.positive s).consistent ∧ s ⪯ φ.positive s)

def Semantics.Dynamic.Core.BilateralDen.entails {W : Type u_1} {E : Type u_2} (φ ψ : BilateralDen W E) : Prop

Bilateral entailment: φ entails ψ iff for all consistent states s, s[φ]⁺ supports ψ.

Equations

• (φ ⊨ᵇ ψ) = ∀ (s : Semantics.Dynamic.Core.InfoState W E), (φ.positive s).consistent → Semantics.Dynamic.Core.BilateralDen.supports (φ.positive s) ψ

def Semantics.Dynamic.Core.BilateralDen.«term_⊨ᵇ_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.Core.BilateralDen.egli {W : Type u_1} {E : Type u_2} (x : ℕ) (domain : Set E) (φ ψ : BilateralDen W E) (s : InfoState W E) : (exists_ x domain φ ⊙ ψ).positive s ⊆ (exists_ x domain (φ ⊙ ψ)).positive s

Egli's theorem: ∃x.φ ∧ ψ ⊨ ∃x[φ ∧ ψ]

When an existential takes wide scope over conjunction, the variable it introduces is accessible in the second conjunct. This is the key property for cross-sentential anaphora.

In bilateral semantics, this follows from the sequencing of updates.

def Semantics.Dynamic.Core.BilateralDen.pred1 {W : Type u_1} {E : Type u_2} (p : E → W → Bool) (t : ℕ) : BilateralDen W E

Create bilateral from predicate over entities

Equations

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

def Semantics.Dynamic.Core.BilateralDen.pred2 {W : Type u_1} {E : Type u_2} (p : E → E → W → Bool) (t₁ t₂ : ℕ) : BilateralDen W E

Create bilateral from binary predicate

Equations

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

def Semantics.Dynamic.Core.BilateralDen.UnilateralDen (W : Type u_3) (E : Type u_4) : Type (max u_4 u_3)

Unilateral denotation: single update function

Equations

• Semantics.Dynamic.Core.BilateralDen.UnilateralDen W E = (Semantics.Dynamic.Core.InfoState W E → Semantics.Dynamic.Core.InfoState W E)

def Semantics.Dynamic.Core.BilateralDen.toPair {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : (InfoState W E → InfoState W E) × (InfoState W E → InfoState W E)

View bilateral as pair of updates

Equations

• φ.toPair = (φ.positive, φ.negative)

def Semantics.Dynamic.Core.BilateralDen.ofPair {W : Type u_1} {E : Type u_2} (p : (InfoState W E → InfoState W E) × (InfoState W E → InfoState W E)) : BilateralDen W E

Construct bilateral from pair

Equations

• Semantics.Dynamic.Core.BilateralDen.ofPair p = { positive := p.fst, negative := p.snd }

theorem Semantics.Dynamic.Core.BilateralDen.toPair_ofPair {W : Type u_1} {E : Type u_2} (p : (InfoState W E → InfoState W E) × (InfoState W E → InfoState W E)) : (ofPair p).toPair = p

theorem Semantics.Dynamic.Core.BilateralDen.ofPair_toPair {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : ofPair φ.toPair = φ

theorem Semantics.Dynamic.Core.BilateralDen.neg_eq_swap {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : (~φ).toPair = φ.toPair.swap

Negation = swap on pairs

theorem Semantics.Dynamic.Core.BilateralDen.dne_from_swap {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : (~~φ).toPair = φ.toPair

DNE follows from swap ∘ swap = id

def Semantics.Dynamic.Core.BilateralDen.toUnilateral {W : Type u_1} {E : Type u_2} (φ : BilateralDen W E) : UnilateralDen W E

Projection: bilateral → unilateral (forgets negative)

Equations

• φ.toUnilateral = φ.positive

instance Semantics.Dynamic.Core.BilateralDen.instInvolutiveNeg {W : Type u_1} {E : Type u_2} : InvolutiveNeg (BilateralDen W E)

Equations

• Semantics.Dynamic.Core.BilateralDen.instInvolutiveNeg = { neg := Semantics.Dynamic.Core.BilateralDen.neg, neg_neg := ⋯ }