class LO.InterpretabilityLogic.Entailment.ILM₀ {S : Type u_1} {F : Type u_2} [InterpretabilityLogicalConnective F] [Entailment S F] (𝓢 : S) extends LO.InterpretabilityLogic.Entailment.IL 𝓢, LO.InterpretabilityLogic.Entailment.HasAxiomM₀ 𝓢 : Type (max u_2 u_3)

• mdp {φ ψ : F} : 𝓢 ⊢! φ ➝ ψ → 𝓢 ⊢! φ → 𝓢 ⊢! ψ
• negEquiv {φ : F} : 𝓢 ⊢! Axioms.NegEquiv φ
• verum : 𝓢 ⊢! Axioms.Verum
• implyK {φ ψ : F} : 𝓢 ⊢! Axioms.ImplyK φ ψ
• implyS {φ ψ χ : F} : 𝓢 ⊢! Axioms.ImplyS φ ψ χ
• and₁ {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₁ φ ψ
• and₂ {φ ψ : F} : 𝓢 ⊢! Axioms.AndElim₂ φ ψ
• and₃ {φ ψ : F} : 𝓢 ⊢! Axioms.AndInst φ ψ
• or₁ {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₁ φ ψ
• or₂ {φ ψ : F} : 𝓢 ⊢! Axioms.OrInst₂ φ ψ
• or₃ {φ ψ χ : F} : 𝓢 ⊢! Axioms.OrElim φ ψ χ
• dne {φ : F} : 𝓢 ⊢! Axioms.DNE φ
• nec {φ : F} : 𝓢 ⊢! φ → 𝓢 ⊢! □φ
• K (φ ψ : F) : 𝓢 ⊢! Axioms.K φ ψ
• dia_dual (φ : F) : 𝓢 ⊢! Axioms.DiaDuality φ
• L (φ : F) : 𝓢 ⊢! Axioms.L φ
• axiomJ1! {φ ψ : F} : 𝓢 ⊢! Axioms.J1 φ ψ
• axiomJ2! {φ ψ χ : F} : 𝓢 ⊢! Axioms.J2 φ ψ χ
• axiomJ3! {φ ψ χ : F} : 𝓢 ⊢! Axioms.J3 φ ψ χ
• axiomJ4! {φ ψ : F} : 𝓢 ⊢! Axioms.J4 φ ψ
• axiomJ5! {φ : F} : 𝓢 ⊢! Axioms.J5 φ
• axiomM₀! {φ ψ χ : F} : 𝓢 ⊢! Axioms.M₀ φ ψ χ