Reservoir

Arithmetization

Formalization of weak arithmetic and arithmetization of metamathematics. This project depends on lean4-logic.

https://iehality.github.io/Arithmetization/

Table of Contents

• Arithmetization
  • Table of Contents
  • Usage
  • Structure
  • Definions
  • Theorems
  • References

Usage

Add following to lakefile.lean.

require arithmetization from git "https://github.com/iehality/Arithmetization"

Structure

• Vorspiel: Supplementary definitions and theorems for Mathlib
• Definability: Definability of relations and functions
• Basic: Basic theories such as ,
• ISigmaZero: Theory
  • Exponential
• OmegaOne: Theory
• ISigmaOne: Theory

Definions

Theorems

• Order induction

  theorem LO.FirstOrder.Arith.Model.order_induction_h
      {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
      [M ⊧ₘ* 𝐏𝐀⁻]
      {L : LO.FirstOrder.Language} [LO.FirstOrder.Language.ORing L]
      [LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.ORing L M]
      (Γ : LO.Polarity) (s : ℕ)
      [M ⊧ₘ* LO.FirstOrder.Arith.Theory.indScheme L (LO.FirstOrder.Arith.Hierarchy Γ s)]
      {P : M → Prop} (hP : LO.FirstOrder.Arith.Model.DefinablePred L Γ s P)
      (ind : ∀ (x : M), (∀ y < x, P y) → P x) (x : M) :
      P x
  

• Least number principle

  theorem LO.FirstOrder.Arith.Model.least_number_h
      {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
      [M ⊧ₘ* 𝐏𝐀⁻]
      {L : LO.FirstOrder.Language} [LO.FirstOrder.Language.ORing L]
      [LO.FirstOrder.Structure L M] [LO.FirstOrder.Structure.ORing L M]
      [LO.FirstOrder.Structure.Monotone L M]
      (Γ : LO.Polarity) (s : ℕ)
      [M ⊧ₘ* LO.FirstOrder.Arith.Theory.indScheme L (LO.FirstOrder.Arith.Hierarchy Γ s)]
      {P : M → Prop} (hP : LO.FirstOrder.Arith.Model.DefinablePred L Γ s P)
      {x : M} (h : P x) :
      ∃ (y : M), P y ∧ ∀ z < y, ¬P z
  

• theorem LO.FirstOrder.Arith.Model.models_iSigma_iff_models_iPi
      {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M] {n : ℕ} :
      M ⊧ₘ* 𝐈𝚺n ↔ M ⊧ₘ* 𝐈𝚷n
  

• Exponential is definable in by formula

  • LO.FirstOrder.Arith.Model.Exponential.defined

    theorem LO.FirstOrder.Arith.Model.Exponential.defined
        {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
        [M ⊧ₘ* 𝐈𝚺₀] :
        𝚺₀-Relation (LO.FirstOrder.Arith.Model.Exponential : M → M → Prop) via LO.FirstOrder.Arith.Model.Exponential.def
    

  • Representation of definition of exponential

• Nuon (number of ones) is definable in by formula

  • LO.FirstOrder.Arith.Model.nuon_defined

    theorem LO.FirstOrder.Arith.Model.nuon_defined
        {M : Type} [Zero M] [One M] [Add M] [Mul M] [LT M]
        [M ⊧ₘ* 𝐈𝚺₀ + 𝛀₁]  :
        𝚺₀-Function₁ LO.FirstOrder.Arith.Model.nuon via LO.FirstOrder.Arith.Model.nuonDef
    

References

• P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic
• S. Cook, P. Nguyen, Logical Foundations of Proof Complexity