class LO.InterpretabilityLogic.Entailment.ILMinus_J1 {S : Type u_1} {F : Type u_2} [InterpretabilityLogicalConnective F] [Entailment S F] (𝓢 : S) extends LO.InterpretabilityLogic.Entailment.ILMinus 𝓢, LO.InterpretabilityLogic.Entailment.HasAxiomJ1 𝓢 : 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 φ
• axiomJ3! {φ ψ χ : F} : 𝓢 ⊢! Axioms.J3 φ ψ χ
• axiomJ6! {φ : F} : 𝓢 ⊢! Axioms.J6 φ
• R1! {φ ψ χ : F} : 𝓢 ⊢! φ 🡒 ψ → 𝓢 ⊢! χ ▷ φ 🡒 χ ▷ ψ
• R2! {φ ψ χ : F} : 𝓢 ⊢! φ 🡒 ψ → 𝓢 ⊢! ψ ▷ χ 🡒 φ ▷ χ
• axiomJ1! {φ ψ : F} : 𝓢 ⊢! Axioms.J1 φ ψ

@[implicit_reducible]

instance LO.InterpretabilityLogic.Entailment.instHasAxiomJ1' {S : Type u_1} {F : Type u_2} [InterpretabilityLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.ILMinus_J1 𝓢] : HasAxiomJ1' 𝓢

Equations

• LO.InterpretabilityLogic.Entailment.instHasAxiomJ1' = { axiomJ1'! := fun {φ : F} => LO.InterpretabilityLogic.Entailment.axiomJ1!⨀LO.Modal.Entailment.nec LO.Entailment.C_id }

class LO.InterpretabilityLogic.Entailment.ILMinus_J1' {S : Type u_1} {F : Type u_2} [InterpretabilityLogicalConnective F] [Entailment S F] (𝓢 : S) extends LO.InterpretabilityLogic.Entailment.ILMinus 𝓢, LO.InterpretabilityLogic.Entailment.HasAxiomJ1' 𝓢 : 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 φ
• axiomJ3! {φ ψ χ : F} : 𝓢 ⊢! Axioms.J3 φ ψ χ
• axiomJ6! {φ : F} : 𝓢 ⊢! Axioms.J6 φ
• R1! {φ ψ χ : F} : 𝓢 ⊢! φ 🡒 ψ → 𝓢 ⊢! χ ▷ φ 🡒 χ ▷ ψ
• R2! {φ ψ χ : F} : 𝓢 ⊢! φ 🡒 ψ → 𝓢 ⊢! ψ ▷ χ 🡒 φ ▷ χ
• axiomJ1'! {φ : F} : 𝓢 ⊢! Axioms.J1' φ

@[implicit_reducible]

instance LO.InterpretabilityLogic.Entailment.instHasAxiomJ1 {S : Type u_1} {F : Type u_2} [DecidableEq F] [InterpretabilityLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.ILMinus_J1' 𝓢] : HasAxiomJ1 𝓢

Equations

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