Formalize formal logic (mathematical logic) in Lean Theorem Prover.
Our main results are in Foundation. See Book (In progress) and Doc for more results and details.
- Propositional Logic
- Completeness for Classical Logic
- Kripke semantics for Intuitionistic Logics and Superintuitionistic Logics.
- First-Order Logic and Arithmetics
- Completeness Theorem
- Cut-elimination of First-Order Sequent Calculus (Gentzen's Hauptsatz)
- Gödel's First and Second Incompleteness Theorems
- Basic Modal Logic (with modal operators
$\Box, \Diamond$ )- Kripke Semantics and Completeness
- Modal Cube
- Modal Companion
- 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)
