Formalized basic results about formal logic in Lean 4.
- Book: Summary of results.
- Full Documentation: Generated documentation by doc-gen4.
- Classical Propositional Logic
- First-Order Logic: First-Order Logic and Arithmetic.
- Superintuitionistic Logic: Intuitionistic propositional logic and some variants.
- Intuitionistic First-Order Logic: The constructive counterpart of first-order logic.
-
Standard Modal Logic: Propositional logic extended modal operators
$\Box$ and$\Diamond$ .
This project is supported by Proxima Technology.
