Arithmetization
Formalization of weak arithmetic and arithmetization of metamathematics. This project depends on Foundation.
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
Sponsor
This project is supported by Proxima Technology.
