Foundation
Formalizing mathematical logics in Lean 4.
Summary
Main Result in this repository. More results and details are in Book and Doc.
- Propositional Logic
- Tait-style calculus and completeness
- Completeness for Kripke semantics
- Disjunctive Property of intuitionistic logic
- Rejection Law of Excluded Middle in intuitionistic logic and sublogic relations
- First-Order Logic and Arithmetics
- Completeness Theorem
- Gödel-Gentzen Translation
- Cut-elimination of first-order sequent calculus (Gentzen's Hauptsatz)
- Arithmetic and Arithmetization
- Gödel's First and Second Incompleteness Theorems
- Basic Modal Logic (with modal operators
) - Provability Logic
Documents
Financial Supports
Any financial supports would greatly helps us. If you considered, please contact us: palalansouki@gmail.com
Previous Sponsors
Companies and organizations that have supported us in the past.
- Proxima Technology (2024-2025)