structure Model.Bisimulation {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} (M₁ : Model κ₁ α) (M₂ : Model κ₂ α) : Type (max u_1 u_2)

• toRel : M₁.World → M₂.World → Prop
• atomic {x₁ : M₁.World} {x₂ : M₂.World} {a : α} : self.toRel x₁ x₂ → (Val x₁ a ↔ Val x₂ a)
• forth {x₁ y₁ : M₁.World} {x₂ : M₂.World} : self.toRel x₁ x₂ → x₁ ≺ y₁ → ∃ (y₂ : M₂.World), self.toRel y₁ y₂ ∧ x₂ ≺ y₂
• back {x₁ : M₁.World} {x₂ y₂ : M₂.World} : self.toRel x₁ x₂ → x₂ ≺ y₂ → ∃ (y₁ : M₁.World), self.toRel y₁ y₂ ∧ x₁ ≺ y₁

def Model.«term_⇄_» : Lean.TrailingParserDescr

Equations

• Model.«term_⇄_» = Lean.ParserDescr.trailingNode `Model.«term_⇄_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇄ ") (Lean.ParserDescr.cat `term 81))

@[implicit_reducible]

instance Model.instCoeFunBisimulationForallWorldForallProp {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} : CoeFun (M₁ ⇄ M₂) fun (x : M₁ ⇄ M₂) => M₁.World → M₂.World → Prop

Equations

• Model.instCoeFunBisimulationForallWorldForallProp = { coe := Model.Bisimulation.toRel }

def Model.Bisimulation.symm {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (bi : M₁ ⇄ M₂) : M₂ ⇄ M₁

Equations

• bi.symm = { toRel := fun (x : M₂.World) (y : M₁.World) => bi.toRel y x, atomic := ⋯, forth := ⋯, back := ⋯ }

def Model.World.ModalEquivalent {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (x₁ : M₁.World) (x₂ : M₂.World) : Prop

Equations

• (x₁ ↭ x₂) = ∀ {A : Formula α}, x₁ ⊩[M₁] A ↔ x₂ ⊩[M₂] A

def Model.«term_↭_» : Lean.TrailingParserDescr

Equations

• Model.«term_↭_» = Lean.ParserDescr.trailingNode `Model.«term_↭_» 50 51 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ↭ ") (Lean.ParserDescr.cat `term 51))

theorem Model.World.modal_equivalent_of_bisimilar {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} {x₁ : M₁.World} {x₂ : M₂.World} (Bi : M₁ ⇄ M₂) (bisx : Bi.toRel x₁ x₂) : x₁ ↭ x₂

def Model.World.ModalEquivalent.symm {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} {x₁ : M₁.World} {x₂ : M₂.World} (h : x₁ ↭ x₂) : x₂ ↭ x₁

Equations

• ⋯ = ⋯

structure Model.PseudoEpimorphism {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} (M₁ : Model κ₁ α) (M₂ : Model κ₂ α) : Type (max u_1 u_2)

• toFun : M₁.World → M₂.World
• forth {x y : M₁.World} : x ≺ y → self.toFun x ≺ self.toFun y
• back {w : M₁.World} {v : M₂.World} : self.toFun w ≺ v → ∃ (u : M₁.World), self.toFun u = v ∧ w ≺ u
• atomic {w : M₁.World} {a : α} : Val w a ↔ Val (self.toFun w) a

def Model.«term_→ₚ_» : Lean.TrailingParserDescr

Equations

• Model.«term_→ₚ_» = Lean.ParserDescr.trailingNode `Model.«term_→ₚ_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ₚ ") (Lean.ParserDescr.cat `term 81))

@[implicit_reducible]

instance Model.instCoeFunPseudoEpimorphismForallWorld {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} : CoeFun (M₁ →ₚ M₂) fun (x : M₁ →ₚ M₂) => M₁.World → M₂.World

Equations

• Model.instCoeFunPseudoEpimorphismForallWorld = { coe := Model.PseudoEpimorphism.toFun }

def Model.PseudoEpimorphism.id {κ : Type u_1} {α : Type u_2} [Nonempty κ] {M : Model κ α} : M →ₚ M

Equations

• Model.PseudoEpimorphism.id = { toFun := id, forth := ⋯, back := ⋯, atomic := ⋯ }

def Model.PseudoEpimorphism.comp {κ₁ : Type u_1} {κ₂ : Type u_2} {κ₃ : Type u_3} [Nonempty κ₁] [Nonempty κ₂] [Nonempty κ₃] {α : Type u_4} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} {M₃ : Model κ₃ α} (f : M₁ →ₚ M₂) (g : M₂ →ₚ M₃) : M₁ →ₚ M₃

Equations

• f.comp g = { toFun := g.toFun ∘ f.toFun, forth := ⋯, back := ⋯, atomic := ⋯ }

theorem Model.PseudoEpimorphism.forth_iterate {κ₁ : Type u_1} {κ₂ : Type u_3} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_2} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (f : M₁ →ₚ M₂) {x y : M₁.World} {n : ℕ} : x ≺^[n] y → f.toFun x ≺^[n] f.toFun y

theorem Model.PseudoEpimorphism.back_iterate {κ₁ : Type u_1} {κ₂ : Type u_3} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_2} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (f : M₁ →ₚ M₂) {w : M₁.World} {v : M₂.World} {n : ℕ} : f.toFun w ≺^[n] v → ∃ (u : M₁.World), f.toFun u = v ∧ w ≺^[n] u

theorem Model.PseudoEpimorphism.toFun_rel_toFun_iff_of_inj {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (f : M₁ →ₚ M₂) (inj : Function.Injective f.toFun) {x y : M₁.World} : f.toFun x ≺ f.toFun y ↔ x ≺ y

theorem Model.PseudoEpimorphism.toFun_relItr_toFun_iff_of_inj {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (f : M₁ →ₚ M₂) (inj : Function.Injective f.toFun) {x y : M₁.World} {n : ℕ} : f.toFun x ≺^[n] f.toFun y ↔ x ≺^[n] y

def Model.PseudoEpimorphism.bisimulation {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (f : M₁ →ₚ M₂) : M₁ ⇄ M₂

Equations

• f.bisimulation = { toRel := fun (x : M₁.World) (y : M₂.World) => y = f.toFun x, atomic := ⋯, forth := ⋯, back := ⋯ }

theorem Model.PseudoEpimorphism.modal_equivalence {κ₁ : Type u_1} {κ₂ : Type u_3} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_2} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (f : M₁ →ₚ M₂) (w : M₁.World) : w ↭ f.toFun w

theorem Model.validate_of_surjective_pseudoEpimorphism {κ₁ : Type u_2} {κ₂ : Type u_3} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_1} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} {A : Formula α} (f : M₁ →ₚ M₂) (f_surjective : Function.Surjective f.toFun) : M₁ ⊧ A → M₂ ⊧ A

structure Model.BisimulationUnder {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} (P : Finset α) (M₁ : Model κ₁ α) (M₂ : Model κ₂ α) : Type (max u_1 u_2)

A bisimulation-under-P: a bisimulation that is only required to match the valuation on atoms in P. Formalizes the notion of "cones 𝒳_a, 𝒳_y are p̄-isomorphic" ("Removal of a redundant cone"): rather than requiring a literal frame isomorphism, we ask for bisimilarity-under-P, the modally correct and more flexible notion that suffices for (and is used directly in) the forcing-preservation argument.

• [Bek90, §4, item 3, Lemma 6, Lemma 8]

• toRel : M₁.World → M₂.World → Prop
• atomic {x₁ : M₁.World} {x₂ : M₂.World} {a : α} : a ∈ P → self.toRel x₁ x₂ → (Val x₁ a ↔ Val x₂ a)
• forth {x₁ y₁ : M₁.World} {x₂ : M₂.World} : self.toRel x₁ x₂ → x₁ ≺ y₁ → ∃ (y₂ : M₂.World), self.toRel y₁ y₂ ∧ x₂ ≺ y₂
• back {x₁ : M₁.World} {x₂ y₂ : M₂.World} : self.toRel x₁ x₂ → x₂ ≺ y₂ → ∃ (y₁ : M₁.World), self.toRel y₁ y₂ ∧ x₁ ≺ y₁

def Model.«term_⇄[_]_» : Lean.TrailingParserDescr

A bisimulation-under-P: a bisimulation that is only required to match the valuation on atoms in P. Formalizes the notion of "cones 𝒳_a, 𝒳_y are p̄-isomorphic" ("Removal of a redundant cone"): rather than requiring a literal frame isomorphism, we ask for bisimilarity-under-P, the modally correct and more flexible notion that suffices for (and is used directly in) the forcing-preservation argument.

• [Bek90, §4, item 3, Lemma 6, Lemma 8]

Equations

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

@[implicit_reducible]

instance Model.instCoeFunBisimulationUnderForallWorldForallProp {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} {P : Finset α} : CoeFun (BisimulationUnder P M₁ M₂) fun (x : BisimulationUnder P M₁ M₂) => M₁.World → M₂.World → Prop

Equations

• Model.instCoeFunBisimulationUnderForallWorldForallProp = { coe := Model.BisimulationUnder.toRel }

def Model.BisimulationUnder.symm {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} {P : Finset α} (bi : BisimulationUnder P M₁ M₂) : BisimulationUnder P M₂ M₁

Equations

• bi.symm = { toRel := fun (x : M₂.World) (y : M₁.World) => bi.toRel y x, atomic := ⋯, forth := ⋯, back := ⋯ }

theorem Model.World.forces_iff_of_pbisimilar {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} [DecidableEq α] {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} {P : Finset α} {x₁ : M₁.World} {x₂ : M₂.World} (Bi : BisimulationUnder P M₁ M₂) (bisx : Bi.toRel x₁ x₂) {A : Formula α} : A.atoms ⊆ P → (x₁ ⊩[M₁] A ↔ x₂ ⊩[M₂] A)

A bisimulation-under-P forces agreement on every formula whose atoms lie in P (the ω-analogue of World.modal_equivalent_of_bisimilar).

structure Model.GeneratedSub {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} (M₁ : Model κ₁ α) (M₂ : Model κ₂ α) extends M₁ →ₚ M₂ : Type (max u_1 u_2)

• toFun : M₁.World → M₂.World
• forth {x y : M₁.World} : x ≺ y → self.toFun x ≺ self.toFun y
• back {w : M₁.World} {v : M₂.World} : self.toFun w ≺ v → ∃ (u : M₁.World), self.toFun u = v ∧ w ≺ u
• atomic {w : M₁.World} {a : α} : Val w a ↔ Val (self.toFun w) a
• monic : Function.Injective self.toFun

def Model.«term_⥹_» : Lean.TrailingParserDescr

Equations

• Model.«term_⥹_» = Lean.ParserDescr.trailingNode `Model.«term_⥹_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⥹ ") (Lean.ParserDescr.cat `term 81))

def Model.GeneratedSub.bisimulation {κ₁ : Type u_1} {κ₂ : Type u_2} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_3} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (g : M₁ ⥹ M₂) : M₁ ⇄ M₂

Equations

• g.bisimulation = g.bisimulation

theorem Model.GeneratedSub.modal_equivalence {κ₁ : Type u_1} {κ₂ : Type u_3} [Nonempty κ₁] [Nonempty κ₂] {α : Type u_2} {M₁ : Model κ₁ α} {M₂ : Model κ₂ α} (g : M₁ ⥹ M₂) (w : M₁.World) : w ↭ g.toFun w

structure Model.FrameBisimulation {κ₁ : Type u_3} {κ₂ : Type u_4} [Nonempty κ₁] [Nonempty κ₂] {α₁ : Type u_1} {α₂ : Type u_2} (M₁ : Model κ₁ α₁) (M₂ : Model κ₂ α₂) : Type (max u_3 u_4)

A frame bisimulation between M₁ and M₂: a Bisimulation-like relation that only needs to respect the accessibility relation (forth/back) and drops the atomic condition, so it makes sense across models M₁ : Model κ₁ α₁, M₂ : Model κ₂ α₂ with different propositional-variable types α₁, α₂. It records exactly enough structure to preserve forcing of letterless formulas.

• toRel : M₁.World → M₂.World → Prop
• forth {x₁ y₁ : M₁.World} {x₂ : M₂.World} : self.toRel x₁ x₂ → x₁ ≺ y₁ → ∃ (y₂ : M₂.World), self.toRel y₁ y₂ ∧ x₂ ≺ y₂
• back {x₁ : M₁.World} {x₂ y₂ : M₂.World} : self.toRel x₁ x₂ → x₂ ≺ y₂ → ∃ (y₁ : M₁.World), self.toRel y₁ y₂ ∧ x₁ ≺ y₁

def Model.«term_⇄ᶠ_» : Lean.TrailingParserDescr

Equations

• Model.«term_⇄ᶠ_» = Lean.ParserDescr.trailingNode `Model.«term_⇄ᶠ_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ⇄ᶠ ") (Lean.ParserDescr.cat `term 81))

@[implicit_reducible]

instance Model.instCoeFunFrameBisimulationForallWorldForallProp {κ₁ : Type u_3} {κ₂ : Type u_4} [Nonempty κ₁] [Nonempty κ₂] {α₁ : Type u_1} {α₂ : Type u_2} {M₁ : Model κ₁ α₁} {M₂ : Model κ₂ α₂} : CoeFun (M₁ ⇄ᶠ M₂) fun (x : M₁ ⇄ᶠ M₂) => M₁.World → M₂.World → Prop

Equations

• Model.instCoeFunFrameBisimulationForallWorldForallProp = { coe := Model.FrameBisimulation.toRel }

def Model.FrameBisimulation.symm {κ₁ : Type u_3} {κ₂ : Type u_4} [Nonempty κ₁] [Nonempty κ₂] {α₁ : Type u_1} {α₂ : Type u_2} {M₁ : Model κ₁ α₁} {M₂ : Model κ₂ α₂} (bi : M₁ ⇄ᶠ M₂) : M₂ ⇄ᶠ M₁

Equations

• bi.symm = { toRel := fun (x : M₂.World) (y : M₁.World) => bi.toRel y x, forth := ⋯, back := ⋯ }

theorem Model.FrameBisimulation.forth_iterate {κ₁ : Type u_3} {κ₂ : Type u_4} [Nonempty κ₁] [Nonempty κ₂] {α₁ : Type u_1} {α₂ : Type u_2} {M₁ : Model κ₁ α₁} {M₂ : Model κ₂ α₂} {x₁ : M₁.World} {x₂ : M₂.World} (Bi : M₁ ⇄ᶠ M₂) (bisx : Bi.toRel x₁ x₂) {y₁ : M₁.World} {n : ℕ} : x₁ ≺^[n] y₁ → ∃ (y₂ : M₂.World), Bi.toRel y₁ y₂ ∧ x₂ ≺^[n] y₂

theorem Model.World.letterless_modal_equivalent_of_frameBisimilar {κ₁ : Type u_3} {κ₂ : Type u_4} [Nonempty κ₁] [Nonempty κ₂] {α₁ : Type u_1} {α₂ : Type u_2} {M₁ : Model κ₁ α₁} {M₂ : Model κ₂ α₂} {x₁ : M₁.World} {x₂ : M₂.World} (Bi : M₁ ⇄ᶠ M₂) (bisx : Bi.toRel x₁ x₂) {B : LetterlessFormula} : x₁ ⊩[M₁] B.lift ↔ x₂ ⊩[M₂] B.lift

A frame bisimulation forces agreement on every letterless formula (the atomic-condition-free analogue of World.modal_equivalent_of_bisimilar).

structure Model.FramePseudoEpimorphism {κ₁ : Type u_3} {κ₂ : Type u_4} [Nonempty κ₁] [Nonempty κ₂] {α₁ : Type u_1} {α₂ : Type u_2} (M₁ : Model κ₁ α₁) (M₂ : Model κ₂ α₂) : Type (max u_3 u_4)

A frame pseudo-epimorphism from M₁ to M₂: a PseudoEpimorphism-like function that only needs to respect the accessibility relation (forth/back) and drops the atomic condition, so it makes sense across models M₁ : Model κ₁ α₁, M₂ : Model κ₂ α₂ with different propositional-variable types α₁, α₂.

• toFun : M₁.World → M₂.World
• forth {x y : M₁.World} : x ≺ y → self.toFun x ≺ self.toFun y
• back {w : M₁.World} {v : M₂.World} : self.toFun w ≺ v → ∃ (u : M₁.World), self.toFun u = v ∧ w ≺ u

def Model.«term_→ᶠ_» : Lean.TrailingParserDescr

Equations

• Model.«term_→ᶠ_» = Lean.ParserDescr.trailingNode `Model.«term_→ᶠ_» 80 81 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " →ᶠ ") (Lean.ParserDescr.cat `term 81))

@[implicit_reducible]

instance Model.instCoeFunFramePseudoEpimorphismForallWorld {κ₁ : Type u_3} {κ₂ : Type u_4} [Nonempty κ₁] [Nonempty κ₂] {α₁ : Type u_1} {α₂ : Type u_2} {M₁ : Model κ₁ α₁} {M₂ : Model κ₂ α₂} : CoeFun (M₁ →ᶠ M₂) fun (x : M₁ →ᶠ M₂) => M₁.World → M₂.World

Equations

• Model.instCoeFunFramePseudoEpimorphismForallWorld = { coe := Model.FramePseudoEpimorphism.toFun }

def Model.FramePseudoEpimorphism.bisimulation {κ₁ : Type u_3} {κ₂ : Type u_4} [Nonempty κ₁] [Nonempty κ₂] {α₁ : Type u_1} {α₂ : Type u_2} {M₁ : Model κ₁ α₁} {M₂ : Model κ₂ α₂} (f : M₁ →ᶠ M₂) : M₁ ⇄ᶠ M₂

Equations

• f.bisimulation = { toRel := fun (x : M₁.World) (y : M₂.World) => y = f.toFun x, forth := ⋯, back := ⋯ }

theorem Model.FramePseudoEpimorphism.letterless_modal_equivalence {κ₁ : Type u_3} {κ₂ : Type u_4} [Nonempty κ₁] [Nonempty κ₂] {α₁ : Type u_1} {α₂ : Type u_2} {M₁ : Model κ₁ α₁} {M₂ : Model κ₂ α₂} (f : M₁ →ᶠ M₂) (w : M₁.World) {B : LetterlessFormula} : w ⊩[M₁] B.lift ↔ f.toFun w ⊩[M₂] B.lift