def LO.System.KD.axiomP {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.KD 𝓢] : 𝓢 ⊢ LO.Axioms.P

Equations

• LO.System.KD.axiomP = LO.System.contra₀' LO.System.axiomD⨀(LO.System.contra₀' (LO.System.and₁' LO.System.diaDuality)⨀LO.System.dni' (LO.System.nec LO.System.notbot))

instance LO.System.KD.instHasAxiomP {S : Type u_1} {F : Type u_2} [LO.BasicModalLogicalConnective F] [DecidableEq F] [LO.System F S] {𝓢 : S} [LO.System.KD 𝓢] : LO.System.HasAxiomP 𝓢

Equations

• LO.System.KD.instHasAxiomP = { P := LO.System.KD.axiomP }