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