Foundation
Formalized basic results about formal logic in Lean 4.
Documents
- Book: Summary of results.
- Full Documentation: Generated documentation by doc-gen4.
Formalized Logics
- 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
and .
Sponsor
This project is supported by Proxima Technology.
