Triv

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.Triv.axiomGrz = LO.Entailment.impTrans'' LO.Entailment.axiomT (LO.Entailment.pPqQ⨀LO.Entailment.nec LO.Entailment.axiomTc)

@[implicit_reducible]

instance LO.Entailment.Triv.instHasAxiomGrz {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.Triv 𝓢] : HasAxiomGrz 𝓢

Equations

• LO.Entailment.Triv.instHasAxiomGrz = { Grz := fun (x : F) => LO.Entailment.Triv.axiomGrz }