update README

FormalizedFormalLogic · Mar 29, 2024 · 37baae6 · 37baae6
1 parent 8888111
commit 37baae6
Showing 1 changed file with 20 additions and 14 deletions.
diff --git a/README.md b/README.md
@@ -1,6 +1,6 @@
 # Arithmetization
 
-Formalization of Arithmetization of Metamathematics.
+Formalization of Arithmetization of Metamathematics. This project depends on [lean4-logic](https://github.com/iehality/lean4-logic/tree/master).
 
 https://iehality.github.io/Arithmetization/
 
@@ -47,6 +47,7 @@ https://iehality.github.io/Arithmetization/
       (ind : ∀ (x : M), (∀ y < x, P y) → P x) (x : M) :
       P x
   ```
+
 - [Least number principle](https://iehality.github.io/Arithmetization/Arithmetization/Basic/Ind.html#LO.FirstOrder.Arith.Model.least_number_h)
   ```lean
   theorem LO.FirstOrder.Arith.Model.least_number_h
@@ -60,23 +61,28 @@ https://iehality.github.io/Arithmetization/
       {x : M} (h : P x) :
       ∃ (y : M), P y ∧ ∀ z < y, ¬P z
   ```
+
 - [$\mathbf{I\Sigma_n} = \mathbf{I\Pi_n}$](https://iehality.github.io/Arithmetization/Arithmetization/Basic/Ind.html#LO.FirstOrder.Arith.Model.models_iSigma_iff_models_iPi)
   ```lean
   theorem LO.FirstOrder.Arith.Model.models_iSigma_iff_models_iPi
       {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] {ν : ℕ} :
       M ⊧ₘ* 𝐈𝚺ν ↔ M ⊧ₘ* 𝐈𝚷ν
   ```
-- [Exponential is definable in $\mathbf{I\Delta_0}$ by $\mathbf{\Delta_0}$ formula](https://iehality.github.io/Arithmetization/Arithmetization/IDeltaZero/Exponential/Exp.html#LO.FirstOrder.Arith.Model.Exp.defined)
-  ```lean
-  theorem LO.FirstOrder.Arith.Model.Exp.defined
-      {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [LO.FirstOrder.Theory.Mod M 𝐈𝚫₀] :
-      Δ₀-Relation LO.FirstOrder.Arith.Model.Exp via LO.FirstOrder.Arith.Model.Exp.def
-  ```
+
+- Exponential is definable in $\mathbf{I\Delta_0}$ by $\mathbf{\Delta_0}$ formula
+  - [LO.FirstOrder.Arith.Model.Exp.defined](https://iehality.github.io/Arithmetization/Arithmetization/IDeltaZero/Exponential/Exp.html#LO.FirstOrder.Arith.Model.Exp.defined)
+    ```lean
+    theorem LO.FirstOrder.Arith.Model.Exp.defined
+        {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] [LO.FirstOrder.Theory.Mod M 𝐈𝚫₀] :
+        Δ₀-Relation LO.FirstOrder.Arith.Model.Exp via LO.FirstOrder.Arith.Model.Exp.def
+    ```
+
   - [Representation of $\mathbf{\Delta_0}$ definition of exponential](https://github.com/iehality/Arithmetization/blob/master/Arithmetization/IDeltaZero/Exponential/exp.pdf)
-- [Nuon (number of ones) is definable in $\mathbf{I\Delta_0 + \Omega_1}$ by $\mathbf{\Delta_0}$ formula](https://iehality.github.io/Arithmetization/Arithmetization/OmegaOne/Nuon.html#LO.FirstOrder.Arith.Model.nuon_defined)
-  ```lean
-  theorem LO.FirstOrder.Arith.Model.nuon_defined
-      {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
-      [LO.FirstOrder.Theory.Mod M 𝐈𝚫₀] [LO.FirstOrder.Theory.Mod M 𝛀₁] :
-      Δ₀-Function₁ LO.FirstOrder.Arith.Model.nuon via LO.FirstOrder.Arith.Model.nuonDef
-  ```
+- Nuon (number of ones) is definable in $\mathbf{I\Delta_0 + \Omega_1}$ by $\mathbf{\Delta_0}$ formula
+  - [LO.FirstOrder.Arith.Model.nuon_defined](https://iehality.github.io/Arithmetization/Arithmetization/OmegaOne/Nuon.html#LO.FirstOrder.Arith.Model.nuon_defined)
+    ```lean
+    theorem LO.FirstOrder.Arith.Model.nuon_defined
+        {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
+        [LO.FirstOrder.Theory.Mod M 𝐈𝚫₀] [LO.FirstOrder.Theory.Mod M 𝛀₁] :
+        Δ₀-Function₁ LO.FirstOrder.Arith.Model.nuon via LO.FirstOrder.Arith.Model.nuonDef
+    ```