def LO.System.lem₁_diaT_of_S5Grz {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} {φ : F} [LO.System.S5 𝓢] : 𝓢 ⊢ (∼□(∼φ) ➝ ∼□(∼□φ)) ➝ ◇φ ➝ ◇□φ

Equations

• LO.System.lem₁_diaT_of_S5Grz = LO.System.impTrans'' (LO.System.rev_dhyp_imp' LO.System.diaDuality_mp) (LO.System.dhyp_imp' LO.System.diaDuality_mpr)

def LO.System.lem₂_diaT_of_S5Grz {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} {φ : F} [LO.System.S5 𝓢] : 𝓢 ⊢ (◇φ ➝ ◇□φ) ➝ ◇φ ➝ φ

Equations

• LO.System.lem₂_diaT_of_S5Grz = LO.System.dhyp_imp' LO.System.rm_diabox

class LO.System.S5Grz {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [LO.System F S] (𝓢 : S) extends LO.System.S5 𝓢, LO.System.HasAxiomGrz 𝓢 : Type (max u_2 u_3)

• mdp : {φ ψ : F} → 𝓢 ⊢ φ ➝ ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• neg_equiv : (φ : F) → 𝓢 ⊢ LO.Axioms.NegEquiv φ
• verum : 𝓢 ⊢ LO.Axioms.Verum
• imply₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.Imply₁ φ ψ
• imply₂ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.Imply₂ φ ψ χ
• and₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₁ φ ψ
• and₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndElim₂ φ ψ
• and₃ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.AndInst φ ψ
• or₁ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₁ φ ψ
• or₂ : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.OrInst₂ φ ψ
• or₃ : (φ ψ χ : F) → 𝓢 ⊢ LO.Axioms.OrElim φ ψ χ
• dne : (φ : F) → 𝓢 ⊢ LO.Axioms.DNE φ
• nec : {φ : F} → 𝓢 ⊢ φ → 𝓢 ⊢ □φ
• K : (φ ψ : F) → 𝓢 ⊢ LO.Axioms.K φ ψ
• dia_dual : (φ : F) → 𝓢 ⊢ LO.Axioms.DiaDuality φ
• T : (φ : F) → 𝓢 ⊢ LO.Axioms.T φ
• Five : (φ : F) → 𝓢 ⊢ LO.Axioms.Five φ
• Grz : (φ : F) → 𝓢 ⊢ LO.Axioms.Grz φ

def LO.System.S5Grz.diaT {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.S5Grz 𝓢] {φ : F} : 𝓢 ⊢ ◇φ ➝ φ

Equations

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

def LO.System.S5Grz.Tc {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.S5Grz 𝓢] {φ : F} : 𝓢 ⊢ φ ➝ □φ

Equations

• LO.System.S5Grz.Tc = LO.System.impTrans'' (LO.System.contra₃' (LO.System.impTrans'' (LO.System.and₂' LO.System.diaDuality) LO.System.S5Grz.diaT)) LO.System.box_dne

instance LO.System.S5Grz.instHasAxiomTc {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.S5Grz 𝓢] : LO.System.HasAxiomTc 𝓢

Equations

• LO.System.S5Grz.instHasAxiomTc = { Tc := fun (x : F) => LO.System.S5Grz.Tc }

@[reducible, inline]

abbrev LO.Modal.Hilbert.S5Grz (α : Type u_1) : LO.Modal.Hilbert α

Equations

• LO.Modal.Hilbert.S5Grz α = LO.Modal.Hilbert.ExtK (𝗧 ∪ 𝟱 ∪ 𝗚𝗿𝘇)

instance LO.Modal.Hilbert.instS5GrzFormulaS5Grz {α : Type u_1} : LO.System.S5Grz (LO.Modal.Hilbert.S5Grz α)

Equations

• LO.Modal.Hilbert.instS5GrzFormulaS5Grz = LO.System.S5Grz.mk

theorem LO.Modal.Hilbert.S5Grz_weakerThan_Triv {α : Type u_1} [DecidableEq α] : LO.Modal.Hilbert.S5Grz α ≤ₛ LO.Modal.Hilbert.Triv α

theorem LO.Modal.Hilbert.Triv_weakerThan_S5Grz {α : Type u_1} [DecidableEq α] : LO.Modal.Hilbert.Triv α ≤ₛ LO.Modal.Hilbert.S5Grz α

theorem LO.Modal.Hilbert.S5Grz_equiv_Triv {α : Type u_1} [DecidableEq α] : LO.Modal.Hilbert.S5Grz α =ₛ LO.Modal.Hilbert.Triv α