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.