Fix typos (#6)

src/first_order/arithmetics.md

@@ -1,12 +1,12 @@
 # Arithmetics
 
-In this formalization, we prefer developping arithmetic _model theoretic_, i.e.
+In this formalization, we prefer developing arithmetic _model theoretic_, i.e.
 show $T \models \sigma$ instead of $T \vdash \sigma$ (They are equivalent thanks to the completeness theorem.). This approach has several advantages:
 
 1. In general, writing a formalized proof (in formalized system!) is very tedious. Meta-proofs, on the other hand, tend to be relatively concise.
 2. Many definitions and proofs of logic and algebra in Mathlib can be used.
 3. Metaprogramming can streamline the proof process (especially `definability`).
-4. It is easy to extend predicates and functions. When adding predicates or functions, it is necessary to extend its language by _extension by definition_ in case of formalized proof, but not in model theoretic approarch.
+4. It is easy to extend predicates and functions. When adding predicates or functions, it is necessary to extend its language by _extension by definition_ in case of formalized proof, but not in model theoretic approach.
 
 This procedure is done as follows.
 Suppose we wish to prove that the totality of an exponential function can be proved in $\mathsf{I}\Sigma_1$.
@@ -38,7 +38,7 @@ Since `Exponential` and `Exponential.total` are defined in all the model of $\ma
 
 ## Defined Predicates and Functions
 
-|               Predicate/Funcrion                | Notation                |                Defined in                |          Totality is proved in           | Complexity | Polynomial Bound |
+|               Predicate/Function                | Notation                |                Defined in                |          Totality is proved in           | Complexity | Polynomial Bound |
 | :---------------------------------------------: | :---------------------- | :--------------------------------------: | :--------------------------------------: | :--------: | :--------------: |
 |                       $0$                       | `0`                     |                 $\empty$                 |                 $\empty$                 | $\Sigma_0$ |       $0$        |
 |                       $1$                       | `1`                     |                 $\empty$                 |                 $\empty$                 | $\Sigma_0$ |       $1$        |

src/first_order/goedel1.md

@@ -31,7 +31,7 @@ This theorem is proved two distinct approach.
 - [G1 in `FirstIncompleteness.lean`](https://formalizedformallogic.github.io/Foundation/docs/Logic/FirstOrder/Incompleteness/FirstIncompleteness.html#LO.FirstOrder.Arith.first_incompleteness)
 - [G1 in `SelfReference.lean`](https://formalizedformallogic.github.io/Foundation/docs/Logic/FirstOrder/Incompleteness/SelfReference.html#LO.FirstOrder.Arith.FirstIncompletenessBySelfReference.not_complete)
 
-`FirstIncompleteness.lean` is computability theoretic proof, while `SelfReference.lean` uses a well-known self-referencial argument.
+`FirstIncompleteness.lean` is computability theoretic proof, while `SelfReference.lean` uses a well-known self-referential argument.
 
 ### G1 in `FirstIncompleteness.lean`
 

src/standard_modal/GL.md

@@ -2,7 +2,7 @@
 
 ## Logics Equivalent to GL
 
-Introduct Henkin Axiom `𝗛`, Löb Rule `(𝐋)`, Henkin Rule `(𝐇)`.
+Let's introduce Henkin Axiom `𝗛`, Löb Rule `(𝐋)`, Henkin Rule `(𝐇)`.
 
 ```lean
 protected abbrev H := □(□p ⟷ p) ⟶ □p
@@ -26,7 +26,7 @@ lemma reducible_K4Loeb_K4Henkin: 𝐊𝟒(𝐋) ≤ₛ 𝐊𝟒(𝐇)
 lemma reducible_K4Henkin_K4H : 𝐊𝟒(𝐇) ≤ₛ 𝐊𝟒𝐇
 lemma reducible_K4Henkin_GL : 𝐊𝟒𝐇 ≤ₛ 𝐆𝐋
 
---- Obviously `𝐆𝐋 =ₛ 𝐊𝟒(𝐋) =ₛ 𝐊𝟒(𝐇) =ₛ 𝐊𝟒𝐇`, since transivity of `≤ₛ` and definition of `=ₛ`.
+--- Obviously `𝐆𝐋 =ₛ 𝐊𝟒(𝐋) =ₛ 𝐊𝟒(𝐇) =ₛ 𝐊𝟒𝐇`, since transitivity of `≤ₛ` and definition of `=ₛ`.
 ```
 
 Note: `𝐊𝐇` (normal logic that axioms are `𝗞`, `𝗛`) is proper weak logic of `𝐆𝐋` and not Kripke complete.

src/standard_modal/README.md

@@ -5,7 +5,7 @@ As a general term for various modal logics commonly known as $\bf K$, $\bf S4$,
 > Be cautious similar notations for different concepts.
 > We use $\TeX$ notation for concept that unrelated to our formalization, and code block \`\` for related our formalization.
 > - $\sf K$ (`\sf K`) is axiom schema unrelated to formalization.
-> - $\bf K$ (`\bf K`) is logic urelated to formalization.
+> - $\bf K$ (`\bf K`) is logic unrelated to formalization.
 > - `𝗞` (Mathematical Sans-Serif Bold) is `AxiomSet` in formalization.
 > - `𝐊` (Mathematical Bold Capital) is `DeductionParameter` in formalization.
 

src/standard_modal/deduction.md

@@ -9,7 +9,7 @@ structure DeductionParameter (α) where
   nec : Bool
 ```
 
-- `axiomSet` is set of formula (aximos), For example, `𝗞`, `𝗞 ∪ 𝗧 ∪ 𝟰`.
+- `axiomSet` is set of formulas (axioms), For example, `𝗞`, `𝗞 ∪ 𝗧 ∪ 𝟰`.
 - `nec` is flag to contain necessitation rule.
 
 The parameter is called _Normal_ if `axiomSet` includes `𝗞` and `nec` is `true`.

src/superntuitionistic/deduction.md

@@ -8,7 +8,7 @@ structure DeductionParameter (α) where
   axiomSet : AxiomSet α
 ```
 
-- `axiomSet` is set of formula (aximos), For example, `𝗘𝗙𝗤`, `𝗘𝗙𝗤 ∪ 𝗟𝗘𝗠`.
+- `axiomSet` is set of formulas (axioms), For example, `𝗘𝗙𝗤`, `𝗘𝗙𝗤 ∪ 𝗟𝗘𝗠`.
 
 In this formalization, logics that we usually refer to as $\bf Int$ (Intuitionistic Propositional Logic), $\bf Cl$ (Classical Propositional Logic), etc. is characterized by deduction parameter.