@[reducible, inline]

abbrev Semantics.Dynamic.BUS.BUSDen (W : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

BUS denotation as bilateral denotation.

Equations

• Semantics.Dynamic.BUS.BUSDen W E = Semantics.Dynamic.Core.BilateralDen W E

def Semantics.Dynamic.BUS.BUSDen.hasGap {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Core.InfoState W E) : Prop

Truth-value gap: presupposition failure.

Equations

• φ.hasGap s = (φ.positive s ∪ φ.negative s ⊂ s)

def Semantics.Dynamic.BUS.BUSDen.defined {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Core.InfoState W E) : Prop

Sentence is defined (no presupposition failure).

Equations

• φ.defined s = (φ.positive s ∪ φ.negative s = s)

def Semantics.Dynamic.BUS.BUSDen.skConj {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : BUSDen W E

Strong Kleene conjunction.

Equations

• φ.skConj ψ = φ ⊙ ψ

def Semantics.Dynamic.BUS.BUSDen.pConj {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : BUSDen W E

Presupposition-preserving conjunction.

Equations

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

def Semantics.Dynamic.BUS.BUSDen.strawsonEntails {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : Prop

Strawson entailment: φ entails ψ when φ is defined and true.

Equations

• φ.strawsonEntails ψ = ∀ (s : Semantics.Dynamic.Core.InfoState W E), φ.defined s → (φ.positive s).consistent → φ.positive s ⊆ ψ.positive (φ.positive s)

def Semantics.Dynamic.BUS.BUSDen.strongEntails {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) : Prop

Strong entailment: φ entails ψ with no presupposition failure.

Equations

• φ.strongEntails ψ = ∀ (s : Semantics.Dynamic.Core.InfoState W E), (φ.positive s).consistent → ψ.defined (φ.positive s) ∧ φ.positive s ⊆ ψ.positive (φ.positive s)

theorem Semantics.Dynamic.BUS.BUSDen.neg_positive_eq_negative {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Core.InfoState W E) : (~φ).positive s = φ.negative s

theorem Semantics.Dynamic.BUS.BUSDen.neg_negative_eq_positive {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Core.InfoState W E) : (~φ).negative s = φ.positive s

theorem Semantics.Dynamic.BUS.BUSDen.disj_negative {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : Core.InfoState W E) : (φ ⊕ ψ).negative s = ψ.negative (φ.negative s)

theorem Semantics.Dynamic.BUS.BUSDen.conj_negative {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : Core.InfoState W E) : (φ ⊙ ψ).negative s = φ.negative s ∪ ψ.negative (φ.positive s) ∪ ψ.negative (Core.BilateralDen.unknownUpdate φ s)

def Semantics.Dynamic.BUS.BUSDen.diamond {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : BUSDen W E

Epistemic possibility: ◇φ as a bilateral denotation.

• s[◇φ]⁺ = s if s[φ]⁺ is consistent, else ∅
• s[◇φ]⁻ = s if s subsists in s[φ]⁻, else ∅

Equation (73) of @cite{elliott-sudo-2025}.

Equations

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

def Semantics.Dynamic.BUS.BUSDen.box {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : BUSDen W E

Epistemic necessity: □φ = ¬◇¬φ.

Equations

• □ᵇφ = ~◇ᵇ~φ

def Semantics.Dynamic.BUS.BUSDen.«term◇ᵇ_» : Lean.ParserDescr

Equations

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

def Semantics.Dynamic.BUS.BUSDen.«term□ᵇ_» : Lean.ParserDescr

Equations

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

theorem Semantics.Dynamic.BUS.BUSDen.diamond_positive_isTest {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : Core.IsTest (◇ᵇφ).positive

Diamond positive is a test (returns s or ∅).

theorem Semantics.Dynamic.BUS.BUSDen.diamond_negative_isTest {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : Core.IsTest (◇ᵇφ).negative

Diamond negative is a test (returns s or ∅).

theorem Semantics.Dynamic.BUS.BUSDen.diamond_positive_eliminative {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : Core.IsEliminative (◇ᵇφ).positive

Diamond positive is eliminative (from IsTest).

theorem Semantics.Dynamic.BUS.BUSDen.diamond_positive_subset {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Core.InfoState W E) : (◇ᵇφ).positive s ⊆ s

Diamond positive subset (convenience form).

theorem Semantics.Dynamic.BUS.BUSDen.diamond_negative_eliminative {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : Core.IsEliminative (◇ᵇφ).negative

Diamond negative is eliminative (from IsTest).

theorem Semantics.Dynamic.BUS.BUSDen.diamond_negative_subset {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) (s : Core.InfoState W E) : (◇ᵇφ).negative s ⊆ s

Diamond negative subset (convenience form).

theorem Semantics.Dynamic.BUS.BUSDen.box_positive_eliminative {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : Core.IsEliminative (□ᵇφ).positive

Box positive is eliminative (□φ = ¬◇¬φ, so positive = diamond negative of ¬φ).

theorem Semantics.Dynamic.BUS.BUSDen.box_negative_eliminative {W : Type u_1} {E : Type u_2} (φ : BUSDen W E) : Core.IsEliminative (□ᵇφ).negative

Box negative is eliminative.