Skip to content

Commit

Permalink
fix
Browse files Browse the repository at this point in the history
  • Loading branch information
@iehality
iehality committed Aug 16, 2024
1 parent d67f6e1 commit 61719af
Show file tree
Hide file tree
Showing 3 changed files with 43 additions and 43 deletions.
60 changes: 30 additions & 30 deletions src/first_order/arithmetics.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -81,33 +81,33 @@ Since `Exponential` and `Exponential.total` are defined in all the model of $\ma
| $\mathrm{Semiformula}_x(y)$ | [`L.Semiformula x y`] | $\mathsf{I}\Sigma_1$ | - | $\Delta_1$ | - |

[`x ≤ y`]: https://formalizedformallogic.github.io/Foundation/docs/Logic/FirstOrder/Arith/PeanoMinus.html#LO.Arith.instLE_logic
[`x - y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/PeanoMinus.html#LO.Arith.sub
[`x ∣ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/PeanoMinus.html#LO.FirstOrder.Arith.dvd
[`x / y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.instDiv_arithmetization
[`x % y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.rem
[`√x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.sqrt
[`⟪x, y⟫`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.pair
[`π₁ x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.pi%E2%82%81
[`π₂ x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/Basic/IOpen.html#LO.Arith.pi%E2%82%82
[`exp x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.Exponential
[`log x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Log.html#LO.Arith.log
[`‖x‖`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Log.html#LO.Arith.binaryLength
[`x # y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/OmegaOne/Basic.html#LO.Arith.instHash
[`nuon x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/OmegaOne/Nuon.html#LO.Arith.nuon
[`x ∈ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.Arith.Bit
[`∅`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.Arith.instEmptyCollection_arithmetization
[`x ⊆ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.Arith.instHasSubset_arithmetization
[`⋃ʰᶠ x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.sUnion
[`x ∪ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.union
[`x ∩ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.inter
[`⋂ʰᶠ x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.sInter
[`x ×ʰᶠ y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.product
[`domain x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.domain
[`IsMapping x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.IsMapping
[`Seq x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.Seq
[`lh x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.lh
[`x ⁀' y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.seqCons
[`znth x`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.znth
[`L.Semiterm x y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Metamath/Term/Basic.html#LO.Arith.Language.Semiterm
[`L.termSubst n m w t`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Metamath/Term/Functions.html#LO.Arith.Language.termSubst
[`L.Semiformula x y`]: https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Metamath/Formula/Basic.html#LO.Arith.Language.Semiformula
[`x - y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/PeanoMinus.html#LO.Arith.sub
[`x ∣ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/PeanoMinus.html#LO.FirstOrder.Arith.dvd
[`x / y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.instDiv_arithmetization
[`x % y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.rem
[`√x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.sqrt
[`⟪x, y⟫`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.pair
[`π₁ x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.pi%E2%82%81
[`π₂ x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/Basic/IOpen.html#LO.Arith.pi%E2%82%82
[`exp x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.Exponential
[`log x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Log.html#LO.Arith.log
[`‖x‖`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Log.html#LO.Arith.binaryLength
[`x # y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/OmegaOne/Basic.html#LO.Arith.instHash
[`nuon x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/OmegaOne/Nuon.html#LO.Arith.nuon
[`x ∈ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.Bit
[`∅`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.instEmptyCollection_arithmetization
[`x ⊆ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.instHasSubset_arithmetization
[`⋃ʰᶠ x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.sUnion
[`x ∪ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.union
[`x ∩ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.inter
[`⋂ʰᶠ x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.sInter
[`x ×ʰᶠ y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.product
[`domain x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.domain
[`IsMapping x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.IsMapping
[`Seq x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.Seq
[`lh x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.lh
[`x ⁀' y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.seqCons
[`znth x`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.znth
[`L.Semiterm x y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Metamath/Term/Basic.html#LO.Arith.Language.Semiterm
[`L.termSubst n m w t`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Metamath/Term/Functions.html#LO.Arith.Language.termSubst
[`L.Semiformula x y`]: https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Metamath/Formula/Basic.html#LO.Arith.Language.Semiformula
6 changes: 3 additions & 3 deletions src/first_order/isigma0.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -11,7 +11,7 @@ and its inductive properties are proved in $\mathsf{I}\Sigma_0$.
instance exponential_definable [M ⊧ₘ* 𝐈𝚺₀] : 𝚺₀-Relation (Exponential : M → M → Prop)
```

- [LO.FirstOrder.Arith.Model.exponential_definable](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.FirstOrder.Arith.Model.exponential_definable)
- [LO.Arith.exponential_definable](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.exponential_definable)

![Import Graph](./exp.png)

Expand All @@ -20,13 +20,13 @@ lemma exponential_zero_one [M ⊧ₘ* 𝐈𝚺₀] :
Exponential 0 1
```

- [LO.FirstOrder.Arith.Model.Exponential.exponential_zero_one](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.FirstOrder.Arith.Model.Exponential.exponential_zero_one)
- [LO.Arith.Exponential.exponential_zero_one](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.Exponential.exponential_zero_one)

```lean
lemma exponential_succ_mul_two [M ⊧ₘ* 𝐈𝚺₀] {x y : M} :
Exponential (x + 1) (2 * y) ↔ Exponential x y
```

- [LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_two](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.FirstOrder.Arith.Model.Exponential.exponential_succ_mul_two)
- [LO.Arith.Exponential.exponential_succ_mul_two](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaZero/Exponential/Exp.html#LO.Arith.Exponential.exponential_succ_mul_two)

Other basic functions, such as $\log x, |x|$ are defined by using exponential.
20 changes: 10 additions & 10 deletions src/first_order/isigma1.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ Weak theory of sets in $V_\omega$ (Hereditary Finite Sets) can be developed insi
lemma mem_iff_bit [M ⊧ₘ* 𝐈𝚺₁] {i a : M} : i ∈ a ↔ Bit i a
```

- [LO.FirstOrder.Arith.Model.mem_iff_bit](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.FirstOrder.Arith.Model.mem_iff_bit)
- [LO.Arith.mem_iff_bit](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.mem_iff_bit)

The following comprehension holds.

Expand All @@ -26,11 +26,11 @@ theorem finset_comprehension₁ [M ⊧ₘ* 𝐈𝚺₁]
∃ s < exp a, ∀ i < a, i ∈ s ↔ P i
```

- [LO.FirstOrder.Arith.Model.finset_comprehension₁](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/Bit.html#LO.FirstOrder.Arith.Model.finset_comprehension%E2%82%81)
- [LO.Arith.finset_comprehension₁](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/Bit.html#LO.Arith.finset_comprehension%E2%82%81)

The basic concepts of set theory, such as [union](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.FirstOrder.Arith.Model.union), [inter](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.FirstOrder.Arith.Model.inter),
[cartesian product](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.FirstOrder.Arith.Model.product),
and [mapping](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Basic.html#LO.FirstOrder.Arith.Model.IsMapping), etc. are defined.
The basic concepts of set theory, such as [union](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.union), [inter](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.inter),
[cartesian product](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.product),
and [mapping](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Basic.html#LO.Arith.IsMapping), etc. are defined.

### Seq

Expand All @@ -40,7 +40,7 @@ $\mathrm{Seq}(s)$ iff $s$ is a mapping and its domain is $[0, l)$ for some $l$.
def Seq [M ⊧ₘ* 𝐈𝚺₁] (s : M) : Prop := IsMapping s ∧ ∃ l, domain s = under l
```

- [LO.FirstOrder.Arith.Model.Seq](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Seq.html#LO.FirstOrder.Arith.Model.Seq)
- [LO.Arith.Seq](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Seq.html#LO.Arith.Seq)

### Primitive Recursion

Expand Down Expand Up @@ -76,7 +76,7 @@ theorem Construction.result_succ (u : M) :
c.result v (u + 1) = c.succ v u (c.result v u)
```

- [Formulae](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Formulae), [Construction](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Construction), [Construction.result](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Construction.result), [Construction.result_zero](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Construction.result_zero), [Construction.result_succ](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/PRF.html#LO.FirstOrder.Arith.Model.PR.Construction.result_succ)
- [Formulae](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Formulae), [Construction](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Construction), [Construction.result](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Construction.result), [Construction.result_zero](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Construction.result_zero), [Construction.result_succ](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/PRF.html#LO.Arith.PR.Construction.result_succ)

### Fixpoint

Expand Down Expand Up @@ -114,7 +114,7 @@ theorem Construction.case :
c.Fixpoint v x ↔ c.Φ v {z | c.Fixpoint v z} x
```

- [Blueprint](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Blueprint), [Construction](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.FirstOrder.Arith.Model.Fixpoint.Construction), [Construction.Finite](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.Finite), [Construction.Fixpoint](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.FirstOrder.Arith.Model.Fixpoint.Construction.Fixpoint), [Construction.case](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.FirstOrder.Arith.Model.Fixpoint.Construction.case)
- [Blueprint](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Blueprint), [Construction](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction), [Construction.Finite](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.Finite), [Construction.Fixpoint](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.Fixpoint), [Construction.case](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.case)

$\mathsf{Fix}_\Phi(\vec v, x)$ is $\Delta_1$ if $\Phi$ satisfies strong finiteness:

Expand All @@ -123,7 +123,7 @@ class Construction.StrongFinite (c : Construction M φ) where
strong_finite {C : Set M} {v x} : c.Φ v C x → c.Φ v {y ∈ C | y < x} x
```

- [StrongFinite](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.StrongFinite)
- [StrongFinite](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.StrongFinite)

Also structural induction holds.

Expand All @@ -134,4 +134,4 @@ theorem Construction.induction [c.StrongFinite]
∀ x, c.Fixpoint v x → P x
```

- [LO.Arith.Fixpoint.Construction.induction](https://formalizedformallogic.github.io/Arithmetization/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.induction)
- [LO.Arith.Fixpoint.Construction.induction](https://formalizedformallogic.github.io/Arithmetization/docs/Arithmetization/ISigmaOne/HFS/Fixpoint.html#LO.Arith.Fixpoint.Construction.induction)

0 comments on commit 61719af

Please sign in to comment.