lean4-logic
Formalizing Logic in Lean4
Documents
- Book: Summary of results. TODO
- Full Documentation
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 .