class LO.InterpretabilityLogic.Entailment.IL_Rstar {S : Type u_1} {F : Type u_2} [InterpretabilityLogicalConnective F] [Entailment S F] (𝓢 : S) extends LO.InterpretabilityLogic.Entailment.IL 𝓢, LO.InterpretabilityLogic.Entailment.HasAxiomRstar 𝓢 : 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 φ
• axiomRstar! {φ ψ χ : F} : 𝓢 ⊢! Axioms.Rstar φ ψ χ

instance LO.InterpretabilityLogic.Entailment.instHasAxiomR {S : Type u_1} {F : Type u_2} [DecidableEq F] [InterpretabilityLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.IL_Rstar 𝓢] : HasAxiomR 𝓢

Equations

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

instance LO.InterpretabilityLogic.Entailment.instIL_R {S : Type u_1} {F : Type u_2} [DecidableEq F] [InterpretabilityLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.IL_Rstar 𝓢] : Entailment.IL_R 𝓢

Equations

• LO.InterpretabilityLogic.Entailment.instIL_R = { toIL := inst✝.toIL, toHasAxiomR := LO.InterpretabilityLogic.Entailment.instHasAxiomR }

instance LO.InterpretabilityLogic.Entailment.instHasAxiomW_1 {S : Type u_1} {F : Type u_2} [DecidableEq F] [InterpretabilityLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.IL_Rstar 𝓢] : HasAxiomW 𝓢

E. Goris & J. Joosten 2011, Lemma 4.5

Equations

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

instance LO.InterpretabilityLogic.Entailment.instIL_W {S : Type u_1} {F : Type u_2} [DecidableEq F] [InterpretabilityLogicalConnective F] [Entailment S F] {𝓢 : S} [Entailment.IL_Rstar 𝓢] : Entailment.IL_W 𝓢

Equations

• LO.InterpretabilityLogic.Entailment.instIL_W = { toIL := inst✝.toIL, toHasAxiomW := LO.InterpretabilityLogic.Entailment.instHasAxiomW_1 }