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

Equations

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

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

Equations

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

class LO.Entailment.Modal.S5Grz {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] (𝓢 : S) extends LO.Entailment.Modal.S5 𝓢, LO.Entailment.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.Entailment.S5Grz.diaT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [DecidableEq F] [Modal.S5Grz 𝓢] {φ : F} : 𝓢 ⊢ ◇φ ➝ φ

Equations

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

instance LO.Entailment.S5Grz.instHasAxiomDiaT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [DecidableEq F] [Modal.S5Grz 𝓢] : HasAxiomDiaT 𝓢

Equations

• LO.Entailment.S5Grz.instHasAxiomDiaT = { diaT := fun (x : F) => LO.Entailment.S5Grz.diaT }

instance LO.Entailment.S5Grz.instKTc' {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [DecidableEq F] [Modal.S5Grz 𝓢] : Modal.KTc' 𝓢

Equations

• LO.Entailment.S5Grz.instKTc' = LO.Entailment.Modal.KTc'.mk

@[reducible, inline]

abbrev LO.Modal.Hilbert.S5Grz : Hilbert ℕ

Equations

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

instance LO.Modal.Hilbert.instHasKNatS5Grz : Hilbert.S5Grz.HasK

Equations

• LO.Modal.Hilbert.instHasKNatS5Grz = { p := 0, q := 1, ne_pq := LO.Modal.Hilbert.instHasKNatS5Grz.proof_1, mem_K := LO.Modal.Hilbert.instHasKNatS5Grz.proof_2 }

instance LO.Modal.Hilbert.instHasTNatS5Grz : Hilbert.S5Grz.HasT

Equations

• LO.Modal.Hilbert.instHasTNatS5Grz = { p := 0, mem_T := LO.Modal.Hilbert.instHasTNatS5Grz.proof_1 }

instance LO.Modal.Hilbert.instHasFiveNatS5Grz : Hilbert.S5Grz.HasFive

Equations

• LO.Modal.Hilbert.instHasFiveNatS5Grz = { p := 0, mem_Five := LO.Modal.Hilbert.instHasFiveNatS5Grz.proof_1 }

instance LO.Modal.Hilbert.instHasGrzNatS5Grz : Hilbert.S5Grz.HasGrz

Equations

• LO.Modal.Hilbert.instHasGrzNatS5Grz = { p := 0, mem_Grz := LO.Modal.Hilbert.instHasGrzNatS5Grz.proof_1 }

instance LO.Modal.Hilbert.instS5GrzNatFormulaS5Grz : Entailment.Modal.S5Grz Hilbert.S5Grz

Equations

• LO.Modal.Hilbert.instS5GrzNatFormulaS5Grz = LO.Entailment.Modal.S5Grz.mk

instance LO.Modal.Hilbert.instKTc'NatFormulaS5Grz : Entailment.Modal.KTc' Hilbert.S5Grz

Equations

• LO.Modal.Hilbert.instKTc'NatFormulaS5Grz = LO.Entailment.Modal.KTc'.mk

theorem LO.Modal.Hilbert.iff_provable_S5Grz_provable_Triv {φ : Formula ℕ} : Hilbert.S5Grz ⊢! φ ↔ Hilbert.Triv ⊢! φ