Arithmetics

In this formalization, we prefer developing arithmetic model theoretic, i.e. show $T ⊨ σ$ instead of $T ⊢ σ$ (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 $I Σ_{1}$ . 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 $I Σ_{1}$ , 𝐈𝚺₁ ⊢! ∀' ∃' 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$	`0`	$\emptyset$	$\emptyset$	$Σ_{0}$	$0$
$1$	`1`	$\emptyset$	$\emptyset$	$Σ_{0}$	$1$
$x + y$	`x + y`	$\emptyset$	$\emptyset$	$Σ_{0}$	$x + y$
$x \cdot y$	`x * y`	$\emptyset$	$\emptyset$	$Σ_{0}$	$x \cdot y$
$x = y$	`x = y`	$\emptyset$	-	$Σ_{0}$	-
$x < y$	`x < y`	$\emptyset$	-	$Σ_{0}$	-
$x \leq y$	`x ≤ y`	$P A^{-}$	-	$Σ_{0}$	-
$x \dot{-} y$ (modified subtraction)	`x - y`	$P A^{-}$	$P A^{-}$	$Σ_{0}$	$x$
$x ∣ y$ (devides)	`x ∣ y`	$P A^{-}$	-	$Σ_{0}$	-
$min (x, y)$	`min x y`	$P A^{-}$	$P A^{-}$	$Σ_{0}$	$x$
$max (x, y)$	`max x y`	$P A^{-}$	$P A^{-}$	$Σ_{0}$	$x + y$
$⌊ x / y ⌋$	`x / y`	$I_{open}$	$I_{open}$	$Σ_{0}$	$x$
$rem (x, y)$ (remainder)	`x % y`	$I_{open}$	$I_{open}$	$Σ_{0}$	$x$
$⌊ x ⌋$	`√x`	$I_{open}$	$I_{open}$	$Σ_{0}$	$x$
$(x, y)$	`⟪x, y⟫`	$I_{open}$	$I_{open}$	$Σ_{0}$	$(x + y + 1)^{2}$
$π_{1} (x)$ (first inversion of pairing)	`π₁ x`	$I_{open}$	$I_{open}$	$Σ_{0}$	$x$
$π_{2} (x)$ (second inversion of pairing)	`π₂ x`	$I_{open}$	$I_{open}$	$Σ_{0}$	$x$
$2^{x}$	`exp x`	$I Σ_{0}$	$I Σ_{1}$	$Σ_{0}$	none
$⌊ lo g_{2} (x)⌋$	`log x`	$I Σ_{0}$	$I Σ_{0}$	$Σ_{0}$	$x$
$∥ x ∥$ (binary length)	`‖x‖`	$I Σ_{0}$	$I Σ_{0}$	$Σ_{0}$	$x$
$x # y$	`x # y`	$I Σ_{0} + Ω_{1}$	$I Σ_{0} + Ω_{1}$	$Σ_{0}$	none
$Nuon (x)$ (number of ones)	`nuon x`	$I Σ_{0} + Ω_{1}$	$I Σ_{0} + Ω_{1}$	$Σ_{0}$	$x$
$x \in y$ , $Bit (x, y)$	`x ∈ y`	$I Σ_{1}$	-	$Σ_{0}$	-
$\emptyset$	`∅`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	$0$
$x \subseteq y$	`x ⊆ y`	$I Σ_{1}$	-	$Σ_{0}$	-
$⋃ x$	`⋃ʰᶠ x`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	none
$x \cup y$	`x ∪ y`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	$2 (x + y)$
$⋂ x$	`⋂ʰᶠ x`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	?
$x \cap y$	`x ∩ y`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	$x$
$x \times y$ (cartesian product)	`x ×ʰᶠ y`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	?
$domain (x)$ (domain of relation)	`domain x`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	$2 x$
$Mapping (x)$	`IsMapping x`	$I Σ_{1}$	-	$Σ_{0}$	-
$Seq (x)$	`Seq x`	$I Σ_{1}$	-	$Σ_{0}$	-
$lh (x)$ (length of sequence)	`lh x`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	$x$
$x^{⌢} ⟨ y ⟩$ (concatation of sequence)	`x ⁀' y`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	none
$(x)_{y}$ ( $y$ -th element of sequence)	`znth x`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{0}$	$x$
$Semiterm_{x} (y)$	`L.Semiterm x y`	$I Σ_{1}$	-	$Δ_{1}$	-
$t [w]$	`L.termSubst n m w t`	$I Σ_{1}$	$I Σ_{1}$	$Σ_{1}$	none
$Semiformula_{x} (y)$	`L.Semiformula x y`	$I Σ_{1}$	-	$Δ_{1}$	-

Logic Formalization in Lean 4

Arithmetics

Defined Predicates and Functions