Skip to content

SnO2WMaN/Arithmetization

 
 

Repository files navigation

Arithmetization

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

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

Table of Contents

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

About

Formalization of Arithmetization of Metamathematics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published

Languages

  • Lean 100.0%