def LO.System.KD.axiomP {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.KD 𝓢] : 𝓢 ⊢ 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} [BasicModalLogicalConnective F] [DecidableEq F] [System F S] {𝓢 : S} [System.KD 𝓢] : HasAxiomP 𝓢

Equations

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