Documentation

Foundation.Modal.Hilbert.S5Grz

class LO.Modal.Entailment.S5Grz {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] (𝓢 : S) extends LO.Modal.Entailment.S5 𝓢, LO.Modal.Entailment.HasAxiomGrz 𝓢 :
Type (max u_2 u_3)
Instances
def LO.Modal.Entailment.S5Grz.diaT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [DecidableEq F] [Entailment.S5Grz 𝓢] {φ : F} :
𝓢 φ φ
Equations
  • One or more equations did not get rendered due to their size.
Equations
  • One or more equations did not get rendered due to their size.