done.

Author: SnO2WMaN

Foundation.lean

@@ -477,27 +477,23 @@ public import Foundation.Propositional.Kripke.Hilbert.KreiselPutnam
 public import Foundation.Propositional.Kripke.Hilbert.LC
 public import Foundation.Propositional.Kripke.Preservation
 public import Foundation.Propositional.Kripke.Rooted
-public import Foundation.Propositional.Kripke2.AxiomCorfl
-public import Foundation.Propositional.Kripke2.AxiomHrd
-public import Foundation.Propositional.Kripke2.AxiomPCon
-public import Foundation.Propositional.Kripke2.AxiomPSCon
-public import Foundation.Propositional.Kripke2.AxiomRfl
-public import Foundation.Propositional.Kripke2.AxiomSer
-public import Foundation.Propositional.Kripke2.AxiomSym
-public import Foundation.Propositional.Kripke2.AxiomTra
+public import Foundation.Propositional.Kripke2.Axiom.Corfl
+public import Foundation.Propositional.Kripke2.Axiom.Hrd
+public import Foundation.Propositional.Kripke2.Axiom.PCon
+public import Foundation.Propositional.Kripke2.Axiom.PSCon
+public import Foundation.Propositional.Kripke2.Axiom.Rfl
+public import Foundation.Propositional.Kripke2.Axiom.Ser
+public import Foundation.Propositional.Kripke2.Axiom.Sym
+public import Foundation.Propositional.Kripke2.Axiom.Tra
 public import Foundation.Propositional.Kripke2.Basic
-public import Foundation.Propositional.Kripke2.FTheory
-public import Foundation.Propositional.Kripke2.Hilbert
-public import Foundation.Propositional.Kripke2.Logic
-public import Foundation.Propositional.Kripke2.Logic.F
-public import Foundation.Propositional.Kripke2.Logic.F_Rfl
-public import Foundation.Propositional.Kripke2.Logic.F_Rfl_Sym
-public import Foundation.Propositional.Kripke2.Logic.F_Rfl_Tra1
-public import Foundation.Propositional.Kripke2.Logic.F_Rfl_Tra1_Hrd
-public import Foundation.Propositional.Kripke2.Logic.F_Ser
-public import Foundation.Propositional.Kripke2.Logic.F_Sym
-public import Foundation.Propositional.Kripke2.Logic.F_Tra1
-public import Foundation.Propositional.Kripke2.Logic.F_Tra1_Hrd
+public import Foundation.Propositional.Kripke2.Hilbert.Basic
+public import Foundation.Propositional.Kripke2.Hilbert.F
+public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl
+public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Sym
+public import Foundation.Propositional.Kripke2.Hilbert.F_Rfl_Tra1
+public import Foundation.Propositional.Kripke2.Hilbert.F_Ser
+public import Foundation.Propositional.Kripke2.Hilbert.F_Sym
+public import Foundation.Propositional.Kripke2.Hilbert.F_Tra1
 public import Foundation.Propositional.Logic.Basic
 public import Foundation.Propositional.Logic.Letterless_Int_Cl
 public import Foundation.Propositional.Logic.PostComplete

…on/Propositional/Kripke2/AxiomCorfl.lean …n/Propositional/Kripke2/Axiom/Corfl.leanFoundation/Propositional/Kripke2/AxiomCorfl.lean renamed to Foundation/Propositional/Kripke2/Axiom/Corfl.lean Foundation/Propositional/Kripke2/AxiomCorfl.lean renamed to Foundation/Propositional/Kripke2/Axiom/Corfl.lean

@@ -1,6 +1,6 @@
 module
 
-public import Foundation.Propositional.Kripke2.AxiomSer
+public import Foundation.Propositional.Kripke2.Axiom.Ser
 
 @[expose] public section
 
@@ -44,12 +44,6 @@ lemma isReflexive_of_valid_axiomRfl (h : F ⊧ Axioms.Rfl #0 #1) : F.IsReflexive
       tauto;
   exact this;
 
-instance [Entailment.F L] [Entailment.HasAxiomRfl L] [Entailment.Disjunctive L] : Frame.IsReflexive (canonicalModel L).toFrame where
-  refl := by
-    rintro T φ ψ hφψ hφ;
-    apply T.imp_closed (show L ⊢ Axioms.Rfl φ ψ from by simp);
-    apply T.andIR <;> assumption;
-
 end Kripke2
 
 end LO.Propositional

…tion/Propositional/Kripke2/AxiomHrd.lean …ion/Propositional/Kripke2/Axiom/Hrd.leanFoundation/Propositional/Kripke2/AxiomHrd.lean renamed to Foundation/Propositional/Kripke2/Axiom/Hrd.lean Foundation/Propositional/Kripke2/AxiomHrd.lean renamed to Foundation/Propositional/Kripke2/Axiom/Hrd.lean

@@ -1,6 +1,6 @@
 module
 
-public import Foundation.Propositional.Kripke2.FTheory
+public import Foundation.Propositional.Kripke2.Basic
 public import Foundation.Vorspiel.Rel.Serial
 
 @[expose] public section
@@ -37,16 +37,6 @@ lemma isSerial_of_valid_axiomSer (h : F ⊧ Axioms.Ser) : F.IsSerial := by
   intro x;
   simpa [Satisfies] using @h (λ v a => True) F.root x F.rooted;
 
-instance [Entailment.F L] [Entailment.HasAxiomSer L] [Entailment.Disjunctive L] : Frame.IsSerial (canonicalModel L).toFrame where
-  serial := by
-    rintro T;
-    obtain ⟨U, _, _, _⟩ := FTheory.lindenbaum (T := T.toFTheory) $ show ∼⊤ ∉ T.theory by
-      by_contra hC;
-      apply T.no_bot;
-      apply T.imp_closed ?_ hC;
-      exact Entailment.Corsi.axiomSer;
-    use U;
-
 end Kripke2
 
 end LO.Propositional

…ion/Propositional/Kripke2/AxiomPCon.lean …on/Propositional/Kripke2/Axiom/PCon.leanFoundation/Propositional/Kripke2/AxiomPCon.lean renamed to Foundation/Propositional/Kripke2/Axiom/PCon.lean Foundation/Propositional/Kripke2/AxiomPCon.lean renamed to Foundation/Propositional/Kripke2/Axiom/PCon.lean

@@ -1,6 +1,6 @@
 module
 
-public import Foundation.Propositional.Kripke2.AxiomSer
+public import Foundation.Propositional.Kripke2.Axiom.Ser
 
 @[expose] public section
 

…on/Propositional/Kripke2/AxiomPSCon.lean …n/Propositional/Kripke2/Axiom/PSCon.leanFoundation/Propositional/Kripke2/AxiomPSCon.lean renamed to Foundation/Propositional/Kripke2/Axiom/PSCon.lean Foundation/Propositional/Kripke2/AxiomPSCon.lean renamed to Foundation/Propositional/Kripke2/Axiom/PSCon.lean

@@ -1,7 +1,6 @@
 module
 
-public import Foundation.Propositional.Kripke2.FTheory
-
+public import Foundation.Propositional.Kripke2.Axiom.Ser
 
 @[expose] public section
 
@@ -62,14 +61,6 @@ lemma TFAE_IsTransitive : [
   tfae_have 3 → 1 := IsTransitive_of_valid_axiomTra₂
   tfae_finish;
 
-instance [Entailment.F L] [Entailment.HasAxiomTra1 L] [Entailment.Disjunctive L] : Frame.IsTransitive (canonicalModel L).toFrame where
-  trans := by
-    rintro T U V RTU RUV φ ψ hφψ hφ;
-    apply RUV (RTU ?_ (show ⊤ ∈ U.theory by simp)) hφ;
-    apply T.imp_closed (φ := φ 🡒 ψ);
-    . exact Entailment.Corsi.axiomTra1;
-    . simpa;
-
 end Kripke2
 
 end LO.Propositional