KP

def LO.Entailment.KP.axiomD {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KP 𝓢] {φ : F} : 𝓢 ⊢ Axioms.D φ

Imported declaration from the Incompleteness formalization.

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance LO.Entailment.KP.instHasAxiomD {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KP 𝓢] : HasAxiomD 𝓢

Equations

• LO.Entailment.KP.instHasAxiomD = { D := fun (x : F) => LO.Entailment.KP.axiomD }