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

Possibility: state s makes ◇φ true iff s[φ]⁺ is consistent.

In BUS, possibility checks whether the positive update yields a non-empty state.

Equations

• Semantics.Dynamic.BUS.FreeChoice.possible φ s = (φ.positive s).consistent

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

Necessity: state s makes □φ true iff s subsists in s[φ]⁺.

Every possibility in s has a descendant that survives the positive update.

Equations

• Semantics.Dynamic.BUS.FreeChoice.necessary φ s = (s ⪯ φ.positive s)

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

Impossibility: ¬◇φ iff s[φ]⁺ is empty.

Equations

• Semantics.Dynamic.BUS.FreeChoice.impossible φ s = ¬(φ.positive s).consistent

theorem Semantics.Dynamic.BUS.FreeChoice.impossible_iff_empty {W : Type u_1} {E : Type u_2} (φ : Core.BilateralDen W E) (s : Core.InfoState W E) : impossible φ s ↔ φ.positive s = ∅

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

Standard disjunction: the basic bilateral disjunction without FC preconditions.

Equations

• Semantics.Dynamic.BUS.FreeChoice.disjStd φ ψ = φ ⊕ ψ

def Semantics.Dynamic.BUS.FreeChoice.disjPos1 {W : Type u_1} {E : Type u_2} (φ ψ : Core.BilateralDen W E) (s : Core.InfoState W E) : Core.InfoState W E

The part of the positive update that φ (first disjunct) is responsible for.

Equations

• Semantics.Dynamic.BUS.FreeChoice.disjPos1 φ ψ s = φ.positive s

def Semantics.Dynamic.BUS.FreeChoice.disjPos2 {W : Type u_1} {E : Type u_2} (φ ψ : Core.BilateralDen W E) (s : Core.InfoState W E) : Core.InfoState W E

The part of the positive update that ψ (second disjunct) is responsible for.

The key case for bathroom disjunctions: s[φ]⁻[ψ]⁺ When φ = ¬∃x.P(x), this is s[∃x.P(x)]⁺[ψ]⁺ by DNE.

Equations

• Semantics.Dynamic.BUS.FreeChoice.disjPos2 φ ψ s = ψ.positive (φ.negative s)

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

Modal Disjunction: semantic disjunction that validates FC.

Modal disjunction adds a precondition to the positive update requiring that each disjunct contribute at least some possibilities. This semantically derives FC without pragmatic reasoning.

Equations

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

def Semantics.Dynamic.BUS.FreeChoice.«term_∨ᶠᶜ_» : Lean.TrailingParserDescr

Equations

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

theorem Semantics.Dynamic.BUS.FreeChoice.fc_semantic_first_disjunct {W : Type u_1} {E : Type u_2} (φ ψ : Core.BilateralDen W E) (s : Core.InfoState W E) (h : possible (φ ∨ᶠᶜ ψ) s) : possible φ s

FC is semantically derived from modal disjunction.

If possible (φ ∨ᶠᶜ ψ) s, then by the definition of disjModal:

1. disjPos1 φ ψ s is non-empty (i.e., φ contributes possibilities)
2. disjPos2 φ ψ s is non-empty (i.e., ψ contributes possibilities)

This directly implies possible φ s since disjPos1 φ ψ s = φ.positive s.

theorem Semantics.Dynamic.BUS.FreeChoice.fc_semantic_second_disjunct {W : Type u_1} {E : Type u_2} (φ ψ : Core.BilateralDen W E) (s : Core.InfoState W E) (h : possible (φ ∨ᶠᶜ ψ) s) : Set.Nonempty (ψ.positive (φ.negative s))

The second component: ψ contributes possibilities via φ.negative.

theorem Semantics.Dynamic.BUS.FreeChoice.modified_fc_semantic {W : Type u_1} {E : Type u_2} (φ ψ : Core.BilateralDen W E) (s : Core.InfoState W E) (h : possible (φ ∨ᶠᶜ ψ) s) : possible φ s ∧ Set.Nonempty (ψ.positive (φ.negative s))

Modified FC: ◇(φ ∨ ψ) ⊨ ◇φ ∧ ◇(¬φ ∧ ψ)

This is semantically derived.

structure Semantics.Dynamic.BUS.FreeChoice.BathroomConfig (W : Type u_3) (E : Type u_4) : Type (max u_3 u_4)

The bathroom disjunction configuration.

"Either there's no bathroom or it's in a funny place"

• bathroom : Core.BilateralDen W E

  The existential: ∃x.bathroom(x)

• funnyPlace : Core.BilateralDen W E

  The predicate on x: funny-place(x)

• x : ℕ

  The variable bound by the existential

def Semantics.Dynamic.BUS.FreeChoice.bathroomSentence {W : Type u_1} {E : Type u_2} (cfg : BathroomConfig W E) : Core.BilateralDen W E

The bathroom disjunction sentence: ¬∃x.bathroom(x) ∨ funny-place(x)

Equations

• Semantics.Dynamic.BUS.FreeChoice.bathroomSentence cfg = ~cfg.bathroom ∨ᶠᶜ cfg.funnyPlace

theorem Semantics.Dynamic.BUS.FreeChoice.fc_with_anaphora {W : Type u_1} {E : Type u_2} (cfg : BathroomConfig W E) (s : Core.InfoState W E) (h_poss : possible (bathroomSentence cfg) s) (h_no_bath : Set.Nonempty ((~cfg.bathroom).positive s)) (h_bath_funny : Set.Nonempty ((cfg.bathroom ⊙ cfg.funnyPlace).positive s)) : possible (~cfg.bathroom) s ∧ possible (cfg.bathroom ⊙ cfg.funnyPlace) s

FC with anaphora: bathroom disjunction inference pattern.

theorem Semantics.Dynamic.BUS.FreeChoice.dual_prohibition {W : Type u_1} {E : Type u_2} (φ ψ : Core.BilateralDen W E) (s : Core.InfoState W E) (h_φ : impossible φ s) (h_ψ : impossible ψ s) : impossible (φ ∨ᶠᶜ ψ) s

Dual prohibition: ¬◇φ ∧ ¬◇ψ ⊨ ¬◇(φ ∨ ψ)

If neither disjunct is possible, the disjunction is impossible.

theorem Semantics.Dynamic.BUS.FreeChoice.negation_swaps_dims {W : Type u_1} {E : Type u_2} (φ : Core.BilateralDen W E) (s : Core.InfoState W E) : (~φ).positive s = φ.negative s ∧ (~φ).negative s = φ.positive s

In BUS, negation swaps positive and negative updates.

theorem Semantics.Dynamic.BUS.FreeChoice.anaphora_via_dne {W : Type u_1} {E : Type u_2} (cfg : BathroomConfig W E) : ~~cfg.bathroom = cfg.bathroom

DNE as structural equality.

theorem Semantics.Dynamic.BUS.FreeChoice.exists_in_neg_dimension {W : Type u_1} {E : Type u_2} (x : ℕ) (dom : Set E) (φ : Core.BilateralDen W E) (s : Core.InfoState W E) : (~(exists_ x dom φ)).negative s = (exists_ x dom φ).positive s

Negated existential has existential in negative dimension.

theorem Semantics.Dynamic.BUS.FreeChoice.dne_preserves_binding {W : Type u_1} {E : Type u_2} (x : ℕ) (dom : Set E) (φ ψ : Core.BilateralDen W E) (s : Core.InfoState W E) : (~~(exists_ x dom φ) ⊙ ψ).positive s = (exists_ x dom φ ⊙ ψ).positive s

DNE preserves binding.

inductive Semantics.Dynamic.BUS.FreeChoice.BathroomWorld : Type

A concrete example setup for testing.

• noBathroom : BathroomWorld
• bathroomNormal : BathroomWorld
• bathroomFunny : BathroomWorld

instance Semantics.Dynamic.BUS.FreeChoice.instDecidableEqBathroomWorld : DecidableEq BathroomWorld

Equations

• Semantics.Dynamic.BUS.FreeChoice.instDecidableEqBathroomWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Dynamic.BUS.FreeChoice.instReprBathroomWorld : Repr BathroomWorld

Equations

• Semantics.Dynamic.BUS.FreeChoice.instReprBathroomWorld = { reprPrec := Semantics.Dynamic.BUS.FreeChoice.instReprBathroomWorld.repr }

def Semantics.Dynamic.BUS.FreeChoice.instReprBathroomWorld.repr : BathroomWorld → ℕ → Std.Format

Equations

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

inductive Semantics.Dynamic.BUS.FreeChoice.BathroomEntity : Type

• theBathroom : BathroomEntity

instance Semantics.Dynamic.BUS.FreeChoice.instDecidableEqBathroomEntity : DecidableEq BathroomEntity

Equations

• Semantics.Dynamic.BUS.FreeChoice.instDecidableEqBathroomEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Semantics.Dynamic.BUS.FreeChoice.instReprBathroomEntity.repr : BathroomEntity → ℕ → Std.Format

Equations

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

instance Semantics.Dynamic.BUS.FreeChoice.instReprBathroomEntity : Repr BathroomEntity

Equations

• Semantics.Dynamic.BUS.FreeChoice.instReprBathroomEntity = { reprPrec := Semantics.Dynamic.BUS.FreeChoice.instReprBathroomEntity.repr }

def Semantics.Dynamic.BUS.FreeChoice.isBathroom : BathroomEntity → BathroomWorld → Bool

Equations

• Semantics.Dynamic.BUS.FreeChoice.isBathroom Semantics.Dynamic.BUS.FreeChoice.BathroomEntity.theBathroom Semantics.Dynamic.BUS.FreeChoice.BathroomWorld.noBathroom = false
• Semantics.Dynamic.BUS.FreeChoice.isBathroom Semantics.Dynamic.BUS.FreeChoice.BathroomEntity.theBathroom x✝ = true

def Semantics.Dynamic.BUS.FreeChoice.inFunnyPlace : BathroomEntity → BathroomWorld → Bool

Equations

• Semantics.Dynamic.BUS.FreeChoice.inFunnyPlace Semantics.Dynamic.BUS.FreeChoice.BathroomEntity.theBathroom Semantics.Dynamic.BUS.FreeChoice.BathroomWorld.bathroomFunny = true
• Semantics.Dynamic.BUS.FreeChoice.inFunnyPlace x✝¹ x✝ = false

def Semantics.Dynamic.BUS.FreeChoice.exampleBathroomConfig : BathroomConfig BathroomWorld BathroomEntity

Equations

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