def LO.System.lem₁_diaT_of_S5Grz {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} {φ : F} [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} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} {φ : F} [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} [BasicModalLogicalConnective F] [System F S] (𝓢 : S) extends LO.System.S5 𝓢, LO.System.HasAxiomGrz 𝓢 : Type (max u_2 u_3)

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

def LO.System.S5Grz.diaT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [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} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [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} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.S5Grz 𝓢] : HasAxiomTc 𝓢

Equations

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

@[reducible, inline]

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

Equations

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

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

Equations

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

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

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

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