refactor

src/SUMMARY.md

@@ -24,9 +24,9 @@
   - [Completeness](./first_order/completeness.md)
   - [Arithmetics](./first_order/arithmetics.md)
     - [Theories of Arithmetics](./first_order/arithmetic_theories.md)
-    - [Gödel's First Incompleteness Theorem](./first_order/goedel1.md)
     - [Theory IΣ₀](./first_order/isigma0.md)
     - [Theory IΣ₁](./first_order/isigma1.md)
+    - [Gödel's First Incompleteness Theorem](./first_order/goedel1.md)
     - [Gödel's Second Incompleteness Theorem](./first_order/goedel2.md)
   - [Interpretation](./first_order/interpretation.md)
 

src/first_order/goedel1.md

@@ -1,15 +1,13 @@
 # Gödel's First Incompleteness Theorem
 
-An outline of the formalized proof of Gödel's first incompleteness theorem.
-
-## Definition
-
 A deduction system $\mathcal{S}$ is _complete_ iff it can prove or refute every sentence $\sigma$.
 Otherwise, $\mathcal{S}$ is _incomplete_.
 
 ```lean
-def LO.System.Complete : Prop := ∀ f, 𝓢 ⊢! f ∨ 𝓢 ⊢! ~f
+def System.Complete {F S} [System F S] [LogicalConnective F] (𝓢 : S) : Prop :=
+    ∀ f, 𝓢 ⊢! f ∨ 𝓢 ⊢! ~f
 ```
+- [System.Complete](https://formalizedformallogic.github.io/Incompleteness/docs/Logic/Logic/System.html#LO.System.Complete)
 
 ## Theorem
 

src/first_order/goedel2.md

@@ -1,7 +1,5 @@
 # Gödel's Second Incompleteness Theorem
 
-_These results are/will be included in [Arithmetization](https://github.com/iehality/Arithmetization/tree/master)._
-
 Recall that inside $\mathsf{I}\Sigma_1$ we can do basic set theory and primitive recursion.
 Many inductive notions and functions on them are defined in $\Delta_1$ or $\Sigma_1$ using 
 the [fixpoint construction](./isigma1.md#fixpoint).
@@ -242,8 +240,13 @@ $$
 #### Lemma: Gödel sentence is undecidable, i.e., $T \nvdash \mathrm{G}$ if $T$ is consistent, and $T \nvdash \lnot\mathrm{G}$ if $\mathbb{N} \models T$.
 
 ```lean
-lemma goedel_unprovable [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] : T ⊬ ↑𝗚
-lemma not_goedel_unprovable [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] : T ⊬ ∼↑𝗚
+lemma goedel_unprovable
+    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] :
+    T ⊬ ↑𝗚
+
+lemma not_goedel_unprovable
+    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] :
+    T ⊬ ∼↑𝗚
 ```
 - [goedel_unprovable](https://formalizedformallogic.github.io/Incompleteness/docs/Incompleteness/Arith/Second.html#LO.FirstOrder.Arith.goedel_unprovable)
 - [not_goedel_unprovable](https://formalizedformallogic.github.io/Incompleteness/docs/Incompleteness/Arith/Second.html#LO.FirstOrder.Arith.not_goedel_unprovable)
@@ -255,15 +258,22 @@ $$
 
 #### Lemma: $T \vdash \mathrm{Con}_T \leftrightarrow G_T$
 ```lean
-lemma consistent_iff_goedel [𝐈𝚺₁ ≼ T] [T.Delta1Definable] : T ⊢! ↑𝗖𝗼𝗻 ⭤ ↑𝗚
+lemma consistent_iff_goedel
+    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] :
+    T ⊢! ↑𝗖𝗼𝗻 ⭤ ↑𝗚
 ```
 - [consistent_iff_goedel](https://formalizedformallogic.github.io/Incompleteness/docs/Incompleteness/Arith/Second.html#LO.FirstOrder.Arith.consistent_iff_goedel)
 
 #### Theorem: $T$ cannot prove its own consistency, i.e., $T \nvdash \mathrm{Con}_T$ if $T$ is consistent. Moreover, $\mathrm{Con}_T$ is undecidable from $T$ if $\mathbb{N} \models T$.
 
 ```lean
-theorem goedel_second_incompleteness [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] : T ⊬ ↑𝗖𝗼𝗻 
-theorem inconsistent_undecidable [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] : System.Undecidable T ↑𝗖𝗼𝗻
+theorem goedel_second_incompleteness
+    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [System.Consistent T] :
+    T ⊬ ↑𝗖𝗼𝗻 
+
+theorem inconsistent_undecidable
+    (T : Theory ℒₒᵣ) [𝐈𝚺₁ ≼ T] [T.Delta1Definable] [ℕ ⊧ₘ* T] :
+    System.Undecidable T ↑𝗖𝗼𝗻
 ```
 - [goedel_second_incompleteness](https://formalizedformallogic.github.io/Incompleteness/docs/Incompleteness/Arith/Second.html#LO.FirstOrder.Arith.goedel_second_incompleteness)
 - [inconsistent_undecidable](https://formalizedformallogic.github.io/Incompleteness/docs/Incompleteness/Arith/Second.html#LO.FirstOrder.Arith.inconsistent_undecidable)