KT

def LO.Entailment.KT.axiomDiaTc {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KT 𝓢] {φ : F} : 𝓢 ⊢ φ ==> ◇φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.KT.axiomDiaTc = LO.Entailment.impTrans'' (LO.Entailment.impTrans'' LO.Entailment.dni (LO.Entailment.contra₀' LO.Entailment.axiomT)) (LO.Entailment.and₂' LO.Entailment.diaDuality)

@[implicit_reducible]

instance LO.Entailment.KT.instHasAxiomDiaTc {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KT 𝓢] : HasAxiomDiaTc 𝓢

Equations

• LO.Entailment.KT.instHasAxiomDiaTc = { diaTc := fun (x : F) => LO.Entailment.KT.axiomDiaTc }

def LO.Entailment.KT.axiomP {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.KT 𝓢] : 𝓢 ⊢ ∼□⊥

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.KT.axiomP = LO.Entailment.negEquiv'.mpr LO.Entailment.axiomT

@[implicit_reducible]

instance LO.Entailment.KT.instHasAxiomP {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.KT 𝓢] : HasAxiomP 𝓢

Equations

• LO.Entailment.KT.instHasAxiomP = { P := LO.Entailment.KT.axiomP }

@[implicit_reducible]

instance LO.Entailment.KT.instKP {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.KT 𝓢] : Entailment.KP 𝓢

Equations

• LO.Entailment.KT.instKP = { toK := inst✝.toK, toHasAxiomP := LO.Entailment.KT.instHasAxiomP }

@[implicit_reducible]

instance LO.Entailment.KT.instKD {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KT 𝓢] : Entailment.KD 𝓢

Equations

• LO.Entailment.KT.instKD = { toK := inst✝.toK, toHasAxiomD := LO.Entailment.KP.instHasAxiomD }

def LO.Entailment.KT'.axiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KT' 𝓢] {φ : F} : 𝓢 ⊢ □φ ==> φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.KT'.axiomT = LO.Entailment.impTrans'' LO.Entailment.boxDni (LO.Entailment.contra₃' (LO.Entailment.impTrans'' LO.Entailment.diaTc LO.Entailment.diaDualityMp))

@[implicit_reducible]

instance LO.Entailment.KT'.instHasAxiomT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KT' 𝓢] : HasAxiomT 𝓢

Equations

• LO.Entailment.KT'.instHasAxiomT = { T := fun (x : F) => LO.Entailment.KT'.axiomT }

@[implicit_reducible]

instance LO.Entailment.KT'.instKT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KT' 𝓢] : Entailment.KT 𝓢

Equations

• LO.Entailment.KT'.instKT = { toK := inst✝.toK, toHasAxiomT := LO.Entailment.KT'.instHasAxiomT }

@[implicit_reducible]

instance LO.Entailment.KT'.instKD {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KT' 𝓢] : Entailment.KD 𝓢

Equations

• LO.Entailment.KT'.instKD = { toK := inst✝.toK, toHasAxiomD := LO.Entailment.KP.instHasAxiomD }