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
, - ISigmaZero: Theory
- Exponential
- OmegaOne: Theory
- ISigmaOne: Theory
References
- P. Hájek, P. Pudlák, Metamathematics of First-Order Arithmetic
- S. Cook, P. Nguyen, Logical Foundations of Proof Complexity