Foundation

Formalizing mathematical logics in Lean 4.

Summary

Main Result in this repository. More results and details are in Book and Doc.

• Propositional Logic
  • Tait-style calculus and completeness
  • Completeness for Kripke semantics
  • Disjunctive Property of intuitionistic logic
  • Rejection Law of Excluded Middle in intuitionistic logic and sublogic relations
  • Propositional Logic Zoo
• First-Order Logic and Arithmetics
  • Completeness Theorem
  • Gödel-Gentzen Translation
  • Cut-elimination of first-order sequent calculus (Gentzen's Hauptsatz)
  • Arithmetic
  • Gödel's First and Second Incompleteness Theorems
  • Arithmetic Theory Zoo
• Basic Modal Logic (with modal operators )
  • Kripke completeness for well-known subsystems
  • Modal Logic Zoo
  • Gödel-McKinsey-Tarski Theorem and Modal Companions
• Provability Logic
  • Solovay's Arithmetical Completeness Theorem for GL

Documents

• Book, summary of results.
• Doc, documentation generated by doc-gen4.

Zoo

Lines represent subset relations of theories/logics. Solid lines are represent proper subset.

Disclaimer: Zoo generators is broken since 2025/07/07 (Updated to v4.22.0-rc3). See Issue#447. These figures are snapshot on d4f889a.

Arithmetic Theory Zoo

Modal Logic Zoo

Propositional Logic Zoo

Financial Supports

Any financial supports would greatly helps us. If you considered, please contact us: palalansouki@gmail.com

Previous Sponsors

Companies and organizations that have supported us in the past.

• Proxima Technology (2024-2025)