rename

src/README.md

@@ -1,11 +1,11 @@
-# lean4-logic
+# Formalized Formal Logic
 
 [This project](https://github.com/FormalizedFormalLogic/Foundation) is aim to formalize some various results of mathematical logic in [Lean Theorem Prover](https://lean-lang.org).
 
 This book provides explanation and summaries of formalized concepts, theorems, propositions.
 Proofs of them are not explained, refer to the code or the [references](./references.md).
 
-Full documentation is [here](https://formalizedformallogic.github.io/Foundation/docs).
+Full documentation is [here](https://formalizedformallogic.github.io/Incompleteness/docs/).
 
 ## Main Results
 

src/first_order/notation.md

@@ -8,10 +8,12 @@ variables `x y z` is just an example and can take any number of `ident`s.
 ## Binder Notation
 
 Binder notation of term takes either form:
-- Term: `‘x y z | e’`, Formula: `“x y z | e”`
+- Term: `‘x y z. e’`, Formula: `“x y z. e”`
   - `x y z` is the symbol for the bound variables, `k:num`-variables denotes the terms in `Semiterm L ξ (n + $k)`/`Semiformula L ξ (n + $k)`. (`n` can be variable)
+- Term: `‘x y z | e’`, Formula: `“x y z | e”`
+  - `x y z` is the symbol for the free variables, `k:num`-variables denotes the terms in `Semiterm L ξ n`/`Semiformula L ξ n`. (`n` can be variable)
 - Term: `‘e’`, Formula: `“e”`
-  - An abbreviation of `‘ | e’`/`“ | e”`
+  - An abbreviation of `‘ . e’`/`“ . e”`
 
 
 ## Expression of term/formula