refactor: Remove InterpretabilityLogic (#831)

Co-authored-by: Claude Opus 4.8 <noreply@anthropic.com>

Author: SnO2WMaN

Foundation.lean

@@ -120,72 +120,6 @@ public import Foundation.FirstOrder.SetTheory.Z
 public import Foundation.FirstOrder.Skolemization.Hull
 public import Foundation.FirstOrder.Ultraproduct
 public import Foundation.Init
-public import Foundation.InterpretabilityLogic.Axioms
-public import Foundation.InterpretabilityLogic.Entailment
-public import Foundation.InterpretabilityLogic.Entailment.Basic
-public import Foundation.InterpretabilityLogic.Entailment.CL
-public import Foundation.InterpretabilityLogic.Entailment.IL
-public import Foundation.InterpretabilityLogic.Entailment.ILMinus
-public import Foundation.InterpretabilityLogic.Entailment.ILMinus_J1
-public import Foundation.InterpretabilityLogic.Entailment.ILMinus_J2
-public import Foundation.InterpretabilityLogic.Entailment.ILMinus_J4
-public import Foundation.InterpretabilityLogic.Entailment.ILMinus_J5
-public import Foundation.InterpretabilityLogic.Entailment.ILMinus_M
-public import Foundation.InterpretabilityLogic.Entailment.IL_KW1Zero
-public import Foundation.InterpretabilityLogic.Entailment.IL_KW2
-public import Foundation.InterpretabilityLogic.Entailment.IL_M
-public import Foundation.InterpretabilityLogic.Entailment.IL_M₀
-public import Foundation.InterpretabilityLogic.Entailment.IL_M₀_W
-public import Foundation.InterpretabilityLogic.Entailment.IL_P
-public import Foundation.InterpretabilityLogic.Entailment.IL_R
-public import Foundation.InterpretabilityLogic.Entailment.IL_R_W
-public import Foundation.InterpretabilityLogic.Entailment.IL_Rstar
-public import Foundation.InterpretabilityLogic.Entailment.IL_W
-public import Foundation.InterpretabilityLogic.Entailment.IL_Wstar
-public import Foundation.InterpretabilityLogic.Formula.Basic
-public import Foundation.InterpretabilityLogic.Formula.OfModal
-public import Foundation.InterpretabilityLogic.Formula.Substitution
-public import Foundation.InterpretabilityLogic.Formula.ToModal
-public import Foundation.InterpretabilityLogic.Hilbert.Axiom
-public import Foundation.InterpretabilityLogic.Hilbert.Basic.Basic
-public import Foundation.InterpretabilityLogic.Hilbert.Basic_Minimal
-public import Foundation.InterpretabilityLogic.Hilbert.Minimal.Basic
-public import Foundation.InterpretabilityLogic.Logic.Basic
-public import Foundation.InterpretabilityLogic.LogicSymbol
-public import Foundation.InterpretabilityLogic.Veltman.AxiomJ1
-public import Foundation.InterpretabilityLogic.Veltman.AxiomJ2
-public import Foundation.InterpretabilityLogic.Veltman.AxiomJ4
-public import Foundation.InterpretabilityLogic.Veltman.AxiomJ5
-public import Foundation.InterpretabilityLogic.Veltman.AxiomM
-public import Foundation.InterpretabilityLogic.Veltman.AxiomM₀
-public import Foundation.InterpretabilityLogic.Veltman.AxiomP
-public import Foundation.InterpretabilityLogic.Veltman.AxiomR
-public import Foundation.InterpretabilityLogic.Veltman.AxiomW
-public import Foundation.InterpretabilityLogic.Veltman.Basic
-public import Foundation.InterpretabilityLogic.Veltman.Hilbert
-public import Foundation.InterpretabilityLogic.Veltman.Logic.CL
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J2
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J2_J5
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J4Plus
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J4Plus_J5
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J1_J5
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J2Plus
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J2Plus_J5
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J4Plus
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J4Plus_J5
-public import Foundation.InterpretabilityLogic.Veltman.Logic.ILMinus_J5
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_F
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_M
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_M₀
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_M₀_W
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_P
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_P₀
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_R
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_R_W
-public import Foundation.InterpretabilityLogic.Veltman.Logic.IL_W
 public import Foundation.LinearLogic.FirstOrder.Calculus
 public import Foundation.LinearLogic.FirstOrder.ClassicalEmbedding
 public import Foundation.LinearLogic.FirstOrder.Formula