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.
  • Gödel's First Incompleteness
• Superintuitionistic Logic: Intuitionistic propositional logic and some variants.
• Standard Modal Logic: Propositional logic extended modal operators $\Box$ and $\Diamond$.