Formalizing mathematical logics in Lean 4.
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
$\Box, \Diamond$ )- Kripke completeness for well-known subsystems
- Modal Cube, and sublogic relations for other logics
- Gödel-McKinsey-Tarski Theorem and Modal Companions
- Provability Logic
Any financial supports would greatly helps us. If you considered, please contact us: palalansouki@gmail.com
Companies and organizations that have supported us in the past.
- Proxima Technology (2024-2025)