@[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.de_morgan_disj_negative {W : Type u_1} {E : Type u_2} (φ ψ : BUSDen W E) (s : Core.InfoState W E) : (φ ⊕ ψ).negative s = φ.negative s ∩ ψ.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 ∪ φ.positive s ∩ ψ.negative (φ.positive s)