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

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

• Arithmetization
  • Table of Contents
  • Structure
  • References

• Vorspiel: Supplementary definitions and theorems for Mathlib
• Definability: Definability of relations and functions
• Basic: Basic theories such as $\mathsf{PA}^-$, $\mathsf{I_{open}}$
• ISigmaZero: Theory $\mathsf{I}\Sigma_0$
  • Exponential
• OmegaOne: Theory $\mathsf{I} \Sigma_0 + \mathsf{\Omega_1}$
• ISigmaOne: Theory $\mathsf{I}\Sigma_1$

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