Documentation

LeanPool.Incompleteness.Foundation.Modal.Entailment.KD

KD #

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

Imported declaration from the Incompleteness formalization.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    @[implicit_reducible]
    instance LO.Entailment.KD.instHasAxiomP {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KD 𝓢] :
    HasAxiomP 𝓢
    Equations