S5Grz

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.lem₁DiaTOfS5Grz = LO.Entailment.impTrans'' (LO.Entailment.revDhypImp' LO.Entailment.diaDualityMp) (LO.Entailment.dhypImp' LO.Entailment.diaDualityMpr)

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.lem₂DiaTOfS5Grz = LO.Entailment.dhypImp' LO.Entailment.rmDiabox

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

Imported declaration from the Incompleteness formalization.

• mdp {φ ψ : F} : 𝓢 ⊢ φ ==> ψ → 𝓢 ⊢ φ → 𝓢 ⊢ ψ
• negEquiv (φ : 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 φ ψ
• diaDual (φ : 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] [Entailment.S5Grz 𝓢] {φ : F} : 𝓢 ⊢ ◇φ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• LO.Entailment.S5Grz.instKTc' = { toK := inst✝.toK, toHasAxiomDiaT := LO.Entailment.S5Grz.instHasAxiomDiaT }

@[reducible, inline]

abbrev LO.Modal.Hilbert.S5Grz : Hilbert ℕ

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.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 }

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

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

@[implicit_reducible]

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

Equations

• LO.Modal.Hilbert.instKTc'NatFormulaS5Grz = { toK := LO.Modal.Hilbert.instS5GrzNatFormulaS5Grz.toK, toHasAxiomDiaT := LO.Entailment.S5Grz.instHasAxiomDiaT }

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