MDP

@[reducible, inline]

abbrev LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame (F₁ F₂ : Kripke.FiniteTransitiveTree) : Kripke.FiniteTransitiveTree

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.instCoeWorld {F₁ F₂ : Kripke.FiniteTransitiveTree} : Coe F₁.World (MDPCounterexampleFrame F₁ F₂).World

Equations

• LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.instCoeWorld = { coe := Sum.inr ∘ Sum.inl }

@[implicit_reducible]

instance LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.instCoeWorld_1 {F₁ F₂ : Kripke.FiniteTransitiveTree} : Coe F₂.World (MDPCounterexampleFrame F₁ F₂).World

Equations

• LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.instCoeWorld_1 = { coe := Sum.inr ∘ Sum.inr }

def LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.pMorphism₁ {F₁ F₂ : Kripke.FiniteTransitiveTree} : F₁.toFrame →ₚ (MDPCounterexampleFrame F₁ F₂).toFrame

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.pMorphism₁ = { toFun := fun (x : F₁.World) => Sum.inr (Sum.inl x), forth := ⋯, back := ⋯ }

def LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.pMorphism₂ {F₁ F₂ : Kripke.FiniteTransitiveTree} : F₂.toFrame →ₚ (MDPCounterexampleFrame F₁ F₂).toFrame

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.pMorphism₂ = { toFun := fun (x : F₂.World) => Sum.inr (Sum.inr x), forth := ⋯, back := ⋯ }

theorem LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.through_original_root {F₁ F₂ : Kripke.FiniteTransitiveTree} {x : (MDPCounterexampleFrame F₁ F₂).World} (h : (MDPCounterexampleFrame F₁ F₂).root ≺ x) : (x = (Sum.inr ∘ Sum.inl) F₁.root ∨ Sum.inr (Sum.inl F₁.root) ≺ x) ∨ x = (Sum.inr ∘ Sum.inr) F₂.root ∨ Sum.inr (Sum.inr F₂.root) ≺ x

@[reducible, inline]

abbrev LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel (M₁ M₂ : Kripke.FiniteTransitiveTreeModel) : Kripke.FiniteTransitiveTreeModel

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.instCoeWorld {M₁ M₂ : Kripke.FiniteTransitiveTreeModel} : Coe M₁.World (MDPCounterexampleModel M₁ M₂).World

Equations

• LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.instCoeWorld = { coe := Sum.inr ∘ Sum.inl }

@[implicit_reducible]

instance LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.instCoeWorld_1 {M₁ M₂ : Kripke.FiniteTransitiveTreeModel} : Coe M₂.World (MDPCounterexampleModel M₁ M₂).World

Equations

• LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.instCoeWorld_1 = { coe := Sum.inr ∘ Sum.inr }

def LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.pMorphism₁ {M₁ M₂ : Kripke.FiniteTransitiveTreeModel} : M₁.toModel →ₚ (MDPCounterexampleModel M₁ M₂).toModel

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.pMorphism₁ = LO.Modal.Kripke.Model.PseudoEpimorphism.ofAtomic LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.pMorphism₁ ⋯

theorem LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.modal_equivalence_original_world₁ {M₁ M₂ : Kripke.FiniteTransitiveTreeModel} {x : M₁.toModel.World} : x ↭ (Sum.inr ∘ Sum.inl) x

def LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.pMorphism₂ {M₁ M₂ : Kripke.FiniteTransitiveTreeModel} : M₂.toModel →ₚ (MDPCounterexampleModel M₁ M₂).toModel

Imported declaration from the Incompleteness formalization.

Equations

• LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.pMorphism₂ = LO.Modal.Kripke.Model.PseudoEpimorphism.ofAtomic LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleFrame.pMorphism₂ ⋯

theorem LO.Modal.Hilbert.GL.Kripke.MDPCounterexampleModel.modal_equivalence_original_world₂ {M₁ M₂ : Kripke.FiniteTransitiveTreeModel} {x : M₂.toModel.World} : x ↭ (Sum.inr ∘ Sum.inr) x

theorem LO.Modal.Hilbert.GL.MDP_Aux {X : Set (Formula ℕ)} {φ₁ φ₂ : Formula ℕ} (h : (□''X) *⊢[Hilbert.GL]! □φ₁ ⋎ □φ₂) : (□''X) *⊢[Hilbert.GL]! □φ₁ ∨ (□''X) *⊢[Hilbert.GL]! □φ₂

theorem LO.Modal.Hilbert.GL.modal_disjunctive {φ₁ φ₂ : Formula ℕ} (h : Hilbert.GL ⊢! □φ₁ ⋎ □φ₂) : Hilbert.GL ⊢! φ₁ ∨ Hilbert.GL ⊢! φ₂