Algebraic hauptsatz (#170)

* wip

* fix

* forces

* rm

* main

* refactor

Foundation/FirstOrder/Basic/Calculus.lean

@@ -495,6 +495,25 @@ def exOfInstances' (v : List (SyntacticTerm L)) (φ : SyntacticSemiformula L 1)
 
 end Derivation
 
+def newVar (Γ : Sequent L) : ℕ := (Γ.map Semiformula.fvSup).foldr max 0
+
+lemma not_fvar?_newVar {φ : SyntacticFormula L} {Γ : Sequent L} (h : φ ∈ Γ) : ¬FVar? φ (newVar Γ) :=
+  not_fvar?_of_lt_fvSup φ (by simpa[newVar] using List.le_max_of_le (List.mem_map_of_mem _ h) (by simp))
+
+namespace Derivation
+
+open Semiformula
+variable {P : SyntacticFormula L → Prop} {T : Theory L} {Δ : Sequent L}
+
+def allNvar {φ} (h : ∀' φ ∈ Δ) : T ⟹ φ/[&(newVar Δ)] :: Δ → T ⟹ Δ := fun b ↦
+  let b : T ⟹ (∀' φ) :: Δ :=
+    genelalizeByNewver (by simpa[FVar?] using not_fvar?_newVar h) (fun _ ↦ not_fvar?_newVar) b
+  Tait.wk b (by simp[h])
+
+protected def id {φ} (hp : φ ∈ T) : T ⟹ ∼∀∀ φ :: Δ → T ⟹ Δ := fun b ↦ Tait.cut (Tait.wk (toClose (root hp)) (by simp)) b
+
+end Derivation
+
 namespace Theory
 
 instance {T U : Theory L} : T ≼ T + U := System.Axiomatized.subtheoryOfSubset (by simp [add_def])

Foundation/FirstOrder/Completeness/Coding.lean

@@ -7,25 +7,6 @@ namespace FirstOrder
 open Semiformula
 variable {L : Language.{u}}
 
-def newVar (Γ : Sequent L) : ℕ := (Γ.map Semiformula.fvSup).foldr max 0
-
-lemma not_fvar?_newVar {φ : SyntacticFormula L} {Γ : Sequent L} (h : φ ∈ Γ) : ¬FVar? φ (newVar Γ) :=
-  not_fvar?_of_lt_fvSup φ (by simpa[newVar] using List.le_max_of_le (List.mem_map_of_mem _ h) (by simp))
-
-namespace Derivation
-
-open Semiformula
-variable {P : SyntacticFormula L → Prop} {T : Theory L} {Δ : Sequent L}
-
-def allNvar {φ} (h : ∀' φ ∈ Δ) : T ⟹ φ/[&(newVar Δ)] :: Δ → T ⟹ Δ := fun b ↦
-  let b : T ⟹ (∀' φ) :: Δ :=
-    genelalizeByNewver (by simpa[FVar?] using not_fvar?_newVar h) (fun _ ↦ not_fvar?_newVar) b
-  Tait.wk b (by simp[h])
-
-protected def id {φ} (hp : φ ∈ T) : T ⟹ ∼∀∀ φ :: Δ → T ⟹ Δ := fun b ↦ Tait.cut (Tait.wk (toClose (root hp)) (by simp)) b
-
-end Derivation
-
 namespace System
 
 inductive Code (L : Language.{u})