Arithmetics
In this formalization, we prefer developing arithmetic model theoretic, i.e. show instead of (They are equivalent thanks to the completeness theorem.). This approach has several advantages:
- In general, writing a formalized proof (in formalized system!) is very tedious. Meta-proofs, on the other hand, tend to be relatively concise.
- Many definitions and proofs of logic and algebra in Mathlib can be used.
- Metaprogramming can streamline the proof process (especially
definability
). - 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 . First, the graph of the exponential function must be defined. This is achieved by the following two definitions.
-
Semantic definition.
def Exponential {M : Type*} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐈𝚺₀] : M → M → Prop
-
Syntactic definition that expresses the semantic definition.
def exponentialDef : 𝚺₀-Semisentence 2 lemma Exponential.defined : 𝚺₀-Relation (Exponential : M → M → Prop) via exponentialDef ``` Then prove the totality.
theorem Exponential.total {M : Type*} [Zero M] [One M] [Add M] [Mul M] [LT M] [M ⊧ₘ* 𝐈𝚺₀] (x : M) : ∃ y, Exponential x y
Since Exponential
and Exponential.total
are defined in all the model of ,
𝐈𝚺₁ ⊢! ∀' ∃' exponentialDef
is obtained by the completeness theorem. This was the result we wanted to achieve.
Defined Predicates and Functions
Predicate/Function | Notation | Defined in | Totality is proved in | Complexity | Polynomial Bound |
---|---|---|---|---|---|
0 | |||||
1 | |||||
x + y | |||||
x * y | |||||
x = y | - | - | |||
x < y | - | - | |||
x ≤ y | - | - | |||
(modified subtraction) | x - y | ||||
(devides) | x ∣ y | - | - | ||
min x y | |||||
max x y | |||||
x / y | |||||
(remainder) | x % y | ||||
√x | |||||
⟪x, y⟫ | |||||
(first inversion of pairing) | π₁ x | ||||
(second inversion of pairing) | π₂ x | ||||
exp x | none | ||||
log x | |||||
(binary length) | ‖x‖ | ||||
x # y | none | ||||
(number of ones) | nuon x | ||||
, | x ∈ y | - | - | ||
∅ | |||||
x ⊆ y | - | - | |||
⋃ʰᶠ x | none | ||||
x ∪ y | |||||
⋂ʰᶠ x | ? | ||||
x ∩ y | |||||
(cartesian product) | x ×ʰᶠ y | ? | |||
(domain of relation) | domain x | ||||
IsMapping x | - | - | |||
Seq x | - | - | |||
(length of sequence) | lh x | ||||
(concatation of sequence) | x ⁀' y | none | |||
(-th element of sequence) | znth x | ||||
L.Semiterm x y | - | - | |||
L.termSubst n m w t | none | ||||
L.Semiformula x y | - | - |