Grz

noncomputable def LO.Entailment.Grz.lemmaAxiomFourAxiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.Grz 𝓢] {φ : F} : 𝓢 ⊢ □φ ==> φ ⋏ (□φ ==> □□φ)

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.Grz.lemmaAxiomFourAxiomT = LO.Entailment.impTrans'' LO.Entailment.lemmaGrz₁ LO.Entailment.axiomGrz

noncomputable def LO.Entailment.Grz.axiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.Grz 𝓢] {φ : F} : 𝓢 ⊢ □φ ==> □□φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.Grz.axiomFour = LO.Entailment.ppq (LO.Entailment.impTrans'' LO.Entailment.Grz.lemmaAxiomFourAxiomT LO.Entailment.and₂)

@[implicit_reducible]

noncomputable instance LO.Entailment.Grz.instHasAxiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.Grz 𝓢] : HasAxiomFour 𝓢

Equations

• LO.Entailment.Grz.instHasAxiomFour = { Four := fun (x : F) => LO.Entailment.Grz.axiomFour }

noncomputable def LO.Entailment.Grz.axiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.Grz 𝓢] {φ : F} : 𝓢 ⊢ □φ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.Grz.axiomT = LO.Entailment.impTrans'' LO.Entailment.Grz.lemmaAxiomFourAxiomT LO.Entailment.and₁

@[implicit_reducible]

noncomputable instance LO.Entailment.Grz.instHasAxiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.Grz 𝓢] : HasAxiomT 𝓢

Equations

• LO.Entailment.Grz.instHasAxiomT = { T := fun (x : F) => LO.Entailment.Grz.axiomT }