Arithmetization

Formalization of weak arithmetic and arithmetization of metamathematics. This project depends on Foundation.

Table of Contents

• Arithmetization
  • Table of Contents
  • Structure
  • References
  • Sponsor

Structure

• 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$

References

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

Sponsor

This project is supported by Proxima Technology.