Foundation
Formalized basic results about formal logic in Lean 4.
Documents
- Book: Summary of results.
- Full Documentation: Generated documentation by doc-gen4.
Main Results
- Classical Propositional Logic
- First-Order Logic: First-Order Logic and Arithmetic.
- Superintuitionistic Logic: Intuitionistic propositional logic and some variants.
- Standard Modal Logic: Propositional logic extended modal operators
and .