file restructure

Author: SnO2WMaN

SeqPL.lean

@@ -1,17 +1,29 @@
-module  -- shake: keep-all
+module  -- shake: keep-all --deprecated_module: ignore
 
-public import SeqPL.Arithmetic.Interpret
-public import SeqPL.Classification.Letterless
+public import SeqPL.DFormula.Basic
 public import SeqPL.Formula.Basic
 public import SeqPL.Formula.Letterless
 public import SeqPL.Gentzen.Basic
 public import SeqPL.Gentzen.WithCut
 public import SeqPL.Hilbert.Basic
 public import SeqPL.Kripke.Basic
 public import SeqPL.Kripke.Gentzen
+public import SeqPL.Kripke.PointGenerate
 public import SeqPL.Kripke.Rank
 public import SeqPL.Kripke.RootExtension
--- public import SeqPL.Kripke.Tail
+public import SeqPL.Kripke.Tail
 public import SeqPL.Logic.Basic
+public import SeqPL.Logic.D.Basic
+public import SeqPL.Logic.GL.Basic
+public import SeqPL.Logic.GLPlusBoxBot.Basic
+public import SeqPL.Logic.S.Basic
 public import SeqPL.Logic.SumQuasiNormal
+public import SeqPL.ProvabilityLogic.Classification.Full
+public import SeqPL.ProvabilityLogic.Classification.Letterless
+public import SeqPL.ProvabilityLogic.GL.Basic
+public import SeqPL.ProvabilityLogic.GLPlusBoxBot.Basic
+public import SeqPL.ProvabilityLogic.Interpret
+public import SeqPL.ProvabilityLogic.SolovaySentences
+public import SeqPL.Tait.Basic
 public import SeqPL.Vorspiel.CWF
+public import SeqPL.Vorspiel.Set.Cofinite

SeqPL/Arithmetic/Completeness.lean

@@ -11,41 +11,4 @@ variable {α : Type u}
 
 abbrev Logic (α) := Set (Formula α)
 
-abbrev LogicGL (α) : Logic α := { A | ⊢ʰ A }
-
-theorem LogicGL_TFAE [DecidableEq α] {A : Formula α} : [
-  A ∈ LogicGL α,
-  ⊢ʰ A,
-  ⊢ᵍ (∅ ⟹ {A}),
-  ⊢ᵍᶜ (∅ ⟹ {A}),
-  ∀ {κ : Type u}, [Nonempty κ] → ∀ M : Model κ α, [M.IsFiniteGL] → M ⊧ A
-].TFAE
-  := by
-  tfae_have 1 ↔ 2 := by grind;
-  tfae_have 2 → 3 := ProvableGentzen.of_provableHilbert;
-  tfae_have 3 → 2 := by
-    intro h;
-    simpa using ProvableHilbert.mdp (ProvableHilbert.of_provableGentzen (S := ∅ ⟹ {A}) h) (by simp);
-  tfae_have 3 → 4 := GentzenWithCutProvable.of_without_cut;
-  tfae_have 4 → 3 := ProvableGentzen.of_with_cut;
-  tfae_have 2 → 5 := by
-    intro h κ _;
-    apply ProvableHilbert.Kripke.finite_soundness h;
-  tfae_have 5 → 2 := ProvableHilbert.Kripke.completeness;
-  tfae_finish;
-
-theorem LogicGL_semantical_TFAE [DecidableEq α] {A : Formula α} : [
-  A ∈ LogicGL α,
-  ∀ {κ : Type u}, [Nonempty κ] → ∀ M : Model κ α, [M.IsFiniteGL] → M ⊧ A,
-  ∀ {κ : Type u}, [Nonempty κ] → ∀ M : RootedModel κ α, [M.IsFiniteGL] → M.root.1 ⊩ A
-].TFAE := by
-  tfae_have 1 ↔ 2 := LogicGL_TFAE.out 0 4;
-  tfae_have 2 → 3 := by
-    intro h κ _ M _;
-    apply h;
-  tfae_have 3 → 2 := by
-    intro h κ _ M _ x;
-    exact Model.toRootedModel.forces_same_at_root.mp $ h (M.toRootedModel x);
-  tfae_finish;
-
 end

SeqPL/Arithmetic/Soundness.lean

@@ -0,0 +1,24 @@
+module
+
+public import SeqPL.Logic.SumQuasiNormal
+public import SeqPL.Logic.S.Basic
+
+@[expose]
+public section
+
+abbrev LogicD {α} : Logic α := (LogicGL) +ᴸ (insert (∼□⊥) { □(□A ⋎ □B) 🡒 (□A ⋎ □B) | (A) (B) })
+
+lemma LogicS_subset_LogicD : LogicD (α := α) ⊆ LogicS := by
+  intro A h;
+  induction h with
+  | mem₁ h => apply Logic.sumQuasiNormal.mem₁; exact h
+  | mdp h₁ h₂ ih₁ ih₂ => apply Logic.sumQuasiNormal.mdp; exact ih₁; exact ih₂
+  | subst h ih => apply Logic.sumQuasiNormal.subst; exact ih
+  | mem₂ h =>
+    rcases h with (rfl | ⟨A, B, rfl⟩);
+    . apply Logic.sumQuasiNormal.mem₂;
+      use ⊥;
+    . apply Logic.sumQuasiNormal.mem₂;
+      use (□A ⋎ □B);
+
+end

SeqPL/Logic/Basic.lean

@@ -0,0 +1,50 @@
+module
+
+public import SeqPL.Logic.SumQuasiNormal
+public import SeqPL.Hilbert.Basic
+public import SeqPL.Kripke.PointGenerate
+public import Mathlib.Tactic.TFAE
+
+@[expose]
+public section
+
+variable {α : Type u}
+
+abbrev LogicGL {α} : Logic α := { A | ⊢ʰ A }
+
+theorem LogicGL_TFAE [DecidableEq α] {A : Formula α} : [
+  A ∈ LogicGL,
+  ⊢ʰ A,
+  ⊢ᵍ (∅ ⟹ {A}),
+  ⊢ᵍᶜ (∅ ⟹ {A}),
+  ∀ {κ : Type u}, [Nonempty κ] → ∀ M : Model κ α, [M.IsFiniteGL] → M ⊧ A
+].TFAE
+  := by
+  tfae_have 1 ↔ 2 := by grind;
+  tfae_have 2 → 3 := ProvableGentzen.of_provableHilbert;
+  tfae_have 3 → 2 := by
+    intro h;
+    simpa using ProvableHilbert.mdp (ProvableHilbert.of_provableGentzen (S := ∅ ⟹ {A}) h) (by simp);
+  tfae_have 3 → 4 := GentzenWithCutProvable.of_without_cut;
+  tfae_have 4 → 3 := ProvableGentzen.of_with_cut;
+  tfae_have 2 → 5 := by
+    intro h κ _;
+    apply ProvableHilbert.Kripke.finite_soundness h;
+  tfae_have 5 → 2 := ProvableHilbert.Kripke.completeness;
+  tfae_finish;
+
+theorem LogicGL_semantical_TFAE [DecidableEq α] {A : Formula α} : [
+  A ∈ LogicGL,
+  ∀ {κ : Type u}, [Nonempty κ] → ∀ M : Model κ α, [M.IsFiniteGL] → M ⊧ A,
+  ∀ {κ : Type u}, [Nonempty κ] → ∀ M : RootedModel κ α, [M.IsFiniteGL] → M.root.1 ⊩ A
+].TFAE := by
+  tfae_have 1 ↔ 2 := LogicGL_TFAE.out 0 4;
+  tfae_have 2 → 3 := by
+    intro h κ _ M _;
+    apply h;
+  tfae_have 3 → 2 := by
+    intro h κ _ M _ x;
+    exact Model.toRootedModel.forces_same_at_root.mp $ h (M.toRootedModel x);
+  tfae_finish;
+
+end

SeqPL/Logic/D/Basic.lean

@@ -0,0 +1,33 @@
+module
+
+public import Foundation.FirstOrder.Incompleteness.ProvabilityAbstraction.Height
+public import SeqPL.Logic.GL.Basic
+public import SeqPL.Logic.SumQuasiNormal
+
+@[expose] public section
+
+open Classical
+open LO
+open LO.FirstOrder.ProvabilityAbstraction
+
+def LogicGLPlusBoxBot {α} : ℕ∞ → Logic α
+  | .some n => LogicGL +ᴸ □^[n]⊥
+  | .none   => LogicGL
+
+lemma LogicGLPlusBoxBot.iff_provable_provable_GL {n : ℕ} : A ∈ LogicGLPlusBoxBot n ↔ (□^[n]⊥ 🡒 A) ∈ LogicGL := by
+  constructor;
+  . intro h;
+    induction h with
+    | mem₁ hA =>
+      sorry;
+    | mem₂ hB =>
+      sorry;
+    | mdp _ _ ihAB ihA =>
+      sorry;
+    | subst _ ihA => sorry;
+  . intro h;
+    apply Logic.sumQuasiNormal.mdp;
+    . exact Logic.sumQuasiNormal.mem₁ h;
+    . exact Logic.sumQuasiNormal.mem₂ rfl;
+
+end

SeqPL/Logic/GL/Basic.lean

@@ -0,0 +1,11 @@
+module
+
+public import SeqPL.Logic.SumQuasiNormal
+public import SeqPL.Logic.GL.Basic
+
+@[expose]
+public section
+
+abbrev LogicS {α} : Logic α := (LogicGL) +ᴸ ({ □A 🡒 A | A })
+
+end