ProvabilityLogic.Kripke.Preservation

source

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₁

Instances For

source

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))

Instances For

source

@[instance_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 }

source

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 := ⋯ }

Instances For

source

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

Instances For

source

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))

Instances For

source

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₂

source

theorem 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₁

source

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

Instances For

source

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))

Instances For

source

@[instance_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 }

source

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

M →ₚ M

Equations

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

Instances For

source

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 := ⋯ }

Instances For

source

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

source

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

source

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

source

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

source

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 := ⋯ }

Instances For

source

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

source

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

source

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 required to match the valuation only on atoms in P. This is how "the cones 𝒳_a, 𝒳_y are p̄-isomorphic" is formalized here.

[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₁

Instances For

source

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

Lean.TrailingParserDescr

A bisimulation-under-P: a bisimulation required to match the valuation only on atoms in P. This is how "the cones 𝒳_a, 𝒳_y are p̄-isomorphic" is formalized here.

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

Equations

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

Instances For

source

@[instance_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 }

source

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 := ⋯ }

Instances For

source

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)

source

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

Instances For

source

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))

Instances For

source

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

Instances For

source

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

source

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 Bisimulation without the atomic condition, so that it makes sense across models with different propositional-variable types. It preserves 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₁

Instances For

source

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))

Instances For

source

@[instance_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 }

source

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 := ⋯ }

Instances For

source

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₂

source

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

source

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 PseudoEpimorphism without the atomic condition, so that it makes sense across models 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

Instances For

source

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))

Instances For

source

@[instance_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 }

source

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 := ⋯ }

Instances For

source

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