Formalization of weak arithmetic and arithmetization of metamathematics. This project depends on lean4-logic.
https://iehality.github.io/Arithmetization/
- 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