KTc

def LO.Entailment.KTc.axiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.KTc 𝓢] {φ : F} : 𝓢 ⊢ Axioms.Four φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.KTc.axiomFour = LO.Entailment.axiomTc

@[implicit_reducible]

instance LO.Entailment.KTc.instHasAxiomFour {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.KTc 𝓢] : HasAxiomFour 𝓢

Equations

• LO.Entailment.KTc.instHasAxiomFour = { Four := fun (x : F) => LO.Entailment.KTc.axiomFour }

def LO.Entailment.KTc.axiomFive {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.KTc 𝓢] {φ : F} : 𝓢 ⊢ ◇φ ==> □◇φ

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.KTc.axiomFive = LO.Entailment.axiomTc

@[implicit_reducible]

instance LO.Entailment.KTc.instHasAxiomFive {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [Entailment F S] {𝓢 : S} [Entailment.KTc 𝓢] : HasAxiomFive 𝓢

Equations

• LO.Entailment.KTc.instHasAxiomFive = { Five := fun (x : F) => LO.Entailment.KTc.axiomFive }

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

Imported declaration from the Incompleteness formalization.

Equations

• LO.Entailment.KTc.axiomDiaT = LO.Entailment.impTrans'' (LO.Entailment.and₁' LO.Entailment.diaDuality) (LO.Entailment.contra₂' LO.Entailment.axiomTc)

@[implicit_reducible]

instance LO.Entailment.KTc.instHasAxiomDiaT {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KTc 𝓢] : HasAxiomDiaT 𝓢

Equations

• LO.Entailment.KTc.instHasAxiomDiaT = { diaT := fun (x : F) => LO.Entailment.KTc.axiomDiaT }

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

Imported declaration from the Incompleteness formalization.

Equations

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

@[implicit_reducible]

instance LO.Entailment.KTc'.instHasAxiomTc {S : Type u_1} {F : Type u_2} [BasicModalLogicalConnective F] [DecidableEq F] [Entailment F S] {𝓢 : S} [Entailment.KTc' 𝓢] : HasAxiomTc 𝓢

Equations

• LO.Entailment.KTc'.instHasAxiomTc = { Tc := fun (x : F) => LO.Entailment.KTc'.axiomTc }