@[reducible, inline]

abbrev LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame (F₁ F₂ : Kripke.Frame) (r₁ : F₁.World) (r₂ : F₂.World) [F₁.IsFiniteTree r₁] [F₂.IsFiniteTree r₂] : Kripke.Frame

Equations

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

instance LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.instCoeWorld {F₁ F₂ : Kripke.Frame} {r₁ : F₁.World} {r₂ : F₂.World} [F₁.IsFiniteTree r₁] [F₂.IsFiniteTree r₂] : Coe F₁.World (mdpCounterexmpleFrame F₁ F₂ r₁ r₂).World

Equations

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

instance LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.instCoeWorld_1 {F₁ F₂ : Kripke.Frame} {r₁ : F₁.World} {r₂ : F₂.World} [F₁.IsFiniteTree r₁] [F₂.IsFiniteTree r₂] : Coe F₂.World (mdpCounterexmpleFrame F₁ F₂ r₁ r₂).World

Equations

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

instance LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.instIsFiniteTreeInlUnitSumWorldUnit {F₁ F₂ : Kripke.Frame} {r₁ : F₁.World} {r₂ : F₂.World} [tree₁ : F₁.IsFiniteTree r₁] [tree₂ : F₂.IsFiniteTree r₂] : (mdpCounterexmpleFrame F₁ F₂ r₁ r₂).IsFiniteTree (Sum.inl ())

@[reducible, inline]

abbrev LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.root {F₁ F₂ : Kripke.Frame} {r₁ : F₁.World} {r₂ : F₂.World} [F₁.IsFiniteTree r₁] [F₂.IsFiniteTree r₂] : (mdpCounterexmpleFrame F₁ F₂ r₁ r₂).World

Equations

• LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.root = Sum.inl ()

def LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.pMorphism₁ {F₁ F₂ : Kripke.Frame} {r₁ : F₁.World} {r₂ : F₂.World} [F₁.IsFiniteTree r₁] [F₂.IsFiniteTree r₂] : F₁ →ₚ mdpCounterexmpleFrame F₁ F₂ r₁ r₂

Equations

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

def LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.pMorphism₂ {F₁ F₂ : Kripke.Frame} {r₁ : F₁.World} {r₂ : F₂.World} [F₁.IsFiniteTree r₁] [F₂.IsFiniteTree r₂] : F₂ →ₚ mdpCounterexmpleFrame F₁ F₂ r₁ r₂

Equations

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

theorem LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.through_original_root {F₁ F₂ : Kripke.Frame} {r₁ : F₁.World} {r₂ : F₂.World} [F₁.IsFiniteTree r₁] [F₂.IsFiniteTree r₂] {x : (mdpCounterexmpleFrame F₁ F₂ r₁ r₂).World} (h : mdpCounterexmpleFrame.root ≺ x) : (x = (Sum.inr ∘ Sum.inl) r₁ ∨ Sum.inr (Sum.inl r₁) ≺ x) ∨ x = (Sum.inr ∘ Sum.inr) r₂ ∨ Sum.inr (Sum.inr r₂) ≺ x

@[reducible, inline]

abbrev LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel (M₁ M₂ : Kripke.Model) (r₁ : M₁.World) (r₂ : M₂.World) [M₁.IsFiniteTree r₁] [M₂.IsFiniteTree r₂] : Kripke.Model

Equations

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

instance LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.instCoeWorld {M₁ M₂ : Kripke.Model} {r₁ : M₁.World} {r₂ : M₂.World} [tree₁ : M₁.IsFiniteTree r₁] [tree₂ : M₂.IsFiniteTree r₂] : Coe M₁.World (mdpCounterexmpleModel M₁ M₂ r₁ r₂).World

Equations

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

instance LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.instCoeWorld_1 {M₁ M₂ : Kripke.Model} {r₁ : M₁.World} {r₂ : M₂.World} [tree₁ : M₁.IsFiniteTree r₁] [tree₂ : M₂.IsFiniteTree r₂] : Coe M₂.World (mdpCounterexmpleModel M₁ M₂ r₁ r₂).World

Equations

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

@[reducible, inline]

abbrev LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.root {M₁ M₂ : Kripke.Model} {r₁ : M₁.World} {r₂ : M₂.World} [tree₁ : M₁.IsFiniteTree r₁] [tree₂ : M₂.IsFiniteTree r₂] : (mdpCounterexmpleModel M₁ M₂ r₁ r₂).World

Equations

• LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.root = LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.root

def LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.pMorphism₁ {M₁ M₂ : Kripke.Model} {r₁ : M₁.World} {r₂ : M₂.World} [tree₁ : M₁.IsFiniteTree r₁] [tree₂ : M₂.IsFiniteTree r₂] : M₁ →ₚ mdpCounterexmpleModel M₁ M₂ r₁ r₂

Equations

• LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.pMorphism₁ = LO.Modal.Kripke.Model.PseudoEpimorphism.ofAtomic LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.pMorphism₁ ⋯

def LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.pMorphism₂ {M₁ M₂ : Kripke.Model} {r₁ : M₁.World} {r₂ : M₂.World} [tree₁ : M₁.IsFiniteTree r₁] [tree₂ : M₂.IsFiniteTree r₂] : M₂ →ₚ mdpCounterexmpleModel M₁ M₂ r₁ r₂

Equations

• LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.pMorphism₂ = LO.Modal.Kripke.Model.PseudoEpimorphism.ofAtomic LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleFrame.pMorphism₂ ⋯

theorem LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.modal_equivalence_original_world₁ {M₁ M₂ : Kripke.Model} {r₁ : M₁.World} {r₂ : M₂.World} [tree₁ : M₁.IsFiniteTree r₁] [tree₂ : M₂.IsFiniteTree r₂] {x : M₁.World} : x ↭ (Sum.inr ∘ Sum.inl) x

theorem LO.Modal.Hilbert.GL.Kripke.mdpCounterexmpleModel.modal_equivalence_original_world₂ {M₁ M₂ : Kripke.Model} {r₁ : M₁.World} {r₂ : M₂.World} [tree₁ : M₁.IsFiniteTree r₁] [tree₂ : M₂.IsFiniteTree r₂] {x : M₂.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 ⊢! φ₂