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
This project is supported by Proxima Technology.
